instIsStableUnderCobaseChangeMonomorphisms

English

In an abelian category, monomorphisms are stable under cobase change.

Русский

В абелевой категории монооморфизмы сохраняются под базовым изменением (пушпо́том).

LaTeX

$$$\\text{monomorphisms} \\text{ is stable under cobase change}$$$

Lean4

instance : (monomorphisms C).IsStableUnderCobaseChange :=
  IsStableUnderCobaseChange.mk'
    (fun _ _ _ f g _ hf ↦ by
      simp only [monomorphisms.iff] at hf ⊢
      infer_instance)

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