mathlib3 documentation

order.category.BddOrd

The category of bounded orders #

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

This defines BddOrd, the category of bounded orders.

structure BddOrd :

Type (u_1+1)

to_PartOrd : PartOrd
is_bounded_order : bounded_order ↥(self.to_PartOrd)

The category of bounded orders with monotone functions.

Instances for BddOrd

@[protected, instance]

def BddOrd.has_coe_to_sort :

has_coe_to_sort BddOrd (Type u_1)

Equations

BddOrd.has_coe_to_sort = category_theory.induced_category.has_coe_to_sort BddOrd.to_PartOrd

@[protected, instance]

def BddOrd.partial_order (X : BddOrd) :

partial_order ↥X

Equations

X.partial_order = X.to_PartOrd.str

def BddOrd.of (α : Type u_1) [partial_order α] [bounded_order α] :

Construct a bundled BddOrd from a fintype partial_order.

Equations

BddOrd.of α = BddOrd.mk {α := α, str := _inst_1}

@[simp]

theorem BddOrd.coe_of (α : Type u_1) [partial_order α] [bounded_order α] :

↥(BddOrd.of α) = α

@[protected, instance]

def BddOrd.inhabited :

inhabited BddOrd

Equations

BddOrd.inhabited = {default := BddOrd.of punit boolean_algebra.to_bounded_order}

@[protected, instance]

def BddOrd.large_category :

category_theory.large_category BddOrd

Equations

BddOrd.large_category = {to_category_struct := {to_quiver := {hom := λ (X Y : BddOrd), bounded_order_hom ↥X ↥Y}, id := λ (X : BddOrd), bounded_order_hom.id ↥X, comp := λ (X Y Z : BddOrd) (f : X ⟶ Y) (g : Y ⟶ Z), bounded_order_hom.comp g f}, id_comp' := BddOrd.large_category._proof_1, comp_id' := BddOrd.large_category._proof_2, assoc' := BddOrd.large_category._proof_3}

@[protected, instance]

def BddOrd.concrete_category :

category_theory.concrete_category BddOrd

Equations

BddOrd.concrete_category = category_theory.concrete_category.mk {obj := coe_sort BddOrd.has_coe_to_sort, map := λ (X Y : BddOrd), coe_fn, map_id' := BddOrd.concrete_category._proof_1, map_comp' := BddOrd.concrete_category._proof_2}

@[protected, instance]

def BddOrd.has_forget_to_PartOrd :

category_theory.has_forget₂ BddOrd PartOrd

Equations

BddOrd.has_forget_to_PartOrd = {forget₂ := {obj := λ (X : BddOrd), X.to_PartOrd, map := λ (X Y : BddOrd), bounded_order_hom.to_order_hom, map_id' := BddOrd.has_forget_to_PartOrd._proof_1, map_comp' := BddOrd.has_forget_to_PartOrd._proof_2}, forget_comp := BddOrd.has_forget_to_PartOrd._proof_3}

@[protected, instance]

def BddOrd.has_forget_to_Bipointed :

category_theory.has_forget₂ BddOrd Bipointed

Equations

BddOrd.has_forget_to_Bipointed = {forget₂ := {obj := λ (X : BddOrd), {X := ↥X, to_prod := (⊥, ⊤)}, map := λ (X Y : BddOrd) (f : X ⟶ Y), {to_fun := ⇑f, map_fst := _, map_snd := _}, map_id' := BddOrd.has_forget_to_Bipointed._proof_3, map_comp' := BddOrd.has_forget_to_Bipointed._proof_4}, forget_comp := BddOrd.has_forget_to_Bipointed._proof_5}

@[simp]

theorem BddOrd.dual_obj (X : BddOrd) :

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

def BddOrd.dual :

BddOrd ⥤ BddOrd

order_dual as a functor.

Equations

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

@[simp]

theorem BddOrd.dual_map (X Y : BddOrd) (ᾰ : bounded_order_hom ↥X ↥Y) :

BddOrd.dual.map ᾰ = ⇑bounded_order_hom.dual ᾰ

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

α ≅ β

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

Equations

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem BddOrd.dual_equiv_inverse :

BddOrd.dual_equiv.inverse = BddOrd.dual

@[simp]

theorem BddOrd.dual_equiv_functor :

BddOrd.dual_equiv.functor = BddOrd.dual

def BddOrd.dual_equiv :

BddOrd ≌ BddOrd

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

Equations

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

theorem BddOrd_dual_comp_forget_to_PartOrd :

BddOrd.dual ⋙ category_theory.forget₂ BddOrd PartOrd = category_theory.forget₂ BddOrd PartOrd ⋙ PartOrd.dual

theorem BddOrd_dual_comp_forget_to_Bipointed :

BddOrd.dual ⋙ category_theory.forget₂ BddOrd Bipointed = category_theory.forget₂ BddOrd Bipointed ⋙ Bipointed.swap