Theorems · Definition · group theory

Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [inst_2 : Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) →
              HomologicalComplex.coinvariantsTensorObj A (Rep.FiniteCyclicGroup.resolution k g⁻¹ ⋯).complex ≅
                Rep.FiniteCyclicGroup.moduleCatChainComplex A g

Given a finite cyclic group G generated by g : G and a k-linear G-representation A, the period chain complex ... ⟶ (A ⊗ₖ k[G])_G --⟦Id ⊗ N⟧--> (A ⊗ₖ k[G])_G --⟦Id ⊗ (ρ(g⁻¹) - 𝟙)⟧--> (A ⊗ₖ k[G])_G ⟶ 0 is isomorphic as a complex in ModuleCat k to ... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommGroupFintype