Explicit inflation is canonical inflation

For a normal subgroup N of a topological group G and a discrete G-module M, inflation exists twice. On the explicit low-degree complex it is TauCeti.ContCohomology.explicitInfl0, explicitInfl1 and explicitInfl2: pullback along G → G ⧸ N paired with the inclusion M ^ N ↪ M. On Mathlib's continuous cohomology it is TauCeti.ContinuousCohomology.infl, whose source is the cohomology of the canonical N-invariants TopRep.quotientToInvariants X N of X = ofDiscreteModule ℤ G M. The coefficient dictionary TauCeti.ofDiscreteModuleQuotient identifies the explicit fixed-point module M ^ N, as a discrete G ⧸ N-module, with those canonical invariants.

This file proves that the comparison isomorphisms between the explicit and the canonical models carry the first inflation to the second in degree 0, and in degrees 1 and 2 when G is compact and its action on M is continuous. The input is a single identity of coefficient morphisms, ofDiscreteModulePair_quotientMk_subtype: the canonical inflation pair, read through the dictionary, is the compatible pair of explicit inflation. It turns canonical inflation after the dictionary into a single compatible-pair pullback in every degree (coeffMap_ofDiscreteModuleQuotient_comp_infl), and the naturality of each low-degree comparison in compatible pairs then gives the transport squares.

Main results

• TauCeti.ContCohomology.coeffMap_ofDiscreteModuleQuotient_comp_infl: in every degree, canonical inflation after the dictionary morphism is the pullback along the explicit inflation pair.
• TauCeti.ContCohomology.explicitH0Iso_infl, explicitIso_infl and explicitIso_infl2: the comparison isomorphisms in degrees 0, 1 and 2 carry explicit inflation to canonical inflation.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2 for the comparison of inhomogeneous and homogeneous cochains, and Ch. I, §5 for inflation.

theorem TauCeti.ContCohomology.ofDiscreteModulePair_quotientMk_subtype (G M : Type u) [Group G] [TopologicalSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] : ofDiscreteModulePair (↑(ContinuousMonoidHom.quotientMk N)) (FixedPoints.addSubgroup (↥N) M).subtype.toIntLinearMap ⋯ = CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑(ContinuousMonoidHom.quotientMk N)).map (ofDiscreteModuleQuotient G M N)) ((ofDiscreteModule ℤ G M).quotientToInvariantsι N)

The inflation pair through the dictionary. Composing the dictionary morphism M ^ N ⟶ (ofDiscreteModule ℤ G M)ᴺ with the inclusion of the canonical invariants gives the compatible pair of explicit inflation: the quotient map G → G ⧸ N with the inclusion M ^ N ↪ M.

theorem TauCeti.ContCohomology.coeffMap_ofDiscreteModuleQuotient_comp_infl (G M : Type u) [Group G] [TopologicalSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] [IsTopologicalGroup G] (n : ℕ) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.coeffMap (ofDiscreteModuleQuotient G M N) n) (ContinuousCohomology.infl N (ofDiscreteModule ℤ G M) n) = ContinuousCohomology.map (ContinuousMonoidHom.quotientMk N) (ofDiscreteModulePair (↑(ContinuousMonoidHom.quotientMk N)) (FixedPoints.addSubgroup (↥N) M).subtype.toIntLinearMap ⋯) n

Canonical inflation on the dictionary. In every degree, the canonical inflation map of ofDiscreteModule ℤ G M, precomposed with the coefficient map of the dictionary morphism ofDiscreteModuleQuotient, is the pullback along the compatible pair of explicit inflation.

theorem TauCeti.ContCohomology.coeffMap_ofDiscreteModuleQuotient_comp_infl_assoc (G M : Type u) [Group G] [TopologicalSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] [IsTopologicalGroup G] (n : ℕ) {Z : TopModuleCat ℤ} (h : continuousCohomology n (ofDiscreteModule ℤ G M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.coeffMap (ofDiscreteModuleQuotient G M N) n) (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.infl N (ofDiscreteModule ℤ G M) n) h) = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map (ContinuousMonoidHom.quotientMk N) (ofDiscreteModulePair (↑(ContinuousMonoidHom.quotientMk N)) (FixedPoints.addSubgroup (↥N) M).subtype.toIntLinearMap ⋯) n) h

Canonical inflation on the dictionary. In every degree, the canonical inflation map of ofDiscreteModule ℤ G M, precomposed with the coefficient map of the dictionary morphism ofDiscreteModuleQuotient, is the pullback along the compatible pair of explicit inflation.

@[simp]

theorem TauCeti.ContCohomology.explicitH0Iso_infl (G M : Type u) [Group G] [TopologicalSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] [IsTopologicalGroup G] (x : ↥(H0 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M))) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.infl N (ofDiscreteModule ℤ G M) 0)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleQuotient G M N) 0)) ((CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)).hom) x)) = (CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G M).hom) ((explicitInfl0 G M N) x)

Transport of inflation in degree zero. The degree-zero comparison carries explicit inflation to canonical inflation, read through the dictionary morphism ofDiscreteModuleQuotient.

@[simp]

theorem TauCeti.ContCohomology.explicitIso_infl (G M : Type u) [Group G] [TopologicalSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] [IsTopologicalGroup G] [ContinuousSMul G M] [CompactSpace G] (x : DiscreteH1 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.infl N (ofDiscreteModule ℤ G M) 1)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleQuotient G M N) 1)) ((CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)).hom) x)) = (CategoryTheory.ConcreteCategory.hom (explicitH1IsoContinuousCohomology G M).hom) ((discreteH1Equiv G M).symm ((explicitInfl1 G M N) ((discreteH1Equiv (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)) x)))

Transport of inflation in degree one. The degree-one comparison carries explicit inflation to canonical inflation, read through the dictionary morphism ofDiscreteModuleQuotient.

@[simp]

theorem TauCeti.ContCohomology.explicitIso_infl2 (G M : Type u) [Group G] [TopologicalSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] [IsTopologicalGroup G] [ContinuousSMul G M] [CompactSpace G] (x : DiscreteH2 (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.infl N (ofDiscreteModule ℤ G M) 2)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleQuotient G M N) 2)) ((CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)).hom) x)) = (CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology G M).hom) ((discreteH2Equiv G M).symm ((explicitInfl2 G M N) ((discreteH2Equiv (G ⧸ N) ↥(FixedPoints.addSubgroup (↥N) M)) x)))

Transport of inflation in degree two. The degree-two comparison carries explicit inflation to canonical inflation, read through the dictionary morphism ofDiscreteModuleQuotient.