Constructible set API

Author: YaelDillies

LeanCamCombi.lean

@@ -42,14 +42,18 @@ import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
+import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.Finite
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import LeanCamCombi.Mathlib.Order.Interval.Finset.Defs
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
+import LeanCamCombi.Mathlib.Order.SupClosed
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.Mathlib.RingTheory.Ideal.Span
+import LeanCamCombi.Mathlib.Topology.Defs.Induced
+import LeanCamCombi.Mathlib.Topology.Spectral.Hom
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.OrderShatter

LeanCamCombi/GrowthInGroups/BooleanSubalgebra.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Order.Sublattice
+import LeanCamCombi.Mathlib.Order.SupClosed
 
 /-!
 # Boolean subalgebras
@@ -13,16 +14,19 @@ This file defines boolean subalgebras.
 
 open Function Set
 
-variable {ι : Sort*} {α β γ : Type*} [BooleanAlgebra α] [BooleanAlgebra β] [BooleanAlgebra γ]
+variable {ι : Sort*} {α β γ : Type*}
 
 variable (α) in
-/-- A boolean subalgebra of a boolean algebra is a set containing the suprema, infima of any of its elements. -/
-structure BooleanSubalgebra extends Sublattice α where
+/-- A boolean subalgebra of a boolean algebra is a set containing the bottom and top elements, and
+closed under suprema, infima and complements. -/
+structure BooleanSubalgebra [BooleanAlgebra α] extends Sublattice α where
   compl_mem' {a} : a ∈ carrier → aᶜ ∈ carrier
   bot_mem' : ⊥ ∈ carrier
 
 namespace BooleanSubalgebra
-variable {L M : BooleanSubalgebra α} {f : BoundedLatticeHom α β} {s t : Set α} {a b : α}
+section BooleanAlgebra
+variable [BooleanAlgebra α] [BooleanAlgebra β] [BooleanAlgebra γ] {L M : BooleanSubalgebra α}
+  {f : BoundedLatticeHom α β} {s t : Set α} {a b : α}
 
 initialize_simps_projections BooleanSubalgebra (carrier → coe)
 
@@ -39,21 +43,23 @@ lemma compl_mem (ha : a ∈ L) : aᶜ ∈ L := L.compl_mem' ha
 @[simp] lemma compl_mem_iff : aᶜ ∈ L ↔ a ∈ L := ⟨fun ha ↦ by simpa using compl_mem ha, compl_mem⟩
 @[simp] lemma bot_mem : ⊥ ∈ L := L.bot_mem'
 @[simp] lemma top_mem : ⊤ ∈ L := by simpa using compl_mem L.bot_mem
+lemma sup_mem (ha : a ∈ L) (hb : b ∈ L) : a ⊔ b ∈ L := L.supClosed ha hb
+lemma inf_mem (ha : a ∈ L) (hb : b ∈ L) : a ⊓ b ∈ L := L.infClosed ha hb
 lemma sdiff_mem (ha : a ∈ L) (hb : b ∈ L) : a \ b ∈ L := by
   simpa [sdiff_eq] using L.infClosed ha (compl_mem hb)
 lemma himp_mem (ha : a ∈ L) (hb : b ∈ L) : a ⇨ b ∈ L := by
   simpa [himp_eq] using L.supClosed hb (compl_mem ha)
 
-@[simp] lemma mem_carrier : a ∈ L.carrier ↔ a ∈ L := Iff.rfl
+@[simp] lemma mem_carrier : a ∈ L.carrier ↔ a ∈ L := .rfl
 @[simp] lemma mem_mk {L : Sublattice α} (h_compl h_bot) : a ∈ mk L h_compl h_bot ↔ a ∈ L := .rfl
 @[simp] lemma coe_mk (L : Sublattice α) (h_compl h_bot) : (mk L h_compl h_bot : Set α) = L := rfl
 @[simp] lemma mk_le_mk {L M : Sublattice α} (hL_compl hL_bot hM_compl hM_bot) :
     mk L hL_compl hL_bot ≤ mk M hM_compl hM_bot ↔ L ≤ M := .rfl
 @[simp] lemma mk_lt_mk{L M : Sublattice α} (hL_compl hL_bot hM_compl hM_bot) :
     mk L hL_compl hL_bot < mk M hM_compl hM_bot ↔ L < M := .rfl
 
-/-- Copy of a boolean subalgebra with a new `carrier` equal to the old one. Useful to fix definitional
-equalities. -/
+/-- Copy of a boolean subalgebra with a new `carrier` equal to the old one. Useful to fix
+definitional equalities. -/
 protected def copy (L : BooleanSubalgebra α) (s : Set α) (hs : s = L) : BooleanSubalgebra α where
   toSublattice := L.toSublattice.copy s <| by subst hs; rfl
   compl_mem' := by subst hs; exact L.compl_mem'
@@ -140,7 +146,7 @@ lemma inclusion_apply (h : L ≤ M) (a : L) : inclusion h a = Set.inclusion h a
 
 lemma inclusion_injective (h : L ≤ M) : Injective <| inclusion h := Set.inclusion_injective h
 
-@[simp] lemma inclusion_rfl (L : BooleanSubalgebra α) : inclusion le_rfl = BoundedLatticeHom.id L := rfl
+@[simp] lemma inclusion_rfl (L : BooleanSubalgebra α) : inclusion le_rfl = .id L := rfl
 @[simp] lemma subtype_comp_inclusion (h : L ≤ M) : M.subtype.comp (inclusion h) = L.subtype := rfl
 
 /-- The maximum boolean subalgebra of a lattice. -/
@@ -230,17 +236,17 @@ def comap (f : BoundedLatticeHom α β) (L : BooleanSubalgebra β) : BooleanSuba
   supClosed' := L.supClosed.preimage _
   infClosed' := L.infClosed.preimage _
 
-@[simp, norm_cast] lemma coe_comap (L : BooleanSubalgebra β) (f : BoundedLatticeHom α β) : L.comap f = f ⁻¹' L :=
-  rfl
+@[simp, norm_cast]
+lemma coe_comap (L : BooleanSubalgebra β) (f : BoundedLatticeHom α β) : L.comap f = f ⁻¹' L := rfl
 
-@[simp] lemma mem_comap {L : BooleanSubalgebra β} : a ∈ L.comap f ↔ f a ∈ L := Iff.rfl
+@[simp] lemma mem_comap {L : BooleanSubalgebra β} : a ∈ L.comap f ↔ f a ∈ L := .rfl
 
 lemma comap_mono : Monotone (comap f) := fun _ _ ↦ preimage_mono
 
 @[simp] lemma comap_id (L : BooleanSubalgebra α) : L.comap (BoundedLatticeHom.id _) = L := rfl
 
-@[simp] lemma comap_comap (L : BooleanSubalgebra γ) (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) :
-    (L.comap g).comap f = L.comap (g.comp f) := rfl
+@[simp] lemma comap_comap (L : BooleanSubalgebra γ) (g : BoundedLatticeHom β γ)
+    (f : BoundedLatticeHom α β) : (L.comap g).comap f = L.comap (g.comp f) := rfl
 
 /-- The image of a boolean subalgebra along a monoid homomorphism is a boolean subalgebra. -/
 def map (f : BoundedLatticeHom α β) (L : BooleanSubalgebra α) : BooleanSubalgebra β where
@@ -250,11 +256,16 @@ def map (f : BoundedLatticeHom α β) (L : BooleanSubalgebra α) : BooleanSubalg
   supClosed' := L.supClosed.image f
   infClosed' := L.infClosed.image f
 
-@[simp] lemma coe_map (f : BoundedLatticeHom α β) (L : BooleanSubalgebra α) : (L.map f : Set β) = f '' L := rfl
-@[simp] lemma mem_map {b : β} : b ∈ L.map f ↔ ∃ a ∈ L, f a = b := Iff.rfl
+@[simp] lemma coe_map (f : BoundedLatticeHom α β) (L : BooleanSubalgebra α) :
+    (L.map f : Set β) = f '' L := rfl
+
+@[simp] lemma mem_map {b : β} : b ∈ L.map f ↔ ∃ a ∈ L, f a = b := .rfl
+
+lemma mem_map_of_mem (f : BoundedLatticeHom α β) {a : α} : a ∈ L → f a ∈ L.map f :=
+  mem_image_of_mem f
 
-lemma mem_map_of_mem (f : BoundedLatticeHom α β) {a : α} : a ∈ L → f a ∈ L.map f := mem_image_of_mem f
-lemma apply_coe_mem_map (f : BoundedLatticeHom α β) (a : L) : f a ∈ L.map f := mem_map_of_mem f a.prop
+lemma apply_coe_mem_map (f : BoundedLatticeHom α β) (a : L) : f a ∈ L.map f :=
+  mem_map_of_mem f a.prop
 
 lemma map_mono : Monotone (map f) := fun _ _ ↦ image_subset _
 
@@ -278,19 +289,20 @@ lemma map_symm_eq_iff_eq_map {M : BooleanSubalgebra β} {e : β ≃o α} :
     L.map ↑e.symm = M ↔ L = M.map ↑e := by
   simp_rw [← coe_inj]; exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm
 
-lemma map_le_iff_le_comap {f : BoundedLatticeHom α β} {M : BooleanSubalgebra β} : L.map f ≤ M ↔ L ≤ M.comap f :=
-  image_subset_iff
+lemma map_le_iff_le_comap {f : BoundedLatticeHom α β} {M : BooleanSubalgebra β} :
+    L.map f ≤ M ↔ L ≤ M.comap f := image_subset_iff
 
 lemma gc_map_comap (f : BoundedLatticeHom α β) : GaloisConnection (map f) (comap f) :=
   fun _ _ ↦ map_le_iff_le_comap
 
-@[simp] lemma map_bot (f : BoundedLatticeHom α β) : (⊥ : BooleanSubalgebra α).map f = ⊥ := (gc_map_comap f).l_bot
+@[simp] lemma map_bot (f : BoundedLatticeHom α β) : (⊥ : BooleanSubalgebra α).map f = ⊥ :=
+  (gc_map_comap f).l_bot
 
-lemma map_sup (f : BoundedLatticeHom α β) (L M : BooleanSubalgebra α) : (L ⊔ M).map f = L.map f ⊔ M.map f :=
-  (gc_map_comap f).l_sup
+lemma map_sup (f : BoundedLatticeHom α β) (L M : BooleanSubalgebra α) :
+    (L ⊔ M).map f = L.map f ⊔ M.map f := (gc_map_comap f).l_sup
 
-lemma map_iSup (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra α) : (⨆ i, L i).map f = ⨆ i, (L i).map f :=
-  (gc_map_comap f).l_iSup
+lemma map_iSup (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra α) :
+    (⨆ i, L i).map f = ⨆ i, (L i).map f := (gc_map_comap f).l_iSup
 
 @[simp] lemma comap_top (f : BoundedLatticeHom α β) : (⊤ : BooleanSubalgebra β).comap f = ⊤ :=
   (gc_map_comap f).u_top
@@ -318,4 +330,50 @@ lemma map_inf (L M : BooleanSubalgebra α) (f : BoundedLatticeHom α β) (hf : I
 lemma map_top (f : BoundedLatticeHom α β) (h : Surjective f) : BooleanSubalgebra.map f ⊤ = ⊤ :=
   SetLike.coe_injective <| by simp [h.range_eq]
 
+/-- The minimum boolean algebra containing a given set. -/
+def closure (s : Set α) : BooleanSubalgebra α := sInf {L | s ⊆ L}
+
+variable {s : Set α}
+
+lemma mem_closure {x : α} : x ∈ closure s ↔ ∀ ⦃L : BooleanSubalgebra α⦄, s ⊆ L → x ∈ L := mem_sInf
+
+@[aesop safe 20 apply (rule_sets := [SetLike])]
+lemma subset_closure : s ⊆ closure s := fun _ hx ↦ mem_closure.2 fun _ hK ↦ hK hx
+
+@[simp] lemma closure_le : closure s ≤ L ↔ s ⊆ L := ⟨subset_closure.trans, fun h ↦ sInf_le h⟩
+
+/-- An induction principle for closure membership. If `p` holds for `⊥` and all elements of `s`, and
+is preserved under suprema and complement, then `p` holds for all elements of the closure of `s`. -/
+@[elab_as_elim]
+lemma closure_bot_sup_induction {p : ∀ g ∈ closure s, Prop} (mem : ∀ x hx, p x (subset_closure hx))
+    (bot : p ⊥ bot_mem)
+    (sup : ∀ x hx y hy, p x hx → p y hy → p (x ⊔ y) (supClosed _ hx hy))
+    (compl : ∀ x hx, p x hx → p xᶜ (compl_mem hx)) {x} (hx : x ∈ closure s) : p x hx :=
+  have inf ⦃x hx y hy⦄ (hx' : p x hx) (hy' : p y hy) : p (x ⊓ y) (infClosed _ hx hy) := by
+    simpa using compl _ _ <| sup _ _ _ _ (compl _ _ hx') (compl _ _ hy')
+  let L : BooleanSubalgebra α :=
+    { carrier := { x | ∃ hx, p x hx }
+      supClosed' := fun _a ⟨_, ha⟩ _b ⟨_, hb⟩ ↦ ⟨_, sup _ _ _ _ ha hb⟩
+      infClosed' := fun _a ⟨_, ha⟩ _b ⟨_, hb⟩ ↦ ⟨_, inf ha hb⟩
+      bot_mem' := ⟨_, bot⟩
+      compl_mem' := fun ⟨_, hb⟩ ↦ ⟨_, compl _ _ hb⟩ }
+  closure_le (L := L).mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
+
+end BooleanAlgebra
+
+section CompleteBooleanAlgebra
+variable [CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {f : ι → α} {s : Set α}
+
+lemma iSup_mem [Finite ι] (hf : ∀ i, f i ∈ L) : ⨆ i, f i ∈ L := L.supClosed.iSup_mem bot_mem hf
+lemma iInf_mem [Finite ι] (hf : ∀ i, f i ∈ L) : ⨅ i, f i ∈ L := L.infClosed.iInf_mem top_mem hf
+lemma sSup_mem (hs : s.Finite) (hsL : s ⊆ L) : sSup s ∈ L := L.supClosed.sSup_mem hs bot_mem hsL
+lemma sInf_mem (hs : s.Finite) (hsL : s ⊆ L) : sInf s ∈ L := L.infClosed.sInf_mem hs top_mem hsL
+
+lemma biSup_mem {ι : Type*} {t : Set ι} {f : ι → α} (ht : t.Finite) (hf : ∀ i ∈ t, f i ∈ L) :
+    ⨆ i ∈ t, f i ∈ L := L.supClosed.biSup_mem ht bot_mem hf
+
+lemma biInf_mem {ι : Type*} {t : Set ι} {f : ι → α} (ht : t.Finite) (hf : ∀ i ∈ t, f i ∈ L) :
+    ⨅ i ∈ t, f i ∈ L := L.infClosed.biInf_mem ht top_mem hf
+
+end CompleteBooleanAlgebra
 end BooleanSubalgebra

LeanCamCombi/GrowthInGroups/Chevalley.lean

@@ -436,8 +436,7 @@ lemma RingHom.FinitePresentation.polynomial_induction
 
 lemma PrimeSpectrum.isRetroCompact_iff {U : Set (PrimeSpectrum R)} (hU : IsOpen U) :
     IsRetroCompact U ↔ IsCompact U := by
-  refine isRetroCompact_iff_isCompact_of_isTopologicalBasis _ isTopologicalBasis_basic_opens ?_ hU
-  intro i j
+  refine isTopologicalBasis_basic_opens.isRetroCompact_iff_isCompact (fun i j ↦ ?_) hU
   rw [← TopologicalSpace.Opens.coe_inf, ← basicOpen_mul]
   exact isCompact_basicOpen _
 
@@ -514,11 +513,11 @@ lemma isConstructible_comap_C_zeroLocus_sdiff_zeroLocus {R} [CommRing R]
       (isOpenMap_comap_C _ (basicOpen f).2)
   · intro R _ c I H₁ H₂ f
     replace H₁ := (H₁ (mapRingHom (algebraMap _ _) f)).image_of_isOpenEmbedding
-      _ (localization_away_isOpenEmbedding (Localization.Away c) c)
+      (localization_away_isOpenEmbedding (Localization.Away c) c)
       (by rw [localization_away_comap_range _ c]
           exact (isRetroCompact_iff (basicOpen c).2).mpr (isCompact_basicOpen c))
     replace H₂ := (H₂ (mapRingHom (Ideal.Quotient.mk _) f)).image_of_isClosedEmbedding
-      _ (isClosedEmbedding_comap_of_surjective _ _ Ideal.Quotient.mk_surjective)
+      (isClosedEmbedding_comap_of_surjective _ _ Ideal.Quotient.mk_surjective)
       (by rw [range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective]
           simp only [Ideal.mk_ker, zeroLocus_span, ← basicOpen_eq_zeroLocus_compl]
           exact (isRetroCompact_iff (basicOpen c).2).mpr (isCompact_basicOpen c))
@@ -530,16 +529,20 @@ lemma isConstructible_comap_C_zeroLocus_sdiff_zeroLocus {R} [CommRing R]
 lemma isConstructible_image_comap_C {R} [CommRing R] (s : Set (PrimeSpectrum R[X]))
     (hs : IsConstructible s) :
     IsConstructible (comap C '' s) := by
-  apply hs.induction_of_isTopologicalBasis _ isTopologicalBasis_basic_opens
-  · intros i s hs
+  induction s, hs using
+    IsConstructible.induction_of_isTopologicalBasis _ isTopologicalBasis_basic_opens with
+  | compact_inter i j =>
+    rw [← TopologicalSpace.Opens.coe_inf, ← basicOpen_mul]
+    exact isCompact_basicOpen _
+  | union s hs t ht hs' ht' =>
+    rw [Set.image_union]
+    exact hs'.union ht'
+  | sdiff i s hs =>
     simp only [basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂,
       compl_sdiff_compl, ← zeroLocus_iUnion₂, Set.biUnion_of_singleton]
     rw [← zeroLocus_span]
     apply isConstructible_comap_C_zeroLocus_sdiff_zeroLocus
     exact ⟨hs.toFinset, by simp⟩
-  · intros s t hs ht
-    rw [Set.image_union]
-    exact hs.union ht
 
 lemma isConstructible_image_comap {R S} [CommRing R] [CommRing S] (f : R →+* S)
     (hf : RingHom.FinitePresentation f)
@@ -550,7 +553,7 @@ lemma isConstructible_image_comap {R S} [CommRing R] [CommRing S] (f : R →+* S
     (Q := fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
   · exact fun _ ↦ isConstructible_image_comap_C
   · intro R _ S _ f hf hf' s hs
-    refine hs.image_of_isClosedEmbedding _ (isClosedEmbedding_comap_of_surjective _ _ hf) ?_
+    refine hs.image_of_isClosedEmbedding (isClosedEmbedding_comap_of_surjective _ _ hf) ?_
     rw [range_comap_of_surjective _ _ hf, isRetroCompact_iff (isClosed_zeroLocus _).isOpen_compl]
     obtain ⟨t, ht⟩ := hf'
     rw [← ht, ← t.toSet.iUnion_of_singleton_coe, zeroLocus_span, zeroLocus_iUnion, Set.compl_iInter]