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 ⊤
.
class
NonemptyFiniteLinearOrder
(α : Type u_1)
extends
Fintype
,
LinearOrder
,
PartialOrder
,
Min
,
Max
,
Ord
,
Preorder
,
LE
,
LT
:
Type u_1
A typeclass for nonempty finite linear orders.
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
- 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}
{β : NonemptyFinLinOrd}
(e : ↑α ≃o ↑β)
:
(NonemptyFinLinOrd.Iso.mk e).hom = ↑e
@[simp]
theorem
NonemptyFinLinOrd.Iso.mk_inv
{α : NonemptyFinLinOrd}
{β : 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.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.
Instances For
The generating arrow i ⟶ i+1
in the category Fin n
.
Equations
- i.hom_succ = CategoryTheory.homOfLE ⋯