Tate cohomology of a finite cyclic group is two-periodic

For a finite cyclic group G generated by g, the standard periodic resolution alternates the norm map N with ρ(g) - 𝟙. Consequently the whole two-sided family of Tate groups of a representation M collapses onto just two modules: every even Tate degree is the homology of

M --N--> M --(ρ(g) - 𝟙)--> M,

and every odd Tate degree is the homology of the same two maps in the opposite order.

Mathlib supplies this periodic resolution and its two homology calculations for ordinary group cohomology in positive degrees and for ordinary group homology, together with the comparisons of Tate cohomology with ordinary cohomology in degrees ≥ 1 and with ordinary homology in degrees ≤ -2. This file assembles those comparisons over all of ℤ. The four degree ranges are treated separately, because the two middle degrees are not ordinary (co)homology at all: degree 0 is Mᴳ / N M and degree -1 is ker N / I_G M, and they are matched with the same two periodic models through the low-degree identifications of TauCeti.RepresentationTheory.Homological.TateCohomology.LowDegree.

The parities line up across the splice: for n ≥ 1 an even degree is ordinary cohomology in an even degree, while for n = -(i + 1) ≤ -2 an even degree is ordinary homology in an odd degree, and Mathlib's homology calculation in odd degrees produces exactly the model that its cohomology calculation produces in even degrees.

Provenance

The corresponding all-degree construction is Rep.periodicTateCohomology in ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean from kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509. That development builds a periodic complex of its own; the construction below instead reads the periodicity off Mathlib's imported Tate groups, through the periodic-resolution calculations Rep.FiniteCyclicGroup.groupCohomologyIsoEven, groupCohomologyIsoOdd, groupHomologyIsoEven and groupHomologyIsoOdd.

Main definitions

• Rep.FiniteCyclicGroup.tateCohomologyIso₀: degree zero is the homology of M --N--> M --(ρ(g) - 𝟙)--> M.
• Rep.FiniteCyclicGroup.tateCohomologyIsoNegOne: degree -1 is the homology of M --(ρ(g) - 𝟙)--> M --N--> M.
• Rep.FiniteCyclicGroup.tateCohomologyIsoEven: the common explicit model for every even integer degree.
• Rep.FiniteCyclicGroup.tateCohomologyIsoOdd: the common explicit model for every odd integer degree.
• Rep.FiniteCyclicGroup.periodicIso: two-periodicity, an isomorphism between any two Tate degrees congruent modulo two. Taking n and n + 2 gives the usual statement.
• Rep.FiniteCyclicGroup.periodicFunctor: the periodic chain complex of underlying modules, as a functor of the coefficients. Its homology in an odd degree is the model of degree-zero Tate cohomology and in a nonzero even degree the model of Tate cohomology in degree -1 (periodicHomologyIsoOdd, periodicHomologyIsoEven). Passing to a functor is what makes a short exact sequence of representations induce one of complexes, hence a long exact sequence of these homology groups; splicing it against the two-periodicity above is the exact hexagon that computes Herbrand quotients.
• Rep.FiniteCyclicGroup.normHomCompSubMap and subCompNormHomMap: functoriality of the two short complexes obtained by alternating the norm and ρ(g) - 𝟙.

Main results

• Rep.FiniteCyclicGroup.natCard_tateCohomology_eq_of_modEq: Tate degrees congruent modulo two have the same cardinality. This is the form the Herbrand quotient is computed with.
• Rep.FiniteCyclicGroup.shortExact_map_periodicFunctor: a short exact sequence of representations induces a short exact sequence of periodic chain complexes.
• Rep.FiniteCyclicGroup.homologyMap_comp_periodicHomologyIsoOdd and homologyMap_comp_periodicHomologyIsoEven: the odd- and nonzero-even-degree identifications of the homology of the periodic complex are natural in the coefficients.
• Rep.FiniteCyclicGroup.natCard_periodicHomology_odd and natCard_periodicHomology_even: the homology of the periodic complex in an odd, respectively a nonzero even, degree has the cardinality of Tate cohomology in degree 0, respectively -1.

References

• K. S. Brown, Cohomology of Groups, Chapter VI, §9.
• J.-P. Serre, Local Fields, Chapter VIII, §4.

noncomputable def Rep.FiniteCyclicGroup.tateCohomologyIso₀ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : have x := ⋯; let x := IsCyclic.commGroup; tateCohomology M 0 ≅ (normHomCompSub M g).homology

Degree-zero Tate cohomology of a finite cyclic group generated by g is the homology of M --N--> M --(ρ(g) - 𝟙)--> M.

Both sides are Mᴳ / N M: the left-hand side by the low-degree identification of degree zero, the right-hand side because g generates, so the kernel of ρ(g) - 𝟙 is the invariants.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Rep.FiniteCyclicGroup.tateCohomologyIsoNegOne {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : have x := ⋯; let x := IsCyclic.commGroup; tateCohomology M (-1) ≅ (subCompNormHom M g).homology

Degree -1 Tate cohomology of a finite cyclic group generated by g is the homology of M --(ρ(g) - 𝟙)--> M --N--> M.

Both sides are ker N / I_G M: the left-hand side by the low-degree identification of degree -1, the right-hand side because g generates, so the augmentation submodule is the image of ρ(g) - 𝟙.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Rep.FiniteCyclicGroup.tateCohomologyIsoEven {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (n : ℤ) (hn : Even n) : have x := ⋯; let x := IsCyclic.commGroup; tateCohomology M n ≅ (normHomCompSub M g).homology

In every even integer degree, Tate cohomology of a finite cyclic group generated by g is the homology of M --N--> M --(ρ(g) - 𝟙)--> M.

Positive even degrees are ordinary cohomology in an even degree, degree zero is tateCohomologyIso₀, and a degree -(i + 1) ≤ -2 is even exactly when i is odd, where it is ordinary homology in an odd degree.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Rep.FiniteCyclicGroup.tateCohomologyIsoOdd {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (n : ℤ) (hn : Odd n) : have x := ⋯; let x := IsCyclic.commGroup; tateCohomology M n ≅ (subCompNormHom M g).homology

In every odd integer degree, Tate cohomology of a finite cyclic group generated by g is the homology of M --(ρ(g) - 𝟙)--> M --N--> M.

Positive odd degrees are ordinary cohomology in an odd degree, degree -1 is tateCohomologyIsoNegOne, and a degree -(i + 1) ≤ -2 is odd exactly when i is even and nonzero, where it is ordinary homology in a nonzero even degree.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rep.FiniteCyclicGroup.tateCohomologyIsoEven_zero {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (h0 : Even 0) : tateCohomologyIsoEven M g hg 0 h0 = tateCohomologyIso₀ M g hg

In degree zero, the all-degree even comparison is tateCohomologyIso₀.

@[simp]

theorem Rep.FiniteCyclicGroup.tateCohomologyIsoEven_ofNat_succ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (k : ℕ) (hk : Even (↑k + 1)) : have x := ⋯; let x := IsCyclic.commGroup; tateCohomologyIsoEven M g hg (↑k + 1) hk = (TateCohomology.isoGroupCohomology (k + 1)).app M ≪≫ groupCohomologyIsoEven M g hg (k + 1) ⋯

In a positive even degree, the all-degree comparison is the composite through ordinary group cohomology.

@[simp]

theorem Rep.FiniteCyclicGroup.tateCohomologyIsoEven_negSucc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (k : ℕ) (hk : Even (Int.negSucc k)) : have x := ⋯; let x := IsCyclic.commGroup; tateCohomologyIsoEven M g hg (Int.negSucc k) hk = have hk' := ⋯; have x_1 := ⋯; have x_2 := Classical.decEq G; (TateCohomology.isoGroupHomology (Int.negSucc k) k ⋯).app M ≪≫ groupHomologyIsoOdd M g hg k hk'

In a degree at most -2, the all-degree even comparison is the composite through ordinary group homology in the corresponding odd degree.

@[simp]

theorem Rep.FiniteCyclicGroup.tateCohomologyIsoOdd_ofNat {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (k : ℕ) (hk : Odd ↑k) : have x := ⋯; let x := IsCyclic.commGroup; tateCohomologyIsoOdd M g hg (↑k) hk = have hk' := ⋯; have x_1 := ⋯; (TateCohomology.isoGroupCohomology k).app M ≪≫ groupCohomologyIsoOdd M g hg k hk'

In a positive odd degree, the all-degree comparison is the composite through ordinary group cohomology.

@[simp]

theorem Rep.FiniteCyclicGroup.tateCohomologyIsoOdd_negOne {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (hneg : Odd (-1)) : tateCohomologyIsoOdd M g hg (-1) hneg = tateCohomologyIsoNegOne M g hg

In degree -1, the all-degree odd comparison is tateCohomologyIsoNegOne.

@[simp]

theorem Rep.FiniteCyclicGroup.tateCohomologyIsoOdd_negSucc_succ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (j : ℕ) (hj : Odd (Int.negSucc (j + 1))) : have x := ⋯; let x := IsCyclic.commGroup; tateCohomologyIsoOdd M g hg (Int.negSucc (j + 1)) hj = have hj' := ⋯; have x_1 := Classical.decEq G; (TateCohomology.isoGroupHomology (Int.negSucc (j + 1)) (j + 1) ⋯).app M ≪≫ groupHomologyIsoEven M g hg (j + 1) hj'

In a degree at most -2, the all-degree odd comparison is the composite through ordinary group homology in the corresponding nonzero even degree.

noncomputable def Rep.FiniteCyclicGroup.periodicIsoOfGenerator {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (m n : ℤ) (hmn : m ≡ n [ZMOD 2]) : tateCohomology M m ≅ tateCohomology M n

The generator-dependent comparison underlying two-periodicity. It compares two degrees of the same parity with the same homology object of the standard periodic resolution, using the even model or the odd model according to that common parity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rep.FiniteCyclicGroup.periodicIsoOfGenerator_hom_comp_tateCohomologyIsoEven_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (m n : ℤ) (hmn : m ≡ n [ZMOD 2]) (hn : Even n) : CategoryTheory.CategoryStruct.comp (periodicIsoOfGenerator M g hg m n hmn).hom (tateCohomologyIsoEven M g hg n hn).hom = (tateCohomologyIsoEven M g hg m ⋯).hom

In even degrees, periodicIsoOfGenerator is the comparison obtained by identifying both Tate groups with the even homology object of the periodic resolution. Only n is assumed even: m is then even because m ≡ n [ZMOD 2].

@[simp]

theorem Rep.FiniteCyclicGroup.periodicIsoOfGenerator_hom_comp_tateCohomologyIsoEven_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (m n : ℤ) (hmn : m ≡ n [ZMOD 2]) (hn : Even n) {Z : ModuleCat R} (h : (normHomCompSub M g).homology ⟶ Z) : CategoryTheory.CategoryStruct.comp (periodicIsoOfGenerator M g hg m n hmn).hom (CategoryTheory.CategoryStruct.comp (tateCohomologyIsoEven M g hg n hn).hom h) = CategoryTheory.CategoryStruct.comp (tateCohomologyIsoEven M g hg m ⋯).hom h

In even degrees, periodicIsoOfGenerator is the comparison obtained by identifying both Tate groups with the even homology object of the periodic resolution. Only n is assumed even: m is then even because m ≡ n [ZMOD 2].

@[simp]

theorem Rep.FiniteCyclicGroup.periodicIsoOfGenerator_hom_comp_tateCohomologyIsoOdd_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (m n : ℤ) (hmn : m ≡ n [ZMOD 2]) (hn : Odd n) : CategoryTheory.CategoryStruct.comp (periodicIsoOfGenerator M g hg m n hmn).hom (tateCohomologyIsoOdd M g hg n hn).hom = (tateCohomologyIsoOdd M g hg m ⋯).hom

In odd degrees, periodicIsoOfGenerator is the comparison obtained by identifying both Tate groups with the odd homology object of the periodic resolution. Only n is assumed odd: m is then odd because m ≡ n [ZMOD 2].

@[simp]

theorem Rep.FiniteCyclicGroup.periodicIsoOfGenerator_hom_comp_tateCohomologyIsoOdd_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (m n : ℤ) (hmn : m ≡ n [ZMOD 2]) (hn : Odd n) {Z : ModuleCat R} (h : (subCompNormHom M g).homology ⟶ Z) : CategoryTheory.CategoryStruct.comp (periodicIsoOfGenerator M g hg m n hmn).hom (CategoryTheory.CategoryStruct.comp (tateCohomologyIsoOdd M g hg n hn).hom h) = CategoryTheory.CategoryStruct.comp (tateCohomologyIsoOdd M g hg m ⋯).hom h

In odd degrees, periodicIsoOfGenerator is the comparison obtained by identifying both Tate groups with the odd homology object of the periodic resolution. Only n is assumed odd: m is then odd because m ≡ n [ZMOD 2].

noncomputable def Rep.FiniteCyclicGroup.periodicIso {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) [IsCyclic G] (m n : ℤ) (hmn : m ≡ n [ZMOD 2]) : tateCohomology M m ≅ tateCohomology M n

Two-periodicity for Tate cohomology of a finite cyclic group. Tate degrees congruent modulo two are isomorphic; the case n and n + 2 is the usual periodicity statement.

Equations

• Rep.FiniteCyclicGroup.periodicIso M m n hmn = Rep.FiniteCyclicGroup.periodicIsoOfGenerator M ⋯.choose ⋯ m n hmn

theorem Rep.FiniteCyclicGroup.natCard_tateCohomology_eq_of_modEq {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) [IsCyclic G] (m n : ℤ) (hmn : m ≡ n [ZMOD 2]) : Nat.card ↑(tateCohomology M m) = Nat.card ↑(tateCohomology M n)

Tate cohomology groups of a finite cyclic group in degrees congruent modulo two have the same cardinality. This is the form used in Herbrand-quotient computations.

noncomputable def Rep.FiniteCyclicGroup.periodicFunctor (R : Type u) {G : Type u} [CommRing R] [CommGroup G] [Fintype G] (g : G) : CategoryTheory.Functor (Rep R G) (ChainComplex (ModuleCat R) ℕ)

The periodic chain complex ... ⟶ M --N--> M --(ρ(g) - 𝟙)--> M ⟶ 0 of underlying modules, as a functor of the coefficient representation. It is obtained from Mathlib's Rep.FiniteCyclicGroup.chainComplexFunctor by applying the forgetful functor from representations to modules degreewise. A morphism of representations therefore acts by its underlying linear map in every degree.

The body is exposed because consumers identify the value of the functor with Rep.FiniteCyclicGroup.moduleCatChainComplex and its action on a morphism with the underlying linear map.

Equations

• Rep.FiniteCyclicGroup.periodicFunctor R g = (Rep.FiniteCyclicGroup.chainComplexFunctor R g).comp ((CategoryTheory.forget₂ (Rep R G) (ModuleCat R)).mapHomologicalComplex (ComplexShape.down ℕ))

@[simp]

theorem Rep.FiniteCyclicGroup.periodicFunctor_map_f {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) (i : ℕ) : ((periodicFunctor R g).map f).f i = ModuleCat.ofHom (Hom.hom f).toLinearMap

In every degree, periodicFunctor sends a morphism of representations to its underlying linear map.

noncomputable def Rep.FiniteCyclicGroup.periodicFunctorObjIso {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (g : G) (M : Rep R G) : (periodicFunctor R g).obj M ≅ moduleCatChainComplex M g

The value of periodicFunctor is the underlying-module periodic chain complex.

Equations

• Rep.FiniteCyclicGroup.periodicFunctorObjIso g M = HomologicalComplex.Hom.isoOfComponents (fun (x : ℕ) => CategoryTheory.Iso.refl (((Rep.FiniteCyclicGroup.periodicFunctor R g).obj M).X x)) ⋯

instance Rep.FiniteCyclicGroup.instPreservesZeroMorphismsChainComplexModuleCatNatPeriodicFunctor {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (g : G) : (periodicFunctor R g).PreservesZeroMorphisms

The periodic chain complex functor sends zero morphisms to zero morphisms.

noncomputable def Rep.FiniteCyclicGroup.periodicFunctorEval (R : Type u) {G : Type u} [CommRing R] [CommGroup G] [Fintype G] (g : G) (i : ℕ) : (periodicFunctor R g).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.down ℕ) i) ≅ CategoryTheory.forget₂ (Rep R G) (ModuleCat R)

Evaluating the periodic chain complex in a single degree forgets the group action.

Equations

• Rep.FiniteCyclicGroup.periodicFunctorEval R g i = CategoryTheory.Iso.refl ((Rep.FiniteCyclicGroup.periodicFunctor R g).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.down ℕ) i))

theorem Rep.FiniteCyclicGroup.shortExact_map_periodicFunctor {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (g : G) {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) : (S.map (periodicFunctor R g)).ShortExact

A short exact sequence of representations induces a short exact sequence of periodic chain complexes, because in each degree it is the underlying short exact sequence of modules.

noncomputable def Rep.FiniteCyclicGroup.periodicScIsoOdd {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Odd j) : HomologicalComplex.sc ((periodicFunctor R g).obj M) j ≅ normHomCompSub M g

In an odd degree, the short complex computing the homology of the periodic chain complex is M --N--> M --(ρ(g) - 𝟙)--> M.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Rep.FiniteCyclicGroup.periodicScIsoEven {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Even j) (hj0 : j ≠ 0) : HomologicalComplex.sc ((periodicFunctor R g).obj M) j ≅ subCompNormHom M g

In a nonzero even degree, the short complex computing the homology of the periodic chain complex is M --(ρ(g) - 𝟙)--> M --N--> M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rep.FiniteCyclicGroup.periodicScIsoOdd_hom_τ₁ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Odd j) : (periodicScIsoOdd M g hj).hom.τ₁ = CategoryTheory.CategoryStruct.id (HomologicalComplex.sc ((periodicFunctor R g).obj M) j).X₁

The odd-degree identification periodicScIsoOdd is the identity on the first object.

@[simp]

theorem Rep.FiniteCyclicGroup.periodicScIsoOdd_hom_τ₂ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Odd j) : (periodicScIsoOdd M g hj).hom.τ₂ = CategoryTheory.CategoryStruct.id (HomologicalComplex.sc ((periodicFunctor R g).obj M) j).X₂

The odd-degree identification periodicScIsoOdd is the identity on the middle object.

@[simp]

theorem Rep.FiniteCyclicGroup.periodicScIsoOdd_hom_τ₃ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Odd j) : (periodicScIsoOdd M g hj).hom.τ₃ = CategoryTheory.CategoryStruct.id (HomologicalComplex.sc ((periodicFunctor R g).obj M) j).X₃

The odd-degree identification periodicScIsoOdd is the identity on the last object.

@[simp]

theorem Rep.FiniteCyclicGroup.periodicScIsoEven_hom_τ₁ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Even j) (hj0 : j ≠ 0) : (periodicScIsoEven M g hj hj0).hom.τ₁ = CategoryTheory.CategoryStruct.id (HomologicalComplex.sc ((periodicFunctor R g).obj M) j).X₁

The even-degree identification periodicScIsoEven is the identity on the first object.

@[simp]

theorem Rep.FiniteCyclicGroup.periodicScIsoEven_hom_τ₂ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Even j) (hj0 : j ≠ 0) : (periodicScIsoEven M g hj hj0).hom.τ₂ = CategoryTheory.CategoryStruct.id (HomologicalComplex.sc ((periodicFunctor R g).obj M) j).X₂

The even-degree identification periodicScIsoEven is the identity on the middle object.

@[simp]

theorem Rep.FiniteCyclicGroup.periodicScIsoEven_hom_τ₃ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Even j) (hj0 : j ≠ 0) : (periodicScIsoEven M g hj hj0).hom.τ₃ = CategoryTheory.CategoryStruct.id (HomologicalComplex.sc ((periodicFunctor R g).obj M) j).X₃

The even-degree identification periodicScIsoEven is the identity on the last object.

noncomputable def Rep.FiniteCyclicGroup.periodicHomologyIsoOdd {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Odd j) : HomologicalComplex.homology ((periodicFunctor R g).obj M) j ≅ (normHomCompSub M g).homology

In an odd degree the periodic chain complex computes the homology of M --N--> M --(ρ(g) - 𝟙)--> M, the model of degree-zero Tate cohomology.

Equations

• Rep.FiniteCyclicGroup.periodicHomologyIsoOdd M g hj = CategoryTheory.ShortComplex.homologyMapIso (Rep.FiniteCyclicGroup.periodicScIsoOdd M g hj)

noncomputable def Rep.FiniteCyclicGroup.periodicHomologyIsoEven {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Even j) (hj0 : j ≠ 0) : HomologicalComplex.homology ((periodicFunctor R g).obj M) j ≅ (subCompNormHom M g).homology

In a nonzero even degree the periodic chain complex computes the homology of M --(ρ(g) - 𝟙)--> M --N--> M, the model of Tate cohomology in degree -1.

Equations

• Rep.FiniteCyclicGroup.periodicHomologyIsoEven M g hj hj0 = CategoryTheory.ShortComplex.homologyMapIso (Rep.FiniteCyclicGroup.periodicScIsoEven M g hj hj0)

@[simp]

theorem Rep.FiniteCyclicGroup.periodicHomologyIsoOdd_hom {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Odd j) : (periodicHomologyIsoOdd M g hj).hom = CategoryTheory.ShortComplex.homologyMap (periodicScIsoOdd M g hj).hom

periodicHomologyIsoOdd is the map on homology induced by periodicScIsoOdd.

@[simp]

theorem Rep.FiniteCyclicGroup.periodicHomologyIsoEven_hom {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) {j : ℕ} (hj : Even j) (hj0 : j ≠ 0) : (periodicHomologyIsoEven M g hj hj0).hom = CategoryTheory.ShortComplex.homologyMap (periodicScIsoEven M g hj hj0).hom

periodicHomologyIsoEven is the map on homology induced by periodicScIsoEven.

noncomputable def Rep.FiniteCyclicGroup.normHomCompSubMap {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) : normHomCompSub M g ⟶ normHomCompSub N g

The short complex M --N--> M --(ρ(g) - 𝟙)--> M is functorial in M: a morphism of representations acts by its underlying linear map in each of the three spots.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rep.FiniteCyclicGroup.normHomCompSubMap_τ₁ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) : (normHomCompSubMap g f).τ₁ = ModuleCat.ofHom (Hom.hom f).toLinearMap

On the first object, normHomCompSubMap g f is the underlying linear map of f.

@[simp]

theorem Rep.FiniteCyclicGroup.normHomCompSubMap_τ₂ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) : (normHomCompSubMap g f).τ₂ = ModuleCat.ofHom (Hom.hom f).toLinearMap

On the middle object, normHomCompSubMap g f is the underlying linear map of f.

@[simp]

theorem Rep.FiniteCyclicGroup.normHomCompSubMap_τ₃ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) : (normHomCompSubMap g f).τ₃ = ModuleCat.ofHom (Hom.hom f).toLinearMap

On the last object, normHomCompSubMap g f is the underlying linear map of f.

noncomputable def Rep.FiniteCyclicGroup.subCompNormHomMap {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) : subCompNormHom M g ⟶ subCompNormHom N g

The short complex M --(ρ(g) - 𝟙)--> M --N--> M is functorial in M: a morphism of representations acts by its underlying linear map in each of the three spots.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rep.FiniteCyclicGroup.subCompNormHomMap_τ₁ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) : (subCompNormHomMap g f).τ₁ = ModuleCat.ofHom (Hom.hom f).toLinearMap

On the first object, subCompNormHomMap g f is the underlying linear map of f.

@[simp]

theorem Rep.FiniteCyclicGroup.subCompNormHomMap_τ₂ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) : (subCompNormHomMap g f).τ₂ = ModuleCat.ofHom (Hom.hom f).toLinearMap

On the middle object, subCompNormHomMap g f is the underlying linear map of f.

@[simp]

theorem Rep.FiniteCyclicGroup.subCompNormHomMap_τ₃ {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) : (subCompNormHomMap g f).τ₃ = ModuleCat.ofHom (Hom.hom f).toLinearMap

On the last object, subCompNormHomMap g f is the underlying linear map of f.

theorem Rep.FiniteCyclicGroup.sc_map_comp_periodicScIsoOdd {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) {j : ℕ} (hj : Odd j) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.shortComplexFunctor (ModuleCat R) (ComplexShape.down ℕ) j).map ((periodicFunctor R g).map f)) (periodicScIsoOdd N g hj).hom = CategoryTheory.CategoryStruct.comp (periodicScIsoOdd M g hj).hom (normHomCompSubMap g f)

The odd-degree identification of the short complexes is natural in the coefficients.

theorem Rep.FiniteCyclicGroup.homologyMap_comp_periodicHomologyIsoOdd {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) {j : ℕ} (hj : Odd j) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((periodicFunctor R g).map f) j) (periodicHomologyIsoOdd N g hj).hom = CategoryTheory.CategoryStruct.comp (periodicHomologyIsoOdd M g hj).hom (CategoryTheory.ShortComplex.homologyMap (normHomCompSubMap g f))

Naturality of the odd-degree periodicity. The homology of the periodic chain complex in an odd degree is identified with the homology of M --N--> M --(ρ(g) - 𝟙)--> M compatibly with morphisms of representations; in particular the identification does not depend on the odd degree chosen.

theorem Rep.FiniteCyclicGroup.sc_map_comp_periodicScIsoEven {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) {j : ℕ} (hj : Even j) (hj0 : j ≠ 0) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.shortComplexFunctor (ModuleCat R) (ComplexShape.down ℕ) j).map ((periodicFunctor R g).map f)) (periodicScIsoEven N g hj hj0).hom = CategoryTheory.CategoryStruct.comp (periodicScIsoEven M g hj hj0).hom (subCompNormHomMap g f)

The even-degree identification of the short complexes is natural in the coefficients.

theorem Rep.FiniteCyclicGroup.homologyMap_comp_periodicHomologyIsoEven {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] {M : Rep R G} (g : G) {N : Rep R G} (f : M ⟶ N) {j : ℕ} (hj : Even j) (hj0 : j ≠ 0) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((periodicFunctor R g).map f) j) (periodicHomologyIsoEven N g hj hj0).hom = CategoryTheory.CategoryStruct.comp (periodicHomologyIsoEven M g hj hj0).hom (CategoryTheory.ShortComplex.homologyMap (subCompNormHomMap g f))

Naturality of the even-degree periodicity. The homology of the periodic chain complex in a nonzero even degree is identified with the homology of M --(ρ(g) - 𝟙)--> M --N--> M compatibly with morphisms of representations.

theorem Rep.FiniteCyclicGroup.natCard_periodicHomology_odd {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {j : ℕ} (hj : Odd j) : Nat.card ↑(HomologicalComplex.homology ((periodicFunctor R g).obj M) j) = Nat.card ↑(tateCohomology M 0)

In an odd degree the homology of the periodic chain complex has the cardinality of degree-zero Tate cohomology.

theorem Rep.FiniteCyclicGroup.natCard_periodicHomology_even {R G : Type u} [CommRing R] [CommGroup G] [Fintype G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {j : ℕ} (hj : Even j) (hj0 : j ≠ 0) : Nat.card ↑(HomologicalComplex.homology ((periodicFunctor R g).obj M) j) = Nat.card ↑(tateCohomology M (-1))

In a nonzero even degree the homology of the periodic chain complex has the cardinality of Tate cohomology in degree -1.