diff --git a/Mathlib/Analysis/Normed/Group/Quotient.lean b/Mathlib/Analysis/Normed/Group/Quotient.lean index 53b898fa9d810a..0a59058684ca56 100644 --- a/Mathlib/Analysis/Normed/Group/Quotient.lean +++ b/Mathlib/Analysis/Normed/Group/Quotient.lean @@ -102,11 +102,16 @@ noncomputable section open Metric Set Topology NNReal namespace QuotientGroup -variable {M : Type*} [SeminormedCommGroup M] {S T : Subgroup M} {x : M ⧸ S} {m : M} {r ε : ℝ} +variable {M : Type*} + +section SeminormedGroup +variable [SeminormedGroup M] {S T : Subgroup M} {x : M ⧸ S} {m : M} {r ε : ℝ} @[to_additive add_norm_aux] private lemma norm_aux (x : M ⧸ S) : {m : M | (m : M ⧸ S) = x}.Nonempty := Quot.exists_rep x +variable [S.Normal] [T.Normal] + /-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on `x * M`. -/ @[to_additive @@ -157,6 +162,29 @@ lemma nhds_one_hasBasis : (𝓝 (1 : M ⧸ S)).HasBasis (fun ε ↦ 0 < ε) fun rw [← mk_one, nhds_eq, ← funext this] exact .map _ Metric.nhds_basis_ball +/-- The norm of the projection is smaller or equal to the norm of the original element. -/ +@[to_additive +/-- The norm of the projection is smaller or equal to the norm of the original element. -/] +lemma norm_mk_le_norm : ‖(m : M ⧸ S)‖ ≤ ‖m‖ := + (infDist_le_dist_of_mem (by simp)).trans_eq (dist_one_left _) + +/-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x` +and `‖m‖ < ‖x‖ + ε`. -/ +@[to_additive /-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x` +and `‖m‖ < ‖x‖ + ε`. -/] +lemma exists_norm_mk_lt (x : M ⧸ S) (hε : 0 < ε) : ∃ m : M, m = x ∧ ‖m‖ < ‖x‖ + ε := + norm_lt_iff.1 <| lt_add_of_pos_right _ hε + +/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m * s‖ < ‖mk' S m‖ + ε`. -/ +@[to_additive +/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m + s‖ < ‖mk' S m‖ + ε`. -/] +lemma exists_norm_mul_lt (S : Subgroup M) [S.Normal] (m : M) {ε : ℝ} (hε : 0 < ε) : + ∃ s ∈ S, ‖m * s‖ < ‖mk' S m‖ + ε := by + obtain ⟨n : M, hn, hn'⟩ := exists_norm_mk_lt (QuotientGroup.mk' S m) hε + exact ⟨m⁻¹ * n, by simpa [eq_comm, QuotientGroup.eq] using hn, by simpa⟩ + +variable [IsIsometricSMul M M] + /-- An alternative definition of the norm on the quotient group: the norm of `((x : M) : M ⧸ S)` is equal to the distance from `x` to `S`. -/ @[to_additive @@ -167,12 +195,6 @@ lemma norm_mk (x : M) : ‖(x : M ⧸ S)‖ = infDist x S := by ← IsometryEquiv.preimage_symm] simp -/-- The norm of the projection is smaller or equal to the norm of the original element. -/ -@[to_additive -/-- The norm of the projection is smaller or equal to the norm of the original element. -/] -lemma norm_mk_le_norm : ‖(m : M ⧸ S)‖ ≤ ‖m‖ := - (infDist_le_dist_of_mem (by simp)).trans_eq (dist_one_left _) - /-- The norm of the image of `m : M` in the quotient by `S` is zero if and only if `m` belongs to the closure of `S`. -/ @[to_additive /-- The norm of the image of `m : M` in the quotient by `S` is zero if and only if `m` @@ -188,27 +210,12 @@ if and only if `m ∈ S`. -/] lemma norm_mk_eq_zero [hS : IsClosed (S : Set M)] : ‖(m : M ⧸ S)‖ = 0 ↔ m ∈ S := by rw [norm_mk_eq_zero_iff_mem_closure, hS.closure_eq, SetLike.mem_coe] -/-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x` -and `‖m‖ < ‖x‖ + ε`. -/ -@[to_additive /-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x` -and `‖m‖ < ‖x‖ + ε`. -/] -lemma exists_norm_mk_lt (x : M ⧸ S) (hε : 0 < ε) : ∃ m : M, m = x ∧ ‖m‖ < ‖x‖ + ε := - norm_lt_iff.1 <| lt_add_of_pos_right _ hε - -/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m * s‖ < ‖mk' S m‖ + ε`. -/ -@[to_additive -/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m + s‖ < ‖mk' S m‖ + ε`. -/] -lemma exists_norm_mul_lt (S : Subgroup M) (m : M) {ε : ℝ} (hε : 0 < ε) : - ∃ s ∈ S, ‖m * s‖ < ‖mk' S m‖ + ε := by - obtain ⟨n : M, hn, hn'⟩ := exists_norm_mk_lt (QuotientGroup.mk' S m) hε - exact ⟨m⁻¹ * n, by simpa [eq_comm, QuotientGroup.eq] using hn, by simpa⟩ - variable (S) in /-- The seminormed group structure on the quotient by a subgroup. -/ @[to_additive /-- The seminormed group structure on the quotient by an additive subgroup. -/] -noncomputable instance instSeminormedCommGroup : SeminormedCommGroup (M ⧸ S) where +noncomputable instance instSeminormedGroup : SeminormedGroup (M ⧸ S) where toUniformSpace := IsTopologicalGroup.rightUniformSpace (M ⧸ S) - __ := groupSeminorm.toSeminormedCommGroup + __ := groupSeminorm.toSeminormedGroup uniformity_dist := by rw [uniformity_eq_comap_nhds_one', (nhds_one_hasBasis.comap _).eq_biInf] simp only [dist, preimage_setOf_eq, norm_eq_groupSeminorm, map_div_rev] @@ -216,18 +223,16 @@ noncomputable instance instSeminormedCommGroup : SeminormedCommGroup (M ⧸ S) w variable (S) in /-- The quotient in the category of normed groups. -/ @[to_additive /-- The quotient in the category of normed groups. -/] -noncomputable instance instNormedCommGroup [hS : IsClosed (S : Set M)] : - NormedCommGroup (M ⧸ S) where +noncomputable instance instNormedGroup [hS : IsClosed (S : Set M)] : NormedGroup (M ⧸ S) where __ := MetricSpace.ofT0PseudoMetricSpace _ -- This is a sanity check left here on purpose to ensure that potential refactors won't destroy -- this important property. example : (instTopologicalSpaceQuotient : TopologicalSpace <| M ⧸ S) = - (instSeminormedCommGroup S).toUniformSpace.toTopologicalSpace := rfl + (instSeminormedGroup S).toUniformSpace.toTopologicalSpace := rfl -example [IsClosed (S : Set M)] : - (instSeminormedCommGroup S) = NormedCommGroup.toSeminormedCommGroup := rfl +example [IsClosed (S : Set M)] : (instSeminormedGroup S) = NormedGroup.toSeminormedGroup := rfl /-- An isometric version of `Subgroup.quotientEquivOfEq`. -/ @[to_additive /-- An isometric version of `AddSubgroup.quotientEquivOfEq`. -/] @@ -245,6 +250,21 @@ def quotientBotIsometryEquiv : M ⧸ (⊥ : Subgroup M) ≃ᵢ M where change ‖x‖ = ‖QuotientGroup.mk x‖ simp [norm_mk] +end SeminormedGroup + +variable [SeminormedCommGroup M] {S T : Subgroup M} + +variable (S) in +/-- The seminormed group structure on the quotient by a subgroup. -/ +@[to_additive /-- The seminormed group structure on the quotient by an additive subgroup. -/] +noncomputable instance instSeminormedCommGroup : SeminormedCommGroup (M ⧸ S) where + +variable (S) in +/-- The quotient in the category of normed groups. -/ +@[to_additive /-- The quotient in the category of normed groups. -/] +noncomputable instance instNormedCommGroup [hS : IsClosed (S : Set M)] : + NormedCommGroup (M ⧸ S) where + /-- An isometric version of `QuotientGroup.quotientQuotientEquivQuotient`. -/ @[to_additive /-- An isometric version of `QuotientAddGroup.quotientQuotientEquivQuotient`. -/] def quotientQuotientIsometryEquivQuotient (h : S ≤ T) : (M ⧸ S) ⧸ T.map (mk' S) ≃ᵢ M ⧸ T where diff --git a/Mathlib/Analysis/Normed/Group/Uniform.lean b/Mathlib/Analysis/Normed/Group/Uniform.lean index 5cd99c3e8dd118..fa963fa12ad9bf 100644 --- a/Mathlib/Analysis/Normed/Group/Uniform.lean +++ b/Mathlib/Analysis/Normed/Group/Uniform.lean @@ -21,7 +21,7 @@ groups. variable {𝓕 E F : Type*} -open Filter Function Metric Bornology +open Filter Function Metric Bornology Finset open scoped ENNReal NNReal Uniformity Pointwise Topology section SeminormedGroup @@ -187,15 +187,15 @@ theorem uniformContinuous_norm' : UniformContinuous (norm : E → ℝ) := theorem uniformContinuous_nnnorm' : UniformContinuous fun a : E => ‖a‖₊ := uniformContinuous_norm'.subtype_mk _ -end SeminormedGroup +namespace AntilipschitzWith -section SeminormedCommGroup +@[to_additive le_mul_norm_sub] +theorem le_mul_norm_div {K : ℝ≥0} {f : E → F} (hf : AntilipschitzWith K f) (x y : E) : + ‖x / y‖ ≤ K * ‖f x / f y‖ := by simp [← dist_eq_norm_div, hf.le_mul_dist x y] -variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} +end AntilipschitzWith -@[to_additive] -instance NormedGroup.to_isIsometricSMul_left : IsIsometricSMul E E := - ⟨fun a => Isometry.of_dist_eq fun b c => by simp [dist_eq_norm_div]⟩ +variable [IsIsometricSMul E E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} @[to_additive (attr := simp)] theorem dist_self_mul_right (a b : E) : dist a (a * b) = ‖b‖ := by @@ -237,8 +237,6 @@ theorem abs_dist_sub_le_dist_mul_mul (a₁ a₂ b₁ b₂ : E) : simpa only [dist_mul_left, dist_mul_right, dist_comm b₂] using abs_dist_sub_le (a₁ * a₂) (b₁ * b₂) (b₁ * a₂) -open Finset - @[to_additive] theorem nndist_mul_mul_le (a₁ a₂ b₁ b₂ : E) : nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂ := @@ -252,8 +250,7 @@ theorem edist_mul_mul_le (a₁ a₂ b₁ b₂ : E) : apply nndist_mul_mul_le section PseudoEMetricSpace -variable {α E : Type*} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K Kf Kg : ℝ≥0} - {f g : α → E} {s : Set α} +variable {α : Type*} [PseudoEMetricSpace α] {K Kf Kg : ℝ≥0} {f g : α → E} {s : Set α} @[to_additive (attr := simp)] lemma lipschitzWith_inv_iff : LipschitzWith K f⁻¹ ↔ LipschitzWith K f := by simp [LipschitzWith] @@ -343,17 +340,47 @@ theorem mul_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y) _ ≤ _ := le_trans (le_abs_self _) (abs_dist_sub_le_dist_mul_mul _ _ _ _) +end AntilipschitzWith +end PseudoEMetricSpace + +-- See note [lower instance priority] +@[to_additive] +instance (priority := 100) SeminormedGroup.to_lipschitzMul : LipschitzMul E := + ⟨⟨1 + 1, LipschitzWith.prod_fst.mul LipschitzWith.prod_snd⟩⟩ + +-- See note [lower instance priority] +/-- A seminormed group is a uniform group, i.e., multiplication and division are uniformly +continuous. -/ +@[to_additive /-- A seminormed group is a uniform additive group, i.e., addition and subtraction are +uniformly continuous. -/] +instance (priority := 100) SeminormedGroup.to_isUniformGroup : IsUniformGroup E := + ⟨(LipschitzWith.prod_fst.div LipschitzWith.prod_snd).uniformContinuous⟩ + +-- short-circuit type class inference +-- See note [lower instance priority] +@[to_additive] +instance (priority := 100) SeminormedGroup.toIsTopologicalGroup : IsTopologicalGroup E := + inferInstance + +end SeminormedGroup + +section SeminormedCommGroup +variable [SeminormedCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ} + +-- See note [lower instance priority] +@[to_additive] +instance (priority := 100) NormedGroup.to_isIsometricSMul_left : IsIsometricSMul E E := + ⟨fun a => Isometry.of_dist_eq fun b c => by simp [dist_eq_norm_div]⟩ + +namespace AntilipschitzWith +variable {α : Type*} [PseudoEMetricSpace α] {Kf Kg : ℝ≥0} {f g : α → E} + @[to_additive] theorem mul_div_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f)) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g := by simpa only [Pi.div_apply, mul_div_cancel] using hf.mul_lipschitzWith hg hK -@[to_additive le_mul_norm_sub] -theorem le_mul_norm_div {f : E → F} (hf : AntilipschitzWith K f) (x y : E) : - ‖x / y‖ ≤ K * ‖f x / f y‖ := by simp [← dist_eq_norm_div, hf.le_mul_dist x y] - end AntilipschitzWith -end PseudoEMetricSpace -- See note [lower instance priority] @[to_additive] diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean index 35bc8db580ab34..04d446d9e0b751 100644 --- a/Mathlib/GroupTheory/GroupAction/Quotient.lean +++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean @@ -264,10 +264,12 @@ theorem sum_card_fixedBy_eq_card_orbits_mul_card_group [Fintype α] [∀ a : α, @[to_additive] instance isPretransitive_quotient (G) [Group G] (H : Subgroup G) : IsPretransitive G (G ⧸ H) where - exists_smul_eq := by - { rintro ⟨x⟩ ⟨y⟩ - refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩ - simp only [smul_eq_mul, H.one_mem, inv_mul_cancel, inv_mul_cancel_right]} + exists_smul_eq := by rintro ⟨x⟩ ⟨y⟩; exact ⟨y * x⁻¹, QuotientGroup.eq.mpr <| by simp⟩ + +@[to_additive] +instance isPretransitive_mulOpposite_quotient (G) [Group G] (H : Subgroup G) [H.Normal] : + IsPretransitive Gᵐᵒᵖ (G ⧸ H) where + exists_smul_eq := by rintro ⟨x⟩ ⟨y⟩; exact ⟨.op <| x⁻¹ * y, QuotientGroup.eq.mpr <| by simp⟩ variable {α} diff --git a/Mathlib/Topology/Algebra/ConstMulAction.lean b/Mathlib/Topology/Algebra/ConstMulAction.lean index 43b7bb081f648f..08739ff5affe13 100644 --- a/Mathlib/Topology/Algebra/ConstMulAction.lean +++ b/Mathlib/Topology/Algebra/ConstMulAction.lean @@ -202,6 +202,10 @@ theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} (c : G) Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) := ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul c⁻¹, fun h => h.const_smul _⟩ +@[to_additive] +instance Subgroup.continuousConstSMul {S : Subgroup G} : ContinuousConstSMul S α := + IsInducing.id.continuousConstSMul Subtype.val rfl + variable [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} @[to_additive] diff --git a/Mathlib/Topology/Algebra/Group/Quotient.lean b/Mathlib/Topology/Algebra/Group/Quotient.lean index 16e5b79502ece2..b754871bad6f93 100644 --- a/Mathlib/Topology/Algebra/Group/Quotient.lean +++ b/Mathlib/Topology/Algebra/Group/Quotient.lean @@ -24,7 +24,7 @@ assert_not_exists Cardinal open Topology open scoped Pointwise -variable {G : Type*} [TopologicalSpace G] [Group G] +variable {G M : Type*} [TopologicalSpace G] [Group G] [TopologicalSpace M] [Monoid M] namespace QuotientGroup @@ -44,9 +44,8 @@ theorem isQuotientMap_mk (N : Subgroup G) : IsQuotientMap (mk : G → G ⧸ N) : theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) := continuous_quot_mk -section ContinuousMul - -variable [ContinuousMul G] {N : Subgroup G} +section ContinuousMulConst +variable [ContinuousConstSMul Gᵐᵒᵖ G] {N : Subgroup G} @[to_additive] theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) := isOpenMap_quotient_mk'_mul @@ -65,24 +64,42 @@ theorem dense_image_mk {s : Set G} : 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 +instance instContinuousConstSMul [MulAction M G] [ContinuousConstSMul M G] + [MulAction.QuotientAction M N] : ContinuousConstSMul M (G ⧸ N) where + continuous_const_smul m := by + rw [← isOpenQuotientMap_mk.continuous_comp_iff] + exact continuous_mk.comp (continuous_const_smul _) + +variable (N) in +/-- 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 instContinuousConstSMul : ContinuousConstSMul G (G ⧸ N) := inferInstance +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 + +variable [ContinuousConstSMul G G] @[to_additive] -theorem t1Space_iff : - T1Space (G ⧸ N) ↔ IsClosed (N : Set G) := by +theorem t1Space_iff : T1Space (G ⧸ N) ↔ IsClosed (N : Set G) := by rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.t1Space_iff G (mk 1), - isClosed_coinduced] + isClosed_coinduced] rfl @[to_additive] -theorem discreteTopology_iff : - DiscreteTopology (G ⧸ N) ↔ IsOpen (N : Set G) := by +theorem discreteTopology_iff : DiscreteTopology (G ⧸ N) ↔ IsOpen (N : Set G) := by rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.discreteTopology_iff G (mk 1), isOpen_coinduced] rfl @@ -118,26 +135,16 @@ instance instLocallyCompactSpace [LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N) := QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace -variable (N) +end ContinuousMulConst -/-- 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 +section ContinuousMul +variable [ContinuousMul G] {N : Subgroup G} @[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 +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 end ContinuousMul diff --git a/Mathlib/Topology/Bornology/BoundedOperation.lean b/Mathlib/Topology/Bornology/BoundedOperation.lean index d850dbbbe25cc1..045e5048f27e27 100644 --- a/Mathlib/Topology/Bornology/BoundedOperation.lean +++ b/Mathlib/Topology/Bornology/BoundedOperation.lean @@ -156,8 +156,8 @@ variable {R : Type*} [SeminormedAddCommGroup R] lemma SeminormedAddCommGroup.lipschitzWith_sub : LipschitzWith 2 (fun (p : R × R) ↦ p.1 - p.2) := by - convert LipschitzWith.prod_fst.sub LipschitzWith.prod_snd - norm_num + rw [← one_add_one_eq_two] + exact LipschitzWith.prod_fst.sub LipschitzWith.prod_snd instance : BoundedSub R := boundedSub_of_lipschitzWith_sub SeminormedAddCommGroup.lipschitzWith_sub