diff --git a/Mathlib.lean b/Mathlib.lean index 5c43f1b7e519b..1ecdac31212ba 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4499,6 +4499,7 @@ import Mathlib.Topology.Algebra.FilterBasis import Mathlib.Topology.Algebra.Group.Basic import Mathlib.Topology.Algebra.Group.Compact import Mathlib.Topology.Algebra.Group.OpenMapping +import Mathlib.Topology.Algebra.Group.Quotient import Mathlib.Topology.Algebra.Group.SubmonoidClosure import Mathlib.Topology.Algebra.Group.TopologicalAbelianization import Mathlib.Topology.Algebra.GroupCompletion diff --git a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean index 721c0f2411c57..02c0d1b8c30a6 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean @@ -631,10 +631,7 @@ instance CosetSpace.borelSpace {G : Type*} [TopologicalSpace G] [PolishSpace G] instance QuotientGroup.borelSpace {G : Type*} [TopologicalSpace G] [PolishSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {N : Subgroup G} [N.Normal] [IsClosed (N : Set G)] : BorelSpace (G ⧸ N) := - -- Porting note: 1st and 3rd `haveI`s were not needed in Lean 3 - haveI := Subgroup.t3_quotient_of_isClosed N - haveI := QuotientGroup.secondCountableTopology (Γ := N) - Quotient.borelSpace + ⟨continuous_mk.map_eq_borel mk_surjective⟩ namespace MeasureTheory diff --git a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean index 6cb8d92d7d95f..e552fa14c3286 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean @@ -57,7 +57,7 @@ instance QuotientGroup.measurableSMul {G : Type*} [Group G] {Γ : Subgroup G} [M [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] [BorelSpace (G ⧸ Γ)] : MeasurableSMul G (G ⧸ Γ) where measurable_const_smul g := (continuous_const_smul g).measurable - measurable_smul_const x := (QuotientGroup.continuous_smul₁ x).measurable + measurable_smul_const _ := (continuous_id.smul continuous_const).measurable end diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean index 6ea401ab9a949..bb19df20f7401 100644 --- a/Mathlib/Topology/Algebra/Group/Basic.lean +++ b/Mathlib/Topology/Algebra/Group/Basic.lean @@ -3,13 +3,9 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot -/ -import Mathlib.GroupTheory.GroupAction.ConjAct -import Mathlib.GroupTheory.GroupAction.Quotient -import Mathlib.Topology.Algebra.Monoid -import Mathlib.Topology.Algebra.Constructions -import Mathlib.Topology.Maps.OpenQuotient +import Mathlib.Algebra.Group.Subgroup.Pointwise import Mathlib.Algebra.Order.Archimedean.Basic -import Mathlib.GroupTheory.QuotientGroup.Basic +import Mathlib.Topology.Algebra.Monoid /-! # Topological groups @@ -847,87 +843,6 @@ theorem TopologicalGroup.exists_antitone_basis_nhds_one [FirstCountableTopology end TopologicalGroup -namespace QuotientGroup - -variable [TopologicalSpace G] [Group G] - -@[to_additive] -instance instTopologicalSpace (N : Subgroup G) : TopologicalSpace (G ⧸ N) := - instTopologicalSpaceQuotient - -@[to_additive] -instance [CompactSpace G] (N : Subgroup G) : CompactSpace (G ⧸ N) := - Quotient.compactSpace - -@[to_additive] -theorem quotientMap_mk (N : Subgroup G) : QuotientMap (mk : G → G ⧸ N) := - quotientMap_quot_mk - -@[to_additive] -theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) := - continuous_quot_mk - -section ContinuousMul - -variable [ContinuousMul G] {N : Subgroup G} - -@[to_additive] -theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) := isOpenMap_quotient_mk'_mul - -@[to_additive] -theorem isOpenQuotientMap_mk : IsOpenQuotientMap (mk : G → G ⧸ N) := - MulAction.isOpenQuotientMap_quotientMk - -@[to_additive (attr := simp)] -theorem dense_preimage_mk {s : Set (G ⧸ N)} : Dense ((↑) ⁻¹' s : Set G) ↔ Dense s := - isOpenQuotientMap_mk.dense_preimage_iff - -@[to_additive] -theorem dense_image_mk {s : Set G} : - Dense (mk '' s : Set (G ⧸ N)) ↔ Dense (s * (N : Set G)) := by - rw [← dense_preimage_mk, preimage_image_mk_eq_mul] - -@[to_additive] -instance instContinuousSMul : ContinuousSMul G (G ⧸ N) where - continuous_smul := by - rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff] - exact continuous_mk.comp continuous_mul - -variable (N) - -/-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient. -/ -@[to_additive - "Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient."] -theorem nhds_eq (x : G) : 𝓝 (x : G ⧸ N) = Filter.map (↑) (𝓝 x) := - (isOpenQuotientMap_mk.map_nhds_eq _).symm - -@[to_additive] -instance instFirstCountableTopology [FirstCountableTopology G] : - FirstCountableTopology (G ⧸ N) where - nhds_generated_countable := mk_surjective.forall.2 fun x ↦ nhds_eq N x ▸ inferInstance - -@[to_additive (attr := deprecated (since := "2024-08-05"))] -theorem nhds_one_isCountablyGenerated [FirstCountableTopology G] [N.Normal] : - (𝓝 (1 : G ⧸ N)).IsCountablyGenerated := - inferInstance - -end ContinuousMul - -variable [TopologicalGroup G] (N : Subgroup G) - -@[to_additive] -instance instTopologicalGroup [N.Normal] : TopologicalGroup (G ⧸ N) where - continuous_mul := by - rw [← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff] - exact continuous_mk.comp continuous_mul - continuous_inv := continuous_inv.quotient_map' _ - -@[to_additive (attr := deprecated (since := "2024-08-05"))] -theorem _root_.topologicalGroup_quotient [N.Normal] : TopologicalGroup (G ⧸ N) := - instTopologicalGroup N - -end QuotientGroup - /-- A typeclass saying that `p : G × G ↦ p.1 - p.2` is a continuous function. This property automatically holds for topological additive groups but it also holds, e.g., for `ℝ≥0`. -/ class ContinuousSub (G : Type*) [TopologicalSpace G] [Sub G] : Prop where @@ -1250,13 +1165,6 @@ theorem IsClosed.mul_right_of_isCompact (ht : IsClosed t) (hs : IsCompact s) : rw [← image_op_smul] exact IsClosed.smul_left_of_isCompact ht (hs.image continuous_op) -@[to_additive] -theorem QuotientGroup.isClosedMap_coe {H : Subgroup G} (hH : IsCompact (H : Set G)) : - IsClosedMap ((↑) : G → G ⧸ H) := by - intro t ht - rw [← (quotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul] - exact ht.mul_right_of_isCompact hH - @[to_additive] lemma subset_mul_closure_one {G} [MulOneClass G] [TopologicalSpace G] (s : Set G) : s ⊆ s * (closure {1} : Set G) := by @@ -1382,13 +1290,6 @@ theorem exists_closed_nhds_one_inv_eq_mul_subset {U : Set G} (hU : U ∈ 𝓝 1) variable (S : Subgroup G) [Subgroup.Normal S] [IsClosed (S : Set G)] -@[to_additive] -instance Subgroup.t3_quotient_of_isClosed (S : Subgroup G) [Subgroup.Normal S] - [hS : IsClosed (S : Set G)] : T3Space (G ⧸ S) := by - rw [← QuotientGroup.ker_mk' S] at hS - haveI := TopologicalGroup.t1Space (G ⧸ S) (quotientMap_quotient_mk'.isClosed_preimage.mp hS) - infer_instance - /-- A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the left, if it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also `DiscreteTopology`.) -/ @@ -1618,18 +1519,6 @@ theorem exists_isCompact_isClosed_nhds_one [WeaklyLocallyCompactSpace G] : let ⟨K, hK₁, hKcomp, hKcl⟩ := exists_mem_nhds_isCompact_isClosed (1 : G) ⟨K, hKcomp, hKcl, hK₁⟩ -/-- A quotient of a locally compact group is locally compact. -/ -@[to_additive] -instance [LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N) := by - refine ⟨fun x n hn ↦ ?_⟩ - let π := ((↑) : G → G ⧸ N) - have C : Continuous π := continuous_quotient_mk' - obtain ⟨y, rfl⟩ : ∃ y, π y = x := Quot.exists_rep x - have : π ⁻¹' n ∈ 𝓝 y := preimage_nhds_coinduced hn - rcases local_compact_nhds this with ⟨s, s_mem, hs, s_comp⟩ - exact ⟨π '' s, QuotientGroup.isOpenMap_coe.image_mem_nhds s_mem, mapsTo'.mp hs, - s_comp.image C⟩ - end section @@ -1665,30 +1554,6 @@ instance {G} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : TopologicalGroup (Multiplicative G) where continuous_inv := @continuous_neg G _ _ _ -section Quotient - -variable [Group G] [TopologicalSpace G] [ContinuousMul G] {Γ : Subgroup G} - -@[to_additive] -instance QuotientGroup.continuousConstSMul : ContinuousConstSMul G (G ⧸ Γ) where - continuous_const_smul g := by - convert ((@continuous_const _ _ _ _ g).mul continuous_id).quotient_map' _ - -@[to_additive] -theorem QuotientGroup.continuous_smul₁ (x : G ⧸ Γ) : Continuous fun g : G => g • x := by - induction x using QuotientGroup.induction_on - exact continuous_quotient_mk'.comp (continuous_mul_right _) - -/-- The quotient of a second countable topological group by a subgroup is second countable. -/ -@[to_additive - "The quotient of a second countable additive topological group by a subgroup is second - countable."] -instance QuotientGroup.secondCountableTopology [SecondCountableTopology G] : - SecondCountableTopology (G ⧸ Γ) := - ContinuousConstSMul.secondCountableTopology - -end Quotient - /-- If `G` is a group with topological `⁻¹`, then it is homeomorphic to its units. -/ @[to_additive " If `G` is an additive group with topological negation, then it is homeomorphic to its additive units."] @@ -1944,4 +1809,4 @@ theorem coinduced_continuous {α β : Type*} [t : TopologicalSpace α] [Group β end GroupTopology -set_option linter.style.longFile 2100 +set_option linter.style.longFile 2000 diff --git a/Mathlib/Topology/Algebra/Group/Quotient.lean b/Mathlib/Topology/Algebra/Group/Quotient.lean new file mode 100644 index 0000000000000..08cb4e12c8933 --- /dev/null +++ b/Mathlib/Topology/Algebra/Group/Quotient.lean @@ -0,0 +1,133 @@ +/- +Copyright (c) 2017 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov +-/ +import Mathlib.GroupTheory.GroupAction.Quotient +import Mathlib.GroupTheory.QuotientGroup.Basic +import Mathlib.Topology.Algebra.Group.Basic +import Mathlib.Topology.Maps.OpenQuotient + +/-! +# Topology on the quotient group + +In this file we define topology on `G ⧸ N`, where `N` is a subgroup of `G`, +and prove basic properties of this topology. +-/ + +open scoped Pointwise Topology + +variable {G : Type*} [TopologicalSpace G] [Group G] + +namespace QuotientGroup + +@[to_additive] +instance instTopologicalSpace (N : Subgroup G) : TopologicalSpace (G ⧸ N) := + instTopologicalSpaceQuotient + +@[to_additive] +instance [CompactSpace G] (N : Subgroup G) : CompactSpace (G ⧸ N) := + Quotient.compactSpace + +@[to_additive] +theorem quotientMap_mk (N : Subgroup G) : QuotientMap (mk : G → G ⧸ N) := + quotientMap_quot_mk + +@[to_additive] +theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) := + continuous_quot_mk + +section ContinuousMul + +variable [ContinuousMul G] {N : Subgroup G} + +@[to_additive] +theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) := isOpenMap_quotient_mk'_mul + +@[to_additive] +theorem isOpenQuotientMap_mk : IsOpenQuotientMap (mk : G → G ⧸ N) := + MulAction.isOpenQuotientMap_quotientMk + +@[to_additive (attr := simp)] +theorem dense_preimage_mk {s : Set (G ⧸ N)} : Dense ((↑) ⁻¹' s : Set G) ↔ Dense s := + isOpenQuotientMap_mk.dense_preimage_iff + +@[to_additive] +theorem dense_image_mk {s : Set G} : + Dense (mk '' s : Set (G ⧸ N)) ↔ Dense (s * (N : Set G)) := by + rw [← dense_preimage_mk, preimage_image_mk_eq_mul] + +@[to_additive] +instance instContinuousSMul : ContinuousSMul G (G ⧸ N) where + continuous_smul := by + rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff] + exact continuous_mk.comp continuous_mul + +@[to_additive] +instance instContinuousConstSMul : ContinuousConstSMul G (G ⧸ N) := inferInstance + +/-- A quotient of a locally compact group is locally compact. -/ +@[to_additive] +instance instLocallyCompactSpace [LocallyCompactSpace G] (N : Subgroup G) : + LocallyCompactSpace (G ⧸ N) := + QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace + +@[to_additive (attr := deprecated (since := "2024-10-05"))] +theorem continuous_smul₁ (x : G ⧸ N) : Continuous fun g : G => g • x := + continuous_id.smul continuous_const + +variable (N) + +/-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient. -/ +@[to_additive + "Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient."] +theorem nhds_eq (x : G) : 𝓝 (x : G ⧸ N) = Filter.map (↑) (𝓝 x) := + (isOpenQuotientMap_mk.map_nhds_eq _).symm + +@[to_additive] +instance instFirstCountableTopology [FirstCountableTopology G] : + FirstCountableTopology (G ⧸ N) where + nhds_generated_countable := mk_surjective.forall.2 fun x ↦ nhds_eq N x ▸ inferInstance + +/-- The quotient of a second countable topological group by a subgroup is second countable. -/ +@[to_additive + "The quotient of a second countable additive topological group by a subgroup is second + countable."] +instance instSecondCountableTopology [SecondCountableTopology G] : + SecondCountableTopology (G ⧸ N) := + ContinuousConstSMul.secondCountableTopology + +@[to_additive (attr := deprecated (since := "2024-08-05"))] +theorem nhds_one_isCountablyGenerated [FirstCountableTopology G] [N.Normal] : + (𝓝 (1 : G ⧸ N)).IsCountablyGenerated := + inferInstance + +end ContinuousMul + +variable [TopologicalGroup G] (N : Subgroup G) + +@[to_additive] +instance instTopologicalGroup [N.Normal] : TopologicalGroup (G ⧸ N) where + continuous_mul := by + rw [← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff] + exact continuous_mk.comp continuous_mul + continuous_inv := continuous_inv.quotient_map' _ + +@[to_additive (attr := deprecated (since := "2024-08-05"))] +theorem _root_.topologicalGroup_quotient [N.Normal] : TopologicalGroup (G ⧸ N) := + instTopologicalGroup N + +@[to_additive] +theorem isClosedMap_coe {H : Subgroup G} (hH : IsCompact (H : Set G)) : + IsClosedMap ((↑) : G → G ⧸ H) := by + intro t ht + rw [← (quotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul] + exact ht.mul_right_of_isCompact hH + +@[to_additive] +instance instT3Space [N.Normal] [hN : IsClosed (N : Set G)] : T3Space (G ⧸ N) := by + rw [← QuotientGroup.ker_mk' N] at hN + haveI := TopologicalGroup.t1Space (G ⧸ N) ((quotientMap_mk N).isClosed_preimage.mp hN) + infer_instance + +end QuotientGroup diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index c5fd7f2684f75..1ed9c07b215fe 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Basic.lean @@ -2393,7 +2393,7 @@ instance continuousSMul_quotient [TopologicalSpace R] [TopologicalAddGroup M] [C instance t3_quotient_of_isClosed [TopologicalAddGroup M] [IsClosed (S : Set M)] : T3Space (M ⧸ S) := letI : IsClosed (S.toAddSubgroup : Set M) := ‹_› - S.toAddSubgroup.t3_quotient_of_isClosed + QuotientAddGroup.instT3Space S.toAddSubgroup end Submodule diff --git a/Mathlib/Topology/Algebra/OpenSubgroup.lean b/Mathlib/Topology/Algebra/OpenSubgroup.lean index 99c3a4c276f10..843e91673869b 100644 --- a/Mathlib/Topology/Algebra/OpenSubgroup.lean +++ b/Mathlib/Topology/Algebra/OpenSubgroup.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin, Nailin Guan -/ import Mathlib.RingTheory.Ideal.Basic +import Mathlib.Topology.Algebra.Group.Quotient import Mathlib.Topology.Algebra.Ring.Basic import Mathlib.Topology.Sets.Opens diff --git a/Mathlib/Topology/Algebra/ProperAction/Basic.lean b/Mathlib/Topology/Algebra/ProperAction/Basic.lean index 55f73de488d07..fa7a99510f216 100644 --- a/Mathlib/Topology/Algebra/ProperAction/Basic.lean +++ b/Mathlib/Topology/Algebra/ProperAction/Basic.lean @@ -5,6 +5,7 @@ Authors: Anatole Dedeker, Etienne Marion, Florestan Martin-Baillon, Vincent Guir -/ import Mathlib.Topology.Algebra.MulAction import Mathlib.Topology.Maps.Proper.Basic +import Mathlib.Topology.Maps.OpenQuotient /-! # Proper group action diff --git a/Mathlib/Topology/Algebra/Ring/Ideal.lean b/Mathlib/Topology/Algebra/Ring/Ideal.lean index aa3cf06eb57a1..c72e3ee7afefa 100644 --- a/Mathlib/Topology/Algebra/Ring/Ideal.lean +++ b/Mathlib/Topology/Algebra/Ring/Ideal.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Patrick Massot -/ import Mathlib.Topology.Algebra.Ring.Basic +import Mathlib.Topology.Algebra.Group.Quotient import Mathlib.RingTheory.Ideal.Quotient /-! diff --git a/Mathlib/Topology/Algebra/UniformGroup.lean b/Mathlib/Topology/Algebra/UniformGroup.lean index c05bd7340d340..1c3bc90dfda28 100644 --- a/Mathlib/Topology/Algebra/UniformGroup.lean +++ b/Mathlib/Topology/Algebra/UniformGroup.lean @@ -7,7 +7,7 @@ import Mathlib.Topology.UniformSpace.UniformConvergence import Mathlib.Topology.UniformSpace.UniformEmbedding import Mathlib.Topology.UniformSpace.CompleteSeparated import Mathlib.Topology.UniformSpace.Compact -import Mathlib.Topology.Algebra.Group.Basic +import Mathlib.Topology.Algebra.Group.Quotient import Mathlib.Topology.DiscreteSubset import Mathlib.Tactic.Abel diff --git a/Mathlib/Topology/Compactness/LocallyCompact.lean b/Mathlib/Topology/Compactness/LocallyCompact.lean index e0c44089ecd15..8d10e1ce3da2e 100644 --- a/Mathlib/Topology/Compactness/LocallyCompact.lean +++ b/Mathlib/Topology/Compactness/LocallyCompact.lean @@ -45,6 +45,13 @@ protected theorem IsClosed.weaklyLocallyCompactSpace [WeaklyLocallyCompactSpace {s : Set X} (hs : IsClosed s) : WeaklyLocallyCompactSpace s := (closedEmbedding_subtype_val hs).weaklyLocallyCompactSpace +theorem IsOpenQuotientMap.weaklyLocallyCompactSpace [WeaklyLocallyCompactSpace X] + {f : X → Y} (hf : IsOpenQuotientMap f) : WeaklyLocallyCompactSpace Y where + exists_compact_mem_nhds := by + refine hf.surjective.forall.2 fun x ↦ ?_ + rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩ + exact ⟨f '' K, hKc.image hf.continuous, hf.isOpenMap.image_mem_nhds hKx⟩ + /-- In a weakly locally compact space, every compact set is contained in the interior of a compact set. -/ theorem exists_compact_superset [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) : @@ -166,6 +173,13 @@ theorem exists_compact_between [LocallyCompactSpace X] {K U : Set X} (hK : IsCom let ⟨L, hKL, hL, hLU⟩ := exists_mem_nhdsSet_isCompact_mapsTo continuous_id hK hU h_KU ⟨L, hL, subset_interior_iff_mem_nhdsSet.2 hKL, hLU⟩ +theorem IsOpenQuotientMap.locallyCompactSpace [LocallyCompactSpace X] {f : X → Y} + (hf : IsOpenQuotientMap f) : LocallyCompactSpace Y where + local_compact_nhds := by + refine hf.surjective.forall.2 fun x U hU ↦ ?_ + rcases local_compact_nhds (hf.continuous.continuousAt hU) with ⟨K, hKx, hKU, hKc⟩ + exact ⟨f '' K, hf.isOpenMap.image_mem_nhds hKx, image_subset_iff.2 hKU, hKc.image hf.continuous⟩ + /-- If `f` is a topology inducing map with a locally compact codomain and a locally closed range, then the domain of `f` is a locally compact space. -/ theorem Inducing.locallyCompactSpace [LocallyCompactSpace Y] {f : X → Y} (hf : Inducing f)