order.category.BoolAlg - mathlib3 docs

source

def BoolAlg :

Type (u_1+1)

The category of boolean algebras.

Equations

BoolAlg = category_theory.bundled boolean_algebra

Instances for BoolAlg

source

@[protected, instance]

def BoolAlg.has_coe_to_sort :

has_coe_to_sort BoolAlg (Type u_1)

Equations

BoolAlg.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

@[protected, instance]

def BoolAlg.boolean_algebra (X : BoolAlg) :

boolean_algebra ↥X

Equations

X.boolean_algebra = X.str

source

def BoolAlg.of (α : Type u_1) [boolean_algebra α] :

BoolAlg

Construct a bundled BoolAlg from a boolean_algebra.

Equations

BoolAlg.of α = category_theory.bundled.of α

source

@[simp]

theorem BoolAlg.coe_of (α : Type u_1) [boolean_algebra α] :

↥(BoolAlg.of α) = α

source

@[protected, instance]

def BoolAlg.inhabited :

inhabited BoolAlg

Equations

BoolAlg.inhabited = {default := BoolAlg.of punit punit.boolean_algebra}

source

def BoolAlg.to_BddDistLat (X : BoolAlg) :

BddDistLat

Turn a BoolAlg into a BddDistLat by forgetting its complement operation.

Equations

X.to_BddDistLat = BddDistLat.of ↥X

source

@[simp]

theorem BoolAlg.coe_to_BddDistLat (X : BoolAlg) :

↥(X.to_BddDistLat) = ↥X

source

@[protected, instance]

def BoolAlg.category_theory.large_category :

category_theory.large_category BoolAlg

Equations

BoolAlg.category_theory.large_category = category_theory.induced_category.category BoolAlg.to_BddDistLat

source

@[protected, instance]

def BoolAlg.category_theory.concrete_category :

category_theory.concrete_category BoolAlg

Equations

BoolAlg.category_theory.concrete_category = category_theory.induced_category.concrete_category BoolAlg.to_BddDistLat

source

@[protected, instance]

def BoolAlg.has_forget_to_BddDistLat :

category_theory.has_forget₂ BoolAlg BddDistLat

Equations

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

source

@[simp]

theorem BoolAlg.has_forget_to_HeytAlg_forget₂_obj_str (X : BoolAlg) :

(category_theory.has_forget₂.forget₂.obj X).str = biheyting_algebra.to_heyting_algebra ↥X

source

@[protected, instance]

def BoolAlg.has_forget_to_HeytAlg :

category_theory.has_forget₂ BoolAlg HeytAlg

Equations

BoolAlg.has_forget_to_HeytAlg = {forget₂ := {obj := λ (X : BoolAlg), {α := ↥X, str := biheyting_algebra.to_heyting_algebra ↥X boolean_algebra.to_biheyting_algebra}, map := λ (X Y : BoolAlg) (f : X ⟶ Y), ↑((λ (this : bounded_lattice_hom ↥X ↥Y), this) f), map_id' := BoolAlg.has_forget_to_HeytAlg._proof_1, map_comp' := BoolAlg.has_forget_to_HeytAlg._proof_2}, forget_comp := BoolAlg.has_forget_to_HeytAlg._proof_3}

source

@[simp]

theorem BoolAlg.has_forget_to_HeytAlg_forget₂_obj_α (X : BoolAlg) :

↥(category_theory.has_forget₂.forget₂.obj X) = ↥X

source

@[simp]

theorem BoolAlg.has_forget_to_HeytAlg_forget₂_map (X Y : BoolAlg) (f : X ⟶ Y) :

category_theory.has_forget₂.forget₂.map f = ↑((λ (this : bounded_lattice_hom ↥X ↥Y), this) f)

source

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

α ≅ β

Constructs an equivalence between Boolean algebras from an order isomorphism between them.

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem BoolAlg.dual_obj (X : BoolAlg) :

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

source

@[simp]

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

BoolAlg.dual.map ᾰ = ⇑bounded_lattice_hom.dual ᾰ

source

def BoolAlg.dual :

BoolAlg ⥤ BoolAlg

order_dual as a functor.

Equations

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

source

@[simp]

theorem BoolAlg.dual_equiv_inverse :

BoolAlg.dual_equiv.inverse = BoolAlg.dual

source

def BoolAlg.dual_equiv :

BoolAlg ≌ BoolAlg

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

Equations

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

source

@[simp]

theorem BoolAlg.dual_equiv_functor :

BoolAlg.dual_equiv.functor = BoolAlg.dual

source

theorem BoolAlg_dual_comp_forget_to_BddDistLat :

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

mathlib3 documentation

The category of boolean algebras #