The Dolbeault comparison H¹(X, 𝒪) ≅ H^{0,1}(X) (Jacobian/DolbeaultComparison/Comparison.lean)

Unit: dolbeault-comparison (docs/design/dolbeault-comparison.md §4.4/§6.4). Forster 15.14(a), PDE-free at D = 0: H01 X := Form01 X ⧸ range dbar, the Čech → Dolbeault map cechToH01 (built via H1.lift from the per-good-cover map toDolb, using dolbForm), its injectivity (the CR-bridge argument) and surjectivity (chart-disk dbar-solvability + PoU gluing), packaged as dolbeaultEquiv : H1 (0 : Divisor X) ≃ₗ[ℂ] H01 X.

finiteDimensional_H01 is gated on a [FiniteDimensional ℂ (H1 (0 : Divisor X))] hypothesis: at the time of this build Jacobian/Finiteness/H1Finite.lean (the file that would discharge this hypothesis unconditionally) has not landed; see the unit's build-log entry.

@[instance_reducible]

noncomputable instance RS.instAddCommGroupH1OfNatDivisor {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] : AddCommGroup (Cech.H1 0)

Compat: Module.DirectLimit.addCommGroup (needing the Pi-type hypothesis [∀ 𝒰, AddCommGroup (H1Cover 0 𝒰)]) is not found by plain inferInstance for H1 0 — Lean's instance search does not automatically distribute over the ∀-quantified instance argument of a Module.DirectLimit-style instance with explicit index data; register it once, by hand, as a concrete named instance so ordinary instance search (Sub, LinearMap.ker_eq_bot, LinearEquiv's CoeFun, …) finds it downstream. Spiked/isolated in a throwaway scratch file before landing here.

Equations

• RS.instAddCommGroupH1OfNatDivisor = Module.DirectLimit.addCommGroup (fun (𝒰 : RS.Cech.FinCover ⊤) => RS.Cech.H1Cover 0 𝒰) fun (x x_1 : RS.Cech.FinCover ⊤) (h : x ≤ x_1) => RS.Cech.resH1' 0 h

H01 X

noncomputable def RS.H01 (X : Type u_2) [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Type u_2

The Dolbeault H^{0,1}(X): the naked quotient of Form01 X by range dbar (D3).

Equations

• RS.H01 X = (RS.Form01 X ⧸ RS.dbar.range)

@[instance_reducible]

noncomputable instance RS.instAddCommGroupH01 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : AddCommGroup (H01 X)

Equations

• RS.instAddCommGroupH01 = Submodule.Quotient.addCommGroup RS.dbar.range

@[instance_reducible]

noncomputable instance RS.instModuleComplexH01 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Module ℂ (H01 X)

Equations

• RS.instModuleComplexH01 = Submodule.Quotient.module RS.dbar.range

noncomputable def RS.H01.mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Form01 X →ₗ[ℂ] H01 X

The quotient map onto H01 X.

Equations

• RS.H01.mk = RS.dbar.range.mkQ

theorem RS.H01.mk_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Function.Surjective ⇑mk

theorem RS.H01.mk_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η : Form01 X} : mk η = 0 ↔ ∃ (u : SmoothC X), dbar u = η

theorem RS.H01.mk_eq_mk_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η θ : Form01 X} : mk η = mk θ ↔ ∃ (u : SmoothC X), dbar u = η - θ

toDolb: the Čech → Dolbeault map on a good cover

noncomputable def RS.toDolbRaw {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : Cech.FinCover ⊤} [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) : ↥(Cech.Z1 0 𝒰) →ₗ[ℂ] H01 X

The raw (pre-quotient) map Z1 0 𝒰 → H01 X, f ↦ H01.mk (dolbForm h𝒰 f). Additivity and homogeneity come from dolbForm_add_sub_mem/dolbForm_smul_sub_mem (§6.3): the discrepancies land in range dbar = ker H01.mk.

Equations

• RS.toDolbRaw h𝒰 = { toFun := fun (f : ↥(RS.Cech.Z1 0 𝒰)) => RS.H01.mk (RS.Dolb.dolbForm h𝒰 f), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def RS.toDolb {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : Cech.FinCover ⊤} [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) : Cech.H1Cover 0 𝒰 →ₗ[ℂ] H01 X

The Čech → Dolbeault map on a good cover (Forster 15.14(a) forward map, cover level).

Equations

• RS.toDolb h𝒰 = (Submodule.comap (RS.Cech.Z1 0 𝒰).subtype (RS.Cech.B1 0 𝒰)).liftQ (RS.toDolbRaw h𝒰) ⋯

@[simp]

theorem RS.toDolb_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : Cech.FinCover ⊤} [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) (f : ↥(Cech.Z1 0 𝒰)) : (toDolb h𝒰) ((Cech.H1Cover.mk 0 𝒰) f) = H01.mk (Dolb.dolbForm h𝒰 f)

theorem RS.toDolb_res {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 𝒱 : Cech.FinCover ⊤} [T2Space X] [CompactSpace X] (h𝒰 : 𝒰.IsGood) (h𝒱 : 𝒱.IsGood) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : Cech.IsRefIdx 𝒰 𝒱 τ) : toDolb h𝒱 ∘ₗ Cech.resH1 0 τ hτ = toDolb h𝒰

cechToH01: extend toDolb to the whole colimit via H1.lift

noncomputable def RS.goodRef {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X] (𝒰 : Cech.FinCover ⊤) : Cech.FinCover ⊤

A classical choice of good refinement of any cover.

Equations

• RS.goodRef 𝒰 = ⋯.choose

theorem RS.goodRef_le {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X] (𝒰 : Cech.FinCover ⊤) : 𝒰 ≤ goodRef 𝒰

theorem RS.goodRef_isGood {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X] (𝒰 : Cech.FinCover ⊤) : (goodRef 𝒰).IsGood

noncomputable def RS.toDolbAll {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (𝒰 : Cech.FinCover ⊤) : Cech.H1Cover 0 𝒰 →ₗ[ℂ] H01 X

toDolb extended to every cover by pushing to a good refinement.

Equations

• RS.toDolbAll 𝒰 = RS.toDolb ⋯ ∘ₗ RS.Cech.resH1' 0 ⋯

theorem RS.toDolbAll_compat {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (𝒰 𝒱 : Cech.FinCover ⊤) (h : 𝒰 ≤ 𝒱) (ξ : Cech.H1Cover 0 𝒰) : (toDolbAll 𝒱) ((Cech.resH1' 0 h) ξ) = (toDolbAll 𝒰) ξ

noncomputable def RS.cechToH01 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] : Cech.H1 0 →ₗ[ℂ] H01 X

THE comparison map on the colimit (Forster 15.14(a), forward map).

Equations

• RS.cechToH01 = RS.Cech.H1.lift 0 RS.toDolbAll ⋯

@[simp]

theorem RS.cechToH01_toH1_all {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (𝒰 : Cech.FinCover ⊤) (c : Cech.H1Cover 0 𝒰) : cechToH01 ((Cech.toH1 0 𝒰) c) = (toDolbAll 𝒰) c

theorem RS.cechToH01_toH1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] {𝒰 : Cech.FinCover ⊤} (h𝒰 : 𝒰.IsGood) (c : Cech.H1Cover 0 𝒰) : cechToH01 ((Cech.toH1 0 𝒰) c) = (toDolb h𝒰) c

Injectivity

theorem RS.cechToH01_injective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] : Function.Injective ⇑cechToH01

Surjectivity

theorem RS.cechToH01_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] : Function.Surjective ⇑cechToH01

Assembly

noncomputable def RS.dolbeaultEquiv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] : Cech.H1 0 ≃ₗ[ℂ] H01 X

DOLBEAULT (Forster 15.14(a), PDE-free): H¹(X, 𝒪) ≃ H^{0,1}_dbar(X).

Equations

• RS.dolbeaultEquiv = LinearEquiv.ofBijective RS.cechToH01 ⋯

@[simp]

theorem RS.dolbeaultEquiv_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (ξ : Cech.H1 0) : dolbeaultEquiv ξ = cechToH01 ξ

theorem RS.finiteDimensional_H01 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [FiniteDimensional ℂ (Cech.H1 0)] : FiniteDimensional ℂ (H01 X)

The blueprint's stated purpose: Čech finiteness transfers to H^{0,1}. Gated on [FiniteDimensional ℂ (H1 (0 : Divisor X))] — the unconditional discharge of this hypothesis lives in Jacobian/Finiteness/H1Finite.lean, not yet built at the time of this unit.

theorem RS.exists_dbar_eq_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] {η : Form01 X} {ξ : Cech.H1 0} (hξ : cechToH01 ξ = H01.mk η) : (∃ (u : SmoothC X), dbar u = η) ↔ ξ = 0

Global dbar-solvability criterion (free corollary): solvable iff the Čech class of the Leray cocycle of local solutions vanishes.