mathlib3 documentation

order.category.NonemptyFinLinOrd

Nonempty finite linear orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ⊤.

source
@[class]
structure nonempty_fin_lin_ord (α : Type u_1) :
Type u_1

A typeclass for nonempty finite linear orders.

Instances of this typeclass
Instances of other typeclasses for nonempty_fin_lin_ord
  • nonempty_fin_lin_ord.has_sizeof_inst
source
@[protected, instance]
def nonempty_fin_lin_ord.to_bounded_order (α : Type u_1) [nonempty_fin_lin_ord α] :
bounded_order α
Equations
source
@[protected, instance]
def punit.nonempty_fin_lin_ord  :
nonempty_fin_lin_ord punit
Equations
source
@[protected, instance]
def fin.nonempty_fin_lin_ord (n : ℕ) :
nonempty_fin_lin_ord (fin (n + 1))
Equations
source
@[protected, instance]
def ulift.nonempty_fin_lin_ord (α : Type u) [nonempty_fin_lin_ord α] :
nonempty_fin_lin_ord (ulift α)
Equations
source
@[protected, instance]
def order_dual.nonempty_fin_lin_ord (α : Type u_1) [nonempty_fin_lin_ord α] :
nonempty_fin_lin_ord αᵒᵈ
Equations
source
def NonemptyFinLinOrd  :
Type (u_1+1)

The category of nonempty finite linear orders.

Equations
Instances for NonemptyFinLinOrd
source
@[protected, instance]
def NonemptyFinLinOrd.nonempty_fin_lin_ord.to_linear_order.category_theory.bundled_hom.parent_projection  :
category_theory.bundled_hom.parent_projection nonempty_fin_lin_ord.to_linear_order
Equations
source
@[protected, instance]
def NonemptyFinLinOrd.concrete_category  :
category_theory.concrete_category NonemptyFinLinOrd
source
@[protected, instance]
def NonemptyFinLinOrd.large_category  :
category_theory.large_category NonemptyFinLinOrd
source
@[protected, instance]
def NonemptyFinLinOrd.has_coe_to_sort  :
has_coe_to_sort NonemptyFinLinOrd (Type u_1)
Equations
source
def NonemptyFinLinOrd.of (α : Type u_1) [nonempty_fin_lin_ord α] :
NonemptyFinLinOrd

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations
source
@[simp]
theorem NonemptyFinLinOrd.coe_of (α : Type u_1) [nonempty_fin_lin_ord α] :
↥(NonemptyFinLinOrd.of α) = α
source
@[protected, instance]
def NonemptyFinLinOrd.inhabited  :
inhabited NonemptyFinLinOrd
Equations
source
@[protected, instance]
def NonemptyFinLinOrd.nonempty_fin_lin_ord (α : NonemptyFinLinOrd) :
nonempty_fin_lin_ord ↥α
Equations
source
@[protected, instance]
def NonemptyFinLinOrd.has_forget_to_LinOrd  :
category_theory.has_forget₂ NonemptyFinLinOrd LinOrd
Equations
source
@[protected, instance]
def NonemptyFinLinOrd.has_forget_to_FinPartOrd  :
category_theory.has_forget₂ NonemptyFinLinOrd FinPartOrd
Equations
source
@[simp]
theorem NonemptyFinLinOrd.iso.mk_inv {α β : NonemptyFinLinOrd} (e : ↥α ≃o ↥β) :
(NonemptyFinLinOrd.iso.mk e).inv = ↑(e.symm)
source
def NonemptyFinLinOrd.iso.mk {α β : NonemptyFinLinOrd} (e : ↥α ≃o ↥β) :
α ≅ β

Constructs an equivalence between nonempty finite linear orders from an order isomorphism between them.

Equations
source
@[simp]
theorem NonemptyFinLinOrd.iso.mk_hom {α β : NonemptyFinLinOrd} (e : ↥α ≃o ↥β) :
(NonemptyFinLinOrd.iso.mk e).hom = ↑e
source
@[simp]
theorem NonemptyFinLinOrd.dual_obj (X : NonemptyFinLinOrd) :
NonemptyFinLinOrd.dual.obj X = NonemptyFinLinOrd.of (↥X)ᵒᵈ
source
@[simp]
theorem NonemptyFinLinOrd.dual_map (X Y : NonemptyFinLinOrd) (ᾰ : ↥X →o ↥Y) :
NonemptyFinLinOrd.dual.map ᾰ = ⇑order_hom.dual ᾰ
source
def NonemptyFinLinOrd.dual  :
NonemptyFinLinOrd ⥤ NonemptyFinLinOrd

order_dual as a functor.

Equations
source
def NonemptyFinLinOrd.dual_equiv  :
NonemptyFinLinOrd ≌ NonemptyFinLinOrd

The equivalence between NonemptyFinLinOrd and itself induced by order_dual both ways.

Equations
source
@[simp]
theorem NonemptyFinLinOrd.dual_equiv_functor  :
NonemptyFinLinOrd.dual_equiv.functor = NonemptyFinLinOrd.dual
source
@[simp]
theorem NonemptyFinLinOrd.dual_equiv_inverse  :
NonemptyFinLinOrd.dual_equiv.inverse = NonemptyFinLinOrd.dual
source
theorem NonemptyFinLinOrd.mono_iff_injective {A B : NonemptyFinLinOrd} (f : A ⟶ B) :
category_theory.mono f ↔ function.injective ⇑f
source
theorem NonemptyFinLinOrd.epi_iff_surjective {A B : NonemptyFinLinOrd} (f : A ⟶ B) :
category_theory.epi f ↔ function.surjective ⇑f
source
@[protected, instance]
def NonemptyFinLinOrd.category_theory.split_epi_category  :
category_theory.split_epi_category NonemptyFinLinOrd
Equations
source
@[protected, instance]
def NonemptyFinLinOrd.category_theory.limits.has_strong_epi_mono_factorisations  :
category_theory.limits.has_strong_epi_mono_factorisations NonemptyFinLinOrd
source
theorem NonemptyFinLinOrd_dual_comp_forget_to_LinOrd  :
NonemptyFinLinOrd.dual ⋙ category_theory.forget₂ NonemptyFinLinOrd LinOrd = category_theory.forget₂ NonemptyFinLinOrd LinOrd ⋙ LinOrd.dual
source
def NonemptyFinLinOrd_dual_comp_forget_to_FinPartOrd  :
NonemptyFinLinOrd.dual ⋙ category_theory.forget₂ NonemptyFinLinOrd FinPartOrd ≅ category_theory.forget₂ NonemptyFinLinOrd FinPartOrd ⋙ FinPartOrd.dual

The forgetful functor NonemptyFinLinOrd ⥤ FinPartOrd and order_dual commute.

Equations