Skip to content

Commit ce06cb9

Browse files
YaelDilliesYaelDillies
committed
Boolean subalgebras
1 parent b5e1c18 commit ce06cb9

File tree

3 files changed

+322
-1
lines changed

3 files changed

+322
-1
lines changed

‎LeanCamCombi/GrowthInGroups/BooleanSubalgebra.lean‎

Lines changed: 321 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,321 @@
1+
/-
2+
Copyright (c) 2024 Yaël Dillies. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yaël Dillies
5+
-/
6+
import Mathlib.Order.Sublattice
7+
8+
/-!
9+
# Boolean subalgebras
10+
11+
This file defines boolean subalgebras.
12+
-/
13+
14+
open Function Set
15+
16+
variable {ι : Sort*} {α β γ : Type*} [BooleanAlgebra α] [BooleanAlgebra β] [BooleanAlgebra γ]
17+
18+
variable (α) in
19+
/-- A boolean subalgebra of a boolean algebra is a set containing the suprema, infima of any of its elements. -/
20+
structure BooleanSubalgebra extends Sublattice α where
21+
compl_mem' {a} : a ∈ carrier → aᶜ ∈ carrier
22+
bot_mem' : ⊥ ∈ carrier
23+
24+
namespace BooleanSubalgebra
25+
variable {L M : BooleanSubalgebra α} {f : BoundedLatticeHom α β} {s t : Set α} {a b : α}
26+
27+
initialize_simps_projections BooleanSubalgebra (carrier → coe)
28+
29+
instance instSetLike : SetLike (BooleanSubalgebra α) α where
30+
coe L := L.carrier
31+
coe_injective' L M h := by obtain ⟨⟨_, _⟩, _⟩ := L; congr
32+
33+
lemma coe_inj : (L : Set α) = M ↔ L = M := SetLike.coe_set_eq
34+
35+
@[simp] lemma supClosed (L : BooleanSubalgebra α) : SupClosed (L : Set α) := L.supClosed'
36+
@[simp] lemma infClosed (L : BooleanSubalgebra α) : InfClosed (L : Set α) := L.infClosed'
37+
38+
lemma compl_mem (ha : a ∈ L) : aᶜ ∈ L := L.compl_mem' ha
39+
@[simp] lemma compl_mem_iff : aᶜ ∈ L ↔ a ∈ L := ⟨fun ha ↦ by simpa using compl_mem ha, compl_mem⟩
40+
@[simp] lemma bot_mem : ⊥ ∈ L := L.bot_mem'
41+
@[simp] lemma top_mem : ⊤ ∈ L := by simpa using compl_mem L.bot_mem
42+
lemma sdiff_mem (ha : a ∈ L) (hb : b ∈ L) : a \ b ∈ L := by
43+
simpa [sdiff_eq] using L.infClosed ha (compl_mem hb)
44+
lemma himp_mem (ha : a ∈ L) (hb : b ∈ L) : a ⇨ b ∈ L := by
45+
simpa [himp_eq] using L.supClosed hb (compl_mem ha)
46+
47+
@[simp] lemma mem_carrier : a ∈ L.carrier ↔ a ∈ L := Iff.rfl
48+
@[simp] lemma mem_mk {L : Sublattice α} (h_compl h_bot) : a ∈ mk L h_compl h_bot ↔ a ∈ L := .rfl
49+
@[simp] lemma coe_mk (L : Sublattice α) (h_compl h_bot) : (mk L h_compl h_bot : Set α) = L := rfl
50+
@[simp] lemma mk_le_mk {L M : Sublattice α} (hL_compl hL_bot hM_compl hM_bot) :
51+
mk L hL_compl hL_bot ≤ mk M hM_compl hM_bot ↔ L ≤ M := .rfl
52+
@[simp] lemma mk_lt_mk{L M : Sublattice α} (hL_compl hL_bot hM_compl hM_bot) :
53+
mk L hL_compl hL_bot < mk M hM_compl hM_bot ↔ L < M := .rfl
54+
55+
/-- Copy of a boolean subalgebra with a new `carrier` equal to the old one. Useful to fix definitional
56+
equalities. -/
57+
protected def copy (L : BooleanSubalgebra α) (s : Set α) (hs : s = L) : BooleanSubalgebra α where
58+
toSublattice := L.toSublattice.copy s <| by subst hs; rfl
59+
compl_mem' := by subst hs; exact L.compl_mem'
60+
bot_mem' := by subst hs; exact L.bot_mem'
61+
62+
@[simp, norm_cast]
63+
lemma coe_copy (L : BooleanSubalgebra α) (s : Set α) (hs) : L.copy s hs = s := rfl
64+
65+
lemma copy_eq (L : BooleanSubalgebra α) (s : Set α) (hs) : L.copy s hs = L :=
66+
SetLike.coe_injective hs
67+
68+
/-- Two boolean subalgebras are equal if they have the same elements. -/
69+
lemma ext : (∀ a, a ∈ L ↔ a ∈ M) → L = M := SetLike.ext
70+
71+
/-- A boolean subalgebra of a lattice inherits a bottom element. -/
72+
instance instBotCoe : Bot L where bot := ⟨⊥, bot_mem⟩
73+
74+
/-- A boolean subalgebra of a lattice inherits a top element. -/
75+
instance instTopCoe : Top L where top := ⟨⊤, top_mem⟩
76+
77+
/-- A boolean subalgebra of a lattice inherits a supremum. -/
78+
instance instSupCoe : Sup L where sup a b := ⟨a ⊔ b, L.supClosed a.2 b.2⟩
79+
80+
/-- A boolean subalgebra of a lattice inherits an infimum. -/
81+
instance instInfCoe : Inf L where inf a b := ⟨a ⊓ b, L.infClosed a.2 b.2⟩
82+
83+
/-- A boolean subalgebra of a lattice inherits a complement. -/
84+
instance instHasComplCoe : HasCompl L where compl a := ⟨aᶜ, compl_mem a.2⟩
85+
86+
/-- A boolean subalgebra of a lattice inherits a difference. -/
87+
instance instSDiffCoe : SDiff L where sdiff a b := ⟨a \ b, sdiff_mem a.2 b.2⟩
88+
89+
/-- A boolean subalgebra of a lattice inherits a Heyting implication. -/
90+
instance instHImpCoe : HImp L where himp a b := ⟨a ⇨ b, himp_mem a.2 b.2⟩
91+
92+
@[simp, norm_cast] lemma coe_bot : (⊥ : L) = (⊥ : α) := rfl
93+
@[simp, norm_cast] lemma coe_top : (⊤ : L) = (⊤ : α) := rfl
94+
@[simp, norm_cast] lemma coe_sup (a b : L) : a ⊔ b = (a : α) ⊔ b := rfl
95+
@[simp, norm_cast] lemma coe_inf (a b : L) : a ⊓ b = (a : α) ⊓ b := rfl
96+
@[simp, norm_cast] lemma coe_compl (a : L) : aᶜ = (a : α)ᶜ := rfl
97+
@[simp, norm_cast] lemma coe_sdiff (a b : L) : a \ b = (a : α) \ b := rfl
98+
@[simp, norm_cast] lemma coe_himp (a b : L) : a ⇨ b = (a : α) ⇨ b := rfl
99+
100+
@[simp] lemma mk_bot : (⟨⊥, bot_mem⟩ : L) = ⊥ := rfl
101+
@[simp] lemma mk_top : (⟨⊤, top_mem⟩ : L) = ⊤ := rfl
102+
@[simp] lemma mk_sup_mk (a b : α) (ha hb) : (⟨a, ha⟩ ⊔ ⟨b, hb⟩ : L) = ⟨a ⊔ b, L.supClosed ha hb⟩ :=
103+
rfl
104+
@[simp] lemma mk_inf_mk (a b : α) (ha hb) : (⟨a, ha⟩ ⊓ ⟨b, hb⟩ : L) = ⟨a ⊓ b, L.infClosed ha hb⟩ :=
105+
rfl
106+
@[simp] lemma compl_mk (a : α) (ha) : (⟨a, ha⟩ : L)ᶜ = ⟨aᶜ, compl_mem ha⟩ := rfl
107+
@[simp] lemma mk_sdiff_mk (a b : α) (ha hb) : (⟨a, ha⟩ \ ⟨b, hb⟩ : L) = ⟨a \ b, sdiff_mem ha hb⟩ :=
108+
rfl
109+
@[simp] lemma mk_himp_mk (a b : α) (ha hb) : (⟨a, ha⟩ ⇨ ⟨b, hb⟩ : L) = ⟨a ⇨ b, himp_mem ha hb⟩ :=
110+
rfl
111+
112+
/-- A boolean subalgebra of a lattice inherits a boolean algebra structure. -/
113+
instance instBooleanAlgebraCoe (L : BooleanSubalgebra α) : BooleanAlgebra L :=
114+
Subtype.coe_injective.booleanAlgebra _ coe_sup coe_inf coe_top coe_bot coe_compl coe_sdiff
115+
coe_himp
116+
117+
/-- The natural lattice hom from a boolean subalgebra to the original lattice. -/
118+
def subtype (L : BooleanSubalgebra α) : BoundedLatticeHom L α where
119+
toFun := ((↑) : L → α)
120+
map_bot' := L.coe_bot
121+
map_top' := L.coe_top
122+
map_sup' := coe_sup
123+
map_inf' := coe_inf
124+
125+
@[simp, norm_cast] lemma coe_subtype (L : BooleanSubalgebra α) : L.subtype = ((↑) : L → α) := rfl
126+
lemma subtype_apply (L : BooleanSubalgebra α) (a : L) : L.subtype a = a := rfl
127+
128+
lemma subtype_injective (L : BooleanSubalgebra α) : Injective <| subtype L := Subtype.coe_injective
129+
130+
/-- The inclusion homomorphism from a boolean subalgebra `L` to a bigger boolean subalgebra `M`. -/
131+
def inclusion (h : L ≤ M) : BoundedLatticeHom L M where
132+
toFun := Set.inclusion h
133+
map_bot' := rfl
134+
map_top' := rfl
135+
map_sup' _ _ := rfl
136+
map_inf' _ _ := rfl
137+
138+
@[simp] lemma coe_inclusion (h : L ≤ M) : inclusion h = Set.inclusion h := rfl
139+
lemma inclusion_apply (h : L ≤ M) (a : L) : inclusion h a = Set.inclusion h a := rfl
140+
141+
lemma inclusion_injective (h : L ≤ M) : Injective <| inclusion h := Set.inclusion_injective h
142+
143+
@[simp] lemma inclusion_rfl (L : BooleanSubalgebra α) : inclusion le_rfl = BoundedLatticeHom.id L := rfl
144+
@[simp] lemma subtype_comp_inclusion (h : L ≤ M) : M.subtype.comp (inclusion h) = L.subtype := rfl
145+
146+
/-- The maximum boolean subalgebra of a lattice. -/
147+
instance instTop : Top (BooleanSubalgebra α) where
148+
top.carrier := univ
149+
top.bot_mem' := mem_univ _
150+
top.compl_mem' _ := mem_univ _
151+
top.supClosed' := supClosed_univ
152+
top.infClosed' := infClosed_univ
153+
154+
/-- The trivial boolean subalgebra of a lattice. -/
155+
instance instBot : Bot (BooleanSubalgebra α) where
156+
bot.carrier := {⊥, ⊤}
157+
bot.bot_mem' := by aesop
158+
bot.compl_mem' := by aesop
159+
bot.supClosed' _ := by aesop
160+
bot.infClosed' _ := by aesop
161+
162+
/-- The inf of two boolean subalgebras is their intersection. -/
163+
instance instInf : Inf (BooleanSubalgebra α) where
164+
inf L M := { carrier := L ∩ M
165+
bot_mem' := ⟨bot_mem, bot_mem⟩
166+
compl_mem' := fun ha ↦ ⟨compl_mem ha.1, compl_mem ha.2⟩
167+
supClosed' := L.supClosed.inter M.supClosed
168+
infClosed' := L.infClosed.inter M.infClosed }
169+
170+
/-- The inf of boolean subalgebras is their intersection. -/
171+
instance instInfSet : InfSet (BooleanSubalgebra α) where
172+
sInf S := { carrier := ⋂ L ∈ S, L
173+
bot_mem' := mem_iInter₂.2 fun _ _ ↦ bot_mem
174+
compl_mem' := fun ha ↦ mem_iInter₂.2 fun L hL ↦ compl_mem <| mem_iInter₂.1 ha L hL
175+
supClosed' := supClosed_sInter <| forall_mem_range.2 fun L ↦ supClosed_sInter <|
176+
forall_mem_range.2 fun _ ↦ L.supClosed
177+
infClosed' := infClosed_sInter <| forall_mem_range.2 fun L ↦ infClosed_sInter <|
178+
forall_mem_range.2 fun _ ↦ L.infClosed }
179+
180+
instance instInhabited : Inhabited (BooleanSubalgebra α) := ⟨⊥⟩
181+
182+
/-- The top boolean subalgebra is isomorphic to the lattice.
183+
184+
This is the boolean subalgebra version of `Equiv.Set.univ α`. -/
185+
def topEquiv : (⊤ : BooleanSubalgebra α) ≃o α where
186+
toEquiv := Equiv.Set.univ _
187+
map_rel_iff' := .rfl
188+
189+
@[simp, norm_cast] lemma coe_top' : (⊤ : BooleanSubalgebra α) = (univ : Set α) := rfl
190+
@[simp, norm_cast] lemma coe_bot' : (⊥ : BooleanSubalgebra α) = ({⊥, ⊤} : Set α) := rfl
191+
@[simp, norm_cast] lemma coe_inf' (L M : BooleanSubalgebra α) : L ⊓ M = (L : Set α) ∩ M := rfl
192+
193+
@[simp, norm_cast]
194+
lemma coe_sInf (S : Set (BooleanSubalgebra α)) : sInf S = ⋂ L ∈ S, (L : Set α) := rfl
195+
196+
@[simp, norm_cast]
197+
lemma coe_iInf (f : ι → BooleanSubalgebra α) : ⨅ i, f i = ⋂ i, (f i : Set α) := by simp [iInf]
198+
199+
@[simp, norm_cast] lemma coe_eq_univ : L = (univ : Set α) ↔ L = ⊤ := by rw [← coe_top', coe_inj]
200+
201+
@[simp] lemma mem_bot : a ∈ (⊥ : BooleanSubalgebra α) ↔ a = ⊥ ∨ a = ⊤ := .rfl
202+
@[simp] lemma mem_top : a ∈ (⊤ : BooleanSubalgebra α) := mem_univ _
203+
@[simp] lemma mem_inf : a ∈ L ⊓ M ↔ a ∈ L ∧ a ∈ M := .rfl
204+
@[simp] lemma mem_sInf {S : Set (BooleanSubalgebra α)} : a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L := by
205+
rw [← SetLike.mem_coe]; simp
206+
@[simp] lemma mem_iInf {f : ι → BooleanSubalgebra α} : a ∈ ⨅ i, f i ↔ ∀ i, a ∈ f i := by
207+
rw [← SetLike.mem_coe]; simp
208+
209+
/-- BooleanSubalgebras of a lattice form a complete lattice. -/
210+
instance instCompleteLattice : CompleteLattice (BooleanSubalgebra α) where
211+
bot := ⊥
212+
bot_le _S _a := by aesop
213+
top := ⊤
214+
le_top _S a _ha := mem_top
215+
inf := (· ⊓ ·)
216+
le_inf _L _M _N hM hN _a ha := ⟨hM ha, hN ha⟩
217+
inf_le_left _L _M _a := And.left
218+
inf_le_right _L _M _a := And.right
219+
__ := completeLatticeOfInf (BooleanSubalgebra α)
220+
fun _s ↦ IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf
221+
222+
instance [IsEmpty α] : Subsingleton (BooleanSubalgebra α) := SetLike.coe_injective.subsingleton
223+
instance [IsEmpty α] : Unique (BooleanSubalgebra α) := uniqueOfSubsingleton ⊤
224+
225+
/-- The preimage of a boolean subalgebra along a bounded lattice homomorphism. -/
226+
def comap (f : BoundedLatticeHom α β) (L : BooleanSubalgebra β) : BooleanSubalgebra α where
227+
carrier := f ⁻¹' L
228+
bot_mem' := by simp
229+
compl_mem' := by simp [map_compl']
230+
supClosed' := L.supClosed.preimage _
231+
infClosed' := L.infClosed.preimage _
232+
233+
@[simp, norm_cast] lemma coe_comap (L : BooleanSubalgebra β) (f : BoundedLatticeHom α β) : L.comap f = f ⁻¹' L :=
234+
rfl
235+
236+
@[simp] lemma mem_comap {L : BooleanSubalgebra β} : a ∈ L.comap f ↔ f a ∈ L := Iff.rfl
237+
238+
lemma comap_mono : Monotone (comap f) := fun _ _ ↦ preimage_mono
239+
240+
@[simp] lemma comap_id (L : BooleanSubalgebra α) : L.comap (BoundedLatticeHom.id _) = L := rfl
241+
242+
@[simp] lemma comap_comap (L : BooleanSubalgebra γ) (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) :
243+
(L.comap g).comap f = L.comap (g.comp f) := rfl
244+
245+
/-- The image of a boolean subalgebra along a monoid homomorphism is a boolean subalgebra. -/
246+
def map (f : BoundedLatticeHom α β) (L : BooleanSubalgebra α) : BooleanSubalgebra β where
247+
carrier := f '' L
248+
bot_mem' := ⟨⊥, by simp⟩
249+
compl_mem' := by rintro _ ⟨a, ha, rfl⟩; exact ⟨aᶜ, by simpa [map_compl']⟩
250+
supClosed' := L.supClosed.image f
251+
infClosed' := L.infClosed.image f
252+
253+
@[simp] lemma coe_map (f : BoundedLatticeHom α β) (L : BooleanSubalgebra α) : (L.map f : Set β) = f '' L := rfl
254+
@[simp] lemma mem_map {b : β} : b ∈ L.map f ↔ ∃ a ∈ L, f a = b := Iff.rfl
255+
256+
lemma mem_map_of_mem (f : BoundedLatticeHom α β) {a : α} : a ∈ L → f a ∈ L.map f := mem_image_of_mem f
257+
lemma apply_coe_mem_map (f : BoundedLatticeHom α β) (a : L) : f a ∈ L.map f := mem_map_of_mem f a.prop
258+
259+
lemma map_mono : Monotone (map f) := fun _ _ ↦ image_subset _
260+
261+
@[simp] lemma map_id : L.map (.id α) = L := SetLike.coe_injective <| image_id _
262+
263+
@[simp] lemma map_map (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) :
264+
(L.map f).map g = L.map (g.comp f) := SetLike.coe_injective <| image_image _ _ _
265+
266+
lemma mem_map_equiv {f : α ≃o β} {a : β} : a ∈ L.map f ↔ f.symm a ∈ L := Set.mem_image_equiv
267+
268+
lemma apply_mem_map_iff (hf : Injective f) : f a ∈ L.map f ↔ a ∈ L := hf.mem_set_image
269+
270+
lemma map_equiv_eq_comap_symm (f : α ≃o β) (L : BooleanSubalgebra α) :
271+
L.map f = L.comap (f.symm : BoundedLatticeHom β α) :=
272+
SetLike.coe_injective <| f.toEquiv.image_eq_preimage L
273+
274+
lemma comap_equiv_eq_map_symm (f : β ≃o α) (L : BooleanSubalgebra α) :
275+
L.comap f = L.map (f.symm : BoundedLatticeHom α β) := (map_equiv_eq_comap_symm f.symm L).symm
276+
277+
lemma map_symm_eq_iff_eq_map {M : BooleanSubalgebra β} {e : β ≃o α} :
278+
L.map ↑e.symm = M ↔ L = M.map ↑e := by
279+
simp_rw [← coe_inj]; exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm
280+
281+
lemma map_le_iff_le_comap {f : BoundedLatticeHom α β} {M : BooleanSubalgebra β} : L.map f ≤ M ↔ L ≤ M.comap f :=
282+
image_subset_iff
283+
284+
lemma gc_map_comap (f : BoundedLatticeHom α β) : GaloisConnection (map f) (comap f) :=
285+
fun _ _ ↦ map_le_iff_le_comap
286+
287+
@[simp] lemma map_bot (f : BoundedLatticeHom α β) : (⊥ : BooleanSubalgebra α).map f = ⊥ := (gc_map_comap f).l_bot
288+
289+
lemma map_sup (f : BoundedLatticeHom α β) (L M : BooleanSubalgebra α) : (L ⊔ M).map f = L.map f ⊔ M.map f :=
290+
(gc_map_comap f).l_sup
291+
292+
lemma map_iSup (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra α) : (⨆ i, L i).map f = ⨆ i, (L i).map f :=
293+
(gc_map_comap f).l_iSup
294+
295+
@[simp] lemma comap_top (f : BoundedLatticeHom α β) : (⊤ : BooleanSubalgebra β).comap f = ⊤ :=
296+
(gc_map_comap f).u_top
297+
298+
lemma comap_inf (L M : BooleanSubalgebra β) (f : BoundedLatticeHom α β) :
299+
(L ⊓ M).comap f = L.comap f ⊓ M.comap f := (gc_map_comap f).u_inf
300+
301+
lemma comap_iInf (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra β) :
302+
(⨅ i, L i).comap f = ⨅ i, (L i).comap f := (gc_map_comap f).u_iInf
303+
304+
lemma map_inf_le (L M : BooleanSubalgebra α) (f : BoundedLatticeHom α β) :
305+
map f (L ⊓ M) ≤ map f L ⊓ map f M := map_mono.map_inf_le _ _
306+
307+
lemma le_comap_sup (L M : BooleanSubalgebra β) (f : BoundedLatticeHom α β) :
308+
comap f L ⊔ comap f M ≤ comap f (L ⊔ M) := comap_mono.le_map_sup _ _
309+
310+
lemma le_comap_iSup (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra β) :
311+
⨆ i, (L i).comap f ≤ (⨆ i, L i).comap f := comap_mono.le_map_iSup
312+
313+
lemma map_inf (L M : BooleanSubalgebra α) (f : BoundedLatticeHom α β) (hf : Injective f) :
314+
map f (L ⊓ M) = map f L ⊓ map f M := by
315+
rw [← SetLike.coe_set_eq]
316+
simp [Set.image_inter hf]
317+
318+
lemma map_top (f : BoundedLatticeHom α β) (h : Surjective f) : BooleanSubalgebra.map f ⊤ = ⊤ :=
319+
SetLike.coe_injective <| by simp [h.range_eq]
320+
321+
end BooleanSubalgebra

‎LeanCamCombi/GrowthInGroups/Constructible.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Yaël Dillies
55
-/
66
import Mathlib.Topology.Compactness.Compact
77
import Mathlib.Topology.Separation.Basic
8-
import LeanCamCombi.GrowthInGroups.SubbooleanAlgebra
8+
import LeanCamCombi.GrowthInGroups.BooleanSubalgebra
99

1010
/-!
1111
# Constructible sets

‎LeanCamCombi/GrowthInGroups/SubbooleanAlgebra.lean‎

Whitespace-only changes.

0 commit comments

Comments
 (0)