Theorems · Definition · group theory

Rep.FiniteCyclicGroup.resolution

(k : Type u) →
  {G : Type u} →
    [inst : CommRing k] →
      [inst_1 : CommGroup G] →
        [Fintype G] →
          (g : G) → (∀ (x : G), x ∈ Subgroup.zpowers g) → CategoryTheory.ProjectiveResolution (Rep.trivial k G k)

Given a finite cyclic group G generated by g : G, this is the projective resolution of k as a trivial k-linear G-representation given by periodic complex ... ⟶ k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] ⟶ 0 where ρ is the left regular representation and N is the norm map.

Defined in

Mathlib.RepresentationTheory.Homological.FiniteCyclic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingCommGroupFintype