generatingMonomorphisms_rlp — Mathlib

English

In a Grothendieck abelian category, the right lifting property class of monomorphisms determined by a separator G coincides with the general class of monomorphisms.

Русский

В абелевой категории Гротенштейджа правой гранью свойств-L lifting для мономорфизмов определяется по разделяющему объекту G и совпадает с общим классом мономорфизмов.

LaTeX

$$$ (generatingMonomorphisms\, G).rlp = (monomorphisms)\\,rlp$$$

Lean4

theorem generatingMonomorphisms_rlp [IsGrothendieckAbelian.{w} C] (hG : IsSeparator G) :
    (generatingMonomorphisms G).rlp = (monomorphisms C).rlp :=
  by
  apply le_antisymm
  · intro X Y p hp A B i (_ : Mono i)
    obtain ⟨J, _, _, _, _, ⟨h⟩⟩ := generatingMonomorphisms.exists_transfiniteCompositionOfShape hG i
    exact transfiniteCompositionsOfShape_le_llp_rlp _ _ _ h.mem _ (by simpa)
  · exact antitone_rlp (generatingMonomorphisms_le_monomorphisms _)

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