order.category.BoundedDistribLattice

source

structure BoundedDistribLattice :

Type (u_1+1)

to_DistribLattice : DistribLattice
is_bounded_order : bounded_order ↥(self.to_DistribLattice)

The category of bounded distributive lattices with bounded lattice morphisms.

Instances for BoundedDistribLattice

source

@[protected, instance]

def BoundedDistribLattice.has_coe_to_sort :

has_coe_to_sort BoundedDistribLattice (Type u_1)

Equations

BoundedDistribLattice.has_coe_to_sort = {coe := λ (X : BoundedDistribLattice), ↥(X.to_DistribLattice)}

source

@[protected, instance]

def BoundedDistribLattice.distrib_lattice (X : BoundedDistribLattice) :

distrib_lattice ↥X

Equations

X.distrib_lattice = X.to_DistribLattice.str

source

def BoundedDistribLattice.of (α : Type u_1) [distrib_lattice α] [bounded_order α] :

BoundedDistribLattice

Construct a bundled BoundedDistribLattice from a bounded_order distrib_lattice.

Equations

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

source

@[simp]

theorem BoundedDistribLattice.coe_of (α : Type u_1) [distrib_lattice α] [bounded_order α] :

↥(BoundedDistribLattice.of α) = α

source

@[protected, instance]

def BoundedDistribLattice.inhabited :

inhabited BoundedDistribLattice

Equations

BoundedDistribLattice.inhabited = {default := BoundedDistribLattice.of punit complete_lattice.to_bounded_order}

source

def BoundedDistribLattice.to_BoundedLattice (X : BoundedDistribLattice) :

BoundedLattice

Turn a BoundedDistribLattice into a BoundedLattice by forgetting it is distributive.

Equations

X.to_BoundedLattice = BoundedLattice.of ↥X

source

@[simp]

theorem BoundedDistribLattice.coe_to_BoundedLattice (X : BoundedDistribLattice) :

↥(X.to_BoundedLattice) = ↥X

source

@[protected, instance]

def BoundedDistribLattice.category_theory.large_category :

category_theory.large_category BoundedDistribLattice

Equations

BoundedDistribLattice.category_theory.large_category = category_theory.induced_category.category BoundedDistribLattice.to_BoundedLattice

source

@[protected, instance]

def BoundedDistribLattice.category_theory.concrete_category :

category_theory.concrete_category BoundedDistribLattice

Equations

BoundedDistribLattice.category_theory.concrete_category = category_theory.induced_category.concrete_category BoundedDistribLattice.to_BoundedLattice

source

@[protected, instance]

def BoundedDistribLattice.has_forget_to_DistribLattice :

category_theory.has_forget₂ BoundedDistribLattice DistribLattice

Equations

BoundedDistribLattice.has_forget_to_DistribLattice = {forget₂ := {obj := λ (X : BoundedDistribLattice), {α := ↥X, str := X.distrib_lattice}, map := λ (X Y : BoundedDistribLattice), bounded_lattice_hom.to_lattice_hom, map_id' := BoundedDistribLattice.has_forget_to_DistribLattice._proof_1, map_comp' := BoundedDistribLattice.has_forget_to_DistribLattice._proof_2}, forget_comp := BoundedDistribLattice.has_forget_to_DistribLattice._proof_3}

source

@[protected, instance]

def BoundedDistribLattice.has_forget_to_BoundedLattice :

category_theory.has_forget₂ BoundedDistribLattice BoundedLattice

Equations

BoundedDistribLattice.has_forget_to_BoundedLattice = category_theory.induced_category.has_forget₂ BoundedDistribLattice.to_BoundedLattice

source

theorem BoundedDistribLattice.forget_BoundedLattice_Lattice_eq_forget_DistribLattice_Lattice :

category_theory.forget₂ BoundedDistribLattice BoundedLattice ⋙ category_theory.forget₂ BoundedLattice Lattice = category_theory.forget₂ BoundedDistribLattice DistribLattice ⋙ category_theory.forget₂ DistribLattice Lattice

source

@[simp]

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

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

source

@[simp]

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

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

source

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

α ≅ β

Constructs an equivalence between bounded distributive lattices from an order isomorphism between them.

Equations

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

source

def BoundedDistribLattice.dual :

BoundedDistribLattice ⥤ BoundedDistribLattice

order_dual as a functor.

Equations

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

source

@[simp]

theorem BoundedDistribLattice.dual_obj (X : BoundedDistribLattice) :

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

source

@[simp]

theorem BoundedDistribLattice.dual_map (X Y : BoundedDistribLattice) (ᾰ : bounded_lattice_hom ↥(X.to_BoundedLattice) ↥(Y.to_BoundedLattice)) :

BoundedDistribLattice.dual.map ᾰ = ⇑bounded_lattice_hom.dual ᾰ

source

@[simp]

theorem BoundedDistribLattice.dual_equiv_inverse :

BoundedDistribLattice.dual_equiv.inverse = BoundedDistribLattice.dual

source

@[simp]

theorem BoundedDistribLattice.dual_equiv_functor :

BoundedDistribLattice.dual_equiv.functor = BoundedDistribLattice.dual

source

def BoundedDistribLattice.dual_equiv :

BoundedDistribLattice ≌ BoundedDistribLattice

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

Equations

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

source

theorem BoundedDistribLattice_dual_comp_forget_to_DistribLattice :

BoundedDistribLattice.dual ⋙ category_theory.forget₂ BoundedDistribLattice DistribLattice = category_theory.forget₂ BoundedDistribLattice DistribLattice ⋙ DistribLattice.dual

mathlib documentation

The category of bounded distributive lattices #