English
Projecting a subobject and then lifting it back recovers the original subobject, because there is at most one morphism making the projected subobject into a structured arrow.
Русский
Проецирование подобъекта и последующий возврат к нему восстанавливают исходный подобъект, так как существует не более одного морфизма, делающего спроецированный подобъект структурированной стрелкой.
LaTeX
$$$\\forall A : \\mathrm{StructuredArrow} S T, \\\\forall P : \\mathrm{Subobject} A, \\\\forall q, (hq : q \\\\\\circ T.map (\\\\mathrm{projectSubobject} P).arrow = A.hom) \\\\Rightarrow \\\\mathrm{liftSubobject} (\\\\mathrm{projectSubobject} P) \\\\text{hq} = P.$$$
Lean4
/-- Projecting and then lifting a subobject recovers the original subobject, because there is at
most one morphism making the projected subobject into a structured arrow. -/
theorem lift_projectSubobject [HasFiniteLimits C] [PreservesFiniteLimits T] {A : StructuredArrow S T} :
∀ (P : Subobject A) {q} (hq : q ≫ T.map (projectSubobject P).arrow = A.hom),
liftSubobject (projectSubobject P) hq = P :=
Subobject.ind _
(by
intro P f hf q hq
fapply Subobject.mk_eq_mk_of_comm
· fapply isoMk
· exact Subobject.underlyingIso _
· exact (cancel_mono (T.map f.right)).1 (by dsimp; simpa [← T.map_comp] using hq)
· exact ext _ _ (by simp))
