chainsMap_f_single — Mathlib

English

If f is the identity on G and φ is a mono morphism, then the chain map components are mono.

Русский

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

LaTeX

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

Lean4

theorem chainsMap_f_single (n : ℕ) (x : Fin n → G) (a : A) :
    (chainsMap f φ).f n (single x a) = single (f ∘ x) (φ.hom a) := by simp [chainsMap_f]

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