A machine-checked solution to the Jacobians challenge

19.30. Finiteness.SkyscraperConeRealization🔗

Jacobians.Finiteness.SkyscraperConeRealization — source

coeffWFn_comp_openIncl

Restriction-invariance of coeffWFn at P. For W ≤ V and P ∈ W, the order-k coefficient of f ∘ openIncl at P (read in ↥W's chart) equals that of f at P (read in ↥V's chart).

theorem coeffWFn_comp_openIncl {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {V W : Opens X} (h : W ≤ V) (k : ℤ) (f : V → ℂ) (w : W) :
    coeffWFn k w (f ∘ openIncl h) = coeffWFn k (openIncl h w) f

coeffGermLin_rawRestrictG

Restriction-invariance of coeffGermLin at P (germ-class form). For W ≤ V, P ∈ W, and a 𝒪_{D+P}-germ γ on V, the coefficient of its restriction to W equals the coefficient of γ: the value at P is read at the same ambient point in either chart (coeffWFn_comp_openIncl).

theorem coeffGermLin_rawRestrictG {V W : Opens X} (h : W ≤ V) (hPV : P ∈ V) (hPW : P ∈ W)
    (γ : OmegaDGerm (D + Finsupp.single P 1) V) :
    coeffGermLin hPW (D := D)
        ⟨rawRestrictG h (γ : MGerm V), rawRestrictG_omegaDGerm h γ.2⟩
      = coeffGermLin hPV (D := D) γ

FiniteCover.LocallyRealizable

Local realizability of a cover (local Mittag–Leffler): at every cover-set U j ∋ P, the order-(−D(P)−1) principal-part coefficient coeffGermLin is *surjective* onto ℂ, for every divisor D and every point P. Equivalently: every prescribed top Laurent coefficient at P is realised by some 𝒪_{D+P}(U j)-germ. This is the genuine analytic content of the skyscraper SES, isolated at the level of a single cover-set; for the canonical chart-disk cover it is the explicit product witness (SkyscraperProductWitness.locallyRealizable_chartDiskCover).

def FiniteCover.LocallyRealizable (𝔘 : FiniteCover X) : Prop

coneLift

The lifted witness germ at a star vertex U j ∋ P realising the prescribed coefficient t (extracted from LocallyRealizable); 0 off the star. coneLift is the underlying MGerm.

noncomputable def coneLift (hR : 𝔘.LocallyRealizable) (cw : 𝔘.ι → ℂ) (j : 𝔘.ι) : MGerm (𝔘.U j)

coneLift_mem

theorem coneLift_mem (hR : 𝔘.LocallyRealizable) (cw : 𝔘.ι → ℂ) (j : 𝔘.ι) :
    𝔘.coneLift D P hR cw j ∈ OmegaDGerm (D + Finsupp.single P 1) (𝔘.U j)

coeffGermLin_coneLift

On the star (P ∈ U j) the lifted germ has the prescribed coefficient cw j.

theorem coeffGermLin_coneLift (hR : 𝔘.LocallyRealizable) (cw : 𝔘.ι → ℂ) {j : 𝔘.ι}
    (hj : P ∈ 𝔘.U j) :
    coeffGermLin hj (D := D) ⟨𝔘.coneLift D P hR cw j, 𝔘.coneLift_mem D P hR cw j⟩ = cw j

coneB0

The lifted cochain coneB0, as an element of B0 = sections0(D+P).

noncomputable def coneB0 (hR : 𝔘.LocallyRealizable) (cw : 𝔘.ι → ℂ) :
    (𝔘.skyscraperTwoStep D P).B0

coneB0_coe

@[simp] theorem coneB0_coe (hR : 𝔘.LocallyRealizable) (cw : 𝔘.ι → ℂ) (j : 𝔘.ι) :
    ((𝔘.coneB0 D P hR cw).1 j) = 𝔘.coneLift D P hR cw j

cechDelta0_coneB0_component

The component of δ⁰(coneB0) on the overlap (j,k) is the difference of the two restricted lifted germs (the cechDelta0 formula, with the lifted components plugged in).

theorem cechDelta0_coneB0_component (hR : 𝔘.LocallyRealizable) (cw : 𝔘.ι → ℂ) (j k : 𝔘.ι) :
    𝔘.cechDelta0 (𝔘.coneB0 D P hR cw).1 (j, k)
      = rawRestrictG (inf_le_right : 𝔘.U j ⊓ 𝔘.U k ≤ 𝔘.U k) (𝔘.coneLift D P hR cw k)
        - rawRestrictG (inf_le_left : 𝔘.U j ⊓ 𝔘.U k ≤ 𝔘.U j) (𝔘.coneLift D P hR cw j)

cechDelta0_coneB0_sub_mem_sections1

The cone cocycle property. If the star ℂ-cochain cw is compatible with the target cochain g ∈ sections1(D+P) on every star overlap (cw k − cw j = coeffGermLin g_{jk} whenever P ∈ U j ⊓ U k), then δ⁰(coneB0 cw) − g is an 𝒪_D-cochain. Off the star the D/D+P bounds coincide on the overlap; on the star the coefficient at P of the difference vanishes (restriction-invariance + linearity + compatibility), so injectivity (ker_coeffGermLin) gives 𝒪_D-membership.

theorem cechDelta0_coneB0_sub_mem_sections1 (hR : 𝔘.LocallyRealizable) (cw : 𝔘.ι → ℂ)
    {g : 𝔘.Cochain1} (hg : g ∈ 𝔘.sections1 (D + Finsupp.single P 1))
    (hcompat : ∀ (j k : 𝔘.ι) (hjk : P ∈ 𝔘.U j ⊓ 𝔘.U k),
      cw k - cw j = coeffGermLin (D := D) hjk ⟨g (j, k), hg (j, k)⟩) :
    𝔘.cechDelta0 (𝔘.coneB0 D P hR cw).1 - g ∈ 𝔘.sections1 D

coneB0_mk_mem_H0Q

The coneB0 class lies in H0Q = ker dQ0 when cw is g = 0-compatible (so δ⁰(coneB0) ∈ sections1 D).

theorem coneB0_mk_mem_H0Q (hR : 𝔘.LocallyRealizable) (cw : 𝔘.ι → ℂ)
    (hcompat : ∀ (j k : 𝔘.ι) (_hjk : P ∈ 𝔘.U j ⊓ 𝔘.U k), cw k - cw j = 0) :
    Submodule.Quotient.mk (𝔘.coneB0 D P hR cw) ∈ (𝔘.skyscraperTwoStep D P).H0Q

e0Lin_surjective_of_realizable

e0Lin surjectivity from local realizability. For the apex U i ∋ P, every a : ℂ is realised by the constant-a cone cochain (coneB0): its class lies in H0Q and reads coefficient a at U i. Replaces SkyscraperAssembly.e0Lin_surjective (which needed the singleton-star hstar).

theorem e0Lin_surjective_of_realizable (hR : 𝔘.LocallyRealizable) {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    Function.Surjective (𝔘.e0Lin D P hP)

cwOf

The apex ℂ-cochain for acyclicity: cwOf gB j = coeffGermLin (gB_{i j}) on the star (P ∈ U j), 0 off it. Here i ∋ P is the apex; P ∈ U i ⊓ U j whenever P ∈ U j.

noncomputable def cwOf {i : 𝔘.ι} (hPi : P ∈ 𝔘.U i)
    {gB : 𝔘.Cochain1} (hgB : gB ∈ 𝔘.sections1 (D + Finsupp.single P 1)) (j : 𝔘.ι) : ℂ

cwOf_star

theorem cwOf_star {i : 𝔘.ι} (hPi : P ∈ 𝔘.U i)
    {gB : 𝔘.Cochain1} (hgB : gB ∈ 𝔘.sections1 (D + Finsupp.single P 1)) {j : 𝔘.ι}
    (hj : P ∈ 𝔘.U j) :
    𝔘.cwOf D P hPi hgB j
      = coeffGermLin (D := D) (TopologicalSpace.Opens.mem_inf.mpr ⟨hPi, hj⟩)
          ⟨gB (i, j), hgB (i, j)⟩

cwOf_compat

Apex compatibility (the δ¹gB triple identity). For a Q-cocycle gB (δ¹gB ∈ sections2 D) and star indices j, k (P ∈ U j ⊓ U k), the apex cochain satisfies cwOf k − cwOf j = coeffGermLin gB_{jk}. Read at P on the triple overlap U i ⊓ U j ⊓ U k (which contains P), the (i,j,k) component of δ¹gB ∈ 𝒪_D has coefficient 0 (coeffGermFn_eq_zero_of_mem_OmegaDGerm), giving (via restriction-invariance) coeff gB_{jk} − coeff gB_{ik} + coeff gB_{ij} = 0.

theorem cwOf_compat {i : 𝔘.ι} (hPi : P ∈ 𝔘.U i)
    {gB : 𝔘.Cochain1} (hgB : gB ∈ 𝔘.sections1 (D + Finsupp.single P 1))
    (hcoc : 𝔘.cechDelta1 gB ∈ 𝔘.sections2 D) (j k : 𝔘.ι) (hjk : P ∈ 𝔘.U j ⊓ 𝔘.U k) :
    𝔘.cwOf D P hPi hgB k - 𝔘.cwOf D P hPi hgB j
      = coeffGermLin (D := D) hjk ⟨gB (j, k), hgB (j, k)⟩

mk_mem_range_dQ0_of_cocycle

A Q-1-cocycle mk gB (δ¹gB ∈ sections2 D) lies in range dQ0: the cone builder with apex i ∋ P and cochain cwOf gB produces b with δ⁰b − gB ∈ sections1 D, so dQ0 (mk b) = mk gB.

theorem mk_mem_range_dQ0_of_cocycle (hR : 𝔘.LocallyRealizable) {i : 𝔘.ι} (hPi : P ∈ 𝔘.U i)
    (gB : (𝔘.skyscraperTwoStep D P).B1)
    (hcoc : 𝔘.cechDelta1 (gB.1 : 𝔘.Cochain1) ∈ 𝔘.sections2 D) :
    (Submodule.Quotient.mk gB : (𝔘.skyscraperTwoStep D P).Q1)
      ∈ LinearMap.range (𝔘.skyscraperTwoStep D P).dQ0

subsingleton_H1Q_of_realizable

Subsingleton (H¹(Q)) from local realizability (the cone, apex i ∋ P). Every Q-1-cocycle class is a coboundary (mk_mem_range_dQ0_of_cocycle), so (range dQ0).submoduleOf (ker dQ1) = ⊤ and H¹(Q) = ker dQ1 ⧸ range dQ0 is trivial. Replaces SkyscraperAssembly.subsingleton_H1Q (singleton star).

theorem subsingleton_H1Q_of_realizable (hR : 𝔘.LocallyRealizable) {i : 𝔘.ι} (hPi : P ∈ 𝔘.U i) :
    Subsingleton (𝔘.skyscraperTwoStep D P).H1Q

e0Cone

The local-realization isomorphism e0 : H0Q ≃ₗ[ℂ] ℂ from local realizability (no singleton star). The coefficient e0Lin is injective (e0Lin_injective, always) and surjective (e0Lin_surjective_of_realizable, the cone).

noncomputable def e0Cone (hR : 𝔘.LocallyRealizable) {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    (𝔘.skyscraperTwoStep D P).H0Q ≃ₗ[ℂ] ℂ

e0Cone_apply

@[simp] theorem e0Cone_apply (hR : 𝔘.LocallyRealizable) {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (x : (𝔘.skyscraperTwoStep D P).H0Q) :
    𝔘.e0Cone D P hR hP x = 𝔘.e0Lin D P hP x

e0Cone_hcompat

Compatibility of e0Cone with the principal-part arrow h0ToSky: h0ToSky = e0Cone ∘ h0Map (same proof as SkyscraperAssembly.e0_hcompat: both sides read the order-(−D(P)−1) coefficient of the component on U i; h0Map is mkQ, e0Cone the descended coefficient).

theorem e0Cone_hcompat (hR : 𝔘.LocallyRealizable) {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    𝔘.h0ToSky D P hP
      = (𝔘.e0Cone D P hR hP : (𝔘.skyscraperTwoStep D P).H0Q →ₗ[ℂ] ℂ).comp
          (𝔘.skyscraperTwoStep D P).h0Map

localRealizationData_of_realizable

LocalRealizationData from local realizability — the cone/hstar-free assembly, fully self-contained. Given an apex U i ∋ P and LocallyRealizable 𝔘, the realization datum exists. e0/hcompat/hQac are the cone pieces; finH1D/finH1DP come from finiteDimensional_cechH1_general and finH0DP from the finiteDimensional_globalSections instance, so no finiteness hypothesis is needed.

noncomputable def localRealizationData_of_realizable (hR : 𝔘.LocallyRealizable) {i : 𝔘.ι}
    (hP : P ∈ 𝔘.U i) :
    𝔘.LocalRealizationData D P