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.
- min : α → α → α
- max : α → α → α
- decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- Nonempty : Nonempty α
Instances
@[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
- 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.
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.Iso.mk_hom
{α β : NonemptyFinLinOrd}
(e : ↑α ≃o ↑β)
:
(NonemptyFinLinOrd.Iso.mk e).hom = ↑e
@[simp]
theorem
NonemptyFinLinOrd.Iso.mk_inv
{α β : NonemptyFinLinOrd}
(e : ↑α ≃o ↑β)
:
(NonemptyFinLinOrd.Iso.mk e).inv = ↑e.symm
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
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
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
@[simp]
@[simp]
instance
NonemptyFinLinOrd.instOrderHomClassHomαNonemptyFiniteLinearOrder
{A B : NonemptyFinLinOrd}
:
OrderHomClass (A ⟶ B) ↑A ↑B
theorem
NonemptyFinLinOrd.forget_map_apply
{A B : NonemptyFinLinOrd}
(f : A ⟶ B)
(a : ↑A)
:
(CategoryTheory.forget NonemptyFinLinOrd).map f a = f.toFun a
The forgetful functor NonemptyFinLinOrd ⥤ FinPartOrd
and OrderDual
commute.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The generating arrow i ⟶ i+1
in the category Fin n
.
Equations
- i.hom_succ = CategoryTheory.homOfLE ⋯