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

source

structure NonemptyFinLinOrdextends LinOrd :

Type (u_1 + 1)

The category of nonempty finite linear orders.

carrier : Type u_1
str : LinearOrder ↑self.toLinOrd
nonempty : Nonempty ↑self.toLinOrd
fintype : Fintype ↑self.toLinOrd

Instances For

source

instance NonemptyFinLinOrd.instCoeSortType :

CoeSort NonemptyFinLinOrd (Type u_1)

Equations

source

instance NonemptyFinLinOrd.instLargeCategory :

CategoryTheory.LargeCategory NonemptyFinLinOrd

Equations

source

instance NonemptyFinLinOrd.instConcreteCategoryOrderHomCarrier :

CategoryTheory.ConcreteCategory NonemptyFinLinOrd fun (x1 x2 : NonemptyFinLinOrd) => ↑x1.toLinOrd →o ↑x2.toLinOrd

Equations

source

instance NonemptyFinLinOrd.instBoundedOrderCarrier (X : NonemptyFinLinOrd) :

BoundedOrder ↑X.toLinOrd

Equations

source

@[reducible, inline]

abbrev NonemptyFinLinOrd.of (α : Type u_1) [Nonempty α] [Fintype α] [LinearOrder α] :

NonemptyFinLinOrd

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations

Instances For

source

theorem NonemptyFinLinOrd.coe_of (α : Type u_1) [Nonempty α] [Fintype α] [LinearOrder α] :

↑(of α).toLinOrd = α

source

@[reducible, inline]

abbrev NonemptyFinLinOrd.ofHom {X Y : Type u} [Nonempty X] [LinearOrder X] [Fintype X] [Nonempty Y] [LinearOrder Y] [Fintype Y] (f : X →o Y) :

of X ⟶ of Y

Typecheck a OrderHom as a morphism in NonemptyFinLinOrd.

Equations

Instances For

source

@[simp]

theorem NonemptyFinLinOrd.hom_id {X : NonemptyFinLinOrd} :

LinOrd.Hom.hom (CategoryTheory.CategoryStruct.id X) = OrderHom.id

source

theorem NonemptyFinLinOrd.id_apply (X : NonemptyFinLinOrd) (x : ↑X.toLinOrd) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

source

@[simp]

theorem NonemptyFinLinOrd.hom_comp {X Y Z : NonemptyFinLinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) :

LinOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (LinOrd.Hom.hom g).comp (LinOrd.Hom.hom f)

source

theorem NonemptyFinLinOrd.comp_apply {X Y Z : NonemptyFinLinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toLinOrd) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

source

theorem NonemptyFinLinOrd.hom_ext {X Y : NonemptyFinLinOrd} {f g : X ⟶ Y} (hf : LinOrd.Hom.hom f = LinOrd.Hom.hom g) :

f = g

source

theorem NonemptyFinLinOrd.hom_ext_iff {X Y : NonemptyFinLinOrd} {f g : X ⟶ Y} :

f = g ↔ LinOrd.Hom.hom f = LinOrd.Hom.hom g

source

@[simp]

theorem NonemptyFinLinOrd.hom_ofHom {X Y : Type u} [Nonempty X] [LinearOrder X] [Fintype X] [Nonempty Y] [LinearOrder Y] [Fintype Y] (f : X →o Y) :

LinOrd.Hom.hom (ofHom f) = f

source

@[simp]

theorem NonemptyFinLinOrd.ofHom_hom {X Y : NonemptyFinLinOrd} (f : X ⟶ Y) :

ofHom (LinOrd.Hom.hom f) = f

source

instance NonemptyFinLinOrd.instInhabited :

Inhabited NonemptyFinLinOrd

Equations

source

instance NonemptyFinLinOrd.hasForgetToLinOrd :

CategoryTheory.HasForget₂ NonemptyFinLinOrd LinOrd

Equations

source

instance NonemptyFinLinOrd.hasForgetToFinPartOrd :

CategoryTheory.HasForget₂ NonemptyFinLinOrd FinPartOrd

Equations

source

def NonemptyFinLinOrd.Iso.mk {α β : NonemptyFinLinOrd} (e : ↑α.toLinOrd ≃o ↑β.toLinOrd) :

α ≅ β

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

Equations

Instances For

source

@[simp]

theorem NonemptyFinLinOrd.Iso.mk_hom {α β : NonemptyFinLinOrd} (e : ↑α.toLinOrd ≃o ↑β.toLinOrd) :

(mk e).hom = ofHom ↑e

source

@[simp]

theorem NonemptyFinLinOrd.Iso.mk_inv {α β : NonemptyFinLinOrd} (e : ↑α.toLinOrd ≃o ↑β.toLinOrd) :

(mk e).inv = ofHom ↑e.symm

source

def NonemptyFinLinOrd.dual :

CategoryTheory.Functor NonemptyFinLinOrd NonemptyFinLinOrd

OrderDual as a functor.

Equations

Instances For

source

@[simp]

theorem NonemptyFinLinOrd.dual_map {X✝ Y✝ : NonemptyFinLinOrd} (f : X✝ ⟶ Y✝) :

dual.map f = ofHom (OrderHom.dual (LinOrd.Hom.hom f))

source

def NonemptyFinLinOrd.dualEquiv :

NonemptyFinLinOrd ≌ NonemptyFinLinOrd

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

Equations

Instances For

source

@[simp]

theorem NonemptyFinLinOrd.dualEquiv_functor :

dualEquiv.functor = dual

source

@[simp]

theorem NonemptyFinLinOrd.dualEquiv_inverse :

dualEquiv.inverse = dual

source

theorem NonemptyFinLinOrd.mono_iff_injective {A B : NonemptyFinLinOrd} (f : A ⟶ B) :

CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)

source

theorem NonemptyFinLinOrd.epi_iff_surjective {A B : NonemptyFinLinOrd} (f : A ⟶ B) :

CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)

source

instance NonemptyFinLinOrd.instSplitEpiCategory :

CategoryTheory.SplitEpiCategory NonemptyFinLinOrd

source

instance NonemptyFinLinOrd.instHasStrongEpiMonoFactorisations :

CategoryTheory.Limits.HasStrongEpiMonoFactorisations NonemptyFinLinOrd

source

theorem nonemptyFinLinOrd_dual_comp_forget_to_linOrd :

NonemptyFinLinOrd.dual.comp (CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd) = (CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd).comp LinOrd.dual

source

def nonemptyFinLinOrdDualCompForgetToFinPartOrd :

NonemptyFinLinOrd.dual.comp (CategoryTheory.forget₂ NonemptyFinLinOrd FinPartOrd) ≅ (CategoryTheory.forget₂ NonemptyFinLinOrd FinPartOrd).comp FinPartOrd.dual

The forgetful functor NonemptyFinLinOrd ⥤ FinPartOrd and OrderDual commute.

Equations

Instances For

source

def Fin.hom_succ {n : ℕ} (i : Fin n) :

i.castSucc ⟶ i.succ

The generating arrow i ⟶ i+1 in the category Fin n

Equations

Instances For

Documentation

Mathlib.Order.Category.NonemptyFinLinOrd

Nonempty finite linear orders #