order.category.NonemptyFinLinOrd

source

@[class]

structure nonempty_fin_lin_ord (α : Type u_1) :

Type u_1

to_fintype : fintype α
to_linear_order : linear_order α
nonempty : nonempty α . "apply_instance"

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

nonempty_fin_lin_ord.to_bounded_order α = fintype.to_bounded_order α

source

@[protected, instance]

def punit.nonempty_fin_lin_ord :

nonempty_fin_lin_ord punit

Equations

punit.nonempty_fin_lin_ord = {to_fintype := punit.fintype, to_linear_order := punit.linear_order, nonempty := _}

source

@[protected, instance]

def fin.nonempty_fin_lin_ord (n : ℕ) :

nonempty_fin_lin_ord (fin (n + 1))

Equations

fin.nonempty_fin_lin_ord n = {to_fintype := fin.fintype (n + 1), to_linear_order := fin.linear_order (n + 1), nonempty := _}

source

@[protected, instance]

def ulift.nonempty_fin_lin_ord (α : Type u) [nonempty_fin_lin_ord α] :

nonempty_fin_lin_ord (ulift α)

Equations

ulift.nonempty_fin_lin_ord α = {to_fintype := ulift.fintype α nonempty_fin_lin_ord.to_fintype, to_linear_order := {le := linear_order.le (linear_order.lift' ⇑equiv.ulift _), lt := linear_order.lt (linear_order.lift' ⇑equiv.ulift _), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift' ⇑equiv.ulift _), decidable_eq := linear_order.decidable_eq (linear_order.lift' ⇑equiv.ulift _), decidable_lt := linear_order.decidable_lt (linear_order.lift' ⇑equiv.ulift _), max := linear_order.max (linear_order.lift' ⇑equiv.ulift _), max_def := _, min := linear_order.min (linear_order.lift' ⇑equiv.ulift _), min_def := _}, nonempty := _}

source

@[protected, instance]

def order_dual.nonempty_fin_lin_ord (α : Type u_1) [nonempty_fin_lin_ord α] :

nonempty_fin_lin_ord αᵒᵈ

Equations

order_dual.nonempty_fin_lin_ord α = {to_fintype := {elems := fintype.elems αᵒᵈ (order_dual.fintype α), complete := _}, to_linear_order := order_dual.linear_order α nonempty_fin_lin_ord.to_linear_order, nonempty := _}

source

def NonemptyFinLinOrd :

Type (u_1+1)

The category of nonempty finite linear orders.

Equations

NonemptyFinLinOrd = category_theory.bundled nonempty_fin_lin_ord

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

NonemptyFinLinOrd.nonempty_fin_lin_ord.to_linear_order.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

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

NonemptyFinLinOrd.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

def NonemptyFinLinOrd.of (α : Type u_1) [nonempty_fin_lin_ord α] :

NonemptyFinLinOrd

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations

NonemptyFinLinOrd.of α = category_theory.bundled.of α

source

@[simp]

theorem NonemptyFinLinOrd.coe_of (α : Type u_1) [nonempty_fin_lin_ord α] :

↥(NonemptyFinLinOrd.of α) = α

source

@[protected, instance]

def NonemptyFinLinOrd.inhabited :

inhabited NonemptyFinLinOrd

Equations

NonemptyFinLinOrd.inhabited = {default := NonemptyFinLinOrd.of punit punit.nonempty_fin_lin_ord}

source

@[protected, instance]

def NonemptyFinLinOrd.nonempty_fin_lin_ord (α : NonemptyFinLinOrd) :

nonempty_fin_lin_ord ↥α

Equations

α.nonempty_fin_lin_ord = α.str

source

@[protected, instance]

def NonemptyFinLinOrd.has_forget_to_LinearOrder :

category_theory.has_forget₂ NonemptyFinLinOrd LinearOrder

Equations

NonemptyFinLinOrd.has_forget_to_LinearOrder = category_theory.bundled_hom.forget₂ (category_theory.bundled_hom.map_hom (category_theory.bundled_hom.map_hom order_hom partial_order.to_preorder) linear_order.to_partial_order) nonempty_fin_lin_ord.to_linear_order

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

NonemptyFinLinOrd.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}

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

NonemptyFinLinOrd.dual = {obj := λ (X : NonemptyFinLinOrd), NonemptyFinLinOrd.of (↥X)ᵒᵈ, map := λ (X Y : NonemptyFinLinOrd), ⇑order_hom.dual, map_id' := NonemptyFinLinOrd.dual._proof_1, map_comp' := NonemptyFinLinOrd.dual._proof_2}

source

def NonemptyFinLinOrd.dual_equiv :

NonemptyFinLinOrd ≌ NonemptyFinLinOrd

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

Equations

NonemptyFinLinOrd.dual_equiv = category_theory.equivalence.mk NonemptyFinLinOrd.dual NonemptyFinLinOrd.dual (category_theory.nat_iso.of_components (λ (X : NonemptyFinLinOrd), NonemptyFinLinOrd.iso.mk (order_iso.dual_dual ↥X)) NonemptyFinLinOrd.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : NonemptyFinLinOrd), NonemptyFinLinOrd.iso.mk (order_iso.dual_dual ↥X)) NonemptyFinLinOrd.dual_equiv._proof_2)

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_dual_comp_forget_to_LinearOrder :

NonemptyFinLinOrd.dual ⋙ category_theory.forget₂ NonemptyFinLinOrd LinearOrder = category_theory.forget₂ NonemptyFinLinOrd LinearOrder ⋙ LinearOrder.dual

mathlib documentation

Nonempty finite linear orders #