chainsMap_id — Mathlib

English

If φ is epi, then each component ((chainsMap (id, φ)).f i) is epi.

Русский

Если φ эпиморфизм, то каждый компонент цепной карты эпиморфизм.

LaTeX

$$∀ i, Epi ((chainsMap (MonoidHom.id G) φ).f i)$$

Lean4

@[simp]
theorem chainsMap_id : chainsMap (MonoidHom.id G) (𝟙 A) = 𝟙 (inhomogeneousChains A) :=
  HomologicalComplex.hom_ext _ _ fun _ =>
    ModuleCat.hom_ext <|
      lhom_ext' fun _ => ModuleCat.hom_ext_iff.1 <| lsingle_comp_chainsMap_f (k := k) (MonoidHom.id G) ..

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