Theorem 2: Small Double Complex Homology

If E is a 2×2-double complex (meaning E_{p,q} = 0 for all (p,q) ∉ {0,1}²), then H_n(Tot(E)) ≅ ⊕_{p+q=n} H_p(H_q(E_{•,•}, ∂^v), ∂̄^h).

Main Results

• SmallDC — a concrete 2×2 double complex
• homologyEquiv_n0 — isomorphism at degree 0
• homologyEquiv_n2 — isomorphism at degree 2
• homologyEquiv_n1 — isomorphism at degree 1

structure SmallDC : Type (max (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1)) (u_4 + 1))

A concrete 2×2 double complex over 𝔽₂.

• A₀₀ : Type u_1
• A₀₁ : Type u_2
• A₁₀ : Type u_3
• A₁₁ : Type u_4
• inst₀₀ : AddCommGroup self.A₀₀
• mod₀₀ : Module 𝔽₂ self.A₀₀
• inst₀₁ : AddCommGroup self.A₀₁
• mod₀₁ : Module 𝔽₂ self.A₀₁
• inst₁₀ : AddCommGroup self.A₁₀
• mod₁₀ : Module 𝔽₂ self.A₁₀
• inst₁₁ : AddCommGroup self.A₁₁
• mod₁₁ : Module 𝔽₂ self.A₁₁
• dv₀ : self.A₀₁ →ₗ[𝔽₂] self.A₀₀
• dv₁ : self.A₁₁ →ₗ[𝔽₂] self.A₁₀
• dh₀ : self.A₁₀ →ₗ[𝔽₂] self.A₀₀
• dh₁ : self.A₁₁ →ₗ[𝔽₂] self.A₀₁
• comm : self.dv₀ ∘ₗ self.dh₁ = self.dh₀ ∘ₗ self.dv₁

Total complex

def SmallDC.d₂ (E : SmallDC) : E.A₁₁ →ₗ[𝔽₂] E.A₁₀ × E.A₀₁

Equations

• E.d₂ = E.dv₁.prod E.dh₁

def SmallDC.d₁ (E : SmallDC) : E.A₁₀ × E.A₀₁ →ₗ[𝔽₂] E.A₀₀

Equations

• E.d₁ = E.dh₀.coprod E.dv₀

theorem SmallDC.d₂_fst (E : SmallDC) (x : E.A₁₁) : (E.d₂ x).1 = E.dv₁ x

theorem SmallDC.d₂_snd (E : SmallDC) (x : E.A₁₁) : (E.d₂ x).2 = E.dh₁ x

theorem SmallDC.d₁_comp_d₂ (E : SmallDC) : E.d₁ ∘ₗ E.d₂ = 0

Total complex homology types

def SmallDC.totH₀ (E : SmallDC) : Type u_1

Equations

• E.totH₀ = (E.A₀₀ ⧸ E.d₁.range)

instance SmallDC.instAddCommGroupTotH₀ (E : SmallDC) : AddCommGroup E.totH₀

Equations

• E.instAddCommGroupTotH₀ = Submodule.Quotient.addCommGroup E.d₁.range

instance SmallDC.instModule𝔽₂TotH₀ (E : SmallDC) : Module 𝔽₂ E.totH₀

Equations

• E.instModule𝔽₂TotH₀ = Submodule.Quotient.module E.d₁.range

def SmallDC.totZ₁ (E : SmallDC) : Submodule 𝔽₂ (E.A₁₀ × E.A₀₁)

Equations

• E.totZ₁ = E.d₁.ker

def SmallDC.totB₁ (E : SmallDC) : Submodule 𝔽₂ (E.A₁₀ × E.A₀₁)

Equations

• E.totB₁ = E.d₂.range

theorem SmallDC.totB₁_le_totZ₁ (E : SmallDC) : E.totB₁ ≤ E.totZ₁

def SmallDC.totB₁InZ₁ (E : SmallDC) : Submodule 𝔽₂ ↥E.totZ₁

Equations

• E.totB₁InZ₁ = Submodule.comap E.totZ₁.subtype E.totB₁

def SmallDC.totH₁ (E : SmallDC) : Type (max u_3 u_2)

Equations

• E.totH₁ = (↥E.totZ₁ ⧸ E.totB₁InZ₁)

instance SmallDC.instAddCommGroupTotH₁ (E : SmallDC) : AddCommGroup E.totH₁

Equations

• E.instAddCommGroupTotH₁ = Submodule.Quotient.addCommGroup E.totB₁InZ₁

instance SmallDC.instModule𝔽₂TotH₁ (E : SmallDC) : Module 𝔽₂ E.totH₁

Equations

• E.instModule𝔽₂TotH₁ = Submodule.Quotient.module E.totB₁InZ₁

def SmallDC.totH₂ (E : SmallDC) : Type u_4

Equations

• E.totH₂ = ↥E.d₂.ker

instance SmallDC.instAddCommGroupTotH₂ (E : SmallDC) : AddCommGroup E.totH₂

Equations

• E.instAddCommGroupTotH₂ = E.d₂.ker.addCommGroup

instance SmallDC.instModule𝔽₂TotH₂ (E : SmallDC) : Module 𝔽₂ E.totH₂

Equations

• E.instModule𝔽₂TotH₂ = E.d₂.ker.module

Vertical homology

@[reducible, inline]

abbrev SmallDC.vH₀₀ (E : SmallDC) : Type u_1

Equations

• E.vH₀₀ = (E.A₀₀ ⧸ E.dv₀.range)

@[reducible, inline]

abbrev SmallDC.vH₁₀ (E : SmallDC) : Type u_3

Equations

• E.vH₁₀ = (E.A₁₀ ⧸ E.dv₁.range)

@[reducible, inline]

abbrev SmallDC.vH₀₁ (E : SmallDC) : Type u_2

Equations

• E.vH₀₁ = ↥E.dv₀.ker

@[reducible, inline]

abbrev SmallDC.vH₁₁ (E : SmallDC) : Type u_4

Equations

• E.vH₁₁ = ↥E.dv₁.ker

Induced horizontal differentials

theorem SmallDC.dh₀_maps_range (E : SmallDC) : E.dv₁.range ≤ Submodule.comap E.dh₀ E.dv₀.range

def SmallDC.barDh₀ (E : SmallDC) : E.vH₁₀ →ₗ[𝔽₂] E.vH₀₀

Equations

• E.barDh₀ = E.dv₁.range.mapQ E.dv₀.range E.dh₀ ⋯

theorem SmallDC.dh₁_maps_ker (E : SmallDC) (x : E.A₁₁) (hx : x ∈ E.dv₁.ker) : E.dh₁ x ∈ E.dv₀.ker

def SmallDC.barDh₁ (E : SmallDC) : E.vH₁₁ →ₗ[𝔽₂] E.vH₀₁

Equations

• E.barDh₁ = LinearMap.codRestrict E.dv₀.ker (E.dh₁.domRestrict E.dv₁.ker) ⋯

Iterated homology types

def SmallDC.itH₀ (E : SmallDC) : Type u_1

Equations

• E.itH₀ = (E.vH₀₀ ⧸ E.barDh₀.range)

instance SmallDC.instAddCommGroupItH₀ (E : SmallDC) : AddCommGroup E.itH₀

Equations

• E.instAddCommGroupItH₀ = Submodule.Quotient.addCommGroup E.barDh₀.range

instance SmallDC.instModule𝔽₂ItH₀ (E : SmallDC) : Module 𝔽₂ E.itH₀

Equations

• E.instModule𝔽₂ItH₀ = Submodule.Quotient.module E.barDh₀.range

def SmallDC.itH₂ (E : SmallDC) : Type u_4

Equations

• E.itH₂ = ↥E.barDh₁.ker

instance SmallDC.instAddCommGroupItH₂ (E : SmallDC) : AddCommGroup E.itH₂

Equations

• E.instAddCommGroupItH₂ = E.barDh₁.ker.addCommGroup

instance SmallDC.instModule𝔽₂ItH₂ (E : SmallDC) : Module 𝔽₂ E.itH₂

Equations

• E.instModule𝔽₂ItH₂ = E.barDh₁.ker.module

def SmallDC.itH₁_fst (E : SmallDC) : Type u_3

Equations

• E.itH₁_fst = ↥E.barDh₀.ker

instance SmallDC.instAddCommGroupItH₁_fst (E : SmallDC) : AddCommGroup E.itH₁_fst

Equations

• E.instAddCommGroupItH₁_fst = E.barDh₀.ker.addCommGroup

instance SmallDC.instModule𝔽₂ItH₁_fst (E : SmallDC) : Module 𝔽₂ E.itH₁_fst

Equations

• E.instModule𝔽₂ItH₁_fst = E.barDh₀.ker.module

def SmallDC.itH₁_snd (E : SmallDC) : Type u_2

Equations

• E.itH₁_snd = (E.vH₀₁ ⧸ E.barDh₁.range)

instance SmallDC.instAddCommGroupItH₁_snd (E : SmallDC) : AddCommGroup E.itH₁_snd

Equations

• E.instAddCommGroupItH₁_snd = Submodule.Quotient.addCommGroup E.barDh₁.range

instance SmallDC.instModule𝔽₂ItH₁_snd (E : SmallDC) : Module 𝔽₂ E.itH₁_snd

Equations

• E.instModule𝔽₂ItH₁_snd = Submodule.Quotient.module E.barDh₁.range

Isomorphism at degree 2

theorem SmallDC.ker_d₂_eq (E : SmallDC) : E.d₂.ker = E.dv₁.ker ⊓ E.dh₁.ker

theorem SmallDC.barDh₁_val (E : SmallDC) (x : E.vH₁₁) : ↑(E.barDh₁ x) = E.dh₁ ↑x

theorem SmallDC.barDh₁_ker_iff (E : SmallDC) (x : E.vH₁₁) : x ∈ E.barDh₁.ker ↔ ↑x ∈ E.dh₁.ker

def SmallDC.homologyEquiv_n2 (E : SmallDC) : E.totH₂ ≃ₗ[𝔽₂] E.itH₂

Equations

• One or more equations did not get rendered due to their size.

Isomorphism at degree 0

theorem SmallDC.range_d₁_eq (E : SmallDC) : E.d₁.range = E.dh₀.range ⊔ E.dv₀.range

theorem SmallDC.barDh₀_range_eq (E : SmallDC) : E.barDh₀.range = Submodule.map E.dv₀.range.mkQ (E.dh₀.range ⊔ E.dv₀.range)

def SmallDC.homologyEquiv_n0 (E : SmallDC) : E.totH₀ ≃ₗ[𝔽₂] E.itH₀

Equations

• One or more equations did not get rendered due to their size.

Isomorphism at degree 1

We construct the isomorphism H₁(Tot(E)) ≃ ker(barDh₀) × (vH₀₁ / range(barDh₁)) via a short exact sequence that splits over 𝔽₂.

The short exact sequence is: 0 → vH₀₁/range(barDh₁) →ⁱ totH₁ →^π ker(barDh₀) → 0 where i([b]) = [(0,b)] and π([(a,b)]) = [a]. Over 𝔽₂, this splits by Submodule.exists_isCompl.

def SmallDC.piMap (E : SmallDC) : ↥E.totZ₁ →ₗ[𝔽₂] E.vH₁₀

The projection π: totZ₁ → vH₁₀ sending (a,b) ↦ [a].

Equations

• E.piMap = E.dv₁.range.mkQ ∘ₗ LinearMap.fst 𝔽₂ E.A₁₀ E.A₀₁ ∘ₗ E.totZ₁.subtype

theorem SmallDC.piMap_mem_ker (E : SmallDC) (z : ↥E.totZ₁) : E.piMap z ∈ E.barDh₀.ker

π lands in ker(barDh₀).

def SmallDC.piMap' (E : SmallDC) : ↥E.totZ₁ →ₗ[𝔽₂] ↥E.barDh₀.ker

π lifted to land in ker(barDh₀) = itH₁_fst.

Equations

• E.piMap' = LinearMap.codRestrict E.barDh₀.ker E.piMap ⋯

theorem SmallDC.piMap'_vanishes_on_B₁ (E : SmallDC) : E.totB₁InZ₁ ≤ E.piMap'.ker

π vanishes on totB₁InZ₁, so it descends to totH₁.

def SmallDC.piBar (E : SmallDC) : E.totH₁ →ₗ[𝔽₂] E.itH₁_fst

π descended to totH₁ → itH₁_fst.

Equations

• E.piBar = E.totB₁InZ₁.liftQ E.piMap' ⋯

def SmallDC.iotaMap (E : SmallDC) : ↥E.dv₀.ker →ₗ[𝔽₂] ↥E.totZ₁

The inclusion ι: ker(dv₀) → totZ₁ sending b ↦ (0,b).

Equations

• E.iotaMap = LinearMap.codRestrict E.totZ₁ (LinearMap.inr 𝔽₂ E.A₁₀ E.A₀₁ ∘ₗ E.dv₀.ker.subtype) ⋯

theorem SmallDC.iotaMap_vanishes_on_barDh₁ (E : SmallDC) : E.barDh₁.range ≤ (E.totB₁InZ₁.mkQ ∘ₗ E.iotaMap).ker

ι vanishes on range(barDh₁).

def SmallDC.iotaBar (E : SmallDC) : E.itH₁_snd →ₗ[𝔽₂] E.totH₁

ι descended to itH₁_snd = vH₀₁/range(barDh₁) → totH₁.

Equations

• E.iotaBar = E.barDh₁.range.liftQ (E.totB₁InZ₁.mkQ ∘ₗ E.iotaMap) ⋯

theorem SmallDC.piBar_comp_iotaBar (E : SmallDC) : E.piBar ∘ₗ E.iotaBar = 0

Exactness: piBar ∘ iotaBar = 0.

theorem SmallDC.mem_range_barDh₁_of_inr_mem_range_d₂ (E : SmallDC) {b : E.A₀₁} (hb : b ∈ E.dv₀.ker) (h : (0, b) ∈ E.d₂.range) : ⟨b, hb⟩ ∈ E.barDh₁.range

Helper: if (0,b) with b ∈ ker(dv₀) lies in range(d₂), then b ∈ range(barDh₁).

theorem SmallDC.iotaBar_injective (E : SmallDC) : Function.Injective ⇑E.iotaBar

iotaBar is injective.

theorem SmallDC.piBar_surjective (E : SmallDC) : Function.Surjective ⇑E.piBar

piBar is surjective.

theorem SmallDC.piBar_ker_eq_iotaBar_range (E : SmallDC) : E.piBar.ker = E.iotaBar.range

ker(piBar) = range(iotaBar).

def SmallDC.homologyEquiv_n1 (E : SmallDC) : E.totH₁ ≃ₗ[𝔽₂] E.itH₁_fst × E.itH₁_snd

The isomorphism H₁(Tot) ≃ ker(barDh₀) × (vH₀₁ / im(barDh₁)). Constructed via a split short exact sequence over 𝔽₂: 0 → itH₁_snd →^iotaBar totH₁ →^piBar itH₁_fst → 0 which splits because 𝔽₂ is a field.

Equations

• One or more equations did not get rendered due to their size.