English
The morphism π furnishes the projective resolution of the trivial representation by the left regular resolution, providing a concrete chain map.
Русский
Морфизм π образует проективное разрешение тривиального представления через левое регулярное разрешение; это конкретное цепное отображение.
LaTeX
$$$ \text{resolution.π}_{k,g} : (\text{leftRegular}_{k,G}) \to (\text{trivial}_{k,G}) $$$
Lean4
/-- Given a finite cyclic group `G` generated by `g : G`, let `P` denote the periodic chain complex
of `k`-linear `G`-representations given by
`... ⟶ 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. This is the chain morphism from `P` to
the chain complex concentrated at 0 by the trivial representation `k` used to show `P` is a
projective resolution of `k`. It sends `x : k[G]` to the sum of its coefficients. -/
@[simps!]
noncomputable def π (g : G) :
(chainComplexFunctor k g).obj (leftRegular k G) ⟶ (ChainComplex.single₀ (Rep k G)).obj (trivial k G k) :=
(((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv _).symm
⟨leftRegularHom _ 1, (leftRegularHomEquiv _).injective <| by simp [leftRegularHomEquiv]⟩
