The category of distributive lattices #

This file defines DistribLattice, the category of distributive lattices.

Note that DistLat in the literature doesn't always correspond to DistribLattice as we don't require bottom or top elements. Instead, this DistLat corresponds to BoundedDistribLattice.

source

def DistribLattice :

Type (u_1+1)

The category of distributive lattices.

Equations

DistribLattice = category_theory.bundled distrib_lattice

Instances for DistribLattice

source

@[protected, instance]

def DistribLattice.has_coe_to_sort :

has_coe_to_sort DistribLattice (Type u_1)

Equations

DistribLattice.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

@[protected, instance]

def DistribLattice.distrib_lattice (X : DistribLattice) :

distrib_lattice ↥X

Equations

X.distrib_lattice = X.str

source

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

DistribLattice

Construct a bundled DistribLattice from a distrib_lattice underlying type and typeclass.

Equations

DistribLattice.of α = category_theory.bundled.of α

source

@[simp]

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

↥(DistribLattice.of α) = α

source

@[protected, instance]

def DistribLattice.inhabited :

inhabited DistribLattice

Equations

DistribLattice.inhabited = {default := DistribLattice.of punit coframe.to_distrib_lattice}

source

@[protected, instance]

def DistribLattice.distrib_lattice.to_lattice.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection distrib_lattice.to_lattice

Equations

DistribLattice.distrib_lattice.to_lattice.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

@[protected, instance]

def DistribLattice.large_category :

category_theory.large_category DistribLattice

source

@[protected, instance]

def DistribLattice.concrete_category :

category_theory.concrete_category DistribLattice

source

@[protected, instance]

def DistribLattice.has_forget_to_Lattice :

category_theory.has_forget₂ DistribLattice Lattice

Equations

DistribLattice.has_forget_to_Lattice = category_theory.bundled_hom.forget₂ lattice_hom distrib_lattice.to_lattice

source

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

α ≅ β

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

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem DistribLattice.dual_obj (X : DistribLattice) :

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

source

@[simp]

theorem DistribLattice.dual_map (X Y : DistribLattice) (ᾰ : lattice_hom ↥X ↥Y) :

DistribLattice.dual.map ᾰ = ⇑lattice_hom.dual ᾰ

source

def DistribLattice.dual :

DistribLattice ⥤ DistribLattice

order_dual as a functor.

Equations

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

source

@[simp]

theorem DistribLattice.dual_equiv_functor :

DistribLattice.dual_equiv.functor = DistribLattice.dual

source

@[simp]

theorem DistribLattice.dual_equiv_inverse :

DistribLattice.dual_equiv.inverse = DistribLattice.dual

source

def DistribLattice.dual_equiv :

DistribLattice ≌ DistribLattice

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

Equations

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

source

theorem DistribLattice_dual_comp_forget_to_Lattice :

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