mathlib3 documentation

order.category.CompleteLat

The category of complete lattices #

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

This file defines CompleteLat, the category of complete lattices.

def CompleteLat :

Type (u_1+1)

The category of complete lattices.

Equations

CompleteLat = category_theory.bundled complete_lattice

Instances for CompleteLat

@[protected, instance]

def CompleteLat.has_coe_to_sort :

has_coe_to_sort CompleteLat (Type u_1)

Equations

CompleteLat.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

@[protected, instance]

def CompleteLat.complete_lattice (X : CompleteLat) :

complete_lattice ↥X

Equations

X.complete_lattice = X.str

def CompleteLat.of (α : Type u_1) [complete_lattice α] :

Construct a bundled CompleteLat from a complete_lattice.

Equations

CompleteLat.of α = category_theory.bundled.of α

@[simp]

theorem CompleteLat.coe_of (α : Type u_1) [complete_lattice α] :

↥(CompleteLat.of α) = α

@[protected, instance]

def CompleteLat.inhabited :

inhabited CompleteLat

Equations

CompleteLat.inhabited = {default := CompleteLat.of punit (order.coframe.to_complete_lattice punit)}

@[protected, instance]

def CompleteLat.complete_lattice_hom.category_theory.bundled_hom :

category_theory.bundled_hom complete_lattice_hom

Equations

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

@[protected, instance]

def CompleteLat.category_theory.large_category :

category_theory.large_category CompleteLat

Equations

CompleteLat.category_theory.large_category = category_theory.bundled_hom.category complete_lattice_hom

@[protected, instance]

def CompleteLat.category_theory.concrete_category :

category_theory.concrete_category CompleteLat

Equations

CompleteLat.category_theory.concrete_category = category_theory.bundled_hom.concrete_category complete_lattice_hom

@[protected, instance]

def CompleteLat.has_forget_to_BddLat :

category_theory.has_forget₂ CompleteLat BddLat

Equations

CompleteLat.has_forget_to_BddLat = {forget₂ := {obj := λ (X : CompleteLat), BddLat.of ↥X, map := λ (X Y : CompleteLat), complete_lattice_hom.to_bounded_lattice_hom, map_id' := CompleteLat.has_forget_to_BddLat._proof_1, map_comp' := CompleteLat.has_forget_to_BddLat._proof_2}, forget_comp := CompleteLat.has_forget_to_BddLat._proof_3}

@[simp]

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

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

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

α ≅ β

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

Equations

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

@[simp]

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

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

def CompleteLat.dual :

CompleteLat ⥤ CompleteLat

order_dual as a functor.

Equations

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

@[simp]

theorem CompleteLat.dual_obj (X : CompleteLat) :

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

@[simp]

theorem CompleteLat.dual_map (X Y : CompleteLat) (ᾰ : complete_lattice_hom ↥X ↥Y) :

CompleteLat.dual.map ᾰ = ⇑complete_lattice_hom.dual ᾰ

@[simp]

theorem CompleteLat.dual_equiv_inverse :

CompleteLat.dual_equiv.inverse = CompleteLat.dual

@[simp]

theorem CompleteLat.dual_equiv_functor :

CompleteLat.dual_equiv.functor = CompleteLat.dual

def CompleteLat.dual_equiv :

CompleteLat ≌ CompleteLat

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

Equations

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

theorem CompleteLat_dual_comp_forget_to_BddLat :

CompleteLat.dual ⋙ category_theory.forget₂ CompleteLat BddLat = category_theory.forget₂ CompleteLat BddLat ⋙ BddLat.dual