Naturality and bijectivity of the Kronecker classifier over F₂

This file upgrades the evaluation classifier kroneckerMap X n : Hⁿ(X; F₂) ⟶ Hom_{F₂}(Hₙ(X; F₂), F₂) (H1ClassifierZMod2.lean) to:

• its naturality in the space X — the Kronecker pairing is natural, ⟨f^* a, z⟩ = ⟨a, f_* z⟩ (kroneckerMap_naturality, kroneckerMap_naturality_apply);
• its injectivity over the field F₂ (kroneckerMap_injective) — the second, "uniqueness" half of the universal coefficient theorem over a field;
• hence its bijectivity and the bundled universal coefficient isomorphism kroneckerEquiv X n : Hⁿ(X; F₂) ≅ Hom_{F₂}(Hₙ(X; F₂), F₂).

Together with the already-proved kroneckerMap_surjective this completes the degree-n universal coefficient theorem over F₂ for the library's own singular (co)homology, as a natural isomorphism.

Main declarations

• chainMapZMod2 f / homologyPushZMod2 f n — the covariant chain map and the pushforward f_* : Hₙ(X; F₂) ⟶ Hₙ(Y; F₂) of a continuous map f.
• homologyDualMap f n — the dual (precomposition) map Hom(Hₙ(Y; F₂), F₂) ⟶ Hom(Hₙ(X; F₂), F₂).
• kroneckerMap_naturality — the naturality square cohPullback f n ≫ kroneckerMap X n = kroneckerMap Y n ≫ homologyDualMap f n.
• kroneckerMap_injective, kroneckerMap_bijective.
• kroneckerEquiv X n — the universal coefficient isomorphism over F₂.

@[reducible, inline]

noncomputable abbrev SphereOddDegree.chainMapZMod2 {X Y : TopCat} (f : X ⟶ Y) : chainCxZMod2 X ⟶ chainCxZMod2 Y

The covariant F₂ singular chain map induced by a continuous map f.

Equations

• SphereOddDegree.chainMapZMod2 f = ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat (ZMod 2))).obj ↧(ZMod 2)).map f

noncomputable def SphereOddDegree.homologyPushZMod2 {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) : homologyZMod2 X n ⟶ homologyZMod2 Y n

The pushforward f_* : Hₙ(X; F₂) ⟶ Hₙ(Y; F₂) on singular homology.

Equations

• SphereOddDegree.homologyPushZMod2 f n = HomologicalComplex.homologyMap (SphereOddDegree.chainMapZMod2 f) n

noncomputable def SphereOddDegree.homologyDualMap {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) : homologyDualZMod2 Y n ⟶ homologyDualZMod2 X n

The dual / precomposition map Hom(Hₙ(Y; F₂), F₂) ⟶ Hom(Hₙ(X; F₂), F₂) of the homology pushforward.

Equations

• SphereOddDegree.homologyDualMap f n = ModuleCat.ofHom (LinearMap.lcomp (ZMod 2) (ZMod 2) (ModuleCat.Hom.hom (SphereOddDegree.homologyPushZMod2 f n)))

@[simp]

theorem SphereOddDegree.homologyDualMap_hom_apply {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (g : ↑(homologyZMod2 Y n) →ₗ[ZMod 2] ZMod 2) : (ModuleCat.Hom.hom (homologyDualMap f n)) g = g ∘ₗ ModuleCat.Hom.hom (homologyPushZMod2 f n)

theorem SphereOddDegree.cochainPullback_eq_comp {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (φ : singularCochainGroup (ZMod 2) Y n) : cochainPullback f n φ = CategoryTheory.CategoryStruct.comp ((chainMapZMod2 f).f n) φ

The cochain pullback is precomposition with the chain map (definitional).

theorem SphereOddDegree.kroneckerMap_naturality {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) : CategoryTheory.CategoryStruct.comp (cohPullback f n) (kroneckerMap X n) = CategoryTheory.CategoryStruct.comp (kroneckerMap Y n) (homologyDualMap f n)

theorem SphereOddDegree.kroneckerMap_naturality_apply {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (a : ↑(cohomologyZMod2 Y n)) : (ModuleCat.Hom.hom (kroneckerMap X n)) ((ModuleCat.Hom.hom (cohPullback f n)) a) = (ModuleCat.Hom.hom (kroneckerMap Y n)) a ∘ₗ ModuleCat.Hom.hom (homologyPushZMod2 f n)

Element form of kroneckerMap_naturality: ⟨f^* a, z⟩ = ⟨a, f_* z⟩.

theorem SphereOddDegree.zmod2_extend_functional {M : Type} [AddCommGroup M] [Module (ZMod 2) M] (W : Submodule (ZMod 2) M) (f : ↥W →ₗ[ZMod 2] ZMod 2) : ∃ (g : M →ₗ[ZMod 2] ZMod 2), ∀ (w : ↥W), g ↑w = f w

Extension of functionals over the field F₂. Every linear functional on a submodule W of an F₂-module M extends to a functional on all of M. This is the injectivity of the F₂-module ZMod 2.

theorem SphereOddDegree.zmod2_factor_of_ker_le {M N : Type} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup N] [Module (ZMod 2) N] (d : M →ₗ[ZMod 2] N) (φ : M →ₗ[ZMod 2] ZMod 2) (h : d.ker ≤ φ.ker) : ∃ (η : N →ₗ[ZMod 2] ZMod 2), η ∘ₗ d = φ

A functional vanishing on ker d factors through d. If φ : M → F₂ vanishes on the kernel of a linear map d : M → N, then φ = η ∘ d for some functional η : N → F₂. (Over a field: first isomorphism theorem plus the extension zmod2_extend_functional.)

theorem SphereOddDegree.mem_range_iCycles_of_d {X : TopCat} (n : ℕ) (x : ↑((chainCxZMod2 X).X (n + 1))) (hx : (ModuleCat.Hom.hom ((chainCxZMod2 X).d (n + 1) n)) x = 0) : ∃ (c : ↑(HomologicalComplex.cycles (chainCxZMod2 X) (n + 1))), (ModuleCat.Hom.hom (HomologicalComplex.iCycles (chainCxZMod2 X) (n + 1))) c = x

The cycle inclusion realises the kernel of the differential. Any chain element killed by the differential out of degree n+1 is the image of a cycle.

theorem SphereOddDegree.kroneckerMap_injective (X : TopCat) (n : ℕ) : Function.Injective ⇑(ModuleCat.Hom.hom (kroneckerMap X n))

Injectivity of the Kronecker classifier over F₂ (the "uniqueness" half of the universal coefficient theorem over a field): a cohomology class whose Kronecker functional vanishes is zero.

theorem SphereOddDegree.kroneckerMap_bijective (X : TopCat) (n : ℕ) : Function.Bijective ⇑(ModuleCat.Hom.hom (kroneckerMap X n))

The Kronecker classifier is bijective over F₂.

noncomputable def SphereOddDegree.kroneckerEquiv (X : TopCat) (n : ℕ) : cohomologyZMod2 X n ≅ homologyDualZMod2 X n

The universal coefficient isomorphism over F₂: Hⁿ(X; F₂) ≅ Hom_{F₂}(Hₙ(X; F₂), F₂), the Kronecker classifier as an isomorphism of ModuleCat (ZMod 2).

Equations

• SphereOddDegree.kroneckerEquiv X n = (LinearEquiv.ofBijective (ModuleCat.Hom.hom (SphereOddDegree.kroneckerMap X n)) ⋯).toModuleIso