English
For a finite cyclic group generated by g, the range of applyAsHom(leftRegular) − id equals the kernel of the linear combination map that sums coefficients with unit coefficients.
Русский
Для конечной циклической группы, порождаемой g, образ applyAsHom(leftRegular) − id равен ядру линейной комбинации, суммирующей коэффициенты с единичными коэффициентами.
LaTeX
$$$ \operatorname{range}(\mathrm{applyAsHom}(\text{leftRegular})\, g - \mathrm{id}).hom = \ker(\mathrm{linearCombination}_k(\lambda _:\, \_ => 1)) $$
Lean4
/-- Given a finite group `G` and `g : G`, this is the functor `Rep k G ⥤ ChainComplex (Rep k G) ℕ`
sending `A : Rep k G` to the periodic chain complex in `Rep k G` given by
`... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0`
where `N` is the norm map. When `G` is generated by `g` and `A` is the left regular representation
`k[G]`, it is a projective resolution of `k` as a trivial representation.
It sends a morphism `f : A ⟶ B` to the chain morphism defined by `f` in every degree. -/
@[simps]
noncomputable def chainComplexFunctor : Rep k G ⥤ ChainComplex (Rep k G) ℕ
where
obj
A :=
HomologicalComplex.alternatingConst A (φ := A.norm) (ψ := applyAsHom A g - 𝟙 A) (by ext; simp) (by ext; simp)
fun _ _ => ComplexShape.down_nat_odd_add
map
f :=
{ f i := f
comm' := by
rintro i j ⟨rfl⟩
by_cases hj : Even (j + 1)
· simp [if_pos hj, norm_comm]
· simp [if_neg hj, applyAsHom_comm] }
map_id _ := rfl
map_comp _ _ := rfl
