17.9. DolbeaultComparison.GoodCover🔗

Jacobians.DolbeaultComparison.GoodCover — source

cech_to_dolbeault_comp_dolbeault_to_cech

Round-trip 1 (Dolbeault → Čech → Dolbeault = id), IsLeray-free. Identical statement and proof to cech_to_dolbeault_comp_dolbeault_to_cech minus the unused hL.

theorem cech_to_dolbeault_comp_dolbeault_to_cech' (𝔇 : ChartDiskCover X) :
    (cech_to_dolbeault 𝔇) ∘ₗ (dolbeault_to_cech 𝔇) = LinearMap.id

dolbeault_to_cech_comp_cech_to_dolbeault

Round-trip 2 (Čech → Dolbeault → Čech = id), IsLeray-free. Identical statement and proof to dolbeault_to_cech_comp_cech_to_dolbeault minus the unused hL.

theorem dolbeault_to_cech_comp_cech_to_dolbeault' (𝔇 : ChartDiskCover X) :
    (dolbeault_to_cech 𝔇) ∘ₗ (cech_to_dolbeault 𝔇) = LinearMap.id

comparison_linearEquiv

The Dolbeault isomorphism H^{0,1}(X) ≃ₗ[ℝ] H¹(X, 𝒪), with NO IsLeray hypothesis. Assembled from the two IsLeray-free round-trips via LinearEquiv.ofLinear. This is DolbeaultComparisonEquiv.comparison_linearEquiv with the phantom hL argument removed — the concrete demonstration that the proven comparison never used the cover's preconnected-overlap (or even simply-connected) condition.

noncomputable def comparison_linearEquiv' (𝔇 : ChartDiskCover X) :
    DolbeaultH01 X ≃ₗ[ℝ] 𝔇.toFiniteCover.cechH1 0