A machine-checked solution to the Jacobians challenge

19.33. Finiteness.SkyscraperSnake🔗

Jacobians.Finiteness.SkyscraperSnake — source

TwoStepSES

One ambient two-step complex C0 →[d0] C1 →[d1] C2 (with d1 ∘ d0 = 0) together with two nested d-stable subcomplexes A ≤ B. This is exactly the shape of the Čech skyscraper SES (one Čech differential δ, nested 𝒪_D-section subcomplexes).

structure TwoStepSES (R : Type*) [Ring R] where

mem_submoduleOf

Membership in p.submoduleOf q unfolds to membership of the underlying element in p. (Mathlib has submoduleOf := comap q.subtype p but no membership simp-lemma; this is it.)

@[simp] theorem mem_submoduleOf {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
    {p q : Submodule R M} {x : q} : x ∈ p.submoduleOf q ↔ (x : M) ∈ p

H0sub

H⁰ of a subcomplex with degree-0 part S0: the matching global sections ker δ⁰ ∩ S0.

def H0sub (S0 : Submodule R S.C0) : Submodule R S.C0

Z1sub

Z¹ of a subcomplex with degree-1 part S1: the 1-cocycles ker δ¹ ∩ S1.

def Z1sub (S1 : Submodule R S.C1) : Submodule R S.C1

B1sub

B¹ of a subcomplex with degree-0 part S0: the 1-coboundaries δ⁰(S0).

def B1sub (S0 : Submodule R S.C0) : Submodule R S.C1

H1A

H¹ of the A-subcomplex: Z¹(A) ⧸ B¹(A). Matches the Čech cechH1.

abbrev H1A : Type _

H1B

H¹ of the B-subcomplex.

abbrev H1B : Type _

Q0

Degree-0 part of the quotient complex Q0 = B0 ⧸ A0.

abbrev Q0 : Type _

Q1

Degree-1 part of the quotient complex Q1 = B1 ⧸ A1.

abbrev Q1 : Type _

dB0

δ⁰ corestricted to the B-subcomplex, ↥B0 →ₗ ↥B1.

noncomputable def dB0 : S.B0 →ₗ[R] S.B1

dB0_coe

@[simp] theorem dB0_coe (b : S.B0) : (S.dB0 b : S.C1) = S.d0 b

dQ0

The induced differential on the quotient complex, dQ0 : Q0 →ₗ Q1 (Submodule.mapQ of dB0: δ⁰ maps A0 into A1, so it descends to the quotients).

noncomputable def dQ0 : S.Q0 →ₗ[R] S.Q1

dQ0_mk

@[simp] theorem dQ0_mk (b : S.B0) :
    S.dQ0 (Submodule.Quotient.mk b) = Submodule.Quotient.mk (S.dB0 b)

H0Q

H⁰ of the quotient complex Q: ker dQ0 (a submodule of Q0). The snake-lemma middle term.

noncomputable def H0Q : Submodule R S.Q0

D0

D0 = {b ∈ B0 : δ⁰ b ∈ A1}, the elements of B0 whose differential lies in the A-subcomplex. Pulled back along dB0 from A1.submoduleOf B1.

noncomputable def D0 : Submodule R S.B0

mem_D0

@[simp] theorem mem_D0 {b : S.B0} : b ∈ S.D0 ↔ (S.d0 b.1 : S.C1) ∈ S.A1

psi

The corestriction of δ⁰|_{D0} to Z¹(A): for b ∈ D0, δ⁰ b ∈ A1 (by definition) and δ¹(δ⁰ b) = 0 (hd), so δ⁰ b ∈ Z¹(A) = ker δ¹ ⊓ A1.

noncomputable def psi : S.D0 →ₗ[R] S.Z1sub S.A1

psi_coe

@[simp] theorem psi_coe (b : S.D0) : (S.psi b : S.C1) = S.d0 b.1.1

psiBar

ψ descended to H¹(A): ψ̄ : D0 →ₗ H¹(A), the connecting datum before quotienting the source.

noncomputable def psiBar : S.D0 →ₗ[R] S.H1A

psiBar_apply

@[simp] theorem psiBar_apply (b : S.D0) :
    S.psiBar b = Submodule.Quotient.mk (S.psi b)

A0_submoduleOf_le_ker_psiBar

ψ̄ kills A0: for a ∈ A0, ψ a = δ⁰ a ∈ B¹(A) = δ⁰(A0), hence 0 in H¹(A).

theorem A0_submoduleOf_le_ker_psiBar :
    (S.A0.submoduleOf S.B0).submoduleOf S.D0 ≤ LinearMap.ker S.psiBar

theta

The quotient projection mkQ : B0 → Q0, restricted to D0 and corestricted to ker dQ0: for b ∈ D0, dQ0 (mk b) = mk (δ⁰ b) = 0 since δ⁰ b ∈ A1.

noncomputable def theta : S.D0 →ₗ[R] S.H0Q

theta_coe

@[simp] theorem theta_coe (b : S.D0) :
    (S.theta b : S.Q0) = Submodule.Quotient.mk (b.1 : S.B0)

theta_surjective

θ is surjective onto ker dQ0: an element of ker dQ0 is mk b for some b ∈ B0 with mk (δ⁰ b) = 0, i.e. δ⁰ b ∈ A1, i.e. b ∈ D0.

theorem theta_surjective : Function.Surjective S.theta

ker_theta

ker θ = A0 (as a submodule of D0): mk b = 0 in Q0 iff b ∈ A0.

theorem ker_theta :
    LinearMap.ker S.theta = (S.A0.submoduleOf S.B0).submoduleOf S.D0

connecting

The connecting homomorphism δ̄ : H⁰(Q) = ker dQ0 → H¹(A) of the snake lemma, built *canonically*: ψ̄ : D0 → H¹(A) factors through D0/ker θ ≅ ker dQ0 = H⁰(Q) (θ surjective with ker θ = A0 ≤ ker ψ̄). No choice-of-lift well-definedness chase.

noncomputable def connecting : S.H0Q →ₗ[R] S.H1A

connecting_theta

The defining property of connecting. On the surjection θ : D0 ↠ H⁰(Q), the connecting map is just ψ̄ (the class of δ⁰ b): connecting (θ b) = [δ⁰ b]. The workhorse for exactness.

@[simp] theorem connecting_theta (b : S.D0) :
    S.connecting (S.theta b) = S.psiBar b

mem_B0_of_mem_H0sub

A degree-0 B-cochain in H⁰(B) = ker δ⁰ ⊓ B0 lies in B0.

theorem mem_B0_of_mem_H0sub {b : S.C0} (hb : b ∈ S.H0sub S.B0) : b ∈ S.B0

d0_eq_zero_of_mem_H0sub

A degree-0 B-cochain in H⁰(B) is a cocycle (δ⁰ b = 0).

theorem d0_eq_zero_of_mem_H0sub {b : S.C0} (hb : b ∈ S.H0sub S.B0) : S.d0 b = 0

h0Map

β₀* : H⁰(B) = ker δ⁰ ⊓ B0 → H⁰(Q) = ker dQ0, induced by the quotient projection mkQ : B0 → Q0 (it preserves cocycles: dQ0 (mk b) = mk (δ⁰ b) = mk 0 = 0 for a global section b). Built as H⁰(B) ↪ B0 →[mkQ] Q0, corestricted to ker dQ0.

noncomputable def h0Map : ↥(S.H0sub S.B0) →ₗ[R] S.H0Q

h0Map_coe

@[simp] theorem h0Map_coe (b : ↥(S.H0sub S.B0)) :
    (S.h0Map b : S.Q0) = Submodule.Quotient.mk (⟨b.1, S.mem_B0_of_mem_H0sub b.2⟩ : S.B0)

Z1sub_A_le_B

Z¹(A) ≤ Z¹(B) (same ker δ¹, and A1 ≤ B1).

theorem Z1sub_A_le_B : S.Z1sub S.A1 ≤ S.Z1sub S.B1

B1sub_A_le_B

B¹(A) ≤ B¹(B) (δ⁰ of A0 ≤ B0).

theorem B1sub_A_le_B : S.B1sub S.A0 ≤ S.B1sub S.B0

h1MapAbs

α₁* : H¹(A) → H¹(B), induced by the cocycle inclusion Z¹(A) ↪ Z¹(B) (it carries A-coboundaries into B-coboundaries). In the Čech instantiation this is exactly FiniteCover.h1Map.

noncomputable def h1MapAbs : S.H1A →ₗ[R] S.H1B

h1MapAbs_mk

@[simp] theorem h1MapAbs_mk (c : ↥(S.Z1sub S.A1)) :
    S.h1MapAbs (Submodule.Quotient.mk c)
      = Submodule.Quotient.mk (Submodule.inclusion S.Z1sub_A_le_B c)

Q2

Degree-2 part of the quotient complex Q2 = B2 ⧸ A2.

abbrev Q2 : Type _

dB1

δ¹ corestricted to the B-subcomplex, ↥B1 →ₗ ↥B2.

noncomputable def dB1 : S.B1 →ₗ[R] S.B2

dB1_coe

@[simp] theorem dB1_coe (b : S.B1) : (S.dB1 b : S.C2) = S.d1 b

dQ1

The induced second differential dQ1 : Q1 →ₗ Q2.

noncomputable def dQ1 : S.Q1 →ₗ[R] S.Q2

dQ1_mk

@[simp] theorem dQ1_mk (b : S.B1) :
    S.dQ1 (Submodule.Quotient.mk b) = Submodule.Quotient.mk (S.dB1 b)

H1Q

H¹(Q) = Z¹(Q)/B¹(Q) = ker dQ1 ⧸ range dQ0. The cokernel-of-cohomology term whose vanishing gives the surjectivity surj₄.

abbrev H1Q : Type _

exact_h0Map_connecting

Exactness at H⁰(Q): range (β₀* : H⁰(B)→H⁰(Q)) = ker connecting. A cocycle class maps to 0 under the connecting map iff it is β₀ of an honest B-global-section.

theorem exact_h0Map_connecting : Function.Exact S.h0Map S.connecting

exact_connecting_h1Map

Exactness at H¹(A): range connecting = ker (α₁* : H¹(A)→H¹(B)). A class in H¹(A) dies in H¹(B) (becomes a B-coboundary) iff it is in the image of the connecting map.

theorem exact_connecting_h1Map : Function.Exact S.connecting S.h1MapAbs

surjective_h1MapAbs_of_subsingleton

surj₄: α₁* : H¹(A) → H¹(B) is surjective once H¹(Q) = 0 (here Subsingleton H1Q). The last arrow of the six-term sequence … → H¹(A) → H¹(B) → H¹(Q); if H¹(Q) is trivial the map onto H¹(B) is onto. Concretely: a B-1-cocycle c maps to a Q-1-cocycle whose class in H¹(Q) is 0, so c = dB0 b₀ + (A-cochain) for some b₀ ∈ B0; the A-cochain c − dB0 b₀ is an A-cocycle whose α₁*-class is [c].

theorem surjective_h1MapAbs_of_subsingleton (h : Subsingleton S.H1Q) :
    Function.Surjective S.h1MapAbs

sections2

2-cochains that are 𝒪_D-sections on each triple intersection (the degree-2 section subcomplex — not previously needed in CechComplex, supplied here for the Q-degree-2 term of the snake).

def sections2 (𝔘 : FiniteCover X) (D : Divisor X) : Submodule ℂ 𝔘.Cochain2 where

cechDelta1_sections

δ¹ preserves the 𝒪_D section subcomplex (each component of δ¹g is a signed sum of restrictions of 𝒪_D-germs, hence an 𝒪_D-germ).

theorem cechDelta1_sections (𝔘 : FiniteCover X) (D : Divisor X) :
    Submodule.map 𝔘.cechDelta1 (𝔘.sections1 D) ≤ 𝔘.sections2 D

skyscraperTwoStep

The Čech skyscraper TwoStepSES. Ambient germ-class Čech complex δ, with the nested subcomplexes 𝒪_D ≤ 𝒪_{D+P} of section submodules in degrees 0,1,2.

noncomputable def skyscraperTwoStep (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    TwoStepSES ℂ where

LocalRealizationData

The geometric input the snake lemma cannot supply, bundled honestly as explicit hypotheses (NOT a gap): the local-realization iso H⁰(Q) ≅ ℂ compatible with the principal-part arrow h0ToSky, the acyclicity H¹(Q) = 0, and the (Forster 14.9) H¹ finiteness.

structure LocalRealizationData (𝔘 : FiniteCover X) (D : Divisor X) (P : X) where

LocalRealizationData.f₃

The connecting homomorphism f₃ : ℂ_P → H¹(𝒪_D) of the skyscraper LES, from the snake-lemma connecting map precomposed with the realization iso e0.symm : ℂ ≅ H⁰(Q). (Skyscraper D P = ℂ and H1A = cechH1 D are definitional.)

noncomputable def LocalRealizationData.f₃ {𝔘 : FiniteCover X} {D : Divisor X} {P : X}
    (L : 𝔘.LocalRealizationData D P) : 𝔘.Skyscraper D P →ₗ[ℂ] 𝔘.cechH1 D

LocalRealizationData.exact₂

Exactness at ℂ_P (exact₂): range h0ToSky = ker f₃. The snake exactness exact_h0Map_connecting transported across the realization iso e0 (ladder (id, e0, id)).

theorem LocalRealizationData.exact₂ {𝔘 : FiniteCover X} {D : Divisor X} {P : X}
    (L : 𝔘.LocalRealizationData D P) :
    Function.Exact (𝔘.h0ToSky D P L.hP) L.f₃

LocalRealizationData.exact₃

Exactness at H¹(𝒪_D) (exact₃): range f₃ = ker h1Map. The snake exactness exact_connecting_h1Map precomposed by the surjective e0.symm (and h1Map = h1MapAbs).

theorem LocalRealizationData.exact₃ {𝔘 : FiniteCover X} {D : Divisor X} {P : X}
    (L : 𝔘.LocalRealizationData D P) :
    Function.Exact L.f₃ (𝔘.h1Map D P)

LocalRealizationData.surj₄

Surjectivity of h1Map (surj₄): from the acyclicity H¹(Q) = 0 via surjective_h1MapAbs_of_subsingleton (and h1Map = h1MapAbs).

theorem LocalRealizationData.surj₄ {𝔘 : FiniteCover X} {D : Divisor X} {P : X}
    (L : 𝔘.LocalRealizationData D P) :
    Function.Surjective (𝔘.h1Map D P)

skyscraperLES_of_localRealization

The skyscraper long exact sequence from the snake + local realization. Given the geometric LocalRealizationData, the snake lemma produces all four remaining SkyscraperLES fields, completing exists_skyscraperLES. The H⁰-arrow h0ToSky and exact₁₂ come from SkyscraperArrow (exact_h0Incl_h0ToSky); everything else (f₃, exact₂, exact₃, surj₄) is the snake transported across e0 and H¹(Q) = 0.

noncomputable def skyscraperLES_of_localRealization {𝔘 : FiniteCover X} {D : Divisor X} {P : X}
    (L : 𝔘.LocalRealizationData D P) : SkyscraperLES 𝔘 D P