The Kronecker (evaluation) classifier Hⁿ(X; F₂) → Hom(Hₙ(X; F₂), F₂) #
This file builds the honest, general, formalized evaluation classifier map
Hⁿ(X; F₂) ⟶ Hom_{F₂}(Hₙ(X; F₂), F₂)
for the library's constructed singular cohomology cohomologyZMod2 X n
(= Hⁿ(Hom(C_•(X), F₂))) and the singular homology homologyZMod2 X n
(= Hₙ(C_•(X) ⊗ F₂)) of the same F₂ chain complex C_•(X) underlying the
project's cochain complex.
This is the canonical natural map of the universal-coefficient sequence: it
sends a cohomology class [φ] (the class of an n-cocycle φ) to the functional
[z] ↦ φ(z) (evaluate the cocycle on a homology cycle). It is the classifier
map in the always-constructible direction. Concretely it is built by descending,
through the cokernel presentation Hₙ(C) = coker(∂ : C_{n+1} → Z_n(C)), the
evaluation Z_n(C) → F₂, c ↦ φ(c), which kills boundaries exactly because φ
is a cocycle (δφ = ∂^* φ = 0); the bundled map descends, through the
cokernel presentation of Hⁿ(Hom(C, F₂)), the linear assignment cocycle ↦ its Kronecker functional, which kills coboundaries.
Main declarations #
chainCxZMod2 X/homologyZMod2 X n— theF₂singular chain complex ofXunderlying the library's cochain complex, and itsn-th homology object.kroneckerFunctional X n φ hφ : Hₙ(X; F₂) ⟶ F₂— the functional on homology defined by a cocycleφ.kroneckerFunctional_homologyπ— its defining factorization throughhomologyπ.kroneckerFunctional_apply— its value on a homology cycle class:⟨[φ], [c]⟩ = φ(c).kroneckerFunctional_add,kroneckerFunctional_smul—F₂-linearity in the cocycle.kroneckerFunctional_coboundary— the functional of a coboundary is zero.kroneckerMap X n : Hⁿ(X; F₂) ⟶ Hom_{F₂}(Hₙ(X; F₂), F₂)— the bundledF₂-linear classifier map.kroneckerMap_cocycleClass—kroneckerMap [φ] = kroneckerFunctional φ.
Scope / blocker #
The map kroneckerMap is the universal-coefficient evaluation map. Over the
field F₂ it is an isomorphism (the universal coefficient theorem degenerates,
Hom(−, F₂) being exact); its injectivity and surjectivity require that
exactness, which is not available as a packaged instance in pinned Mathlib and is
the precise remaining input toward inverting the classifier (and thereby
producing a class α ∈ H¹(RPⁿ; F₂) from the monodromy character, together with a
degree-one Hurewicz comparison π₁(X)ᵃᵇ ≅ H₁(X; ℤ)).
The F₂ singular chain complex of X underlying the library's cochain
complex cochainCxZMod2 X = Hom(C_•(X), F₂).
Equations
- SphereOddDegree.chainCxZMod2 X = ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat (ZMod 2))).obj ↧(ZMod 2)).obj X
Instances For
The n-th singular homology Hₙ(X; F₂), as a ModuleCat (ZMod 2)-object.
Equations
Instances For
The F₂-linear dual Hom_{F₂}(Hₙ(X; F₂), F₂) of singular homology, the
codomain of the Kronecker classifier.
Equations
- SphereOddDegree.homologyDualZMod2 X n = ↧(↑(SphereOddDegree.homologyZMod2 X n) →ₗ[ZMod 2] ZMod 2)
Instances For
Extensionality for maps out of Hₙ(X; F₂): since homologyπ is an
epimorphism, two morphisms out of homology agree once they agree after
precomposition with homologyπ.
The cocycle condition rewritten on the chain differential: for a cocycle φ,
the composite ∂ ≫ (iCycles ≫ φ) = 0, so iCycles ≫ φ descends along the
cokernel homologyπ.
The Kronecker functional of a cocycle φ: the F₂-linear functional on
Hₙ(X; F₂) obtained by descending the evaluation Z_n(C) → F₂, c ↦ φ(c),
through the cokernel presentation Hₙ(C) = coker(∂ : C_{n+1} → Z_n).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Defining factorization of the Kronecker functional: precomposing with
homologyπ recovers the evaluation iCycles ≫ φ.
Evaluate cocycles on homology classes through the Kronecker pairing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Kronecker map from cohomology to the linear dual of homology.
Equations
- One or more equations did not get rendered due to their size.