Mathlib.CategoryTheory.Category.Preorder

Preorder.smallCategory instance

(α : Type u) [Preorder α] : SmallCategory α

Full source

/--
The category structure coming from a preorder. There is a morphism `X ⟶ Y` if and only if `X ≤ Y`.

Because we don't allow morphisms to live in `Prop`,
we have to define `X ⟶ Y` as `ULift (PLift (X ≤ Y))`.
See `CategoryTheory.homOfLE` and `CategoryTheory.leOfHom`. -/
@[stacks 00D3]
instance (priority := 100) smallCategory (α : Type u) [Preorder α] : SmallCategory α where
  Hom U V := ULift (PLift (U ≤ V))
  id X := ⟨⟨le_refl X⟩⟩
  comp f g := ⟨⟨le_trans _ _ _ f.down.down g.down.down⟩⟩

Category Structure Induced by a Preorder

Informal description

For any preorder $(α, \leq)$, there is a canonical small category structure on $α$ where a morphism $x \to y$ exists if and only if $x \leq y$.

Preorder.subsingleton_hom instance

{α : Type u} [Preorder α] (U V : α) : Subsingleton (U ⟶ V)

Full source

instance subsingleton_hom {α : Type u} [Preorder α] (U V : α) :
  Subsingleton (U ⟶ V) := ⟨fun _ _ => ULift.ext _ _ (Subsingleton.elim _ _ )⟩

Subsingleton Hom-Sets in Preorder Categories

Informal description

For any preorder $(α, \leq)$ and elements $U, V \in α$, the hom-set $\mathrm{Hom}(U, V)$ in the associated category is a subsingleton (i.e., it has at most one element).

CategoryTheory.homOfLE definition

{x y : X} (h : x ≤ y) : x ⟶ y

Full source

/-- Express an inequality as a morphism in the corresponding preorder category.
-/
def homOfLE {x y : X} (h : x ≤ y) : x ⟶ y :=
  ULift.up (PLift.up h)

Morphism from a preorder inequality

Informal description

Given a preorder $(X, \leq)$ and elements $x, y \in X$ with $x \leq y$, the function `homOfLE` constructs a morphism $x \to y$ in the corresponding preorder category.

LE.le.hom abbrev

Full source

@[inherit_doc homOfLE]
abbrev _root_.LE.le.hom := @homOfLE

Morphism Construction from Preorder Inequality

Informal description

Given a preorder $(X, \leq)$ and elements $x, y \in X$ with $x \leq y$, the morphism $x \to y$ in the corresponding preorder category is denoted by $h.\text{hom}$, where $h$ is the proof of $x \leq y$.

CategoryTheory.homOfLE_refl theorem

{x : X} (h : x ≤ x) : h.hom = 𝟙 x

Full source

@[simp]
theorem homOfLE_refl {x : X} (h : x ≤ x) : h.hom = 𝟙 x :=
  rfl

Reflexive Inequality Yields Identity Morphism in Preorder Category

Informal description

For any element $x$ in a preorder $(X, \leq)$, the morphism $h.\text{hom}$ corresponding to the reflexive inequality $x \leq x$ is equal to the identity morphism $\text{id}_x$ in the associated category.

CategoryTheory.homOfLE_comp theorem

{x y z : X} (h : x ≤ y) (k : y ≤ z) : homOfLE h ≫ homOfLE k = homOfLE (h.trans k)

Full source

@[simp]
theorem homOfLE_comp {x y z : X} (h : x ≤ y) (k : y ≤ z) :
    homOfLEhomOfLE h ≫ homOfLE k = homOfLE (h.trans k) :=
  rfl

Composition of Morphisms in Preorder Category Corresponds to Transitive Inequality

Informal description

For any elements $x, y, z$ in a preorder $(X, \leq)$ with $x \leq y$ and $y \leq z$, the composition of the corresponding morphisms $x \to y$ and $y \to z$ in the associated preorder category is equal to the morphism $x \to z$ corresponding to the transitive inequality $x \leq z$. That is, $\text{homOfLE}(h) \circ \text{homOfLE}(k) = \text{homOfLE}(h \circ k)$.

CategoryTheory.leOfHom theorem

{x y : X} (h : x ⟶ y) : x ≤ y

Full source

/-- Extract the underlying inequality from a morphism in a preorder category.
-/
theorem leOfHom {x y : X} (h : x ⟶ y) : x ≤ y :=
  h.down.down

Inequality from Preorder Category Morphism

Informal description

For any morphism $h \colon x \to y$ in the category associated to a preorder $(X, \leq)$, we have $x \leq y$.

Quiver.Hom.le abbrev

Full source

@[nolint defLemma, inherit_doc leOfHom]
abbrev _root_.Quiver.Hom.le := @leOfHom

Inequality from Preorder Category Morphism

Informal description

For any morphism $h \colon x \to y$ in the category associated to a preorder $(X, \leq)$, we have $x \leq y$.

CategoryTheory.homOfLE_leOfHom theorem

{x y : X} (h : x ⟶ y) : h.le.hom = h

Full source

@[simp]
theorem homOfLE_leOfHom {x y : X} (h : x ⟶ y) : h.le.hom = h :=
  rfl

Equality of Constructed Morphism and Original Morphism in Preorder Category

Informal description

For any morphism $h \colon x \to y$ in the category associated to a preorder $(X, \leq)$, the morphism constructed from the inequality $x \leq y$ (denoted $h.\text{le}.\text{hom}$) is equal to $h$.

CategoryTheory.homOfLE_isIso_of_eq theorem

{x y : X} (h : x ≤ y) (heq : x = y) : IsIso (homOfLE h)

Full source

lemma homOfLE_isIso_of_eq {x y : X} (h : x ≤ y) (heq : x = y) :
    IsIso (homOfLE h) :=
  ⟨homOfLE (le_of_eq heq.symm), by simp⟩

Morphism from equality in preorder is isomorphism

Informal description

For any elements $x, y$ in a preorder $(X, \leq)$ with $x \leq y$ and $x = y$, the morphism $\text{homOfLE}(h) : x \to y$ is an isomorphism in the corresponding preorder category.

CategoryTheory.homOfLE_comp_eqToHom theorem

{a b c : X} (hab : a ≤ b) (hbc : b = c) : homOfLE hab ≫ eqToHom hbc = homOfLE (hab.trans (le_of_eq hbc))

Full source

@[simp, reassoc]
lemma homOfLE_comp_eqToHom {a b c : X} (hab : a ≤ b) (hbc : b = c) :
    homOfLEhomOfLE hab ≫ eqToHom hbc = homOfLE (hab.trans (le_of_eq hbc)) :=
  rfl

Composition of Inequality and Equality Morphisms in Preorder Categories

Informal description

Let $(X, \leq)$ be a preorder, viewed as a category where there is a morphism $x \to y$ if and only if $x \leq y$. For any elements $a, b, c \in X$ with $a \leq b$ and $b = c$, the composition of the inequality-induced morphism $a \leq b$ with the equality-induced morphism $b = c$ equals the morphism induced by the composite inequality $a \leq c$. In symbols: $$\text{homOfLE}(a \leq b) \circ \text{eqToHom}(b = c) = \text{homOfLE}(a \leq c)$$

CategoryTheory.eqToHom_comp_homOfLE theorem

{a b c : X} (hab : a = b) (hbc : b ≤ c) : eqToHom hab ≫ homOfLE hbc = homOfLE ((le_of_eq hab).trans hbc)

Full source

@[simp, reassoc]
lemma eqToHom_comp_homOfLE {a b c : X} (hab : a = b) (hbc : b ≤ c) :
    eqToHomeqToHom hab ≫ homOfLE hbc = homOfLE ((le_of_eq hab).trans hbc) :=
  rfl

Composition of Equality and Inequality Morphisms in Preorder Categories

Informal description

Let $(X, \leq)$ be a preorder, viewed as a category where there is a morphism $x \to y$ if and only if $x \leq y$. For any elements $a, b, c \in X$ with $a = b$ and $b \leq c$, the composition of the equality-induced morphism $\text{eqToHom}(a = b)$ with the inequality-induced morphism $\text{homOfLE}(b \leq c)$ equals the morphism induced by the composite inequality $a \leq c$. In symbols: $$\text{eqToHom}(a = b) \circ \text{homOfLE}(b \leq c) = \text{homOfLE}(a \leq c)$$

CategoryTheory.homOfLE_op_comp_eqToHom theorem

 {a b c : X} (hab : b ≤ a) (hbc : op b = op c) :
  (homOfLE hab).op ≫ eqToHom hbc = (homOfLE ((le_of_eq (op_injective hbc.symm)).trans hab)).op

Full source

@[simp, reassoc]
lemma homOfLE_op_comp_eqToHom {a b c : X} (hab : b ≤ a) (hbc : op b = op c) :
    (homOfLE hab).op ≫ eqToHom hbc = (homOfLE ((le_of_eq (op_injective hbc.symm)).trans hab)).op :=
  rfl

Composition of Opposite Inequality and Equality Morphisms in Preorder Categories

Informal description

Let $(X, \leq)$ be a preorder, viewed as a category where there is a morphism $x \to y$ if and only if $x \leq y$. For any elements $a, b, c \in X$ such that $b \leq a$ and $\mathrm{op}\, b = \mathrm{op}\, c$ in the opposite category $X^{\mathrm{op}}$, the composition of the opposite morphism $(b \leq a)^{\mathrm{op}}$ with the equality-induced morphism $\mathrm{eqToHom}\, (\mathrm{op}\, b = \mathrm{op}\, c)$ equals the opposite morphism induced by the composite inequality $(b = c) \leq (b \leq a)$. In symbols: $$(b \leq a)^{\mathrm{op}} \circ \mathrm{eqToHom}\, (\mathrm{op}\, b = \mathrm{op}\, c) = \big((b = c) \leq (b \leq a)\big)^{\mathrm{op}}$$

CategoryTheory.eqToHom_comp_homOfLE_op theorem

 {a b c : X} (hab : op a = op b) (hbc : c ≤ b) :
  eqToHom hab ≫ (homOfLE hbc).op = (homOfLE (hbc.trans (le_of_eq (op_injective hab.symm)))).op

Full source

@[simp, reassoc]
lemma eqToHom_comp_homOfLE_op {a b c : X} (hab : op a = op b) (hbc : c ≤ b) :
    eqToHomeqToHom hab ≫ (homOfLE hbc).op = (homOfLE (hbc.trans (le_of_eq (op_injective hab.symm)))).op :=
  rfl

Composition of Equality and Opposite Inequality Morphisms in Preorder Categories

Informal description

Let $X$ be a preorder category, and let $a, b, c \in X$ such that $\mathrm{op}\, a = \mathrm{op}\, b$ and $c \leq b$. Then the composition of the equality-induced morphism $\mathrm{eqToHom}\, \mathrm{hab}$ with the opposite of the inequality-induced morphism $(\mathrm{homOfLE}\, \mathrm{hbc}).\mathrm{op}$ is equal to the opposite of the morphism induced by the inequality $c \leq b$ followed by the equality $a = b$, i.e., \[ \mathrm{eqToHom}\, \mathrm{hab} \circ (\mathrm{homOfLE}\, \mathrm{hbc}).\mathrm{op} = (\mathrm{homOfLE}\, (hbc \circ \mathrm{le\_of\_eq}\, (\mathrm{op\_injective}\, \mathrm{hab.symm}))).\mathrm{op}. \]

CategoryTheory.opHomOfLE definition

{x y : Xᵒᵖ} (h : unop x ≤ unop y) : y ⟶ x

Full source

/-- Construct a morphism in the opposite of a preorder category from an inequality. -/
def opHomOfLE {x y : Xᵒᵖ} (h : unop x ≤ unop y) : y ⟶ x :=
  (homOfLE h).op

Morphism in opposite preorder category from inequality

Informal description

Given a preorder $(X, \leq)$ and elements $x, y$ in the opposite category $X^{\mathrm{op}}$ with $\mathrm{unop}\, x \leq \mathrm{unop}\, y$, the function constructs a morphism $y \to x$ in $X^{\mathrm{op}}$ by taking the opposite of the corresponding morphism in $X$.

CategoryTheory.le_of_op_hom theorem

{x y : Xᵒᵖ} (h : x ⟶ y) : unop y ≤ unop x

Full source

theorem le_of_op_hom {x y : Xᵒᵖ} (h : x ⟶ y) : unop y ≤ unop x :=
  h.unop.le

Inequality from Opposite Preorder Morphism

Informal description

For any elements $x, y$ in the opposite preorder category $X^{\mathrm{op}}$, if there exists a morphism $h \colon x \to y$ in $X^{\mathrm{op}}$, then $\mathrm{unop}\, y \leq \mathrm{unop}\, x$ in the original preorder $X$.

CategoryTheory.uniqueToTop instance

[OrderTop X] {x : X} : Unique (x ⟶ ⊤)

Full source

instance uniqueToTop [OrderTop X] {x : X} : Unique (x ⟶ ⊤) where
  default := homOfLE le_top
  uniq := fun a => by rfl

Unique Morphism to Top Element in Preorder Category

Informal description

For any preorder $X$ with a top element $\top$ and any element $x \in X$, there is exactly one morphism from $x$ to $\top$ in the associated category structure.

CategoryTheory.uniqueFromBot instance

[OrderBot X] {x : X} : Unique (⊥ ⟶ x)

Full source

instance uniqueFromBot [OrderBot X] {x : X} : Unique (⊥⊥ ⟶ x) where
  default := homOfLE bot_le
  uniq := fun a => by rfl

Unique Morphism from Bottom Element in Preorder Category

Informal description

For any preorder $X$ with a bottom element $\bot$ and any element $x \in X$, there is exactly one morphism from $\bot$ to $x$ in the associated category structure.

CategoryTheory.orderDualEquivalence definition

: Xᵒᵈ ≌ Xᵒᵖ

Full source

/-- The equivalence of categories from the order dual of a preordered type `X`
to the opposite category of the preorder `X`. -/
@[simps]
def orderDualEquivalence : XᵒᵈXᵒᵈ ≌ Xᵒᵖ where
  functor :=
    { obj := fun x => op (OrderDual.ofDual x)
      map := fun f => (homOfLE (leOfHom f)).op }
  inverse :=
    { obj := fun x => OrderDual.toDual x.unop
      map := fun f => (homOfLE (leOfHom f.unop)) }
  unitIso := Iso.refl _
  counitIso := Iso.refl _

Equivalence between order dual and opposite category of a preorder

Informal description

The equivalence of categories between the order dual $X^{\text{op}}$ of a preordered type $X$ and the opposite category $X^{\text{op}}$ of the preorder $X$. The functor maps an element $x$ in $X^{\text{op}}$ to its corresponding element in $X^{\text{op}}$ via the order dual construction, and morphisms are translated accordingly. The inverse functor reverses this process. The unit and counit isomorphisms are both identity isomorphisms.

Monotone.functor definition

{f : X → Y} (h : Monotone f) : X ⥤ Y

Full source

/-- A monotone function between preorders induces a functor between the associated categories.
-/
def Monotone.functor {f : X → Y} (h : Monotone f) : X ⥤ Y where
  obj := f
  map g := CategoryTheory.homOfLE (h g.le)

Functor induced by a monotone function between preorders

Informal description

Given a monotone function $f \colon X \to Y$ between preorders, the functor `Monotone.functor` associated to $f$ maps each object $x \in X$ to $f(x) \in Y$, and each morphism $x \to y$ (which exists if and only if $x \leq y$) to the morphism $f(x) \to f(y)$ (which exists since $f$ is monotone and thus $f(x) \leq f(y)$).

Monotone.functor_obj theorem

{f : X → Y} (h : Monotone f) : h.functor.obj = f

Full source

@[simp]
theorem Monotone.functor_obj {f : X → Y} (h : Monotone f) : h.functor.obj = f :=
  rfl

Object Mapping of Functor Induced by Monotone Function

Informal description

Given a monotone function $f \colon X \to Y$ between preorders, the object mapping of the associated functor `h.functor` coincides with $f$, i.e., for any object $x \in X$, we have $h.functor.obj(x) = f(x)$.

instFullFunctor instance

(f : X ↪o Y) : f.monotone.functor.Full

Full source

instance (f : X ↪o Y) : f.monotone.functor.Full where
  map_surjective h := ⟨homOfLE (f.map_rel_iff.1 h.le), rfl⟩

Fullness of the Functor Induced by an Order Embedding

Informal description

For any order embedding $f \colon X \hookrightarrow Y$ between preorders, the induced functor $f.\text{monotone}.\text{functor} \colon X \to Y$ is full. That is, for any objects $x, y \in X$, every morphism $f(x) \to f(y)$ in $Y$ is the image of some morphism $x \to y$ in $X$ under the functor.

OrderIso.equivalence definition

(e : X ≃o Y) : X ≌ Y

Full source

/-- The equivalence of categories `X ≌ Y` induced by `e : X ≃o Y`. -/
@[simps]
def OrderIso.equivalence (e : X ≃o Y) : X ≌ Y where
  functor := e.monotone.functor
  inverse := e.symm.monotone.functor
  unitIso := NatIso.ofComponents (fun _ ↦ eqToIso (by simp))
  counitIso := NatIso.ofComponents (fun _ ↦ eqToIso (by simp))

Equivalence of categories induced by an order isomorphism

Informal description

Given an order isomorphism $e : X \simeq_o Y$ between preorders $X$ and $Y$, the equivalence of categories $X \simeq Y$ is constructed where: - The functor is induced by the monotone function $e$, - The inverse functor is induced by the monotone function $e^{-1}$, - The unit and counit natural isomorphisms are identity isomorphisms (since $e$ and $e^{-1}$ are inverses).

CategoryTheory.Functor.monotone theorem

(f : X ⥤ Y) : Monotone f.obj

Full source

/-- A functor between preorder categories is monotone.
-/
@[mono]
theorem Functor.monotone (f : X ⥤ Y) : Monotone f.obj := fun _ _ hxy => (f.map hxy.hom).le

Monotonicity of Functors Between Preorder Categories

Informal description

For any functor $f \colon X \to Y$ between preorders viewed as categories, the object function $f.\text{obj}$ is monotone. That is, if $x \leq y$ in $X$, then $f.\text{obj}(x) \leq f.\text{obj}(y)$ in $Y$.

CategoryTheory.Iso.to_eq theorem

{x y : X} (f : x ≅ y) : x = y

Full source

theorem Iso.to_eq {x y : X} (f : x ≅ y) : x = y :=
  le_antisymm f.hom.le f.inv.le

Isomorphism Implies Equality in Preorder Categories

Informal description

For any objects $x$ and $y$ in a preorder category $X$, if there exists an isomorphism $f \colon x \cong y$, then $x = y$.

CategoryTheory.Equivalence.toOrderIso definition

(e : X ≌ Y) : X ≃o Y

Full source

/-- A categorical equivalence between partial orders is just an order isomorphism.
-/
def Equivalence.toOrderIso (e : X ≌ Y) : X ≃o Y where
  toFun := e.functor.obj
  invFun := e.inverse.obj
  left_inv a := (e.unitIso.app a).to_eq.symm
  right_inv b := (e.counitIso.app b).to_eq
  map_rel_iff' {a a'} :=
    ⟨fun h =>
      ((Equivalence.unit e).app a ≫ e.inverse.map h.hom ≫ (Equivalence.unitInv e).app a').le,
      fun h : a ≤ a' => (e.functor.map h.hom).le⟩

Order isomorphism induced by a categorical equivalence

Informal description

Given an equivalence $e$ between two preorders $X$ and $Y$ viewed as categories, the function constructs an order isomorphism $X \simeq_o Y$ where: - The forward map is the object function of the equivalence's functor, $e.\text{functor}.\text{obj}$. - The inverse map is the object function of the equivalence's inverse functor, $e.\text{inverse}.\text{obj}$. - The isomorphism properties follow from the natural isomorphisms of the equivalence. - The order-preserving properties are derived from the functoriality and the equivalence structure.

CategoryTheory.Equivalence.toOrderIso_apply theorem

(e : X ≌ Y) (x : X) : e.toOrderIso x = e.functor.obj x

Full source

@[simp]
theorem Equivalence.toOrderIso_apply (e : X ≌ Y) (x : X) : e.toOrderIso x = e.functor.obj x :=
  rfl

Equivalence-Induced Order Isomorphism Maps Elements via Functor

Informal description

Given an equivalence $e$ between two preorders $X$ and $Y$ viewed as categories, the order isomorphism $e.\text{toOrderIso}$ evaluated at an element $x \in X$ is equal to the image of $x$ under the functor associated to $e$, i.e., $e.\text{toOrderIso}(x) = e.\text{functor}.\text{obj}(x)$.

CategoryTheory.Equivalence.toOrderIso_symm_apply theorem

(e : X ≌ Y) (y : Y) : e.toOrderIso.symm y = e.inverse.obj y

Full source

@[simp]
theorem Equivalence.toOrderIso_symm_apply (e : X ≌ Y) (y : Y) :
    e.toOrderIso.symm y = e.inverse.obj y :=
  rfl

Inverse of Equivalence-Induced Order Isomorphism Equals Inverse Functor Application

Informal description

Given an equivalence $e$ between two preorders $X$ and $Y$ viewed as categories, the inverse of the induced order isomorphism $e.\text{toOrderIso}$ evaluated at any element $y \in Y$ equals the image of $y$ under the inverse functor of $e$, i.e., $e.\text{toOrderIso}^{-1}(y) = e.\text{inverse}.\text{obj}(y)$.

PartialOrder.isIso_iff_eq theorem

{X : Type u} [PartialOrder X] {a b : X} (f : a ⟶ b) : IsIso f ↔ a = b

Full source

lemma PartialOrder.isIso_iff_eq {X : Type u} [PartialOrder X]
    {a b : X} (f : a ⟶ b) : IsIsoIsIso f ↔ a = b := by
  constructor
  · intro _
    exact (asIso f).to_eq
  · rintro rfl
    rw [Subsingleton.elim f (𝟙 _)]
    infer_instance

Isomorphism in Partial Order Categories Implies Equality

Informal description

For any partial order $(X, \leq)$ viewed as a category, a morphism $f \colon a \to b$ is an isomorphism if and only if $a = b$.

Main definitions