mathlib3 documentation

order.category.FinBddDistLat

The category of finite bounded distributive lattices #

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

This file defines FinBddDistLat, the category of finite distributive lattices with bounded lattice homomorphisms.

structure FinBddDistLat :

Type (u_1+1)

to_BddDistLat : BddDistLat
is_fintype : fintype ↥(self.to_BddDistLat)

The category of finite distributive lattices with bounded lattice morphisms.

Instances for FinBddDistLat

@[protected, instance]

def FinBddDistLat.has_coe_to_sort :

has_coe_to_sort FinBddDistLat (Type u_1)

Equations

FinBddDistLat.has_coe_to_sort = {coe := λ (X : FinBddDistLat), ↥(X.to_BddDistLat)}

@[protected, instance]

def FinBddDistLat.distrib_lattice (X : FinBddDistLat) :

distrib_lattice ↥X

Equations

X.distrib_lattice = X.to_BddDistLat.to_DistLat.str

@[protected, instance]

def FinBddDistLat.bounded_order (X : FinBddDistLat) :

bounded_order ↥X

Equations

X.bounded_order = X.to_BddDistLat.is_bounded_order

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

Construct a bundled FinBddDistLat from a nonempty bounded_order distrib_lattice.

Equations

FinBddDistLat.of α = FinBddDistLat.mk (BddDistLat.mk {α := α, str := _inst_1})

def FinBddDistLat.of' (α : Type u_1) [distrib_lattice α] [fintype α] [nonempty α] :

Construct a bundled FinBddDistLat from a nonempty bounded_order distrib_lattice.

Equations

FinBddDistLat.of' α = FinBddDistLat.mk (BddDistLat.mk {α := α, str := _inst_1})

@[protected, instance]

def FinBddDistLat.inhabited :

inhabited FinBddDistLat

Equations

FinBddDistLat.inhabited = {default := FinBddDistLat.of punit punit.fintype}

@[protected, instance]

def FinBddDistLat.large_category :

category_theory.large_category FinBddDistLat

Equations

FinBddDistLat.large_category = category_theory.induced_category.category FinBddDistLat.to_BddDistLat

@[protected, instance]

def FinBddDistLat.concrete_category :

category_theory.concrete_category FinBddDistLat

Equations

FinBddDistLat.concrete_category = category_theory.induced_category.concrete_category FinBddDistLat.to_BddDistLat

@[protected, instance]

def FinBddDistLat.has_forget_to_BddDistLat :

category_theory.has_forget₂ FinBddDistLat BddDistLat

Equations

FinBddDistLat.has_forget_to_BddDistLat = category_theory.induced_category.has_forget₂ FinBddDistLat.to_BddDistLat

@[protected, instance]

def FinBddDistLat.has_forget_to_FinPartOrd :

category_theory.has_forget₂ FinBddDistLat FinPartOrd

Equations

FinBddDistLat.has_forget_to_FinPartOrd = {forget₂ := {obj := λ (X : FinBddDistLat), FinPartOrd.of ↥X, map := λ (X Y : FinBddDistLat) (f : X ⟶ Y), ↑((λ (this : bounded_lattice_hom ↥X ↥Y), this) f), map_id' := FinBddDistLat.has_forget_to_FinPartOrd._proof_1, map_comp' := FinBddDistLat.has_forget_to_FinPartOrd._proof_2}, forget_comp := FinBddDistLat.has_forget_to_FinPartOrd._proof_3}

@[simp]

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

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

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

α ≅ β

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

Equations

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

@[simp]

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

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

@[simp]

theorem FinBddDistLat.dual_map (X Y : FinBddDistLat) (ᾰ : bounded_lattice_hom ↥(X.to_BddDistLat.to_BddLat) ↥(Y.to_BddDistLat.to_BddLat)) :

FinBddDistLat.dual.map ᾰ = ⇑bounded_lattice_hom.dual ᾰ

@[simp]

theorem FinBddDistLat.dual_obj (X : FinBddDistLat) :

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

def FinBddDistLat.dual :

FinBddDistLat ⥤ FinBddDistLat

order_dual as a functor.

Equations

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

def FinBddDistLat.dual_equiv :

FinBddDistLat ≌ FinBddDistLat

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

Equations

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

@[simp]

theorem FinBddDistLat.dual_equiv_functor :

FinBddDistLat.dual_equiv.functor = FinBddDistLat.dual

@[simp]

theorem FinBddDistLat.dual_equiv_inverse :

FinBddDistLat.dual_equiv.inverse = FinBddDistLat.dual

theorem FinBddDistLat_dual_comp_forget_to_BddDistLat :

FinBddDistLat.dual ⋙ category_theory.forget₂ FinBddDistLat BddDistLat = category_theory.forget₂ FinBddDistLat BddDistLat ⋙ BddDistLat.dual