Skip to content

Commit

Permalink
feat(order/category/FinBoolAlg): The category of finite Boolean algeb…
Browse files Browse the repository at this point in the history
…ras (#12906)

Define `FinBoolAlg`, the category of finite Boolean algebras.
  • Loading branch information
YaelDillies committed Mar 25, 2022
1 parent 7ec1a31 commit 3dd8e4d
Show file tree
Hide file tree
Showing 5 changed files with 126 additions and 4 deletions.
5 changes: 4 additions & 1 deletion src/data/set/lattice.lean
Expand Up @@ -1223,7 +1223,7 @@ by simp_rw preimage_Union

@[simp] theorem preimage_sUnion {f : α → β} {s : set (set β)} :
f ⁻¹' (⋃₀ s) = (⋃ t ∈ s, f ⁻¹' t) :=
set.ext $ by simp [preimage]
by rw [sUnion_eq_bUnion, preimage_Union₂]

lemma preimage_Inter {f : α → β} {s : ι → set β} : f ⁻¹' (⋂ i, s i) = (⋂ i, f ⁻¹' s i) :=
by ext; simp
Expand All @@ -1232,6 +1232,9 @@ lemma preimage_Inter₂ {f : α → β} {s : Π i, κ i → set β} :
f ⁻¹' (⋂ i j, s i j) = ⋂ i j, f ⁻¹' s i j :=
by simp_rw preimage_Inter

@[simp] lemma preimage_sInter {f : α → β} {s : set (set β)} : f ⁻¹' (⋂₀ s) = ⋂ t ∈ s, f ⁻¹' t :=
by rw [sInter_eq_bInter, preimage_Inter₂]

@[simp] lemma bUnion_preimage_singleton (f : α → β) (s : set β) : (⋃ y ∈ s, f ⁻¹' {y}) = f ⁻¹' s :=
by rw [← preimage_Union₂, bUnion_of_singleton]

Expand Down
2 changes: 2 additions & 0 deletions src/order/category/BoolAlg.lean
Expand Up @@ -35,6 +35,8 @@ instance : inhabited BoolAlg := ⟨of punit⟩
/-- Turn a `BoolAlg` into a `BoundedDistribLattice` by forgetting its complement operation. -/
def to_BoundedDistribLattice (X : BoolAlg) : BoundedDistribLattice := BoundedDistribLattice.of X

@[simp] lemma coe_to_BoundedDistribLattice (X : BoolAlg) : ↥X.to_BoundedDistribLattice = ↥X := rfl

instance : large_category.{u} BoolAlg := induced_category.category to_BoundedDistribLattice
instance : concrete_category BoolAlg := induced_category.concrete_category to_BoundedDistribLattice

Expand Down
93 changes: 93 additions & 0 deletions src/order/category/FinBoolAlg.lean
@@ -0,0 +1,93 @@
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import order.category.BoolAlg
import order.category.FinPartialOrder
import order.hom.complete_lattice

/-!
# The category of finite boolean algebras
This file defines `FinBoolAlg`, the category of finite boolean algebras.
## TODO
Birkhoff's representation for finite Boolean algebras.
`Fintype_to_FinBoolAlg_op.left_op ⋙ FinBoolAlg.dual ≅ Fintype_to_FinBoolAlg_op.left_op`
`FinBoolAlg` is essentially small.
-/

universes u

open category_theory order_dual opposite

/-- The category of finite boolean algebras with bounded lattice morphisms. -/
structure FinBoolAlg :=
(to_BoolAlg : BoolAlg)
[is_fintype : fintype to_BoolAlg]

namespace FinBoolAlg

instance : has_coe_to_sort FinBoolAlg Type* := ⟨λ X, X.to_BoolAlg⟩
instance (X : FinBoolAlg) : boolean_algebra X := X.to_BoolAlg.str

attribute [instance] FinBoolAlg.is_fintype

@[simp] lemma coe_to_BoolAlg (X : FinBoolAlg) : ↥X.to_BoolAlg = ↥X := rfl

/-- Construct a bundled `FinBoolAlg` from `boolean_algebra` + `fintype`. -/
def of (α : Type*) [boolean_algebra α] [fintype α] : FinBoolAlg := ⟨⟨α⟩⟩

@[simp] lemma coe_of (α : Type*) [boolean_algebra α] [fintype α] : ↥(of α) = α := rfl

instance : inhabited FinBoolAlg := ⟨of punit⟩

instance large_category : large_category FinBoolAlg :=
induced_category.category FinBoolAlg.to_BoolAlg

instance concrete_category : concrete_category FinBoolAlg :=
induced_category.concrete_category FinBoolAlg.to_BoolAlg

instance has_forget_to_BoolAlg : has_forget₂ FinBoolAlg BoolAlg :=
induced_category.has_forget₂ FinBoolAlg.to_BoolAlg

instance forget_to_BoolAlg_full : full (forget₂ FinBoolAlg BoolAlg) := induced_category.full _
instance forget_to_BoolAlg_faithful : faithful (forget₂ FinBoolAlg BoolAlg) :=
induced_category.faithful _

@[simps] instance has_forget_to_FinPartialOrder : has_forget₂ FinBoolAlg FinPartialOrder :=
{ forget₂ := { obj := λ X, FinPartialOrder.of X, map := λ X Y f,
show order_hom X Y, from ↑(show bounded_lattice_hom X Y, from f) } }

instance forget_to_FinPartialOrder_faithful : faithful (forget₂ FinBoolAlg FinPartialOrder) :=
⟨λ X Y f g h, by { have := congr_arg (coe_fn : _ → X → Y) h, exact fun_like.coe_injective this }⟩

/-- Constructs an equivalence between finite Boolean algebras from an order isomorphism between
them. -/
@[simps] def iso.mk {α β : FinBoolAlg.{u}} (e : α ≃o β) : α ≅ β :=
{ hom := (e : bounded_lattice_hom α β),
inv := (e.symm : bounded_lattice_hom β α),
hom_inv_id' := by { ext, exact e.symm_apply_apply _ },
inv_hom_id' := by { ext, exact e.apply_symm_apply _ } }

/-- `order_dual` as a functor. -/
@[simps] def dual : FinBoolAlg ⥤ FinBoolAlg :=
{ obj := λ X, of (order_dual X), map := λ X Y, bounded_lattice_hom.dual }

/-- The equivalence between `FinBoolAlg` and itself induced by `order_dual` both ways. -/
@[simps functor inverse] def dual_equiv : FinBoolAlg ≌ FinBoolAlg :=
equivalence.mk dual dual
(nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
(nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)

end FinBoolAlg

/-- The powerset functor. `set` as a functor. -/
@[simps] def Fintype_to_FinBoolAlg_op : Fintype ⥤ FinBoolAlgᵒᵖ :=
{ obj := λ X, op $ FinBoolAlg.of (set X),
map := λ X Y f, quiver.hom.op $
(complete_lattice_hom.set_preimage f : bounded_lattice_hom (set Y) (set X)) }
5 changes: 3 additions & 2 deletions src/order/category/FinPartialOrder.lean
Expand Up @@ -29,12 +29,13 @@ structure FinPartialOrder :=
[is_fintype : fintype to_PartialOrder]

namespace FinPartialOrder
instance : has_coe_to_sort FinPartialOrder Type* := ⟨λ X, X.to_PartialOrder⟩

instance : has_coe_to_sort FinPartialOrder Type* := ⟨λ X, X.to_PartialOrder⟩
instance (X : FinPartialOrder) : partial_order X := X.to_PartialOrder.str

attribute [instance] FinPartialOrder.is_fintype

@[simp] lemma coe_to_PartialOrder (X : FinPartialOrder) : ↥X.to_PartialOrder = ↥X := rfl

/-- Construct a bundled `FinPartialOrder` from `fintype` + `partial_order`. -/
def of (α : Type*) [partial_order α] [fintype α] : FinPartialOrder := ⟨⟨α⟩⟩

Expand Down
25 changes: 24 additions & 1 deletion src/order/hom/complete_lattice.lean
Expand Up @@ -27,9 +27,13 @@ be satisfied by itself and all stricter types.
* `Inf_hom_class`
* `frame_hom_class`
* `complete_lattice_hom_class`
## Concrete homs
* `complete_lattice.set_preimage`: `set.preimage` as a complete lattice homomorphism.
-/

open function order_dual
open function order_dual set

variables {F α β γ δ : Type*} {ι : Sort*} {κ : ι → Sort*}

Expand Down Expand Up @@ -504,3 +508,22 @@ lattices. -/
right_inv := λ f, ext $ λ a, rfl }

end complete_lattice_hom

/-! ### Concrete homs -/

namespace complete_lattice_hom

/-- `set.preimage` as a complete lattice homomorphism. -/
def set_preimage (f : α → β) : complete_lattice_hom (set β) (set α) :=
{ to_fun := preimage f,
map_Sup' := λ s, preimage_sUnion.trans $ by simp only [set.Sup_eq_sUnion, set.sUnion_image],
map_Inf' := λ s, preimage_sInter.trans $ by simp only [set.Inf_eq_sInter, set.sInter_image] }

@[simp] lemma coe_set_preimage (f : α → β) : ⇑(set_preimage f) = preimage f := rfl
@[simp] lemma set_preimage_apply (f : α → β) (s : set β) : set_preimage f s = s.preimage f := rfl
@[simp] lemma set_preimage_id : set_preimage (id : α → α) = complete_lattice_hom.id _ := rfl
-- This lemma can't be `simp` because `g ∘ f` matches anything (`id ∘ f = f` synctatically)
lemma set_preimage_comp (g : β → γ) (f : α → β) :
set_preimage (g ∘ f) = (set_preimage f).comp (set_preimage g) := rfl

end complete_lattice_hom

0 comments on commit 3dd8e4d

Please sign in to comment.