Theorems · Definition · group theory

Rep.FiniteCyclicGroup.groupHomologyIsoEven

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [inst_2 : Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            [DecidableEq G] →
              (∀ (x : G), x ∈ Subgroup.zpowers g) →
                (i : ℕ) →
                  [h₀ : NeZero i] → Even i → (groupHomology A i ≅ (Rep.FiniteCyclicGroup.subCompNormHom A g).homology)

Given a finite cyclic group G generated by g and A : Rep k G, Hᵢ(G, A) is isomorphic to the homology of the short complex of k-modules A --(ρ(g) - 𝟙)--> A --N--> A when i is nonzero and even.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Cited by

2 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommGroupFintypeDecidableEqNeZero