llp_rlp_monomorphisms — Mathlib

English

There exists a small object argument for generatingMonomorphisms that yields control over transfinite constructions in Grothendieck abelian categories.

Русский

Существует аргумент малого объекта для порождающих мономорфизмов, обеспечивающий управление трансфинитными конструкциями в абелевых категориях Гротенштейда.

LaTeX

$$$\\exists κ\\,\\text{ such that }(generatingMonomorphisms G)\\text{ has a small object argument of size }κ$$$

Lean4

theorem llp_rlp_monomorphisms (hG : IsSeparator G) : (monomorphisms C).rlp.llp = monomorphisms C :=
  by
  refine le_antisymm ?_ (le_llp_rlp _)
  rw [← generatingMonomorphisms_rlp hG, llp_rlp_of_hasSmallObjectArgument]
  trans (transfiniteCompositions.{w} (coproducts.{w} (monomorphisms C)).pushouts).retracts
  · apply retracts_monotone
    apply transfiniteCompositions_monotone
    apply pushouts_monotone
    apply coproducts_monotone
    apply generatingMonomorphisms_le_monomorphisms
  · simp

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