feat(Topology/Algebra): discrete iff finite index subgroup discrete (#29743)

Show that if G is a topological group and H is a finite-index subgroup, then H is discrete iff G is. As application, show that arithmetic subgroups of GL(2, R), which are by definition those commensurable with SL(2, Z), are discrete.

Author: loefflerd

Mathlib.lean

@@ -6444,6 +6444,7 @@ import Mathlib.Topology.Algebra.IsOpenUnits
 import Mathlib.Topology.Algebra.IsUniformGroup.Basic
 import Mathlib.Topology.Algebra.IsUniformGroup.Constructions
 import Mathlib.Topology.Algebra.IsUniformGroup.Defs
+import Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
 import Mathlib.Topology.Algebra.IsUniformGroup.Order
 import Mathlib.Topology.Algebra.LinearTopology
 import Mathlib.Topology.Algebra.Localization

Mathlib/Data/Set/Constructions.lean

@@ -85,3 +85,9 @@ theorem mk₂ (h : ∀ ⦃s⦄, s ∈ S → ∀ ⦃t⦄, t ∈ S → s ∩ t ∈
   inter_mem s hs t ht := by aesop
 
 end FiniteInter
+
+/-- This is a hybrid of `Set.biUnion_empty` and `Finset.biUnion_empty` (the index set on the LHS is
+the empty finset, but `s` is a family of sets, not finsets). -/
+theorem Set.biUnion_empty_finset {ι X : Type*} {s : ι → Set X} :
+    ⋃ i ∈ (∅ : Finset ι), s i = ∅ := by
+  simp only [Finset.notMem_empty, iUnion_of_empty, iUnion_empty]

Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean

@@ -3,10 +3,7 @@ Copyright (c) 2025 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
-import Mathlib.Data.Real.Basic
-import Mathlib.GroupTheory.Commensurable
-import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
-import Mathlib.Topology.Algebra.IsUniformGroup.Basic
+import Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
 import Mathlib.Topology.Algebra.Ring.Real
 import Mathlib.Topology.Instances.Matrix
 import Mathlib.Topology.MetricSpace.Isometry
@@ -114,3 +111,9 @@ lemma isClosedEmbedding_mapGLInt : Topology.IsClosedEmbedding (mapGL ℝ : SL n
   ⟨isEmbedding_mapGL (Isometry.isEmbedding fun _ _ ↦ rfl), (mapGL ℝ).range.isClosed_of_discrete⟩
 
 end Matrix.SpecialLinearGroup
+
+/-- Arithmetic subgroups of `GL(2, ℝ)` are discrete. -/
+instance Subgroup.IsArithmetic.discreteTopology {𝒢 : Subgroup (GL (Fin 2) ℝ)} [IsArithmetic 𝒢] :
+    DiscreteTopology 𝒢 := by
+  rw [is_commensurable.discreteTopology_iff]
+  infer_instance

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

@@ -419,7 +419,14 @@ def symm (cme : M ≃ₜ* N) : N ≃ₜ* M :=
   { cme.toMulEquiv.symm with
   continuous_toFun := cme.continuous_invFun
   continuous_invFun := cme.continuous_toFun }
+
+/-- See Note [custom simps projection] -/
+@[to_additive /-- See Note [custom simps projection] -/]
+def Simps.symm_apply [Mul G] [Mul H] (e : G ≃ₜ* H) : H → G :=
+  e.symm
+
 initialize_simps_projections ContinuousMulEquiv (toFun → apply, invFun → symm_apply)
+
 initialize_simps_projections ContinuousAddEquiv (toFun → apply, invFun → symm_apply)
 
 @[to_additive]
@@ -545,6 +552,38 @@ end unique
 
 end ContinuousMulEquiv
 
+namespace MulEquiv
+
+variable {G H} [Mul G] [Mul H] (e : G ≃* H) (he : ∀ s, IsOpen (e ⁻¹' s) ↔ IsOpen s)
+include he
+
+/-- A `MulEquiv` that respects open sets is a `ContinuousMulEquiv`. -/
+@[to_additive (attr := simps apply symm_apply)
+/-- An `AddEquiv` that respects open sets is a `ContinuousAddEquiv`. -/]
+def toContinuousMulEquiv : G ≃ₜ* H where
+  toFun := e
+  invFun := e.symm
+  __ := e
+  __ := e.toEquiv.toHomeomorph he
+
+variable {e}
+
+@[to_additive, simp]
+lemma toMulEquiv_toContinuousMulEquiv : (e.toContinuousMulEquiv he : G ≃* H) = e :=
+  rfl
+
+@[to_additive, simp] lemma toHomeomorph_toContinuousMulEquiv :
+    (e.toContinuousMulEquiv he : G ≃ₜ H) = e.toHomeomorph he :=
+  rfl
+
+@[to_additive]
+lemma symm_toContinuousMulEquiv :
+    (e.toContinuousMulEquiv he).symm = e.symm.toContinuousMulEquiv
+      (fun s ↦ by convert (he _).symm; exact (e.preimage_symm_preimage s).symm) :=
+  rfl
+
+end MulEquiv
+
 end
 
 end

Mathlib/Topology/Algebra/IsUniformGroup/DiscreteSubgroup.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2025 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+
+import Mathlib.GroupTheory.Commensurable
+import Mathlib.Topology.Algebra.ContinuousMonoidHom
+import Mathlib.Topology.Algebra.Group.ClosedSubgroup
+import Mathlib.Topology.Algebra.IsUniformGroup.Basic
+
+/-!
+# Discrete subgroups of topological groups
+
+Note that the instance `Subgroup.isClosed_of_discrete` does not live here, in order that it can
+be used in other files without requiring lots of group-theoretic imports.
+-/
+
+open Filter Topology Uniformity
+
+variable {G : Type*} [Group G] [TopologicalSpace G]
+
+/-- If `G` has a topology, and `H ≤ K` are subgroups, then `H` as a subgroup of `K` is isomorphic,
+as a topological group, to `H` as a subgroup of `G`. This is `subgroupOfEquivOfLe` upgraded to a
+`ContinuousMulEquiv`. -/
+@[to_additive (attr := simps! apply) /-- If `G` has a topology, and `H ≤ K` are
+subgroups, then `H` as a subgroup of `K` is isomorphic, as a topological group, to `H` as a subgroup
+of `G`. This is `addSubgroupOfEquivOfLe` upgraded to a `ContinuousAddEquiv`.-/]
+def Subgroup.subgroupOfContinuousMulEquivOfLe {H K : Subgroup G} (hHK : H ≤ K) :
+    (H.subgroupOf K) ≃ₜ* H :=
+  (subgroupOfEquivOfLe hHK).toContinuousMulEquiv (by
+    simp only [subgroupOfEquivOfLe, Topology.IsInducing.subtypeVal.isOpen_iff,
+      exists_exists_and_eq_and]
+    simpa [Set.ext_iff] using fun s ↦ exists_congr
+      fun t ↦ and_congr_right fun _ ↦ ⟨fun aux g hgh ↦ aux g (hHK hgh) hgh, by grind⟩)
+
+@[to_additive (attr := simp)]
+lemma Subgroup.subgroupOfContinuousMulEquivOfLe_symm_apply
+    {H K : Subgroup G} (hHK : H ≤ K) (g : H) :
+    (subgroupOfContinuousMulEquivOfLe hHK).symm g = ⟨⟨g.1, hHK g.2⟩, g.2⟩ :=
+  rfl
+
+@[to_additive (attr := simp)]
+lemma Subgroup.subgroupOfContinuousMulEquivOfLe_toMulEquiv {H K : Subgroup G} (hHK : H ≤ K) :
+    (subgroupOfContinuousMulEquivOfLe hHK : H.subgroupOf K ≃* H) = subgroupOfEquivOfLe hHK := by
+  rfl
+
+variable [IsTopologicalGroup G] [T2Space G]
+
+/-- If `G` is a topological group and `H` a finite-index subgroup, then `G` is topologically
+discrete iff `H` is. -/
+@[to_additive]
+lemma Subgroup.discreteTopology_iff_of_finiteIndex {H : Subgroup G} [H.FiniteIndex] :
+    DiscreteTopology H ↔ DiscreteTopology G := by
+  refine ⟨fun hH ↦ ?_, fun hG ↦ inferInstance⟩
+  suffices IsOpen (H : Set G) by
+    rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
+        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]
+  exact H.isOpen_of_isClosed_of_finiteIndex Subgroup.isClosed_of_discrete
+
+@[to_additive]
+lemma Subgroup.discreteTopology_iff_of_isFiniteRelIndex {H K : Subgroup G} (hHK : H ≤ K)
+    [IsFiniteRelIndex H K] : DiscreteTopology H ↔ DiscreteTopology K := by
+  haveI : (H.subgroupOf K).FiniteIndex := IsFiniteRelIndex.to_finiteIndex_subgroupOf
+  rw [← (subgroupOfContinuousMulEquivOfLe hHK).discreteTopology_iff,
+    discreteTopology_iff_of_finiteIndex]
+
+@[to_additive]
+lemma Subgroup.Commensurable.discreteTopology_iff
+    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
+    {H K : Subgroup G} (h : Commensurable H K) :
+    DiscreteTopology H ↔ DiscreteTopology K :=
+  calc DiscreteTopology H ↔ DiscreteTopology ↑(H ⊓ K) :=
+    haveI : IsFiniteRelIndex (H ⊓ K) H := ⟨Subgroup.inf_relIndex_left H K ▸ h.2⟩
+    (Subgroup.discreteTopology_iff_of_isFiniteRelIndex inf_le_left).symm
+  _ ↔ DiscreteTopology K :=
+    haveI : IsFiniteRelIndex (H ⊓ K) K := ⟨Subgroup.inf_relIndex_right H K ▸ h.1⟩
+    Subgroup.discreteTopology_iff_of_isFiniteRelIndex inf_le_right

Mathlib/Topology/Constructions.lean

@@ -237,10 +237,6 @@ theorem nhds_ne_subtype_neBot_iff {S : Set X} {x : S} :
     (𝓝[≠] x).NeBot ↔ (𝓝[≠] (x : X) ⊓ 𝓟 S).NeBot := by
   rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]
 
-theorem discreteTopology_subtype_iff {S : Set X} :
-    DiscreteTopology S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥ := by
-  simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]
-
 end Top
 
 /-- A type synonym equipped with the topology whose open sets are the empty set and the sets with

Mathlib/Topology/DiscreteSubset.lean

@@ -40,18 +40,26 @@ This is the filter of all open codiscrete sets within S. We also define `Filter.
 
 open Set Filter Function Topology
 
-variable {X Y : Type*} [TopologicalSpace Y] {f : X → Y}
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y}
+
+theorem discreteTopology_subtype_iff {S : Set Y} :
+    DiscreteTopology S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥ := by
+  simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]
+
+lemma discreteTopology_subtype_iff' {S : Set Y} :
+    DiscreteTopology S ↔ ∀ y ∈ S, ∃ U : Set Y, IsOpen U ∧ U ∩ S = {y} := by
+  simp [discreteTopology_iff_isOpen_singleton, isOpen_induced_iff, Set.ext_iff]
+  grind
 
 section cofinite_cocompact
 
+omit [TopologicalSpace X] in
 lemma tendsto_cofinite_cocompact_iff :
     Tendsto f cofinite (cocompact _) ↔ ∀ K, IsCompact K → Set.Finite (f ⁻¹' K) := by
   rw [hasBasis_cocompact.tendsto_right_iff]
   refine forall₂_congr (fun K _ ↦ ?_)
   simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]
 
-variable [TopologicalSpace X]
-
 lemma Continuous.discrete_of_tendsto_cofinite_cocompact [T1Space X] [WeaklyLocallyCompactSpace Y]
     (hf' : Continuous f) (hf : Tendsto f cofinite (cocompact _)) :
     DiscreteTopology X := by
@@ -83,8 +91,6 @@ end cofinite_cocompact
 
 section codiscrete_filter
 
-variable [TopologicalSpace X]
-
 /-- Criterion for a subset `S ⊆ X` to be closed and discrete in terms of the punctured
 neighbourhood filter at an arbitrary point of `X`. (Compare `discreteTopology_subtype_iff`.) -/
 theorem isClosed_and_discrete_iff {S : Set X} :
@@ -240,3 +246,33 @@ lemma mem_codiscrete_subtype_iff_mem_codiscreteWithin {S : Set X} {U : Set S} :
       continuous_subtype_val.continuousWithinAt <| eventually_mem_nhdsWithin.mono (by simp)
 
 end codiscrete_filter
+
+section discrete_union
+
+lemma compl_mem_codiscrete_iff {S : Set X} :
+    Sᶜ ∈ codiscrete X ↔ IsClosed S ∧ DiscreteTopology ↑S := by
+  rw [mem_codiscrete, compl_compl, isClosed_and_discrete_iff]
+
+/-- The union of two discrete closed subsets is discrete. -/
+theorem discreteTopology_union {S T : Set X} (hs : DiscreteTopology S) (ht : DiscreteTopology T)
+    (hs' : IsClosed S) (ht' : IsClosed T) : DiscreteTopology ↑(S ∪ T) := by
+  suffices (S ∪ T)ᶜ ∈ codiscrete X from compl_mem_codiscrete_iff.mp this |>.2
+  have hS : Sᶜ ∈ codiscrete X := by simpa [compl_mem_codiscrete_iff] using ⟨hs', hs⟩
+  have hT : Tᶜ ∈ codiscrete X := by simpa [compl_mem_codiscrete_iff] using ⟨ht', ht⟩
+  simpa using inter_mem hS hT
+
+/-- The union of finitely many discrete closed subsets is discrete. -/
+theorem discreteTopology_biUnion_finset {ι : Type*} {I : Finset ι} {s : ι → Set X}
+    (hs : ∀ i ∈ I, DiscreteTopology (s i)) (hs' : ∀ i ∈ I, IsClosed (s i)) :
+    DiscreteTopology (⋃ i ∈ I, s i) := by
+  suffices (⋃ i ∈ I, s i)ᶜ ∈ codiscrete X from (compl_mem_codiscrete_iff.mp this).2
+  simpa [biInter_finset_mem I] using fun i hi ↦ compl_mem_codiscrete_iff.mpr ⟨hs' i hi, hs i hi⟩
+
+/-- The union of finitely many discrete closed subsets is discrete. -/
+theorem discreteTopology_iUnion_fintype {ι : Type*} [Fintype ι] {s : ι → Set X}
+    (hs : ∀ i, DiscreteTopology (s i)) (hs' : ∀ i, IsClosed (s i)) :
+    DiscreteTopology (⋃ i, s i) := by
+  convert discreteTopology_biUnion_finset (I := .univ) (fun i _ ↦ hs i) (fun i _ ↦ hs' i) <;>
+    simp
+
+end discrete_union

Mathlib/Topology/Homeomorph/Defs.lean

@@ -84,7 +84,7 @@ theorem symm_bijective : Function.Bijective (Homeomorph.symm : (X ≃ₜ Y) →
 def Simps.symm_apply (h : X ≃ₜ Y) : Y → X :=
   h.symm
 
-initialize_simps_projections Homeomorph (toFun → apply, invFun → symm_apply)
+initialize_simps_projections Homeomorph (toFun → apply, invFun → symm_apply, as_prefix toEquiv)
 
 @[simp]
 theorem coe_toEquiv (h : X ≃ₜ Y) : ⇑h.toEquiv = h :=
@@ -336,15 +336,19 @@ def toHomeomorph (e : X ≃ Y) (he : ∀ s, IsOpen (e ⁻¹' s) ↔ IsOpen s) :
   continuous_toFun := continuous_def.2 fun _ ↦ (he _).2
   continuous_invFun := continuous_def.2 fun s ↦ by convert (he _).1; simp
 
+@[deprecated (since := "2025-10-09")] alias toHomeomorph_toEquiv := toEquiv_toHomeomorph
+
 @[simp] lemma coe_toHomeomorph (e : X ≃ Y) (he) : ⇑(e.toHomeomorph he) = e := rfl
 lemma toHomeomorph_apply (e : X ≃ Y) (he) (x : X) : e.toHomeomorph he x = e x := rfl
 
 @[simp] lemma toHomeomorph_refl :
     (Equiv.refl X).toHomeomorph (fun _s ↦ Iff.rfl) = Homeomorph.refl _ := rfl
 
-@[simp] lemma toHomeomorph_symm (e : X ≃ Y) (he) :
+@[simp] lemma symm_toHomeomorph (e : X ≃ Y) (he) :
     (e.toHomeomorph he).symm = e.symm.toHomeomorph fun s ↦ by convert (he _).symm; simp := rfl
 
+@[deprecated (since := "2025-10-09")] alias toHomeomorph_symm := symm_toHomeomorph
+
 lemma toHomeomorph_trans (e : X ≃ Y) (f : Y ≃ Z) (he hf) :
     (e.trans f).toHomeomorph (fun _s ↦ (he _).trans (hf _)) =
     (e.toHomeomorph he).trans (f.toHomeomorph hf) := rfl
@@ -371,8 +375,11 @@ def toHomeomorphOfContinuousOpen (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsO
 @[deprecated (since := "2025-04-16")]
 alias _root_.Homeomorph.homeomorphOfContinuousOpen := toHomeomorphOfContinuousOpen
 
+@[deprecated (since := "2025-10-09")] alias toHomeomorphOfContinuousOpen_toEquiv :=
+  toEquiv_toHomeomorphOfContinuousOpen
+
 @[deprecated (since := "2025-04-16")]
-alias _root_.Homeomorph.homeomorphOfContinuousOpen_toEquiv := toHomeomorphOfContinuousOpen_toEquiv
+alias _root_.Homeomorph.homeomorphOfContinuousOpen_toEquiv := toEquiv_toHomeomorphOfContinuousOpen
 
 @[simp]
 theorem toHomeomorphOfContinuousOpen_apply (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) :