The category of distributive lattices #

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

This file defines DistLat, the category of distributive lattices.

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

source

def DistLat :

Type (u_1+1)

The category of distributive lattices.

Equations

DistLat = category_theory.bundled distrib_lattice

Instances for DistLat

source

@[protected, instance]

def DistLat.has_coe_to_sort :

has_coe_to_sort DistLat (Type u_1)

Equations

DistLat.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

@[protected, instance]

def DistLat.distrib_lattice (X : DistLat) :

distrib_lattice ↥X

Equations

X.distrib_lattice = X.str

source

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

DistLat

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

Equations

DistLat.of α = category_theory.bundled.of α

source

@[simp]

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

↥(DistLat.of α) = α

source

@[protected, instance]

def DistLat.inhabited :

inhabited DistLat

Equations

DistLat.inhabited = {default := DistLat.of punit (boolean_algebra.to_distrib_lattice punit)}

source

@[protected, instance]

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

category_theory.bundled_hom.parent_projection distrib_lattice.to_lattice

Equations

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

source

@[protected, instance]

def DistLat.large_category :

category_theory.large_category DistLat

source

@[protected, instance]

def DistLat.concrete_category :

category_theory.concrete_category DistLat

source

@[protected, instance]

def DistLat.has_forget_to_Lat :

category_theory.has_forget₂ DistLat Lat

Equations

DistLat.has_forget_to_Lat = category_theory.bundled_hom.forget₂ lattice_hom distrib_lattice.to_lattice

source

@[simp]

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

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

source

@[simp]

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

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

source

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

α ≅ β

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

Equations

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

source

@[simp]

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

DistLat.dual.map ᾰ = ⇑lattice_hom.dual ᾰ

source

def DistLat.dual :

DistLat ⥤ DistLat

order_dual as a functor.

Equations

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

source

@[simp]

theorem DistLat.dual_obj (X : DistLat) :

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

source

@[simp]

theorem DistLat.dual_equiv_inverse :

DistLat.dual_equiv.inverse = DistLat.dual

source

def DistLat.dual_equiv :

DistLat ≌ DistLat

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

Equations

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

source

@[simp]

theorem DistLat.dual_equiv_functor :

DistLat.dual_equiv.functor = DistLat.dual

source

theorem DistLat_dual_comp_forget_to_Lat :

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