English
An isomorphism in Dial C is determined by isomorphisms on the source and target that respect the given relation via a pullback diagram.
Русский
Изоморфизм в Dial C задаётся изоморфизмами на источник и цель, которые сохраняют данное отношение через диаграмму pullback.
LaTeX
$$$\text{If } e_1,e_2 \text{ are isomorphisms on sources/targets and } eq, \text{ then } X \cong Y$$$
Lean4
theorem comp_le_lemma {X Y Z : Dial C} (F : Dial.Hom X Y) (G : Dial.Hom Y Z) :
(Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 _) ≫ G.F) ≫ F.F)).obj X.rel ≤
(Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel :=
by
refine
le_trans ?_ <|
((Subobject.pullback (π(π₁, prod.map F.f (𝟙 _) ≫ G.F))).monotone F.le).trans <|
le_trans ?_ <| ((Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).monotone G.le).trans ?_ <;>
simp [← Subobject.pullback_comp]
