Low-degree Tate cohomology

This file gives the low-degree descriptions used by the Nakayama map. For a representation M of a finite group, degree zero is the quotient of the invariant submodule by the image of the norm, and degree -1 is the kernel of the norm modulo the augmentation submodule I_G M. For a trivial representation A, the comparison with first group homology identifies degree -2 with Gᵃᵇ ⊗[ℤ] A, and hence, for the trivial integral representation, with the additive form of the abelianization. For the trivial integral representation the same descriptions evaluate degree zero as ZMod |G| and make degree -1 trivial.

The degree-zero and degree--1 constructions are adapted from ClassFieldTheory/Cohomology/TateCohomology.lean and ClassFieldTheory/Cohomology/FiniteCyclic/ExplicitTate.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509; the trivial integral calculations are adapted from ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/Trivial.lean in the same repository and commit. The degree--2 identification combines Mathlib's comparison with group homology, groupHomology.H1AddEquivOfIsTrivial, and the tensor-product right unitor.

Main definitions

• TauCeti.TateCohomology.H0IsoNormQuotient: Ĥ⁰(G, M) ≅ Mᴳ / N_G M.
• TauCeti.TateCohomology.HNegOneIsoNormKernelQuotient: Ĥ⁻¹(G, M) ≅ ker N_G / I_G M.
• TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial: Ĥ⁻²(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A for a trivial representation A.
• TauCeti.TateCohomology.HNegTwoAddEquivAbelianization: Ĥ⁻²(G, ℤ) ≃+ Additive (Gᵃᵇ).
• TauCeti.TateCohomology.H0LinearEquivTrivialIntZModCard: for the trivial integral representation, degree zero is ZMod |G|.

Main results

• TauCeti.TateCohomology.natCard_tateCohomology_zero_trivial_int_eq_card: for trivial integral coefficients, degree zero has order the order of the group.
• TauCeti.TateCohomology.subsingleton_tateCohomology_negOne_trivial_int: for trivial integral coefficients, degree -1 is trivial.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §4.
• K. S. Brown, Cohomology of Groups, Chapter VI, §5.

noncomputable def TauCeti.TateCohomology.H0IsoNormQuotient {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : tateCohomology M 0 ≅ ↧(↥M.ρ.invariants ⧸ (LinearMap.range M.ρ.norm).submoduleOf M.ρ.invariants)

Degree-zero Tate cohomology is the quotient of the invariant submodule by the image of the norm.

Equations

• TauCeti.TateCohomology.H0IsoNormQuotient M = TauCeti.TateCohomology.Zero.homologyIso✝ M ≪≫ TauCeti.TateCohomology.Zero.homologyIsoNormQuotient✝ M

noncomputable def TauCeti.TateCohomology.H0CyclesIso {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : HomologicalComplex.cycles (tateComplex M) 0 ≅ ↧↥M.ρ.invariants

The cycles in degree zero of the Tate complex are the invariant submodule.

Equations

• TauCeti.TateCohomology.H0CyclesIso M = TauCeti.TateCohomology.Zero.cyclesIso✝ M ≪≫ TauCeti.TateCohomology.Zero.cyclesIsoInvariants✝ M

theorem TauCeti.TateCohomology.H0CyclesIso_hom_comp_subtype {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (H0CyclesIso M).hom (ModuleCat.ofHom M.ρ.invariants.subtype) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (tateComplex M) 0) (groupCohomology.cochainsIso₀ M).hom

Under the degree-zero identification, including a cycle into the Tate complex is the same as including the corresponding invariant into the coefficient module.

theorem TauCeti.TateCohomology.H0CyclesIso_hom_comp_subtype_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : ↧↑M ⟶ Z) : CategoryTheory.CategoryStruct.comp (H0CyclesIso M).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom M.ρ.invariants.subtype) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (tateComplex M) 0) (groupCohomology.cochainsIso₀ M).hom) h

Under the degree-zero identification, including a cycle into the Tate complex is the same as including the corresponding invariant into the coefficient module.

theorem TauCeti.TateCohomology.H0CyclesIso_inv_comp_iCycles {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (H0CyclesIso M).inv (HomologicalComplex.iCycles (tateComplex M) 0) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom M.ρ.invariants.subtype) (groupCohomology.cochainsIso₀ M).inv

An invariant element, as a cycle of degree 0 of the Tate complex, is the same element as a 0-cochain.

theorem TauCeti.TateCohomology.H0CyclesIso_inv_comp_iCycles_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : (tateComplex M).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (H0CyclesIso M).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (tateComplex M) 0) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom M.ρ.invariants.subtype) (groupCohomology.cochainsIso₀ M).inv) h

An invariant element, as a cycle of degree 0 of the Tate complex, is the same element as a 0-cochain.

noncomputable def TauCeti.TateCohomology.H0π {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : ↧↥M.ρ.invariants ⟶ tateCohomology M 0

The map from invariant representatives to degree-zero Tate cohomology.

Equations

• TauCeti.TateCohomology.H0π M = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom ((LinearMap.range M.ρ.norm).submoduleOf M.ρ.invariants).mkQ) (TauCeti.TateCohomology.H0IsoNormQuotient M).inv

theorem TauCeti.TateCohomology.H0π_eq_H0CyclesIso_inv_comp_homologyπ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : H0π M = CategoryTheory.CategoryStruct.comp (H0CyclesIso M).inv (HomologicalComplex.homologyπ (tateComplex M) 0)

The representative map to degree-zero Tate cohomology is the canonical projection from degree-zero cycles to homology, after identifying those cycles with the invariants.

theorem TauCeti.TateCohomology.H0CyclesIso_hom_comp_H0π {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (H0CyclesIso M).hom (H0π M) = HomologicalComplex.homologyπ (tateComplex M) 0

Under the degree-zero identification of the cycles with the invariants, H0π is the canonical projection from degree-zero cycles to homology.

theorem TauCeti.TateCohomology.H0CyclesIso_hom_comp_H0π_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : tateCohomology M 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (H0CyclesIso M).hom (CategoryTheory.CategoryStruct.comp (H0π M) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (tateComplex M) 0) h

Under the degree-zero identification of the cycles with the invariants, H0π is the canonical projection from degree-zero cycles to homology.

instance TauCeti.TateCohomology.instEpiModuleCatH0π {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.Epi (H0π M)

The quotient map from invariant representatives onto degree-zero Tate cohomology is an epimorphism.

@[simp]

theorem TauCeti.TateCohomology.H0π_comp_H0IsoNormQuotient_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (H0π M) (H0IsoNormQuotient M).hom = ModuleCat.ofHom ((LinearMap.range M.ρ.norm).submoduleOf M.ρ.invariants).mkQ

Passing an invariant representative to degree-zero Tate cohomology and then applying the low-degree identification is the quotient map by the norm image.

@[simp]

theorem TauCeti.TateCohomology.H0π_comp_H0IsoNormQuotient_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : ↧(↥M.ρ.invariants ⧸ (LinearMap.range M.ρ.norm).submoduleOf M.ρ.invariants) ⟶ Z) : CategoryTheory.CategoryStruct.comp (H0π M) (CategoryTheory.CategoryStruct.comp (H0IsoNormQuotient M).hom h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom ((LinearMap.range M.ρ.norm).submoduleOf M.ρ.invariants).mkQ) h

Passing an invariant representative to degree-zero Tate cohomology and then applying the low-degree identification is the quotient map by the norm image.

@[simp]

theorem TauCeti.TateCohomology.H0π_comp_H0IsoNormQuotient_hom_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (x : ↥M.ρ.invariants) : (CategoryTheory.ConcreteCategory.hom (H0IsoNormQuotient M).hom) ((CategoryTheory.ConcreteCategory.hom (H0π M)) x) = Submodule.Quotient.mk x

Passing an invariant representative to degree-zero Tate cohomology and then applying the low-degree identification is the quotient map by the norm image.

@[simp]

theorem TauCeti.TateCohomology.mkQ_comp_H0IsoNormQuotient_inv {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom ((LinearMap.range M.ρ.norm).submoduleOf M.ρ.invariants).mkQ) (H0IsoNormQuotient M).inv = H0π M

Composing the quotient map by the norm image with the inverse of the low-degree identification is the map from invariant representatives to degree-zero Tate cohomology.

@[simp]

theorem TauCeti.TateCohomology.mkQ_comp_H0IsoNormQuotient_inv_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : tateCohomology M 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom ((LinearMap.range M.ρ.norm).submoduleOf M.ρ.invariants).mkQ) (CategoryTheory.CategoryStruct.comp (H0IsoNormQuotient M).inv h) = CategoryTheory.CategoryStruct.comp (H0π M) h

Composing the quotient map by the norm image with the inverse of the low-degree identification is the map from invariant representatives to degree-zero Tate cohomology.

@[simp]

theorem TauCeti.TateCohomology.mkQ_comp_H0IsoNormQuotient_inv_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (x : ↥M.ρ.invariants) : (CategoryTheory.ConcreteCategory.hom (H0IsoNormQuotient M).inv) (Submodule.Quotient.mk x) = (CategoryTheory.ConcreteCategory.hom (H0π M)) x

Composing the quotient map by the norm image with the inverse of the low-degree identification is the map from invariant representatives to degree-zero Tate cohomology.

@[simp]

theorem TauCeti.TateCohomology.H0π_eq_zero_iff {R G : Type u} [CommRing R] [Group G] [Fintype G] {M : Rep R G} (y : ↥M.ρ.invariants) : (CategoryTheory.ConcreteCategory.hom (H0π M)) y = 0 ↔ y ∈ (LinearMap.range M.ρ.norm).submoduleOf M.ρ.invariants

An invariant represents the zero degree-zero Tate cohomology class exactly when it lies in the image of the norm.

@[simp]

theorem TauCeti.TateCohomology.H0π_eq_iff {R G : Type u} [CommRing R] [Group G] [Fintype G] {M : Rep R G} (y z : ↥M.ρ.invariants) : (CategoryTheory.ConcreteCategory.hom (H0π M)) y = (CategoryTheory.ConcreteCategory.hom (H0π M)) z ↔ y - z ∈ (LinearMap.range M.ρ.norm).submoduleOf M.ρ.invariants

Two invariants represent the same degree-zero Tate cohomology class exactly when their difference lies in the image of the norm.

theorem TauCeti.TateCohomology.H0_induction_on {R G : Type u} [CommRing R] [Group G] [Fintype G] {M : Rep R G} {C : ↑(tateCohomology M 0) → Prop} (x : ↑(tateCohomology M 0)) (h : ∀ (y : ↥M.ρ.invariants), C ((CategoryTheory.ConcreteCategory.hom (H0π M)) y)) : C x

Every degree-zero Tate cohomology class is represented by an invariant, so a property of all classes follows from the property of the classes of invariants.

noncomputable def TauCeti.TateCohomology.HNegOneIsoNormKernelQuotient {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : tateCohomology M (-1) ≅ ↧(↥(LinearMap.ker M.ρ.norm) ⧸ (Representation.Coinvariants.ker M.ρ).submoduleOf (LinearMap.ker M.ρ.norm))

Degree -1 Tate cohomology is the kernel of the norm modulo the augmentation submodule, namely the kernel of the quotient to coinvariants.

Equations

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

noncomputable def TauCeti.TateCohomology.HNegOneπ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : ↧↥(LinearMap.ker M.ρ.norm) ⟶ tateCohomology M (-1)

The quotient map from norm-zero representatives to degree -1 Tate cohomology.

Equations

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

instance TauCeti.TateCohomology.instEpiModuleCatHNegOneπ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.Epi (HNegOneπ M)

The quotient map from norm-zero representatives onto degree -1 Tate cohomology is an epimorphism.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_HNegOneIsoNormKernelQuotient_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (HNegOneπ M) (HNegOneIsoNormKernelQuotient M).hom = ModuleCat.ofHom ((Representation.Coinvariants.ker M.ρ).submoduleOf (LinearMap.ker M.ρ.norm)).mkQ

Under the degree -1 identification, HNegOneπ is the quotient map by the augmentation submodule.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_HNegOneIsoNormKernelQuotient_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : ↧(↥(LinearMap.ker M.ρ.norm) ⧸ (Representation.Coinvariants.ker M.ρ).submoduleOf (LinearMap.ker M.ρ.norm)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HNegOneπ M) (CategoryTheory.CategoryStruct.comp (HNegOneIsoNormKernelQuotient M).hom h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom ((Representation.Coinvariants.ker M.ρ).submoduleOf (LinearMap.ker M.ρ.norm)).mkQ) h

Under the degree -1 identification, HNegOneπ is the quotient map by the augmentation submodule.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_HNegOneIsoNormKernelQuotient_hom_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (x : ↥(LinearMap.ker M.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (HNegOneIsoNormKernelQuotient M).hom) ((CategoryTheory.ConcreteCategory.hom (HNegOneπ M)) x) = Submodule.Quotient.mk x

Under the degree -1 identification, HNegOneπ is the quotient map by the augmentation submodule.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_eq_zero_iff {R G : Type u} [CommRing R] [Group G] [Fintype G] {M : Rep R G} (x : ↥(LinearMap.ker M.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (HNegOneπ M)) x = 0 ↔ x ∈ (Representation.Coinvariants.ker M.ρ).submoduleOf (LinearMap.ker M.ρ.norm)

A norm-zero element represents zero in degree -1 Tate cohomology exactly when it belongs to the augmentation submodule.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_eq_iff {R G : Type u} [CommRing R] [Group G] [Fintype G] {M : Rep R G} (x y : ↥(LinearMap.ker M.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (HNegOneπ M)) x = (CategoryTheory.ConcreteCategory.hom (HNegOneπ M)) y ↔ x - y ∈ (Representation.Coinvariants.ker M.ρ).submoduleOf (LinearMap.ker M.ρ.norm)

Two norm-zero elements represent the same degree -1 Tate class exactly when their difference belongs to the augmentation submodule.

theorem TauCeti.TateCohomology.HNegOne_induction_on {R G : Type u} [CommRing R] [Group G] [Fintype G] {M : Rep R G} {C : ↑(tateCohomology M (-1)) → Prop} (x : ↑(tateCohomology M (-1))) (h : ∀ (y : ↥(LinearMap.ker M.ρ.norm)), C ((CategoryTheory.ConcreteCategory.hom (HNegOneπ M)) y)) : C x

Every degree -1 Tate cohomology class is represented by a norm-zero element, so a property of all classes follows from the property of the classes of norm-zero elements.

noncomputable def TauCeti.TateCohomology.HNegOneCyclesIso {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : HomologicalComplex.cycles (tateComplex M) (-1) ≅ ↧↥(LinearMap.ker M.ρ.norm)

The cycles in degree -1 of the Tate complex are the kernel of the norm.

Equations

• TauCeti.TateCohomology.HNegOneCyclesIso M = TauCeti.TateCohomology.NegOne.cyclesIso✝ M ≪≫ (TauCeti.TateCohomology.NegOne.shortComplex✝ M).moduleCatCyclesIso ≪≫ CategoryTheory.eqToIso ⋯

theorem TauCeti.TateCohomology.HNegOneCyclesIso_hom_comp_subtype {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (HNegOneCyclesIso M).hom (ModuleCat.ofHom (LinearMap.ker M.ρ.norm).subtype) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (tateComplex M) (-1)) (groupHomology.chainsIso₀ M).hom

Under the degree -1 identification, including a cycle into the Tate complex is the same as including the corresponding norm-zero element into the coefficient module.

theorem TauCeti.TateCohomology.HNegOneCyclesIso_hom_comp_subtype_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : ↧↑M ⟶ Z) : CategoryTheory.CategoryStruct.comp (HNegOneCyclesIso M).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.ker M.ρ.norm).subtype) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (tateComplex M) (-1)) (groupHomology.chainsIso₀ M).hom) h

Under the degree -1 identification, including a cycle into the Tate complex is the same as including the corresponding norm-zero element into the coefficient module.

theorem TauCeti.TateCohomology.HNegOneCyclesIso_inv_comp_iCycles {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (HNegOneCyclesIso M).inv (HomologicalComplex.iCycles (tateComplex M) (-1)) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.ker M.ρ.norm).subtype) (groupHomology.chainsIso₀ M).inv

A norm-zero element, as a cycle of degree -1 of the Tate complex, is the same element as a 0-chain.

theorem TauCeti.TateCohomology.HNegOneCyclesIso_inv_comp_iCycles_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : (tateComplex M).X (-1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HNegOneCyclesIso M).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (tateComplex M) (-1)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.ker M.ρ.norm).subtype) (groupHomology.chainsIso₀ M).inv) h

A norm-zero element, as a cycle of degree -1 of the Tate complex, is the same element as a 0-chain.

theorem TauCeti.TateCohomology.HNegOneπ_eq_HNegOneCyclesIso_inv_comp_homologyπ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : HNegOneπ M = CategoryTheory.CategoryStruct.comp (HNegOneCyclesIso M).inv (HomologicalComplex.homologyπ (tateComplex M) (-1))

The representative map to degree -1 Tate cohomology is the canonical projection from degree -1 cycles to homology, after identifying those cycles with the kernel of the norm.

noncomputable def TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial {R G : Type u} [CommRing R] [Group G] [Fintype G] (A : Rep R G) [A.IsTrivial] : ↑(tateCohomology A (-2)) ≃+ TensorProduct ℤ (Additive (Abelianization G)) ↑A

For a trivial representation A, degree--2 Tate cohomology is the tensor product of the additive abelianization of the group with A.

Equations

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

theorem TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (A : Rep R G) [A.IsTrivial] (x : ↑(tateCohomology A (-2))) : (HNegTwoAddEquivTensorOfIsTrivial A) x = (groupHomology.H1AddEquivOfIsTrivial A) ((CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app A)) x)

The degree -2 Tate identification factors through the comparison with first homology.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial_single {R G : Type u} [CommRing R] [Group G] [Fintype G] (A : Rep R G) [A.IsTrivial] (g : G) (a : ↑A) : (HNegTwoAddEquivTensorOfIsTrivial A) ((CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A)) ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial A).inv) (Finsupp.single g a)))) = Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a

The degree--2 identification sends the homology class represented by (g, a) to the elementary tensor ⟦g⟧ ⊗ₜ a.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial_symm_tmul {R G : Type u} [CommRing R] [Group G] [Fintype G] (A : Rep R G) [A.IsTrivial] (g : G) (a : ↑A) : (HNegTwoAddEquivTensorOfIsTrivial A).symm (Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a) = (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A)) ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial A).inv) (Finsupp.single g a)))

The inverse degree--2 identification sends an elementary tensor to the corresponding Tate homology class.

noncomputable def TauCeti.TateCohomology.HNegTwoAddEquivAbelianization {G : Type} [Group G] [Fintype G] : ↑(tateCohomology (Rep.trivial ℤ G ℤ) (-2)) ≃+ Additive (Abelianization G)

The degree--2 Tate cohomology of the trivial integral representation is the additive abelianization of the group.

Equations

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

theorem TauCeti.TateCohomology.HNegTwoAddEquivAbelianization_apply {G : Type} [Group G] [Fintype G] (x : ↑(tateCohomology (Rep.trivial ℤ G ℤ) (-2))) : HNegTwoAddEquivAbelianization x = (TensorProduct.rid ℤ (Additive (Abelianization G))) ((HNegTwoAddEquivTensorOfIsTrivial (Rep.trivial ℤ G ℤ)) x)

The integral degree--2 identification is the tensor description followed by the right unitor.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoAddEquivAbelianization_single_one {G : Type} [Group G] [Fintype G] (g : G) : HNegTwoAddEquivAbelianization ((CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).inv.app (Rep.trivial ℤ G ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π (Rep.trivial ℤ G ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial (Rep.trivial ℤ G ℤ)).inv) (Finsupp.single g 1)))) = Additive.ofMul (Abelianization.of g)

The degree--2 identification sends the homology class represented by (g, 1) to the class of g in the additive abelianization.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoAddEquivAbelianization_symm_of {G : Type} [Group G] [Fintype G] (g : G) : HNegTwoAddEquivAbelianization.symm (Additive.ofMul (Abelianization.of g)) = (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).inv.app (Rep.trivial ℤ G ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π (Rep.trivial ℤ G ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial (Rep.trivial ℤ G ℤ)).inv) (Finsupp.single g 1)))

The inverse integral degree--2 identification sends the class of g to the Tate homology class represented by (g, 1).

noncomputable def TauCeti.TateCohomology.H0LinearEquivTrivialIntZModCard (H : Type) [Group H] [Fintype H] : ↑(tateCohomology (Rep.trivial ℤ H ℤ) 0) ≃ₗ[ℤ] ZMod (Nat.card H)

Degree-zero Tate cohomology with trivial integral coefficients is ZMod |H|.

Equations

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

@[simp]

theorem TauCeti.TateCohomology.H0LinearEquivTrivialIntZModCard_H0π (H : Type) [Group H] [Fintype H] (x : ↥(Rep.trivial ℤ H ℤ).ρ.invariants) : (H0LinearEquivTrivialIntZModCard H) ((CategoryTheory.ConcreteCategory.hom (H0π (Rep.trivial ℤ H ℤ))) x) = ↑↑x

The degree-zero equivalence sends an invariant representative to its residue class modulo the order of the group.

noncomputable def TauCeti.TateCohomology.trivialTateHZeroOne (H : Type) [Group H] [Fintype H] : ↑(tateCohomology (Rep.trivial ℤ H ℤ) 0)

The class of 1 ∈ ℤ in degree-zero Tate cohomology with trivial integral coefficients.

Equations

• TauCeti.TateCohomology.trivialTateHZeroOne H = (CategoryTheory.ConcreteCategory.hom (TauCeti.TateCohomology.H0π (Rep.trivial ℤ H ℤ))) ⟨1, ⋯⟩

theorem TauCeti.TateCohomology.trivialTateHZeroOne_def (H : Type) [Group H] [Fintype H] : trivialTateHZeroOne H = (CategoryTheory.ConcreteCategory.hom (H0π (Rep.trivial ℤ H ℤ))) ⟨1, ⋯⟩

The class of 1 is the degree-zero projection of the invariant 1.

@[simp]

theorem TauCeti.TateCohomology.H0LinearEquivTrivialIntZModCard_trivialTateHZeroOne (H : Type) [Group H] [Fintype H] : (H0LinearEquivTrivialIntZModCard H) (trivialTateHZeroOne H) = 1

The canonical degree-zero class corresponds to 1 modulo the order of the group.

@[simp]

theorem TauCeti.TateCohomology.natCard_tateCohomology_zero_trivial_int_eq_card (H : Type) [Group H] [Fintype H] : Nat.card ↑(tateCohomology (Rep.trivial ℤ H ℤ) 0) = Nat.card H

The order of degree-zero Tate cohomology with trivial integral coefficients is the order of the group.

instance TauCeti.TateCohomology.finite_tateCohomology_zero_trivial_int (H : Type) [Group H] [Fintype H] : Finite ↑(tateCohomology (Rep.trivial ℤ H ℤ) 0)

Degree-zero Tate cohomology with trivial integral coefficients is finite.

instance TauCeti.TateCohomology.subsingleton_tateCohomology_negOne_trivial_int (H : Type) [Group H] [Fintype H] : Subsingleton ↑(tateCohomology (Rep.trivial ℤ H ℤ) (-1))

Degree -1 Tate cohomology with trivial integral coefficients is trivial.