mathlib3 documentation

order.category.Lat

The category of lattices #

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

This defines Lat, the category of lattices.

Note that Lat doesn't correspond to the literature definition of [Lat] (https://ncatlab.org/nlab/show/Lat) as we don't require bottom or top elements. Instead, Lat corresponds to BddLat.

TODO #

The free functor from Lat to BddLat is X → with_top (with_bot X).

def Lat :

Type (u_1+1)

The category of lattices.

Equations

Lat = category_theory.bundled lattice

Instances for Lat

@[protected, instance]

def Lat.has_coe_to_sort :

has_coe_to_sort Lat (Type u_1)

Equations

Lat.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

@[protected, instance]

def Lat.lattice (X : Lat) :

Equations

X.lattice = X.str

def Lat.of (α : Type u_1) [lattice α] :

Construct a bundled Lat from a lattice.

Equations

Lat.of α = category_theory.bundled.of α

@[simp]

theorem Lat.coe_of (α : Type u_1) [lattice α] :

↥(Lat.of α) = α

@[protected, instance]

def Lat.inhabited :

Equations

Lat.inhabited = {default := Lat.of bool (generalized_coheyting_algebra.to_lattice bool)}

@[protected, instance]

def Lat.lattice_hom.category_theory.bundled_hom :

category_theory.bundled_hom lattice_hom

Equations

Lat.lattice_hom.category_theory.bundled_hom = {to_fun := λ (_x _x_1 : Type u_1) (_x_2 : lattice _x) (_x_3 : lattice _x_1), coe_fn, id := lattice_hom.id, comp := lattice_hom.comp, hom_ext := Lat.lattice_hom.category_theory.bundled_hom._proof_1, id_to_fun := Lat.lattice_hom.category_theory.bundled_hom._proof_2, comp_to_fun := Lat.lattice_hom.category_theory.bundled_hom._proof_3}

@[protected, instance]

def Lat.category_theory.large_category :

category_theory.large_category Lat

Equations

Lat.category_theory.large_category = category_theory.bundled_hom.category lattice_hom

@[protected, instance]

def Lat.category_theory.concrete_category :

category_theory.concrete_category Lat

Equations

Lat.category_theory.concrete_category = category_theory.bundled_hom.concrete_category lattice_hom

@[protected, instance]

def Lat.has_forget_to_PartOrd :

category_theory.has_forget₂ Lat PartOrd

Equations

Lat.has_forget_to_PartOrd = {forget₂ := {obj := λ (X : Lat), {α := ↥X, str := semilattice_inf.to_partial_order ↥X (lattice.to_semilattice_inf ↥X)}, map := λ (X Y : Lat) (f : X ⟶ Y), ↑f, map_id' := Lat.has_forget_to_PartOrd._proof_1, map_comp' := Lat.has_forget_to_PartOrd._proof_2}, forget_comp := Lat.has_forget_to_PartOrd._proof_3}

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

α ≅ β

Constructs an isomorphism of lattices from an order isomorphism between them.

Equations

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem Lat.dual_obj (X : Lat) :

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

@[simp]

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

Lat.dual.map ᾰ = ⇑lattice_hom.dual ᾰ

def Lat.dual :

order_dual as a functor.

Equations

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

@[simp]

theorem Lat.dual_equiv_inverse :

Lat.dual_equiv.inverse = Lat.dual

@[simp]

theorem Lat.dual_equiv_functor :

Lat.dual_equiv.functor = Lat.dual

def Lat.dual_equiv :

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

Equations

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

theorem Lat_dual_comp_forget_to_PartOrd :

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