instMonoFOfHasFiniteLimits — Mathlib

English

If C has finite limits, then for any mono φ: K ⟶ L in HomologicalComplex C c, each component φ.f i is mono.

Русский

Если в C есть конечные пределы, тогда любая моно-морфизма φ: K ⟶ L в HomologicalComplex C c имеет моно-компоненты φ.f_i для всех i.

LaTeX

$$$ \forall \phi: K \to L, \ [\text{Mono }\phi] \Rightarrow \forall i, \ \text{Mono}(\phi.f_i). $$$

Lean4

instance [HasFiniteLimits C] {K L : HomologicalComplex C c} (φ : K ⟶ L) [Mono φ] (n : ι) : Mono (φ.f n) :=
  by
  change Mono ((HomologicalComplex.eval C c n).map φ)
  infer_instance

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