English
The ThinSkeleton of a category inherits a natural preorder relation defined via existence of arrows between representatives; reflexivity and transitivity hold.
Русский
У ThinSkeleton для категории задаётся естественный порядковый relation через существование стрелок между представительствами; рефлективность и транзитивность выполняются.
LaTeX
$$Let $X,Y\\in \\mathrm{ThinSkeleton}(C)$. Then define $X \\le Y$ iff there exist representatives $x\\in C$, $y\\in C$ and a morphism $f:x\\to y$ with $X=[x]$, $Y=[y]$; this relation is a preorder, i.e., reflexive and transitive.$$
Lean4
instance preorder : Preorder (ThinSkeleton C)
where
le :=
@Quotient.lift₂ C C _ (isIsomorphicSetoid C) (isIsomorphicSetoid C) (fun X Y => Nonempty (X ⟶ Y))
(by
rintro _ _ _ _ ⟨i₁⟩ ⟨i₂⟩
exact propext ⟨Nonempty.map fun f => i₁.inv ≫ f ≫ i₂.hom, Nonempty.map fun f => i₁.hom ≫ f ≫ i₂.inv⟩)
le_refl := by
refine Quotient.ind fun a => ?_
exact ⟨𝟙 _⟩
le_trans a b c := Quotient.inductionOn₃ a b c fun _ _ _ => Nonempty.map2 (· ≫ ·)
