order.category.LinOrd - mathlib3 docs

source

def LinOrd :

Type (u_1+1)

The category of linear orders.

Equations

LinOrd = category_theory.bundled linear_order

Instances for LinOrd

source

@[protected, instance]

def LinOrd.linear_order.to_partial_order.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection linear_order.to_partial_order

Equations

LinOrd.linear_order.to_partial_order.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

@[protected, instance]

def LinOrd.large_category :

category_theory.large_category LinOrd

source

@[protected, instance]

def LinOrd.concrete_category :

category_theory.concrete_category LinOrd

source

@[protected, instance]

def LinOrd.has_coe_to_sort :

has_coe_to_sort LinOrd (Type u_1)

Equations

LinOrd.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

def LinOrd.of (α : Type u_1) [linear_order α] :

LinOrd

Construct a bundled LinOrd from the underlying type and typeclass.

Equations

LinOrd.of α = category_theory.bundled.of α

source

@[simp]

theorem LinOrd.coe_of (α : Type u_1) [linear_order α] :

↥(LinOrd.of α) = α

source

@[protected, instance]

def LinOrd.inhabited :

inhabited LinOrd

Equations

LinOrd.inhabited = {default := LinOrd.of punit punit.linear_order}

source

@[protected, instance]

def LinOrd.linear_order (α : LinOrd) :

linear_order ↥α

Equations

α.linear_order = α.str

source

@[protected, instance]

def LinOrd.has_forget_to_Lat :

category_theory.has_forget₂ LinOrd Lat

Equations

LinOrd.has_forget_to_Lat = {forget₂ := {obj := λ (X : LinOrd), Lat.of ↥X, map := λ (X Y : LinOrd) (f : X ⟶ Y), order_hom_class.to_lattice_hom ↥X ↥Y f, map_id' := LinOrd.has_forget_to_Lat._proof_1, map_comp' := LinOrd.has_forget_to_Lat._proof_2}, forget_comp := LinOrd.has_forget_to_Lat._proof_3}

source

@[simp]

theorem LinOrd.iso.mk_hom {α β : LinOrd} (e : ↥α ≃o ↥β) :

(LinOrd.iso.mk e).hom = ↑e

source

@[simp]

theorem LinOrd.iso.mk_inv {α β : LinOrd} (e : ↥α ≃o ↥β) :

(LinOrd.iso.mk e).inv = ↑(e.symm)

source

def LinOrd.iso.mk {α β : LinOrd} (e : ↥α ≃o ↥β) :

α ≅ β

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

Equations

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

source

@[simp]

theorem LinOrd.dual_map (X Y : LinOrd) (ᾰ : ↥X →o ↥Y) :

LinOrd.dual.map ᾰ = ⇑order_hom.dual ᾰ

source

@[simp]

theorem LinOrd.dual_obj (X : LinOrd) :

LinOrd.dual.obj X = LinOrd.of (↥X)ᵒᵈ

source

def LinOrd.dual :

LinOrd ⥤ LinOrd

order_dual as a functor.

Equations

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

source

@[simp]

theorem LinOrd.dual_equiv_functor :

LinOrd.dual_equiv.functor = LinOrd.dual

source

def LinOrd.dual_equiv :

LinOrd ≌ LinOrd

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

Equations

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

source

@[simp]

theorem LinOrd.dual_equiv_inverse :

LinOrd.dual_equiv.inverse = LinOrd.dual

source

theorem LinOrd_dual_comp_forget_to_Lat :

LinOrd.dual ⋙ category_theory.forget₂ LinOrd Lat = category_theory.forget₂ LinOrd Lat ⋙ Lat.dual

mathlib3 documentation

Category of linear orders #