Homology in TopModuleCat as a concrete subquotient #
Mathlib proves that TopModuleCat R is a CategoryWithHomology by exhibiting, for a short
complex S, the kernel TopModuleCat.ker S.g with its subspace topology and the cokernel
TopModuleCat.coker with its quotient topology as left and right homology data. On the cycles
side the resulting identification is available generically, as
ShortComplex.isoCyclesOfIsLimit (TopModuleCat.isLimitKer S.g) : TopModuleCat.ker S.g ≅ S.cycles;
on the homology side there is no such generic statement, so this file names it:
ShortComplex.homologyIsoCoker identifies S.homology with the honest cokernel of S.toCycles.
Mathlib's ShortComplex.homologyIsoCokernelLift is the analogous statement for the categorical
cokernel, which says nothing about which topology that object carries; the point of the
isomorphism below is that the topology is the quotient topology on a cokernel.
Two consequences are recorded. The first is that the cycles really are a submodule of the middle
term and the homology really is a quotient of the cycles: ShortComplex.iCycles_injective,
ShortComplex.homologyπ_surjective and ShortComplex.homologyπ_eq_zero_iff describe the cycle
inclusion and the class map elementwise. The surjectivity does not follow from
ShortComplex.homologyπ being an epimorphism, since an epimorphism of topological modules need
not be surjective.
The second is that homology in TopModuleCat R inherits discreteness: a short
complex whose middle term is discrete has discrete cycles and discrete homology, and likewise
degreewise for a homological complex. This is what makes continuous cohomology of a discrete
representation of a compact group an isomorphism problem between discrete topological modules
rather than between the quotient topologies the cochain spaces happen to carry.
Both identifications are then turned into elementwise constructors. ShortComplex.cyclesMkOfEq
builds the cycle determined by an element of the middle term killed by S.g; it is the
counterpart, for TopModuleCat R, of Mathlib's CategoryTheory.ShortComplex.cyclesMk, which asks
for an abelian category and so does not apply here. ShortComplex.descHomologyₗ descends a linear
map out of the cycles that vanishes on the kernel of the class map to a linear map out of the
homology; unlike Mathlib's CategoryTheory.ShortComplex.descHomology it produces a linear map
into an arbitrary module rather than a morphism of TopModuleCat R, which is what a bilinear
operation on homology, such as a cup product, needs in its first variable. Both have degreewise
forms for a homological complex.
Exactness of a pair of composable maps of topological modules follows from exactness of the maps of modules they become after forgetting topologies, up to conjugation by isomorphisms.
The continuous linear equivalence underlying an isomorphism of topological modules acts as the forward morphism of the isomorphism.
The homology of a short complex of topological modules is the cokernel of S.toCycles,
carrying the quotient topology.
Equations
Instances For
homologyIsoCoker identifies the projection S.homologyπ onto homology with the projection
TopModuleCat.cokerπ onto the concrete cokernel.
homologyIsoCoker identifies the projection S.homologyπ onto homology with the projection
TopModuleCat.cokerπ onto the concrete cokernel.
The form of homologyπ_comp_homologyIsoCoker_hom facing the inverse isomorphism: the
projection onto the concrete cokernel, followed back into homology, is S.homologyπ.
The form of homologyπ_comp_homologyIsoCoker_hom facing the inverse isomorphism: the
projection onto the concrete cokernel, followed back into homology, is S.homologyπ.
The class map onto the homology of a short complex of topological modules is surjective: the
homology is a quotient of the cycles, not merely their receptacle of an epimorphism. In
TopModuleCat R an epimorphism need not be surjective, so this does not follow from
CategoryTheory.ShortComplex.homologyπ being an epimorphism.
A cycle of a short complex of topological modules has trivial homology class exactly when it is a boundary.
The inclusion of the cycles of a short complex of topological modules into its middle term is
injective: two cycles with the same underlying element of the middle term are equal, so equalities
between cycles can be checked after applying S.iCycles.
The cycles of a short complex of topological modules with discrete middle term are discrete.
The homology of a short complex of topological modules with discrete middle term is discrete.
The cycle of a short complex of topological modules determined by an element of the middle
term killed by S.g. This is the counterpart for TopModuleCat R of Mathlib's
CategoryTheory.ShortComplex.cyclesMk, which requires an abelian category.
Equations
- S.cyclesMkOfEq x hx = (CategoryTheory.ConcreteCategory.hom (S.isoCyclesOfIsLimit (TopModuleCat.isLimitKer S.g)).hom) ⟨x, hx⟩
Instances For
The underlying element of S.cyclesMkOfEq x hx is x.
A cycle is the cycle determined by its underlying element.
Descent of a linear map to homology. A linear map out of the cycles of a short complex of
topological modules that vanishes on the kernel of the class map S.homologyπ descends to a linear
map out of the homology, with descHomologyₗ_π as its defining equation. Unlike Mathlib's
CategoryTheory.ShortComplex.descHomology, the target is an arbitrary module rather than an object
of TopModuleCat R, so that maps into spaces of linear maps can be descended.
Equations
- S.descHomologyₗ k hk = (↑(TopModuleCat.Hom.hom S.toCycles)).range.liftQ k ⋯ ∘ₗ ↑↑S.homologyIsoCoker.toContinuousLinearEquiv
Instances For
The defining equation of descHomologyₗ: on the class of a cycle it takes the given value.
When the incoming map of a short complex of topological modules vanishes, the class map from its cycles to its homology is injective.
The class map onto the degreewise homology of a homological complex of topological modules is surjective.
A cycle of a homological complex of topological modules has trivial homology class exactly
when it is a boundary, m being the degree preceding n.
The inclusion of the degree-n cycles of a homological complex of topological modules into
its degree-n term is injective.
A homological complex of topological modules that is discrete in degree n has discrete
cycles in degree n.
A homological complex of topological modules that is discrete in degree n has discrete
homology in degree n.
The degree-n cycle of a homological complex of topological modules determined by an element
of degree n killed by the differential to the next degree j. This is the counterpart for
TopModuleCat R of Mathlib's HomologicalComplex.cyclesMk, which requires an abelian category.
Equations
- K.cyclesMkOfEq x j hj hx = (K.sc n).cyclesMkOfEq x ⋯
Instances For
The underlying element of K.cyclesMkOfEq x j hj hx is x.
The differential vanishes on the underlying element of a cycle.
The underlying element of the cycle K.toCycles i n x is the differential of x.
Descent of a linear map to degreewise homology. A linear map out of the degree-n cycles
of a homological complex of topological modules that vanishes on the kernel of the class map
descends to the degree-n homology, with descHomologyₗ_π as its defining equation.
Equations
- K.descHomologyₗ k hk = (K.sc n).descHomologyₗ k hk
Instances For
The defining equation of descHomologyₗ: on the class of a cycle it takes the given value.
When the differential into degree n vanishes, the class map from the degree-n cycles to
the degree-n homology is injective, m being the degree preceding n.