English
There is an equivalence between Subobject (op A) and the data {P, ∃ q, S.map P.arrow.unop ≫ q = A.hom} describing quotients of a costructured arrow A.
Русский
Существует биекция между подобъектами оппонента A и данными {P, ∃ q, S.map P.arrow.unop ≫ q = A.hom}, описывающими квоты A.
LaTeX
$$$\\mathrm{quotientEquiv} : \\mathrm{Subobject} (op A) \\simeq_{\\!\\mathrm{ord}} \\{ P : \\mathrm{Subobject} (op A.left) \\;\\middle|\\; \\exists q, S.map P.arrow.unop ≫ q = A.hom \\}.$$$
Lean4
/-- Technical lemma for `quotientEquiv`. -/
theorem unop_left_comp_ofMkLEMk_unop {A : CostructuredArrow S T} {P Q : (CostructuredArrow S T)ᵒᵖ} {f : P ⟶ op A}
{g : Q ⟶ op A} [Mono f.unop.left.op] [Mono g.unop.left.op]
(h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op) :
g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left :=
by
conv_lhs =>
congr
rw [← Quiver.Hom.unop_op g.unop.left]
rw [← unop_comp]
simp only [Subobject.ofMkLEMk_comp, Quiver.Hom.unop_op]
