English
As above, the morphism π is a quasi-isomorphism for the finite cyclic resolution.
Русский
Как выше, морфизм π является квазиизоморфизмом для разрешения конечной циклической группы.
LaTeX
$$$ \text{QuasiIso}(\mathrm{resolution.π}_{k,g}) $$$
Lean4
/-- 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. -/
@[simps]
noncomputable def resolution (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) : ProjectiveResolution (trivial k G k)
where
complex := (FiniteCyclicGroup.chainComplexFunctor k g).obj (leftRegular k G)
projective _ := inferInstanceAs <| Projective (leftRegular k G)
π := FiniteCyclicGroup.resolution.π k g
quasiIso := resolution_quasiIso k g hg
