Documentation

TauCeti.RepresentationTheory.Homological.TateCohomology.Inflation

Inflation in positive-degree Tate cohomology #

For a normal subgroup S of a finite group G, ordinary group cohomology has the canonical inflation map

H^n(G/S, M^S) ⟶ H^n(G, M).

In positive degrees, Mathlib identifies Tate cohomology naturally with ordinary group cohomology. This file transports ordinary inflation across that identification. The resulting map is natural in the coefficient representation, and the comparison square with ordinary inflation commutes by construction.

Tate degree zero is deliberately excluded: there it is a quotient by the norm and does not carry this naive inflation map.

Main definitions #

Main statements #

References #

source
noncomputable def TauCeti.TateCohomology.inflNatTrans {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [S.Normal] (n : ℕ) [NeZero n] :
(Rep.quotientToInvariantsFunctor R S).comp (tateCohomologyFunctor ↑n) ⟶ tateCohomologyFunctor ↑n

Inflation in positive-degree Tate cohomology. For a normal subgroup S ◁ G, this is the natural transformation

Ĥ^n(G/S, M^S) ⟶ Ĥ^n(G, M),

obtained by transporting ordinary cohomological inflation across Mathlib's natural comparison between positive-degree Tate cohomology and group cohomology.

Instances For
    source
    noncomputable def TauCeti.TateCohomology.infl {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [S.Normal] (M : Rep R G) (n : ℕ) [NeZero n] :
    tateCohomology ((Rep.quotientToInvariantsFunctor R S).obj M) ↑n ⟶ tateCohomology M ↑n

    Positive-degree Tate inflation on a coefficient representation.

    Instances For
      source
      @[simp]
      theorem TauCeti.TateCohomology.inflNatTrans_app {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [S.Normal] (M : Rep R G) (n : ℕ) [NeZero n] :
      (inflNatTrans S n).app M = infl S M n

      Evaluating the natural transformation of positive-degree Tate inflation gives infl.

      source
      theorem TauCeti.TateCohomology.infl_def {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [S.Normal] (M : Rep R G) (n : ℕ) [NeZero n] :
      infl S M n = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app ((Rep.quotientToInvariantsFunctor R S).obj M)) (CategoryTheory.CategoryStruct.comp ((groupCohomology.infNatTrans R S n).app M) ((TateCohomology.isoGroupCohomology n).inv.app M))

      The defining expression for positive-degree Tate inflation: compare with ordinary cohomology, inflate there, and compare back.

      source
      @[simp]
      theorem TauCeti.TateCohomology.infl_comp_isoGroupCohomology_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [S.Normal] (M : Rep R G) (n : ℕ) [NeZero n] :
      CategoryTheory.CategoryStruct.comp (infl S M n) ((TateCohomology.isoGroupCohomology n).hom.app M) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app ((Rep.quotientToInvariantsFunctor R S).obj M)) ((groupCohomology.infNatTrans R S n).app M)

      Positive-degree Tate inflation agrees with ordinary inflation under Mathlib's canonical Tate-to-ordinary comparison.

      source
      @[simp]
      theorem TauCeti.TateCohomology.infl_comp_isoGroupCohomology_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [S.Normal] (M : Rep R G) (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : (groupCohomology.functor R G n).obj M ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (infl S M n) (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app M) h) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app ((Rep.quotientToInvariantsFunctor R S).obj M)) (CategoryTheory.CategoryStruct.comp ((groupCohomology.infNatTrans R S n).app M) h)

      Positive-degree Tate inflation agrees with ordinary inflation under Mathlib's canonical Tate-to-ordinary comparison.

      source
      theorem TauCeti.TateCohomology.map_comp_infl {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [S.Normal] {M N : Rep R G} (f : M ⟶ N) (n : ℕ) [NeZero n] :
      CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor ↑n).map ((Rep.quotientToInvariantsFunctor R S).map f)) (infl S N n) = CategoryTheory.CategoryStruct.comp (infl S M n) ((tateCohomologyFunctor ↑n).map f)

      Positive-degree Tate inflation is natural in the coefficient representation.

      source
      theorem TauCeti.TateCohomology.map_comp_infl_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [S.Normal] {M N : Rep R G} (f : M ⟶ N) (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : tateCohomology N ↑n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor ↑n).map ((Rep.quotientToInvariantsFunctor R S).map f)) (CategoryTheory.CategoryStruct.comp (infl S N n) h) = CategoryTheory.CategoryStruct.comp (infl S M n) (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor ↑n).map f) h)

      Positive-degree Tate inflation is natural in the coefficient representation.