Nonempty finite linear orders #
This defines NonemptyFinLinOrd
, the category of nonempty finite linear
orders with monotone maps. This is the index category for simplicial objects.
Note: NonemptyFinLinOrd
is not a subcategory of FinBddDistLat
because its morphisms do not
preserve ⊥
and ⊤
.
A typeclass for nonempty finite linear orders.
- elems : Finset α
- complete : ∀ (x : α), x ∈ Fintype.elems
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- min : α → α → α
- max : α → α → α
- compare : α → α → Ordering
- decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
- decidableEq : DecidableEq α
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
- Nonempty : Nonempty α
Instances
theorem
NonemptyFiniteLinearOrder.Nonempty
{α : Type u_1}
[self : NonemptyFiniteLinearOrder α]
:
Nonempty α
@[instance 100]
Equations
Equations
The category of nonempty finite linear orders.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- NonemptyFinLinOrd.instCoeSortType = CategoryTheory.Bundled.coeSort
@[simp]
theorem
NonemptyFinLinOrd.coe_of
(α : Type u_1)
[NonemptyFiniteLinearOrder α]
:
↑(NonemptyFinLinOrd.of α) = α
Equations
- NonemptyFinLinOrd.instInhabited = { default := NonemptyFinLinOrd.of PUnit.{?u.3 + 1} }
Equations
- α.instNonemptyFiniteLinearOrderα = α.str
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
NonemptyFinLinOrd.Iso.mk_inv
{α : NonemptyFinLinOrd}
{β : NonemptyFinLinOrd}
(e : ↑α ≃o ↑β)
:
(NonemptyFinLinOrd.Iso.mk e).inv = ↑e.symm
@[simp]
theorem
NonemptyFinLinOrd.Iso.mk_hom
{α : NonemptyFinLinOrd}
{β : NonemptyFinLinOrd}
(e : ↑α ≃o ↑β)
:
(NonemptyFinLinOrd.Iso.mk e).hom = ↑e
Constructs an equivalence between nonempty finite linear orders from an order isomorphism between them.
Equations
- NonemptyFinLinOrd.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
NonemptyFinLinOrd.dual_obj
(X : NonemptyFinLinOrd)
:
NonemptyFinLinOrd.dual.obj X = NonemptyFinLinOrd.of (↑X)ᵒᵈ
@[simp]
theorem
NonemptyFinLinOrd.dual_map :
∀ {X Y : NonemptyFinLinOrd} (a : ↑X →o ↑Y), NonemptyFinLinOrd.dual.map a = OrderHom.dual a
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
The equivalence between NonemptyFinLinOrd
and itself induced by OrderDual
both ways.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
NonemptyFinLinOrd.instFunLikeHomαNonemptyFiniteLinearOrder
{A : NonemptyFinLinOrd}
{B : NonemptyFinLinOrd}
:
instance
NonemptyFinLinOrd.instOrderHomClassHomαNonemptyFiniteLinearOrder
{A : NonemptyFinLinOrd}
{B : NonemptyFinLinOrd}
:
OrderHomClass (A ⟶ B) ↑A ↑B
Equations
- ⋯ = ⋯
theorem
NonemptyFinLinOrd.mono_iff_injective
{A : NonemptyFinLinOrd}
{B : NonemptyFinLinOrd}
(f : A ⟶ B)
:
theorem
NonemptyFinLinOrd.forget_map_apply
{A : NonemptyFinLinOrd}
{B : NonemptyFinLinOrd}
(f : A ⟶ B)
(a : ↑A)
:
(CategoryTheory.forget NonemptyFinLinOrd).map f a = f.toFun a
theorem
NonemptyFinLinOrd.epi_iff_surjective
{A : NonemptyFinLinOrd}
{B : NonemptyFinLinOrd}
(f : A ⟶ B)
:
The forgetful functor NonemptyFinLinOrd ⥤ FinPartOrd
and OrderDual
commute.
Equations
- One or more equations did not get rendered due to their size.