English
If C is well-powered in the opposite sense and cocomplete, and S preserves colimits, then CostructuredArrow S T is well-powered.
Русский
Если C хорошо-обозначено в противоположном виде и когомплектно, и S сохраняет когомоморфизмы, тогда CostructuredArrow S T тоже хорошо-порожденная категория.
LaTeX
$$$[\\text{WellPowered } (C^{op})] \\Rightarrow [\\text{WellPowered } (CostructuredArrow S T)^{op}].$$$
Lean4
/-- Projecting and then lifting a quotient recovers the original quotient, because there is at most
one morphism making the projected quotient into a costructured arrow. -/
theorem lift_projectQuotient [HasFiniteColimits C] [PreservesFiniteColimits S] {A : CostructuredArrow S T} :
∀ (P : Subobject (op A)) {q} (hq : S.map (projectQuotient P).arrow.unop ≫ q = A.hom),
liftQuotient (projectQuotient P) hq = P :=
Subobject.ind _
(by
intro P f hf q hq
fapply Subobject.mk_eq_mk_of_comm
· refine (Iso.op (isoMk ?_ ?_) : _ ≅ op (unop P))
· exact (Subobject.underlyingIso f.unop.left.op).unop
· refine (cancel_epi (S.map f.unop.left)).1 ?_
simpa [← Category.assoc, ← S.map_comp] using hq
· exact Quiver.Hom.unop_inj (by simp))
