English
If A is a structured arrow S ⇒ T and P is a subobject of A.right together with a morphism q making the triangle commute (hq: q ≫ T.map P.arrow = A.hom), then P lifts to a subobject of A via Subobject.mk (homMk P.arrow hq).
Русский
Пусть A — структурированная стрелка S ⇒ T и P — подобъект A.right, обладающий морфизмом q, делающим треугольник коммютативным (hq: q ≫ T.map P.arrow = A.hom). Тогда P поднимается до подобъекта A через Subobject.mk (homMk P.arrow hq).
LaTeX
$$$\\forall A : \\mathrm{StructuredArrow} \\\\ S \\\\ T, \\\\forall P : \\mathrm{Subobject} \\\\ A.right, \\\\forall q, (hq : q \\\\circ T.map P.arrow = A.hom) \\\\Rightarrow \\\\mathrm{liftSubobject}\,P\,hq = \\mathrm{Subobject.mk} (\\\\mathrm{homMk} \\, P.arrow \\, hq).$$$
Lean4
/-- A subobject of the underlying object of a structured arrow can be lifted to a subobject of
the structured arrow, provided that there is a morphism making the subobject into a structured
arrow. -/
@[simp]
def liftSubobject {A : StructuredArrow S T} (P : Subobject A.right) {q} (hq : q ≫ T.map P.arrow = A.hom) :
Subobject A :=
Subobject.mk (homMk P.arrow hq : mk q ⟶ A)
