English
The resolution π is a quasi-isomorphism, hence a projective resolution of the trivial representation in this setting.
Русский
Разрешение π является квазиизоморфизмом, следовательно проективное разрешение тривиального представления в данной конфигурации.
LaTeX
$$$ \text{QuasiIso}(\mathrm{resolution.π}_{k,g}) $$$
Lean4
theorem resolution_quasiIso (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) : QuasiIso (resolution.π k g) where
quasiIsoAt
m := by
induction m with
| zero =>
simp only [resolution.π]
rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros' _ rfl rfl rfl]
constructor
· apply (Action.forget (ModuleCat k) _).reflects_exact_of_faithful
simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker, HomologicalComplex.alternatingConst,
ChainComplex.toSingle₀Equiv] using leftRegular.range_applyAsHom_sub_eq_ker_linearCombination k g hg
· rw [Rep.epi_iff_surjective]
intro x
use single 1 x
simp [ChainComplex.toSingle₀Equiv]
| succ m
_ =>
rw [quasiIsoAt_iff_exactAt' (hL := ChainComplex.exactAt_succ_single_obj ..),
HomologicalComplex.exactAt_iff' _ (m + 2) (m + 1) m (by simp) (by simp)]
apply (Action.forget (ModuleCat k) _).reflects_exact_of_faithful
rw [ShortComplex.moduleCat_exact_iff_range_eq_ker]
by_cases hm : Odd (m + 1)
·
simpa [if_pos (Nat.even_add_one.2 (Nat.not_even_iff_odd.2 hm)), if_neg (Nat.not_even_iff_odd.2 hm)] using
leftRegular.range_norm_eq_ker_applyAsHom_sub k g hg
·
simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker, if_pos (Nat.not_odd_iff_even.1 hm),
if_neg (Nat.not_even_iff_odd.2 <| Nat.odd_add_one.2 hm)] using
leftRegular.range_applyAsHom_sub_eq_ker_norm k g hg
