range_applyAsHom_sub_eq_ker_linearCombination

English

The morphism π in the finite cyclic resolution gives a quasi-isomorphism from the periodic chain complex built from the left regular representation to the trivial complex.

Русский

Морфизм π в разрешении для конечной циклической группы задаёт квазиизоморфизм между периодическим цепным комплексом, построенным из левого регулярного представления, и тривиальным комплексом.

LaTeX

$$$ \text{QuasiIso}(\mathrm{resolution.\pi}_{k,g}) $$$

Lean4

theorem range_applyAsHom_sub_eq_ker_linearCombination (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    LinearMap.range (applyAsHom (leftRegular k G) g - 𝟙 _).hom.hom =
      LinearMap.ker (linearCombination k (fun _ => (1 : k))) :=
  by simp [← FiniteCyclicGroup.coinvariantsKer_eq_range _ _ hg, ← FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker]

Похожие утверждения