Mayer–Vietoris base case: H₁(S¹; ℤ) ≅ ℤ

We compute the integral first homology of the circle S¹ by the singular Mayer–Vietoris sequence applied to the two-punctured cover specialized from the recursive step file (SphereHomologyMVStep.lean), with n = 0:

• U = S¹ \ {north}, V = S¹ \ {south} are contractible;
• U ∩ V (the equatorial band) is homotopy equivalent to S⁰.

Around degree 1 the sequence reads H₁(U) ⊕ H₁(V) → H₁(S¹) → H₀(U ∩ V) → H₀(U) ⊕ H₀(V). The left term vanishes (contractibility), so the connecting map identifies H₁(S¹) ≅ ker(H₀(U ∩ V) → H₀(U) ⊕ H₀(V)). Using the augmentation isomorphism H₀(contractible) ≅ ℤ (SingularH0PathConnected.lean), that kernel coincides with the kernel of the augmentation H₀(U ∩ V) → ℤ, i.e. with the reduced zeroth homology H_tilde₀(S⁰) ≅ ℤ.

The result sphereTopHomologyIsoOne : SphereTopHomologyIso 1 supplies the base field of SphereSuspensionTower.

Setup for the circle cover (the n = 0 specialization)

@[reducible, inline]

abbrev SphereOddDegree.circleTop : TopCat

The circle S¹ as a TopCat (the n = 0 instance of sphereSpace).

Equations

• SphereOddDegree.circleTop = SphereOddDegree.sphereSpace 0

@[reducible, inline]

abbrev SphereOddDegree.circU : TopologicalSpace.Opens ↑circleTop

The upper-punctured open cover member.

Equations

• SphereOddDegree.circU = SphereOddDegree.upperOpens 0

@[reducible, inline]

abbrev SphereOddDegree.circV : TopologicalSpace.Opens ↑circleTop

The lower-punctured open cover member.

Equations

• SphereOddDegree.circV = SphereOddDegree.lowerOpens 0

theorem SphereOddDegree.circUV_top : circU ⊔ circV = ⊤

@[reducible, inline]

abbrev SphereOddDegree.circBand : Set ↑circleTop

The equatorial band S¹ \ {north, south} as a subset.

Equations

• SphereOddDegree.circBand = ↑SphereOddDegree.circU ∩ ↑SphereOddDegree.circV

@[reducible, inline]

noncomputable abbrev SphereOddDegree.circF0 : HomologicalComplex.homology (subChainComplex ℤ circleTop circBand) 0 ⟶ HomologicalComplex.homology (subChainComplex ℤ circleTop ↑circU ⊞ subChainComplex ℤ circleTop ↑circV) 0

The Mayer–Vietoris left map on H₀, H₀(U ∩ V) → H₀(U) ⊕ H₀(V).

Equations

• SphereOddDegree.circF0 = HomologicalComplex.homologyMap (SphereOddDegree.mvShortComplex ℤ SphereOddDegree.circU SphereOddDegree.circV SphereOddDegree.circUV_top).f 0

Reduced H₀(S⁰) ≅ ℤ

instance SphereOddDegree.instNonemptySphere0 : Nonempty (Sphere 0)

A point of S⁰.

theorem SphereOddDegree.linearEquiv_int_of_finrank_one {N : Type} [AddCommGroup N] [Module ℤ N] [Module.Free ℤ N] [Module.Finite ℤ N] (h : Module.finrank ℤ N = 1) : Nonempty (N ≃ₗ[ℤ] ℤ)

theorem SphereOddDegree.ker_linearEquiv_int_of_finrank_two {M : Type} [AddCommGroup M] [Module ℤ M] [Module.Free ℤ M] [Module.Finite ℤ M] (hM : Module.finrank ℤ M = 2) (g : M →ₗ[ℤ] ℤ) (hg : Function.Surjective ⇑g) : Nonempty (↥g.ker ≃ₗ[ℤ] ℤ)

Algebra helper. The kernel of a surjection from a rank-2 finite free ℤ-module onto ℤ is isomorphic to ℤ.

theorem SphereOddDegree.sphere0_equiv_fin2 : Nonempty (Sphere 0 ≃ Fin 2)

theorem SphereOddDegree.h0_sphere0_free_finrank : Module.Free ℤ ↑(HomologicalComplex.homology (AffineBarycentricSubdivision.singularChainComplex ℤ ↧(Sphere 0)) 0) ∧ Module.Finite ℤ ↑(HomologicalComplex.homology (AffineBarycentricSubdivision.singularChainComplex ℤ ↧(Sphere 0)) 0) ∧ Module.finrank ℤ ↑(HomologicalComplex.homology (AffineBarycentricSubdivision.singularChainComplex ℤ ↧(Sphere 0)) 0) = 2

theorem SphereOddDegree.reducedH0_sphere0_iso : Nonempty (CategoryTheory.Limits.kernel (H0aug ↧(Sphere 0)) ≅ ↧ℤ)

The kernel of the band augmentation is ℤ

theorem SphereOddDegree.kerBand_iso : Nonempty (CategoryTheory.Limits.kernel (subH0aug circleTop circBand) ≅ ↧ℤ)

The kernel of the band augmentation H₀(U ∩ V) → ℤ is isomorphic to ℤ, using the homotopy equivalence U ∩ V ≃ S⁰ and reducedH0_sphere0_iso.

The Mayer–Vietoris kernel identity

theorem SphereOddDegree.circF_comp_fst : CategoryTheory.CategoryStruct.comp (mvShortComplex ℤ circU circV circUV_top).f CategoryTheory.Limits.biprod.fst = mvInclUVU ℤ circU circV

theorem SphereOddDegree.circF_comp_snd : CategoryTheory.CategoryStruct.comp (mvShortComplex ℤ circU circV circUV_top).f CategoryTheory.Limits.biprod.snd = -mvInclUVV ℤ circU circV

theorem SphereOddDegree.biprod_homology_zero_iff (y : ↑(HomologicalComplex.homology (subChainComplex ℤ circleTop ↑circU ⊞ subChainComplex ℤ circleTop ↑circV) 0)) : y = 0 ↔ (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap CategoryTheory.Limits.biprod.fst 0)) y = 0 ∧ (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap CategoryTheory.Limits.biprod.snd 0)) y = 0

Joint monomorphism of the homology biproduct projections. An element of H₀(X₂) is zero iff both of its biproduct components vanish.

theorem SphereOddDegree.kerF0_iso_kerBand : Nonempty (CategoryTheory.Limits.kernel circF0 ≅ CategoryTheory.Limits.kernel (subH0aug circleTop circBand))

The Mayer–Vietoris kernel coincides with the reduced-H₀ kernel. ker(H₀(U ∩ V) → H₀(U) ⊕ H₀(V)) ≅ ker(H₀(U ∩ V) → ℤ).

Assembling the Mayer–Vietoris connecting isomorphism

theorem SphereOddDegree.sphereH1_iso_kerF0 : Nonempty (sphereTopHomologyℤ 1 ≅ CategoryTheory.Limits.kernel circF0)

The base case

theorem SphereOddDegree.sphereTopHomology_one_iso_nonempty : Nonempty (sphereTopHomologyℤ 1 ≅ ↧ℤ)

H₁(S¹; ℤ) ≅ ℤ (as a Nonempty package).

noncomputable def SphereOddDegree.sphereTopHomologyIsoOne : SphereTopHomologyIso 1

The base case of the sphere suspension tower: H₁(S¹; ℤ) ≅ ℤ.

Equations

• SphereOddDegree.sphereTopHomologyIsoOne = SphereOddDegree.sphereTopHomology_one_iso_nonempty.some