English
The LLP- and RLP-classes for monomorphisms coincide in a Grothendieck abelian category with separator G.
Русский
Классы LLP и RLP для мономорфизмов совпадают в абелевой категории Гротенштейджа при наличии разделяющего F.
LaTeX
$$$((monomorphisms C).llp) = ((monomorphisms C).rlp)$$$
Lean4
instance : HasSmallObjectArgument.{w} (generatingMonomorphisms G) :=
by
obtain ⟨κ, hκ', hκ⟩ := HasCardinalLT.exists_regular_cardinal.{w} (Subobject G)
have : Fact κ.IsRegular := ⟨hκ'⟩
letI := Cardinal.toTypeOrderBot hκ'.ne_zero
exact
⟨κ, inferInstance, inferInstance,
{
preservesColimit {A B X Y} i hi f
hf :=
by
let hf' : (monomorphisms C).TransfiniteCompositionOfShape κ.ord.toType f :=
{ toTransfiniteCompositionOfShape := hf.toTransfiniteCompositionOfShape
map_mem j
hj := by
have := (hf.attachCells j hj).pushouts_coproducts
simp only [ofHoms_homFamily] at this
refine (?_ : _ ≤ monomorphisms C) _ this
simp only [pushouts_le_iff, coproducts_le_iff]
exact generatingMonomorphisms_le_monomorphisms G }
have (j j' : κ.ord.toType) (φ : j ⟶ j') : Mono (hf'.F.map φ) := hf'.mem_map φ
apply preservesColimit_coyoneda_obj_of_mono (Y := hf'.F) (κ := κ)
obtain ⟨S⟩ := hi
exact Subobject.hasCardinalLT_of_mono hκ S.arrow }⟩
