CategoryTheory.le_of_op_hom
theorem CategoryTheory.le_of_op_hom : ∀ {X : Type u} [inst : Preorder X] {x y : Xᵒᵖ}, (x ⟶ y) → y.unop ≤ x.unop := by
sorry
This theorem states that, given a type `X` with a preorder structure, and two elements `x` and `y` of the opposite type of `X` (notated as `Xᵒᵖ`), if there exists a morphism from `x` to `y` in the category-theoretic sense, then the underlying element of `y` (retrieved by applying the `unop` function) is less than or equal to the underlying element of `x`. This is the opposite of the usual order because `Xᵒᵖ` reverses the order of `X`.
More concisely: Given a preordered type `X` and its opposite type `Xᵒᵖ`, if there is a morphism from `x : Xᵒᵖ` to `y : Xᵒᵖ`, then `unop y ≤ unop x` holds.
|
CategoryTheory.Functor.monotone
theorem CategoryTheory.Functor.monotone :
∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (f : CategoryTheory.Functor X Y),
Monotone f.obj
The theorem `CategoryTheory.Functor.monotone` states that for any two types `X` and `Y` with a preorder relation, any functor `f` from `X` to `Y` in Category Theory is monotone. In other words, if `a` and `b` are elements of `X` such that `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`. This theorem implies that functors preserve the order structure in the context of Preorder Categories.
More concisely: For any preorder (X, ≤) and any functor f from X to a preorder Y, if a ≤ b in X then f(a) ≤ f(b) in Y.
|
CategoryTheory.leOfHom
theorem CategoryTheory.leOfHom : ∀ {X : Type u} [inst : Preorder X] {x y : X}, (x ⟶ y) → x ≤ y
This theorem states that for any given types `X` in a preorder category, where `X` is equipped with a preorder relation, if there exists a morphism from `x` to `y` (written as `x ⟶ y`), then `x` is less than or equal to `y` (written as `x ≤ y`). In other words, in the context of a preorder category, the existence of a morphism from `x` to `y` guarantees that `x` is at most `y` according to the preorder relation.
More concisely: In a preorder category, the existence of a morphism from `x` to `y` implies `x ≤ y`.
|
CategoryTheory.Iso.to_eq
theorem CategoryTheory.Iso.to_eq : ∀ {X : Type u} [inst : PartialOrder X] {x y : X}, (x ≅ y) → x = y
This theorem states that for any type `X` in a partial order, if two elements `x` and `y` of `X` are isomorphic (denoted as `x ≅ y`), then `x` is equal to `y`. In other words, in the context of a partial order, isomorphic elements are necessarily equal.
More concisely: In a partial order, isomorphic elements are equal.
|