noncomputable def TateCohomology.augmentationMap (k : Type u) [CommRing k] (G : Type u) [Group G] : MonoidAlgebra k G →ₐ[k] k

noncomputable def TateCohomology.augmentationIdeal (k : Type u) [CommRing k] (G : Type u) [Group G] : Ideal (MonoidAlgebra k G)

def TateCohomology.normMap (k : Type u) [CommRing k] (G : Type u) [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) : ↑A →ₗ[k] ↑A

theorem TateCohomology.normMap_range_le_invariants {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) : (normMap k G A).range ≤ A.ρ.invariants

def TateCohomology.augmentationSubmodule (k : Type u) [CommRing k] (G : Type u) [Group G] (A : Rep.{u_1, u, u} k G) : Submodule k ↑A

def TateCohomology.GCoinvariants (k : Type u) [CommRing k] (G : Type u) [Group G] (A : Rep.{u, u, u} k G) : Type u

@[implicit_reducible]

instance TateCohomology.GCoinvariants.addCommGroup {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) : AddCommGroup (GCoinvariants k G A)

@[implicit_reducible]

instance TateCohomology.GCoinvariants.module {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep.{u, u, u} k G) : Module k (GCoinvariants k G A)

theorem TateCohomology.augmentationSubmodule_le_ker_norm {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) : augmentationSubmodule k G A ≤ (normMap k G A).ker

noncomputable def TateCohomology.normImageInInvariants {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) : Submodule k ↥A.ρ.invariants

def TateCohomology.tateH0 {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : Type u

@[implicit_reducible]

noncomputable instance TateCohomology.tateH0.addCommGroup {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : AddCommGroup (tateH0 A)

@[implicit_reducible]

noncomputable instance TateCohomology.tateH0.module {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : Module k (tateH0 A)

def TateCohomology.augInKerNorm {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) : Submodule k ↥(normMap k G A).ker

def TateCohomology.tateMinus1 {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : Type u

@[implicit_reducible]

instance TateCohomology.tateMinus1.addCommGroup {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : AddCommGroup (tateMinus1 A)

@[implicit_reducible]

instance TateCohomology.tateMinus1.module {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : Module k (tateMinus1 A)

noncomputable def TateCohomology.tateH0.mk {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : ↥A.ρ.invariants →ₗ[k] tateH0 A

def TateCohomology.tateMinus1.mk {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : ↥(normMap k G A).ker →ₗ[k] tateMinus1 A

def TateCohomology.herbrandQuotient {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u, u, u} k G) [Fintype (tateH0 A)] [Fintype (tateMinus1 A)] : ℚ

theorem TateCohomology.finite_of_exact {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Finite A] [Finite C] (f : A →+ B) (g : B →+ C) (hex : Function.Exact ⇑f ⇑g) : Finite B

theorem TateCohomology.card_eq_of_exact_pair {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] (f : A →+ B) (g : B →+ C) (hex : Function.Exact ⇑f ⇑g) : Nat.card B = Nat.card ↥f.range * Nat.card ↥g.range

theorem TateCohomology.exact_hexagon_card_eq_general {A₁ : Type u_1} {A₂ : Type u_2} {A₃ : Type u_3} {A₄ : Type u_4} {A₅ : Type u_5} {A₆ : Type u_6} [AddCommGroup A₁] [AddCommGroup A₂] [AddCommGroup A₃] [AddCommGroup A₄] [AddCommGroup A₅] [AddCommGroup A₆] [Fintype A₁] [Fintype A₂] [Fintype A₃] [Fintype A₄] [Fintype A₅] [Fintype A₆] (f₁ : A₁ →+ A₂) (f₂ : A₂ →+ A₃) (f₃ : A₃ →+ A₄) (f₄ : A₄ →+ A₅) (f₅ : A₅ →+ A₆) (f₆ : A₆ →+ A₁) (h₁₂ : Function.Exact ⇑f₁ ⇑f₂) (h₂₃ : Function.Exact ⇑f₂ ⇑f₃) (h₃₄ : Function.Exact ⇑f₃ ⇑f₄) (h₄₅ : Function.Exact ⇑f₄ ⇑f₅) (h₅₆ : Function.Exact ⇑f₅ ⇑f₆) (h₆₁ : Function.Exact ⇑f₆ ⇑f₁) : Fintype.card A₁ * Fintype.card A₃ * Fintype.card A₅ = Fintype.card A₂ * Fintype.card A₄ * Fintype.card A₆

def TateCohomology.tateHnAux {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : Bool → Type u

@[implicit_reducible]

noncomputable instance TateCohomology.tateHnAux.addCommGroup {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) (b : Bool) : AddCommGroup (tateHnAux A b)

def TateCohomology.parityBool (n : ℤ) : Bool

def TateCohomology.tateHn (k : Type u) [CommRing k] (G : Type u) [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u, u, u} k G) (n : ℤ) : Type u

@[implicit_reducible]

noncomputable instance TateCohomology.tateHn.addCommGroup {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u, u, u} k G) (n : ℤ) : AddCommGroup (tateHn k G A n)

noncomputable def TateCohomology.tateHnGen (k : Type u) [CommRing k] (G : Type u) [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) (n : ℤ) : Type u

@[implicit_reducible]

noncomputable instance TateCohomology.tateHnGen.addCommGroup {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) (n : ℤ) : AddCommGroup (tateHnGen k G A n)

theorem TateCohomology.tateHnGen_eq_tateHn_of_isCyclic {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u, u, u} k G) (n : ℤ) : Nonempty (tateHnGen k G A n ≃+ tateHn k G A n)

theorem TateCohomology.tateHnGen_zero_iso {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : Nonempty (tateHnGen k G A 0 ≃+ tateH0 A)

theorem TateCohomology.tateHnGen_neg_one_iso {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : Nonempty (tateHnGen k G A (-1) ≃+ tateMinus1 A)

noncomputable def TateCohomology.tateHnGen.inducedMap {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {A B : Rep.{u_1, u, u} k G} (f : A ⟶ B) (n : ℤ) : tateHnGen k G A n →+ tateHnGen k G B n

noncomputable def TateCohomology.tateHnGen.connectingMap {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u_1, u, u} k G)} (hS : S.ShortExact) (n : ℤ) : tateHnGen k G S.X₃ n →+ tateHnGen k G S.X₁ (n + 1)

theorem TateCohomology.tateHnGen_long_exact_sequence_and_naturality {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u_1, u, u} k G)} (hS : S.ShortExact) : (∀ (n : ℤ), Function.Exact ⇑(tateHnGen.inducedMap S.f n) ⇑(tateHnGen.inducedMap S.g n) ∧ Function.Exact ⇑(tateHnGen.inducedMap S.g n) ⇑(tateHnGen.connectingMap hS n) ∧ Function.Exact ⇑(tateHnGen.connectingMap hS n) ⇑(tateHnGen.inducedMap S.f (n + 1))) ∧ ∀ {S' : CategoryTheory.ShortComplex (Rep.{u_1, u, u} k G)} (hS' : S'.ShortExact) (f₁ : S.X₁ ⟶ S'.X₁) (f₂ : S.X₂ ⟶ S'.X₂) (f₃ : S.X₃ ⟶ S'.X₃), CategoryTheory.CategoryStruct.comp S.f f₂ = CategoryTheory.CategoryStruct.comp f₁ S'.f → CategoryTheory.CategoryStruct.comp S.g f₃ = CategoryTheory.CategoryStruct.comp f₂ S'.g → ∀ (n : ℤ) (x : tateHnGen k G S.X₃ n), (tateHnGen.inducedMap f₁ (n + 1)) ((tateHnGen.connectingMap hS n) x) = (tateHnGen.connectingMap hS' n) ((tateHnGen.inducedMap f₃ n) x)

theorem TateCohomology.tateHnGen_long_exact_sequence {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u_1, u, u} k G)} (hS : S.ShortExact) (n : ℤ) : Function.Exact ⇑(tateHnGen.inducedMap S.f n) ⇑(tateHnGen.inducedMap S.g n) ∧ Function.Exact ⇑(tateHnGen.inducedMap S.g n) ⇑(tateHnGen.connectingMap hS n) ∧ Function.Exact ⇑(tateHnGen.connectingMap hS n) ⇑(tateHnGen.inducedMap S.f (n + 1))

theorem TateCohomology.tateHnGen.inducedMap_id_apply {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {A : Rep.{u_1, u, u} k G} {n : ℤ} (x : tateHnGen k G A n) : (inducedMap (CategoryTheory.CategoryStruct.id A) n) x = x

theorem TateCohomology.tateHnGen.inducedMap_comp_apply {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {A B C : Rep.{u_1, u, u} k G} (f : A ⟶ B) (g : B ⟶ C) {n : ℤ} (x : tateHnGen k G A n) : (inducedMap (CategoryTheory.CategoryStruct.comp f g) n) x = (inducedMap g n) ((inducedMap f n) x)

theorem TateCohomology.tateHnGen.inducedMap_zero_apply {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {A B : Rep.{u_1, u, u} k G} {n : ℤ} (x : tateHnGen k G A n) : (inducedMap 0 n) x = 0

theorem TateCohomology.tateHnGen.inducedMap_add_apply {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {A B : Rep.{u_1, u, u} k G} (f g : A ⟶ B) {n : ℤ} (x : tateHnGen k G A n) : (inducedMap (f + g) n) x = (inducedMap f n) x + (inducedMap g n) x

theorem TateCohomology.tateHnGen_periodicity {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u_1, u, u} k G) (n : ℤ) : Nonempty (tateHnGen k G A n ≃+ tateHnGen k G A (n + 2))

theorem TateCohomology.tateHnGen_pos_iso_groupCohomology {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) (n : ℕ) : Nonempty (tateHnGen k G A ↑(n + 1) ≃+ ↑(groupCohomology A (n + 1)))

theorem TateCohomology.tateHnGen_neg_iso_groupHomology {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) (m : ℕ) : Nonempty (tateHnGen k G A (-↑(m + 2)) ≃+ ↑(groupHomology A (m + 1)))

theorem TateCohomology.tateH0_subsingleton_of_induced {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (B : Rep.{u, u, u} k ↥⊥) : Subsingleton (tateH0 (Rep.ind ⊥.subtype B))

noncomputable def TateCohomology.tateMinus1_ind_augRetract {k : Type u} [CommRing k] {G : Type u} [Group G] (B : Rep.{u, u, u} k ↥⊥) : Representation.IndV ⊥.subtype B.ρ →ₗ[k] ↑B

noncomputable def TateCohomology.tateMinus1_ind_proj1 {k : Type u} [CommRing k] {G : Type u} [Group G] (B : Rep.{u, u, u} k ↥⊥) : Representation.IndV ⊥.subtype B.ρ →ₗ[k] ↑B

theorem TateCohomology.tateMinus1_ind_augRetract_mk {k : Type u} [CommRing k] {G : Type u} [Group G] (B : Rep.{u, u, u} k ↥⊥) (h : G) (b : ↑B) : (tateMinus1_ind_augRetract B) ((Representation.IndV.mk ⊥.subtype B.ρ h) b) = b

theorem TateCohomology.tateMinus1_ind_proj1_mk_inv {k : Type u} [CommRing k] {G : Type u} [Group G] [DecidableEq G] (B : Rep.{u, u, u} k ↥⊥) (g : G) (b : ↑B) : (tateMinus1_ind_proj1 B) ((Representation.IndV.mk ⊥.subtype B.ρ g⁻¹) b) = if g = 1 then b else 0

theorem TateCohomology.tateMinus1_ind_proj1_norm_mk1 {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (B : Rep.{u, u, u} k ↥⊥) (b : ↑B) : (tateMinus1_ind_proj1 B) ((Representation.ind ⊥.subtype B.ρ).norm ((Representation.IndV.mk ⊥.subtype B.ρ 1) b)) = b

theorem TateCohomology.tateMinus1_subsingleton_of_induced {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (B : Rep.{u, u, u} k ↥⊥) : Subsingleton (tateMinus1 (Rep.ind ⊥.subtype B))

theorem TateCohomology.tateCohomology_periodicity {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u, u, u} k G) (n : ℤ) : Nonempty (tateHnGen k G A n ≃+ tateHnGen k G A (n + 2))

theorem TateCohomology.tateCohomology_six_term_exact {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) : ∃ (f₁ : tateH0 S.X₁ →+ tateH0 S.X₂) (f₂ : tateH0 S.X₂ →+ tateH0 S.X₃) (δ : tateMinus1 S.X₃ →+ tateH0 S.X₁) (f₄ : tateMinus1 S.X₁ →+ tateMinus1 S.X₂) (f₅ : tateMinus1 S.X₂ →+ tateMinus1 S.X₃), Function.Exact ⇑f₄ ⇑f₅ ∧ Function.Exact ⇑f₅ ⇑δ ∧ Function.Exact ⇑δ ⇑f₁ ∧ Function.Exact ⇑f₁ ⇑f₂

theorem TateCohomology.tateCohomology_connecting {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) (f₂ : tateH0 S.X₂ →+ tateH0 S.X₃) (f₄ : tateMinus1 S.X₁ →+ tateMinus1 S.X₂) : ∃ (f₃ : tateH0 S.X₃ →+ tateMinus1 S.X₁), Function.Exact ⇑f₂ ⇑f₃ ∧ Function.Exact ⇑f₃ ⇑f₄

theorem TateCohomology.exact_hexagon_exists {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) : ∃ (f₁ : tateH0 S.X₁ →+ tateH0 S.X₂) (f₂ : tateH0 S.X₂ →+ tateH0 S.X₃) (f₃ : tateH0 S.X₃ →+ tateMinus1 S.X₁) (f₄ : tateMinus1 S.X₁ →+ tateMinus1 S.X₂) (f₅ : tateMinus1 S.X₂ →+ tateMinus1 S.X₃) (f₆ : tateMinus1 S.X₃ →+ tateH0 S.X₁), Function.Exact ⇑f₁ ⇑f₂ ∧ Function.Exact ⇑f₂ ⇑f₃ ∧ Function.Exact ⇑f₃ ⇑f₄ ∧ Function.Exact ⇑f₄ ⇑f₅ ∧ Function.Exact ⇑f₅ ⇑f₆ ∧ Function.Exact ⇑f₆ ⇑f₁

theorem TateCohomology.exact_hexagon_card_identity {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) [Fintype (tateH0 S.X₁)] [Fintype (tateMinus1 S.X₁)] [Fintype (tateH0 S.X₂)] [Fintype (tateMinus1 S.X₂)] [Fintype (tateH0 S.X₃)] [Fintype (tateMinus1 S.X₃)] : Fintype.card (tateH0 S.X₁) * Fintype.card (tateH0 S.X₃) * Fintype.card (tateMinus1 S.X₂) = Fintype.card (tateH0 S.X₂) * Fintype.card (tateMinus1 S.X₁) * Fintype.card (tateMinus1 S.X₃)

theorem TateCohomology.herbrandQuotient_multiplicative {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) [Fintype (tateH0 S.X₁)] [Fintype (tateMinus1 S.X₁)] [Fintype (tateH0 S.X₂)] [Fintype (tateMinus1 S.X₂)] [Fintype (tateH0 S.X₃)] [Fintype (tateMinus1 S.X₃)] : herbrandQuotient S.X₂ = herbrandQuotient S.X₁ * herbrandQuotient S.X₃

theorem TateCohomology.herbrandQuotient_defined_of_AC {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) [Finite (tateH0 S.X₁)] [Finite (tateMinus1 S.X₁)] [Finite (tateH0 S.X₃)] [Finite (tateMinus1 S.X₃)] : Finite (tateH0 S.X₂) ∧ Finite (tateMinus1 S.X₂)

theorem TateCohomology.herbrandQuotient_defined_of_AB {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) [Finite (tateH0 S.X₁)] [Finite (tateMinus1 S.X₁)] [Finite (tateH0 S.X₂)] [Finite (tateMinus1 S.X₂)] : Finite (tateH0 S.X₃) ∧ Finite (tateMinus1 S.X₃)

theorem TateCohomology.herbrandQuotient_defined_of_BC {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) [Finite (tateH0 S.X₂)] [Finite (tateMinus1 S.X₂)] [Finite (tateH0 S.X₃)] [Finite (tateMinus1 S.X₃)] : Finite (tateH0 S.X₁) ∧ Finite (tateMinus1 S.X₁)

def TateCohomology.HerbrandMultiplicative {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)) : Prop

theorem TateCohomology.herbrandQuotient_directSum {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A B : Rep.{u, u, u} k G) [Fintype (tateH0 A)] [Fintype (tateMinus1 A)] [Fintype (tateH0 B)] [Fintype (tateMinus1 B)] : Finite (tateH0 (A ⊞ B)) ∧ Finite (tateMinus1 (A ⊞ B)) ∧ ∀ (inst1 : Fintype (tateH0 (A ⊞ B))) (inst2 : Fintype (tateMinus1 (A ⊞ B))), herbrandQuotient (A ⊞ B) = herbrandQuotient A * herbrandQuotient B

noncomputable def TateCohomology.tateHnGen_biproduct_addEquiv {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A B : Rep.{u_1, u, u} k G) (n : ℤ) : tateHnGen k G (A ⊞ B) n ≃+ tateHnGen k G A n × tateHnGen k G B n

theorem TateCohomology.tateHnGen_subsingleton_induced {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (B : Rep.{u, u, u} k ↥⊥) (n : ℤ) : Subsingleton (tateHnGen k G (Rep.ind ⊥.subtype B) n)

noncomputable def TateCohomology.tateHnGen_iso_equiv {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {M N : Rep.{u_1, u, u} k G} (iso : M ≅ N) (n : ℤ) : tateHnGen k G M n ≃ tateHnGen k G N n

theorem TateCohomology.free_rep_iso_induced {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (M : Rep.{u, u, u} k G) [Module.Free (MonoidAlgebra k G) M.ρ.asModule] : ∃ (B : Rep.{u, u, u} k ↥⊥), Nonempty (M ≅ Rep.ind ⊥.subtype B)

theorem TateCohomology.tateHnGen_subsingleton_of_free {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (M : Rep.{u, u, u} k G) [Module.Free (MonoidAlgebra k G) M.ρ.asModule] (n : ℤ) : Subsingleton (tateHnGen k G M n)

theorem TateCohomology.card_eq_card_ker_mul_card_range {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) : Nat.card M = Nat.card ↥f.ker * Nat.card ↥f.range

theorem TateCohomology.ker_rho_sub_one_eq_invariants {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) (σ : G) (hσ : ∀ (x : G), x ∈ Subgroup.zpowers σ) : (A.ρ σ - LinearMap.id).ker = A.ρ.invariants

theorem TateCohomology.rho_pow_sub_mem_range_nat {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) (σ : G) (n : ℕ) (a : ↑A) : (A.ρ (σ ^ n)) a - a ∈ (A.ρ σ - LinearMap.id).range

theorem TateCohomology.rho_inv_pow_sub_mem_range {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) (σ : G) (n : ℕ) (a : ↑A) : (A.ρ (σ⁻¹ ^ n)) a - a ∈ (A.ρ σ - LinearMap.id).range

theorem TateCohomology.rho_zpow_sub_mem_range {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u_1, u, u} k G) (σ : G) (n : ℤ) (a : ↑A) : (A.ρ (σ ^ n)) a - a ∈ (A.ρ σ - LinearMap.id).range

theorem TateCohomology.range_rho_sub_one_eq_augmentationSubmodule {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u_1, u, u} k G) (σ : G) (hσ : ∀ (x : G), x ∈ Subgroup.zpowers σ) : (A.ρ σ - LinearMap.id).range = augmentationSubmodule k G A

theorem TateCohomology.card_invariants_mul_augmentation {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u_1, u, u} k G) [Finite ↑A] : Nat.card ↑A = Nat.card ↥A.ρ.invariants * Nat.card ↥(augmentationSubmodule k G A)

theorem TateCohomology.herbrand_quotient_eq_one_of_finite {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u, u, u} k G) [Finite (tateH0 A)] [Finite (tateMinus1 A)] [Finite ↑A] : Nat.card (tateH0 A) = Nat.card (tateMinus1 A)

theorem TateCohomology.herbrandQuotient_eq_of_shortExact_finite {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) (hfin : Finite ↑S.X₁) [Fintype (tateH0 S.X₂)] [Fintype (tateMinus1 S.X₂)] [Fintype (tateH0 S.X₃)] [Fintype (tateMinus1 S.X₃)] : herbrandQuotient S.X₂ = herbrandQuotient S.X₃

theorem TateCohomology.ker_normMap_trivial_int {G₀ : Type} [Group G₀] [Fintype G₀] : (normMap ℤ G₀ (Rep.trivial ℤ G₀ ℤ)).ker = ⊥

noncomputable def TateCohomology.invEquivTrivInt {G₀ : Type} [Group G₀] [Fintype G₀] : ↥(Rep.trivial ℤ G₀ ℤ).ρ.invariants ≃ₗ[ℤ] ℤ

theorem TateCohomology.invEquivTrivInt_apply {G₀ : Type} [Group G₀] [Fintype G₀] (x : ↥(Rep.trivial ℤ G₀ ℤ).ρ.invariants) : invEquivTrivInt x = ↑x

theorem TateCohomology.map_normImage_trivInt {G₀ : Type} [Group G₀] [Fintype G₀] : Submodule.map (↑invEquivTrivInt) (normImageInInvariants (Rep.trivial ℤ G₀ ℤ)) = ℤ ∙ ↑(Fintype.card G₀)

noncomputable def TateCohomology.tateH0_equiv_zmod {G₀ : Type} [Group G₀] [Fintype G₀] : tateH0 (Rep.trivial ℤ G₀ ℤ) ≃ ZMod (Fintype.card G₀)

def TateCohomology.Rep.trivialHom {G₀ : Type u_1} [Monoid G₀] {M N : Type} [AddCommGroup M] [AddCommGroup N] (f : M →ₗ[ℤ] N) : Rep.trivial ℤ G₀ M ⟶ Rep.trivial ℤ G₀ N

theorem TateCohomology.Rep.trivialHom_comp {G₀ : Type u_1} [Monoid G₀] {M N P : Type} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] (f : M →ₗ[ℤ] N) (g : N →ₗ[ℤ] P) : CategoryTheory.CategoryStruct.comp (trivialHom f) (trivialHom g) = trivialHom (g ∘ₗ f)

theorem TateCohomology.Rep.trivialHom_id {G₀ : Type u_1} [Monoid G₀] {M : Type} [AddCommGroup M] : trivialHom LinearMap.id = CategoryTheory.CategoryStruct.id (Rep.trivial ℤ G₀ M)

theorem TateCohomology.herbrandQuotient_eq_of_finite_kernel_cokernel {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {A B : Rep.{u, u, u} k G} (α : A ⟶ B) [Finite ↑(CategoryTheory.Limits.kernel α)] [Finite ↑(CategoryTheory.Limits.cokernel α)] [Fintype (tateH0 A)] [Fintype (tateMinus1 A)] [Fintype (tateH0 B)] [Fintype (tateMinus1 B)] : herbrandQuotient A = herbrandQuotient B

theorem TateCohomology.herbrandQuotient_defined_of_finite_kernel_cokernel_left {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {A B : Rep.{u, u, u} k G} (α : A ⟶ B) [Finite ↑(CategoryTheory.Limits.kernel α)] [Finite ↑(CategoryTheory.Limits.cokernel α)] [Finite (tateH0 A)] [Finite (tateMinus1 A)] : Finite (tateH0 B) ∧ Finite (tateMinus1 B)

theorem TateCohomology.herbrandQuotient_defined_of_finite_kernel_cokernel_right {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {A B : Rep.{u, u, u} k G} (α : A ⟶ B) [Finite ↑(CategoryTheory.Limits.kernel α)] [Finite ↑(CategoryTheory.Limits.cokernel α)] [Finite (tateH0 B)] [Finite (tateMinus1 B)] : Finite (tateH0 A) ∧ Finite (tateMinus1 A)

theorem TateCohomology.finite_kernel_of_mono {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] {A B : Rep.{u_1, u, u} k G} (ι : B ⟶ A) [CategoryTheory.Mono ι] : Finite ↑(CategoryTheory.Limits.kernel ι)

theorem TateCohomology.herbrandQuotient_eq_of_mono_finite_cokernel {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] {A B : Rep.{u, u, u} k G} (ι : B ⟶ A) [CategoryTheory.Mono ι] [Finite ↑(CategoryTheory.Limits.cokernel ι)] [Fintype (tateH0 A)] [Fintype (tateMinus1 A)] [Fintype (tateH0 B)] [Fintype (tateMinus1 B)] : herbrandQuotient A = herbrandQuotient B

theorem TateCohomology.ker_normMap_trivial_finFun {G₀ : Type} [Group G₀] [Fintype G₀] (n : ℕ) : (normMap ℤ G₀ (Rep.trivial ℤ G₀ (Fin n → ℤ))).ker = ⊥

theorem TateCohomology.card_tateMinus1_trivial_finFun (G₀ : Type) [Group G₀] [Fintype G₀] [IsCyclic G₀] (n : ℕ) [Fintype (tateMinus1 (Rep.trivial ℤ G₀ (Fin n → ℤ)))] : Fintype.card (tateMinus1 (Rep.trivial ℤ G₀ (Fin n → ℤ))) = 1

noncomputable def TateCohomology.invEquivTrivFinFun {G₀ : Type} [Group G₀] [Fintype G₀] (n : ℕ) : ↥(Rep.trivial ℤ G₀ (Fin n → ℤ)).ρ.invariants ≃ₗ[ℤ] Fin n → ℤ

theorem TateCohomology.invEquivTrivFinFun_apply {G₀ : Type} [Group G₀] [Fintype G₀] (n : ℕ) (x : ↥(Rep.trivial ℤ G₀ (Fin n → ℤ)).ρ.invariants) : (invEquivTrivFinFun n) x = ↑x

theorem TateCohomology.map_normImage_trivFinFun {G₀ : Type} [Group G₀] [Fintype G₀] (n : ℕ) : Submodule.map (↑(invEquivTrivFinFun n)) (normImageInInvariants (Rep.trivial ℤ G₀ (Fin n → ℤ))) = (↑(Fintype.card G₀) • LinearMap.id).range

theorem TateCohomology.range_smul_id_eq_pi {G₀ : Type} [Group G₀] [Fintype G₀] (n : ℕ) : (↑(Fintype.card G₀) • LinearMap.id).range = Submodule.pi Set.univ fun (x : Fin n) => ℤ ∙ ↑(Fintype.card G₀)

noncomputable def TateCohomology.tateH0_equiv_pi_zmod {G₀ : Type} [Group G₀] [Fintype G₀] (n : ℕ) : tateH0 (Rep.trivial ℤ G₀ (Fin n → ℤ)) ≃ (Fin n → ZMod (Fintype.card G₀))

theorem TateCohomology.card_tateH0_trivial_finFun (G₀ : Type) [Group G₀] [Fintype G₀] [IsCyclic G₀] (n : ℕ) [Fintype (tateH0 (Rep.trivial ℤ G₀ (Fin n → ℤ)))] : Fintype.card (tateH0 (Rep.trivial ℤ G₀ (Fin n → ℤ))) = Fintype.card G₀ ^ n

theorem TateCohomology.herbrandQuotient_trivial_finFun (G₀ : Type) [Group G₀] [Fintype G₀] [IsCyclic G₀] (n : ℕ) [Fintype (tateH0 (Rep.trivial ℤ G₀ (Fin n → ℤ)))] [Fintype (tateMinus1 (Rep.trivial ℤ G₀ (Fin n → ℤ)))] : herbrandQuotient (Rep.trivial ℤ G₀ (Fin n → ℤ)) = ↑(Fintype.card G₀) ^ n

instance TateCohomology.tateH0.finite_trivial_finFun {G₀ : Type} [Group G₀] [Fintype G₀] (n : ℕ) : Finite (tateH0 (Rep.trivial ℤ G₀ (Fin n → ℤ)))

instance TateCohomology.tateMinus1.finite_trivial_finFun {G₀ : Type} [Group G₀] [Fintype G₀] (n : ℕ) : Finite (tateMinus1 (Rep.trivial ℤ G₀ (Fin n → ℤ)))