The category of Boolean algebras

This defines BoolAlg, the category of Boolean algebras.

structure BoolAlg : Type (u_1 + 1)

The category of Boolean algebras.

• of :: (
• carrier : Type u_1

  The underlying Boolean algebra.

• str : BooleanAlgebra ↑self
• )

instance BoolAlg.instCoeSortType : CoeSort BoolAlg (Type u_1)

structure BoolAlg.Hom (X Y : BoolAlg) : Type u

The type of morphisms in BoolAlg R.

• hom' : BoundedLatticeHom ↑X ↑Y

  The underlying BoundedLatticeHom.

theorem BoolAlg.Hom.ext {X Y : BoolAlg} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y

theorem BoolAlg.Hom.ext_iff {X Y : BoolAlg} {x y : X.Hom Y} : x = y ↔ x.hom' = y.hom'

instance BoolAlg.instCategory : CategoryTheory.Category.{u, u + 1} BoolAlg

instance BoolAlg.instConcreteCategoryBoundedLatticeHomCarrier : CategoryTheory.ConcreteCategory BoolAlg fun (x1 x2 : BoolAlg) => BoundedLatticeHom ↑x1 ↑x2

@[reducible, inline]

abbrev BoolAlg.Hom.hom {X Y : BoolAlg} (f : X.Hom Y) : BoundedLatticeHom ↑X ↑Y

Turn a morphism in BoolAlg back into a BoundedLatticeHom.

@[reducible, inline]

abbrev BoolAlg.ofHom {X Y : Type u} [BooleanAlgebra X] [BooleanAlgebra Y] (f : BoundedLatticeHom X Y) : { carrier := X, str := inst✝ } ⟶ { carrier := Y, str := inst✝¹ }

Typecheck a BoundedLatticeHom as a morphism in BoolAlg.

def BoolAlg.Hom.Simps.hom (X Y : BoolAlg) (f : X.Hom Y) : BoundedLatticeHom ↑X ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem BoolAlg.coe_id {X : BoolAlg} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem BoolAlg.coe_comp {X Y Z : BoolAlg} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem BoolAlg.forget_map {X Y : BoolAlg} (f : X ⟶ Y) : (CategoryTheory.forget BoolAlg).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem BoolAlg.ext {X Y : BoolAlg} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem BoolAlg.ext_iff {X Y : BoolAlg} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem BoolAlg.coe_of (X : Type u) [BooleanAlgebra X] : ↑{ carrier := X, str := inst✝ } = X

@[simp]

theorem BoolAlg.hom_id {X : BoolAlg} : Hom.hom (CategoryTheory.CategoryStruct.id X) = BoundedLatticeHom.id ↑X

theorem BoolAlg.id_apply (X : BoolAlg) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem BoolAlg.hom_comp {X Y Z : BoolAlg} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem BoolAlg.comp_apply {X Y Z : BoolAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem BoolAlg.hom_ext {X Y : BoolAlg} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem BoolAlg.hom_ext_iff {X Y : BoolAlg} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem BoolAlg.hom_ofHom {X Y : Type u} [BooleanAlgebra X] [BooleanAlgebra Y] (f : BoundedLatticeHom X Y) : Hom.hom (ofHom f) = f

@[simp]

theorem BoolAlg.ofHom_hom {X Y : BoolAlg} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem BoolAlg.ofHom_id {X : Type u} [BooleanAlgebra X] : ofHom (BoundedLatticeHom.id X) = CategoryTheory.CategoryStruct.id { carrier := X, str := inst✝ }

@[simp]

theorem BoolAlg.ofHom_comp {X Y Z : Type u} [BooleanAlgebra X] [BooleanAlgebra Y] [BooleanAlgebra Z] (f : BoundedLatticeHom X Y) (g : BoundedLatticeHom Y Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem BoolAlg.ofHom_apply {X Y : Type u} [BooleanAlgebra X] [BooleanAlgebra Y] (f : BoundedLatticeHom X Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem BoolAlg.inv_hom_apply {X Y : BoolAlg} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem BoolAlg.hom_inv_apply {X Y : BoolAlg} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

instance BoolAlg.instInhabited : Inhabited BoolAlg

def BoolAlg.toBddDistLat (X : BoolAlg) : BddDistLat

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

@[simp]

theorem BoolAlg.coe_toBddDistLat (X : BoolAlg) : ↑X.toBddDistLat.toDistLat = ↑X

instance BoolAlg.hasForgetToBddDistLat : CategoryTheory.HasForget₂ BoolAlg BddDistLat

instance BoolAlg.hasForgetToHeytAlg : CategoryTheory.HasForget₂ BoolAlg HeytAlg

@[simp]

theorem BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe (X : BoolAlg) : ↑(CategoryTheory.HasForget₂.forget₂.obj X) = ↑X

@[simp]

theorem BoolAlg.hasForgetToHeytAlg_forget₂_map {X Y : BoolAlg} (f : X ⟶ Y) : CategoryTheory.HasForget₂.forget₂.map f = HeytAlg.ofHom { toFun := ⇑(Hom.hom f), map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }

def BoolAlg.Iso.mk {α β : BoolAlg} (e : ↑α ≃o ↑β) : α ≅ β

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

@[simp]

theorem BoolAlg.Iso.mk_inv {α β : BoolAlg} (e : ↑α ≃o ↑β) : (mk e).inv = ofHom (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })

@[simp]

theorem BoolAlg.Iso.mk_hom {α β : BoolAlg} (e : ↑α ≃o ↑β) : (mk e).hom = ofHom (have __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })

def BoolAlg.dual : CategoryTheory.Functor BoolAlg BoolAlg

OrderDual as a functor.

@[simp]

theorem BoolAlg.dual_map {X✝ Y✝ : BoolAlg} (f : X✝ ⟶ Y✝) : dual.map f = ofHom (BoundedLatticeHom.dual (Hom.hom f))

def BoolAlg.dualEquiv : BoolAlg ≌ BoolAlg

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

@[simp]

theorem BoolAlg.dualEquiv_functor : dualEquiv.functor = dual

@[simp]

theorem BoolAlg.dualEquiv_inverse : dualEquiv.inverse = dual

theorem boolAlg_dual_comp_forget_to_bddDistLat : BoolAlg.dual.comp (CategoryTheory.forget₂ BoolAlg BddDistLat) = (CategoryTheory.forget₂ BoolAlg BddDistLat).comp BddDistLat.dual

def typeToBoolAlgOp : CategoryTheory.Functor (Type u) BoolAlgᵒᵖ

The powerset functor. Set as a contravariant functor.

@[simp]

theorem typeToBoolAlgOp_obj (X : Type u) : typeToBoolAlgOp.obj X = Opposite.op { carrier := Set X, str := Set.instBooleanAlgebra }

@[simp]

theorem typeToBoolAlgOp_map {X Y : Type u} (f : X ⟶ Y) : typeToBoolAlgOp.map f = (BoolAlg.ofHom (have __src := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })).op