coinvariantsShortComplex_shortExact

English

The coinvariants short complex is exact in the sense of abelian category theory; i.e., the sequence is short exact.

Русский

Кратная точная последовательность когонвариантов является точной в абелевой категории.

LaTeX

$$(coinvariantsShortComplex A S).ShortExact$$

Lean4

theorem coinvariantsShortComplex_shortExact : (coinvariantsShortComplex A S).ShortExact
    where
  exact :=
    (forget₂ _ (ModuleCat k)).reflects_exact_of_faithful _ <|
      (ShortComplex.moduleCat_exact_iff _).2 fun x hx =>
        ⟨(⟨x, (Submodule.Quotient.mk_eq_zero _).1 hx⟩ : Representation.Coinvariants.ker <| A.ρ.comp S.subtype), rfl⟩
  mono_f := (Rep.mono_iff_injective _).2 fun _ _ h => Subtype.ext h
  epi_g := (Rep.epi_iff_surjective _).2 <| Submodule.mkQ_surjective _

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