feat: add units.embedding_val₀ (#2590)

Forward-port #18536 * [`group_theory.subgroup.basic`@`1f0096e6caa61e9c849ec2adbd227e960e9dff58`..`c10e724be91096453ee3db13862b9fb9a992fef2`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/subgroup/basic?range=1f0096e6caa61e9c849ec2adbd227e960e9dff58..c10e724be91096453ee3db13862b9fb9a992fef2) * [`group_theory.subgroup.pointwise`@`59694bd07f0a39c5beccba34bd9f413a160782bf`..`c10e724be91096453ee3db13862b9fb9a992fef2`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/subgroup/pointwise?range=59694bd07f0a39c5beccba34bd9f413a160782bf..c10e724be91096453ee3db13862b9fb9a992fef2) * [`topology.algebra.constructions`@`d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46`..`c10e724be91096453ee3db13862b9fb9a992fef2`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/constructions?range=d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46..c10e724be91096453ee3db13862b9fb9a992fef2) * [`topology.algebra.group.basic`@`dc6c365e751e34d100e80fe6e314c3c3e0fd2988`..`c10e724be91096453ee3db13862b9fb9a992fef2`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/group/basic?range=dc6c365e751e34d100e80fe6e314c3c3e0fd2988..c10e724be91096453ee3db13862b9fb9a992fef2) * [`topology.algebra.group_with_zero`@`48085f140e684306f9e7da907cd5932056d1aded`..`c10e724be91096453ee3db13862b9fb9a992fef2`](https://leanprover-community.github.io/mathlib-port-status/file/topology/algebra/group_with_zero?range=48085f140e684306f9e7da907cd5932056d1aded..c10e724be91096453ee3db13862b9fb9a992fef2)
leanprover-community · Mar 3, 2023 · 3155a57 · 3155a57
1 parent f03c0dc
commit 3155a57
Show file tree

Hide file tree

Showing 6 changed files with 67 additions and 21 deletions.
diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean
@@ -189,10 +189,10 @@ theorem index_eq_two_iff : H.index = 2 ↔ ∃ a, ∀ b, Xor' (b * a ∈ H) (b
   refine'
     exists_congr fun a => ⟨fun ha b => ⟨fun hba hb => _, fun hb => _⟩, fun ha => ⟨_, fun b hb => _⟩⟩
   · exact ha.1 ((mul_mem_cancel_left hb).1 hba)
-  · exact inv_inv b ▸ ha.2 _ (mt inv_mem_iff.1 hb)
-  · rw [← inv_mem_iff, ← ha, inv_mul_self]
+  · exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)
+  · rw [← inv_mem_iff (x := a), ← ha, inv_mul_self]
     exact one_mem _
-  · rwa [ha, inv_mem_iff]
+  · rwa [ha, inv_mem_iff (x := b)]
 #align subgroup.index_eq_two_iff Subgroup.index_eq_two_iff
 #align add_subgroup.index_eq_two_iff AddSubgroup.index_eq_two_iff
 

diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying
 
 ! This file was ported from Lean 3 source module group_theory.subgroup.basic
-! leanprover-community/mathlib commit 1f0096e6caa61e9c849ec2adbd227e960e9dff58
+! leanprover-community/mathlib commit c10e724be91096453ee3db13862b9fb9a992fef2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -127,6 +127,13 @@ class AddSubgroupClass (S G : Type _) [SubNegMonoid G] [SetLike S G] extends Add
 
 attribute [to_additive] InvMemClass SubgroupClass
 
+@[to_additive (attr := simp)]
+theorem inv_mem_iff {S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G] {H : S}
+    {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
+  ⟨fun h => inv_inv x ▸ inv_mem h, inv_mem⟩
+#align inv_mem_iff inv_mem_iff
+#align neg_mem_iff neg_mem_iff
+
 variable {M S : Type _} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {H K : S}
 
 /-- A subgroup is closed under division. -/
@@ -149,15 +156,9 @@ theorem zpow_mem {x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
 
 variable [SetLike S G] [SubgroupClass S G]
 
-@[to_additive (attr := simp)]
-theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
-  ⟨fun h => inv_inv x ▸ inv_mem h, inv_mem⟩
-#align inv_mem_iff inv_mem_iff
-#align neg_mem_iff neg_mem_iff
-
 @[to_additive]
-theorem div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H := by
-  rw [← inv_mem_iff, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, inv_inv]
+theorem div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
+  inv_div b a ▸ inv_mem_iff
 #align div_mem_comm_iff div_mem_comm_iff
 #align sub_mem_comm_iff sub_mem_comm_iff
 
@@ -2170,7 +2171,7 @@ theorem mem_normalizer_iff {g : G} : g ∈ H.normalizer ↔ ∀ h, h ∈ H ↔ g
 
 @[to_additive]
 theorem mem_normalizer_iff'' {g : G} : g ∈ H.normalizer ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H := by
-  rw [← inv_mem_iff, mem_normalizer_iff, inv_inv]
+  rw [← inv_mem_iff (x := g), mem_normalizer_iff, inv_inv]
 #align subgroup.mem_normalizer_iff'' Subgroup.mem_normalizer_iff''
 #align add_subgroup.mem_normalizer_iff'' AddSubgroup.mem_normalizer_iff''
 

diff --git a/Mathlib/GroupTheory/Subgroup/Pointwise.lean b/Mathlib/GroupTheory/Subgroup/Pointwise.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module group_theory.subgroup.pointwise
-! leanprover-community/mathlib commit 59694bd07f0a39c5beccba34bd9f413a160782bf
+! leanprover-community/mathlib commit c10e724be91096453ee3db13862b9fb9a992fef2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -34,15 +34,16 @@ open Set
 
 open Pointwise
 
-variable {α G A S : Type _} [Group G] [AddGroup A] {s : Set G}
+variable {α G A S : Type _}
 
 @[to_additive (attr := simp)]
-theorem inv_coe_set [SetLike S G] [SubgroupClass S G] {H : S} : (H : Set G)⁻¹ = H := by
-  ext
-  simp
+theorem inv_coe_set [InvolutiveInv G] [SetLike S G] [InvMemClass S G] {H : S} : (H : Set G)⁻¹ = H :=
+  Set.ext fun _ => inv_mem_iff
 #align inv_coe_set inv_coe_set
 #align neg_coe_set neg_coe_set
 
+variable [Group G] [AddGroup A] {s : Set G}
+
 namespace Subgroup
 
 @[to_additive (attr := simp)]

diff --git a/Mathlib/Topology/Algebra/Constructions.lean b/Mathlib/Topology/Algebra/Constructions.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri
 
 ! This file was ported from Lean 3 source module topology.algebra.constructions
-! leanprover-community/mathlib commit d90e4e186f1d18e375dcd4e5b5f6364b01cb3e46
+! leanprover-community/mathlib commit c10e724be91096453ee3db13862b9fb9a992fef2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -112,6 +112,29 @@ theorem embedding_embedProduct : Embedding (embedProduct M) :=
 #align units.embedding_embed_product Units.embedding_embedProduct
 #align add_units.embedding_embed_product AddUnits.embedding_embedProduct
 
+@[to_additive] lemma topology_eq_inf :
+    instTopologicalSpaceUnits =
+      .induced (val : Mˣ → M) ‹_› ⊓ .induced (fun u ↦ ↑u⁻¹ : Mˣ → M) ‹_› := by
+  simp only [inducing_embedProduct.1, instTopologicalSpaceProd, induced_inf,
+    instTopologicalSpaceMulOpposite, induced_compose]; rfl
+#align units.topology_eq_inf Units.topology_eq_inf
+#align add_units.topology_eq_inf AddUnits.topology_eq_inf
+
+/-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding.
+Use `Units.embedding_val₀`, `Units.embedding_val`, or `toUnits_homeomorph` instead. -/
+@[to_additive "An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a
+topological embedding. Use `AddUnits.embedding_val` or `toAddUnits_homeomorph` instead."]
+lemma embedding_val_mk {M : Type _} [DivisionMonoid M] [TopologicalSpace M]
+    (h : ContinuousOn Inv.inv {x : M | IsUnit x}) : Embedding (val : Mˣ → M) := by
+  refine ⟨⟨?_⟩, ext⟩
+  rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced,
+    @continuous_iff_continuousAt _ _ (.induced _ _)]
+  intros u s hs
+  simp only [val_inv_eq_inv_val, nhds_induced, Filter.mem_map] at hs ⊢
+  exact ⟨_, mem_inf_principal.1 (h u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩
+#align units.embedding_coe_mk Units.embedding_val_mk
+#align add_units.embedding_coe_mk AddUnits.embedding_val_mk
+
 @[to_additive]
 theorem continuous_embedProduct : Continuous (embedProduct M) :=
   continuous_induced_dom

diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 
 ! This file was ported from Lean 3 source module topology.algebra.group.basic
-! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
+! leanprover-community/mathlib commit c10e724be91096453ee3db13862b9fb9a992fef2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1730,6 +1730,20 @@ instance QuotientGroup.secondCountableTopology [SecondCountableTopology G] :
 
 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."]
+def toUnits_homeomorph [Group G] [TopologicalSpace G] [ContinuousInv G] : G ≃ₜ Gˣ where
+  toEquiv := toUnits.toEquiv
+  continuous_toFun := Units.continuous_iff.2 ⟨continuous_id, continuous_inv⟩
+  continuous_invFun := Units.continuous_val
+#align to_units_homeomorph toUnits_homeomorph
+#align to_add_units_homeomorph toAddUnits_homeomorph
+
+@[to_additive] theorem Units.embedding_val [Group G] [TopologicalSpace G] [ContinuousInv G] :
+    Embedding (val : Gˣ → G) :=
+  toUnits_homeomorph.symm.embedding
+
 namespace Units
 
 open MulOpposite (continuous_op continuous_unop)

diff --git a/Mathlib/Topology/Algebra/GroupWithZero.lean b/Mathlib/Topology/Algebra/GroupWithZero.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 
 ! This file was ported from Lean 3 source module topology.algebra.group_with_zero
-! leanprover-community/mathlib commit 48085f140e684306f9e7da907cd5932056d1aded
+! leanprover-community/mathlib commit c10e724be91096453ee3db13862b9fb9a992fef2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -142,6 +142,13 @@ theorem ContinuousOn.inv₀ (hf : ContinuousOn f s) (h0 : ∀ x ∈ s, f x ≠ 0
 
 end Inv₀
 
+/-- If `G₀` is a group with zero with topology such that `x ↦ x⁻¹` is continuous at all nonzero
+points. Then the coercion `G₀ˣ → G₀` is a topological embedding. -/
+theorem Units.embedding_val₀ [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] :
+    Embedding (val : G₀ˣ → G₀) :=
+  embedding_val_mk <| (continuousOn_inv₀ (G₀ := G₀)).mono <| fun _ ↦ IsUnit.ne_zero
+#align units.embedding_coe₀ Units.embedding_val₀
+
 /-!
 ### Continuity of division