Inflation with trivial 𝔽_p coefficients #
This file compares the canonical map on continuous cohomology along a quotient with explicit
inflation in degree two. The comparison identifies trivial 𝔽_p coefficients on the quotient
with the fixed points of the subgroup action.
Main results #
TauCeti.cohomFpAddEquivH2_cohomFpMap_quotientMk_eq_explicitInfl2: the canonical degree-two map along a quotient is explicit inflation under the cocycle comparison.
theorem
TauCeti.cohomFpAddEquivH2_cohomFpMap_quotientMk_eq_explicitInfl2
(p : ℕ)
(G : Type u)
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
[CompactSpace G]
(N : Subgroup G)
[N.Normal]
[DistribMulAction G (ZMod p)]
[ContinuousSMul G (ZMod p)]
[DistribMulAction (G ⧸ N) (ZMod p)]
[ContinuousSMul (G ⧸ N) (ZMod p)]
(htrivG : ∀ (g : G) (m : ZMod p), g • m = m)
(htrivQ : ∀ (q : G ⧸ N) (m : ZMod p), q • m = m)
(e : ZMod p ≃+ ↥(FixedPoints.addSubgroup (↥N) (ZMod p)))
(he : ∀ (m : ZMod p), ↑(e m) = m)
(hequiv : ∀ (q : G ⧸ N) (m : ZMod p), e ((ContinuousMulEquiv.refl (G ⧸ N)) q • m) = q • e m)
(x : ↑(cohomFp p (G ⧸ N) 2).toModuleCat)
:
(cohomFpAddEquivH2 p G htrivG)
((CategoryTheory.ConcreteCategory.hom (cohomFpMap p (ContinuousMonoidHom.quotientMk N) 2)) x) = (ContCohomology.explicitInfl2 G (ZMod p) N)
((ContCohomology.explicitMap2Equiv (G ⧸ N) (ZMod p) (G ⧸ N) (↥(FixedPoints.addSubgroup (↥N) (ZMod p)))
(ContinuousMulEquiv.refl (G ⧸ N)) e ⋯ ⋯ hequiv)
((cohomFpAddEquivH2 p (G ⧸ N) htrivQ) x))
Under the explicit degree-two comparison, the canonical cohomology map along a quotient is explicit inflation after identifying the trivial coefficients with the subgroup-fixed points.