English
The subobjects of a structured arrow A are in natural order-isomorphism with subobjects of A.right equipped with a witness of a factoring through T; i.e., Subobject(A) ≃o { P : Subobject(A.right) | ∃ q, q ≫ T.map P.arrow = A.hom }.
Русский
Подобъекты структурированной стрелки A эквивалентны упорядоченной структуре пар: подобъекты B правой части A со свидетельством факторизации через T; то есть Subobject(A) ≃o { P ⊆ A.right | ∃ q, q ≫ T.map P.arrow = A.hom }.
LaTeX
$$$\\mathrm{Subobject}(A) \\cong_{\\!\\mathrm{ord}} \\{ P : \\mathrm{Subobject}(A.right) \\;\\middle|\\; \\exists q,\\ q \\;\\mathrm{≫} \\; T.map P.arrow = A.hom \\}.$$$
Lean4
/-- If `A : S → T.obj B` is a structured arrow for `S : D` and `T : C ⥤ D`, then we can explicitly
describe the subobjects of `A` as the subobjects `P` of `B` in `C` for which `A.hom` factors
through the image of `P` under `T`. -/
def subobjectEquiv [HasFiniteLimits C] [PreservesFiniteLimits T] (A : StructuredArrow S T) :
Subobject A ≃o { P : Subobject A.right // ∃ q, q ≫ T.map P.arrow = A.hom }
where
toFun P := ⟨projectSubobject P, projectSubobject_factors P⟩
invFun P := liftSubobject P.val P.prop.choose_spec
left_inv _ := lift_projectSubobject _ _
right_inv P := Subtype.ext (by simp only [liftSubobject, homMk_right, projectSubobject_mk, Subobject.mk_arrow])
map_rel_iff' := by
apply Subobject.ind₂
intro P Q f g hf hg
refine ⟨fun h => Subobject.mk_le_mk_of_comm ?_ ?_, fun h => ?_⟩
· exact homMk (Subobject.ofMkLEMk _ _ h) ((cancel_mono (T.map g.right)).1 (by simp [← T.map_comp]))
· simp
· refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right ?_
exact congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h)
