feat(GroupTheory/Submonoid): add opposite submonoids (#7415)

We already have API for the multiplicative opposite of subgroups.

This tidies the API for subgroups by introducing separate `.op` and `.unop` definitions (as dot notation on `.opposite` worked in Lean 3 but not Lean 4), and adds the same API for submonoids.

Mathlib.lean

@@ -2110,6 +2110,7 @@ import Mathlib.GroupTheory.Submonoid.Center
 import Mathlib.GroupTheory.Submonoid.Centralizer
 import Mathlib.GroupTheory.Submonoid.Inverses
 import Mathlib.GroupTheory.Submonoid.Membership
+import Mathlib.GroupTheory.Submonoid.MulOpposite
 import Mathlib.GroupTheory.Submonoid.Operations
 import Mathlib.GroupTheory.Submonoid.Pointwise
 import Mathlib.GroupTheory.Submonoid.ZeroDivisors

Mathlib/GroupTheory/Coset.lean

@@ -311,7 +311,7 @@ of a subgroup.-/
 @[to_additive "The equivalence relation corresponding to the partition of a group by left cosets
  of a subgroup."]
 def leftRel : Setoid α :=
-  MulAction.orbitRel (Subgroup.opposite s) α
+  MulAction.orbitRel s.op α
 #align quotient_group.left_rel QuotientGroup.leftRel
 #align quotient_add_group.left_rel QuotientAddGroup.leftRel
 
@@ -320,8 +320,8 @@ variable {s}
 @[to_additive]
 theorem leftRel_apply {x y : α} : @Setoid.r _ (leftRel s) x y ↔ x⁻¹ * y ∈ s :=
   calc
-    (∃ a : Subgroup.opposite s, y * MulOpposite.unop a = x) ↔ ∃ a : s, y * a = x :=
-      s.oppositeEquiv.symm.exists_congr_left
+    (∃ a : s.op, y * MulOpposite.unop a = x) ↔ ∃ a : s, y * a = x :=
+      s.equivOp.symm.exists_congr_left
     _ ↔ ∃ a : s, x⁻¹ * y = a⁻¹ :=
       by simp only [inv_mul_eq_iff_eq_mul, Subgroup.coe_inv, eq_mul_inv_iff_mul_eq]
     _ ↔ x⁻¹ * y ∈ s := by simp [exists_inv_mem_iff_exists_mem]

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -65,7 +65,7 @@ instance left_quotientAction : QuotientAction α H :=
 #align add_action.left_quotient_action AddAction.left_quotientAction
 
 @[to_additive]
-instance right_quotientAction : QuotientAction (opposite (normalizer H)) H :=
+instance right_quotientAction : QuotientAction (normalizer H).op H :=
   ⟨fun b c _ _ => by
     rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
       mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]⟩

Mathlib/GroupTheory/Subgroup/MulOpposite.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex Kontorovich
 -/
 import Mathlib.GroupTheory.Subgroup.Actions
+import Mathlib.GroupTheory.Submonoid.MulOpposite
 
 #align_import group_theory.subgroup.mul_opposite from "leanprover-community/mathlib"@"f93c11933efbc3c2f0299e47b8ff83e9b539cbf6"
 
@@ -20,44 +21,61 @@ variable {G : Type*} [Group G]
 
 namespace Subgroup
 
-/-- A subgroup `H` of `G` determines a subgroup `H.opposite` of the opposite group `Gᵐᵒᵖ`. -/
-@[to_additive "An additive subgroup `H` of `G` determines an additive subgroup `H.opposite` of the
- opposite additive group `Gᵃᵒᵖ`."]
-def opposite : Subgroup G ≃ Subgroup Gᵐᵒᵖ
-    where
-  toFun H :=
-    { carrier := MulOpposite.unop ⁻¹' (H : Set G)
-      one_mem' := H.one_mem
-      mul_mem' := fun ha hb => H.mul_mem hb ha
-      inv_mem' := H.inv_mem }
-  invFun H :=
-    { carrier := MulOpposite.op ⁻¹' (H : Set Gᵐᵒᵖ)
-      one_mem' := H.one_mem
-      mul_mem' := fun ha hb => H.mul_mem hb ha
-      inv_mem' := H.inv_mem }
+/-- Pull a subgroup back to an opposite subgroup along `MulOpposite.unop`-/
+@[to_additive (attr := simps)
+"Pull an additive subgroup back to an opposite additive subgroup along `AddOpposite.unop`"]
+protected def op (H : Subgroup G) : Subgroup Gᵐᵒᵖ where
+  carrier := MulOpposite.unop ⁻¹' (H : Set G)
+  one_mem' := H.one_mem
+  mul_mem' ha hb := H.mul_mem hb ha
+  inv_mem' := H.inv_mem
+
+/-- Pull an opposite subgroup back to a subgroup along `MulOpposite.op`-/
+@[to_additive (attr := simps)
+"Pull an opposite additive subgroup back to an additive subgroup along `AddOpposite.op`"]
+protected def unop (H : Subgroup Gᵐᵒᵖ) : Subgroup G where
+  carrier := MulOpposite.op ⁻¹' (H : Set Gᵐᵒᵖ)
+  one_mem' := H.one_mem
+  mul_mem' := fun ha hb => H.mul_mem hb ha
+  inv_mem' := H.inv_mem
+
+@[to_additive (attr := simp, nolint simpNF)] lemma op_toSubmonoid (H : Subgroup G) :
+    H.op.toSubmonoid = H.toSubmonoid.op :=
+  rfl
+
+@[to_additive (attr := simp, nolint simpNF)] lemma unop_toSubmonoid (H : Subgroup Gᵐᵒᵖ) :
+    H.unop.toSubmonoid = H.toSubmonoid.unop :=
+  rfl
+
+/-- A subgroup `H` of `G` determines a subgroup `H.op` of the opposite group `Gᵐᵒᵖ`. -/
+@[to_additive (attr := simps) "An additive subgroup `H` of `G` determines an additive subgroup
+`H.op` of the opposite additive group `Gᵃᵒᵖ`."]
+def opEquiv : Subgroup G ≃ Subgroup Gᵐᵒᵖ where
+  toFun := Subgroup.op
+  invFun := Subgroup.unop
   left_inv _ := SetLike.coe_injective rfl
   right_inv _ := SetLike.coe_injective rfl
-#align subgroup.opposite Subgroup.opposite
-#align add_subgroup.opposite AddSubgroup.opposite
+#align subgroup.opposite Subgroup.opEquiv
+#align add_subgroup.opposite AddSubgroup.opEquiv
 
 /-- Bijection between a subgroup `H` and its opposite. -/
 @[to_additive (attr := simps!) "Bijection between an additive subgroup `H` and its opposite."]
-def oppositeEquiv (H : Subgroup G) : H ≃ opposite H :=
+def equivOp (H : Subgroup G) : H ≃ H.op :=
   MulOpposite.opEquiv.subtypeEquiv fun _ => Iff.rfl
-#align subgroup.opposite_equiv Subgroup.oppositeEquiv
-#align add_subgroup.opposite_equiv AddSubgroup.oppositeEquiv
-#align subgroup.opposite_equiv_symm_apply_coe Subgroup.oppositeEquiv_symm_apply_coe
+#align subgroup.opposite_equiv Subgroup.equivOp
+#align add_subgroup.opposite_equiv AddSubgroup.equivOp
+#align subgroup.opposite_equiv_symm_apply_coe Subgroup.equivOp_symm_apply_coe
 
 @[to_additive]
-instance (H : Subgroup G) [Encodable H] : Encodable (opposite H) :=
-  Encodable.ofEquiv H H.oppositeEquiv.symm
+instance (H : Subgroup G) [Encodable H] : Encodable H.op :=
+  Encodable.ofEquiv H H.equivOp.symm
 
 @[to_additive]
-instance (H : Subgroup G) [Countable H] : Countable (opposite H) :=
-  Countable.of_equiv H H.oppositeEquiv
+instance (H : Subgroup G) [Countable H] : Countable H.op :=
+  Countable.of_equiv H H.equivOp
 
 @[to_additive]
-theorem smul_opposite_mul {H : Subgroup G} (x g : G) (h : opposite H) :
+theorem smul_opposite_mul {H : Subgroup G} (x g : G) (h : H.op) :
     h • (g * x) = g * h • x :=
   mul_assoc _ _ _
 #align subgroup.smul_opposite_mul Subgroup.smul_opposite_mul

Mathlib/GroupTheory/Subgroup/Pointwise.lean

@@ -240,7 +240,7 @@ theorem smul_opposite_image_mul_preimage' (g : G) (h : Gᵐᵒᵖ) (s : Set G) :
 
 -- porting note: deprecate?
 @[to_additive]
-theorem smul_opposite_image_mul_preimage {H : Subgroup G} (g : G) (h : opposite H) (s : Set G) :
+theorem smul_opposite_image_mul_preimage {H : Subgroup G} (g : G) (h : H.op) (s : Set G) :
     (fun y => h • y) '' ((g * ·) ⁻¹' s) = (g * ·) ⁻¹' ((fun y => h • y) '' s) :=
   smul_opposite_image_mul_preimage' g h s
 #align subgroup.smul_opposite_image_mul_preimage Subgroup.smul_opposite_image_mul_preimage

Mathlib/GroupTheory/Submonoid/MulOpposite.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser, Jujian Zhang
+-/
+import Mathlib.GroupTheory.Submonoid.Basic
+import Mathlib.Algebra.Group.Opposite
+
+/-!
+# Submonoid of opposite monoids
+
+For every monoid `M`, we construct an equivalence between submonoids of `M` and that of `Mᵐᵒᵖ`.
+
+-/
+
+variable {M : Type*} [MulOneClass M]
+
+namespace Submonoid
+
+/-- Pull a submonoid back to an opposite submonoid along `MulOpposite.unop`-/
+@[to_additive (attr := simps) "Pull an additive submonoid back to an opposite submonoid along
+`AddOpposite.unop`"]
+protected def op {M : Type*} [MulOneClass M] (x : Submonoid M) : Submonoid (MulOpposite M) where
+  carrier := MulOpposite.unop ⁻¹' x.1
+  mul_mem' ha hb := x.mul_mem hb ha
+  one_mem' := Submonoid.one_mem' _
+
+/-- Pull an opposite submonoid back to a submonoid along `MulOpposite.op`-/
+@[to_additive (attr := simps) "Pull an opposite additive submonoid back to a submonoid along
+`AddOpposite.op`"]
+protected def unop {M : Type*} [MulOneClass M] (x : Submonoid (MulOpposite M)) : Submonoid M where
+  carrier := MulOpposite.op ⁻¹' x.1
+  mul_mem' ha hb := x.mul_mem hb ha
+  one_mem' := Submonoid.one_mem' _
+
+/-- A submonoid `H` of `G` determines a submonoid `H.op` of the opposite group `Gᵐᵒᵖ`. -/
+@[to_additive (attr := simps) "A additive submonoid `H` of `G` determines an additive submonoid
+`H.op` of the opposite group `Gᵐᵒᵖ`."]
+def opEquiv : Submonoid M ≃ Submonoid Mᵐᵒᵖ where
+  toFun := Submonoid.op
+  invFun := Submonoid.unop
+  left_inv _ := SetLike.coe_injective rfl
+  right_inv _ := SetLike.coe_injective rfl
+
+/-- Bijection between a submonoid `H` and its opposite. -/
+@[to_additive (attr := simps!) "Bijection between an additive submonoid `H` and its opposite."]
+def equivOp (H : Submonoid M) : H ≃ H.op :=
+  MulOpposite.opEquiv.subtypeEquiv fun _ => Iff.rfl
+
+end Submonoid

Mathlib/MeasureTheory/Integral/Periodic.lean

@@ -56,11 +56,11 @@ theorem isAddFundamentalDomain_Ioc {T : ℝ} (hT : 0 < T) (t : ℝ)
 #align is_add_fundamental_domain_Ioc isAddFundamentalDomain_Ioc
 
 theorem isAddFundamentalDomain_Ioc' {T : ℝ} (hT : 0 < T) (t : ℝ) (μ : Measure ℝ := by volume_tac) :
-    IsAddFundamentalDomain (AddSubgroup.opposite <| .zmultiples T) (Ioc t (t + T)) μ := by
+    IsAddFundamentalDomain (AddSubgroup.op <| .zmultiples T) (Ioc t (t + T)) μ := by
   refine' IsAddFundamentalDomain.mk' measurableSet_Ioc.nullMeasurableSet fun x => _
   have : Bijective (codRestrict (fun n : ℤ => n • T) (AddSubgroup.zmultiples T) _) :=
     (Equiv.ofInjective (fun n : ℤ => n • T) (zsmul_strictMono_left hT).injective).bijective
-  refine' (AddSubgroup.oppositeEquiv _).bijective.comp this |>.existsUnique_iff.2 _
+  refine' (AddSubgroup.equivOp _).bijective.comp this |>.existsUnique_iff.2 _
   simpa using existsUnique_add_zsmul_mem_Ioc hT x t
 #align is_add_fundamental_domain_Ioc' isAddFundamentalDomain_Ioc'
 

Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

@@ -49,7 +49,7 @@ instance QuotientGroup.measurableSMul [MeasurableSpace (G ⧸ Γ)] [BorelSpace (
 #align quotient_group.has_measurable_smul QuotientGroup.measurableSMul
 #align quotient_add_group.has_measurable_vadd QuotientAddGroup.measurableVAdd
 
-variable {𝓕 : Set G} (h𝓕 : IsFundamentalDomain (Subgroup.opposite Γ) 𝓕 μ)
+variable {𝓕 : Set G} (h𝓕 : IsFundamentalDomain Γ.op 𝓕 μ)
 
 variable [Countable Γ] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)]
 
@@ -80,7 +80,7 @@ theorem MeasureTheory.IsFundamentalDomain.smulInvariantMeasure_map [μ.IsMulLeft
         simp [Set.preimage]
       rw [measure_preimage_mul]
     rw [this]
-    have h𝓕_translate_fundom : IsFundamentalDomain (Subgroup.opposite Γ) (g • 𝓕) μ :=
+    have h𝓕_translate_fundom : IsFundamentalDomain Γ.op (g • 𝓕) μ :=
       h𝓕.smul_of_comm g
     rw [h𝓕.measure_set_eq h𝓕_translate_fundom meas_πA, ← preimage_smul_inv]; rfl
     rintro ⟨γ, γ_in_Γ⟩
@@ -217,9 +217,9 @@ lemma QuotientGroup.integral_eq_integral_automorphize {E : Type*} [NormedAddComm
     [NormedSpace ℝ E] [μ.IsMulRightInvariant] {f : G → E}
     (hf₁ : Integrable f μ) (hf₂ : AEStronglyMeasurable (automorphize f) μ_𝓕) :
     ∫ x : G, f x ∂μ = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 := by
-  calc ∫ x : G, f x ∂μ = ∑' γ : (Subgroup.opposite Γ), ∫ x in 𝓕, f (γ • x) ∂μ :=
+  calc ∫ x : G, f x ∂μ = ∑' γ : Γ.op, ∫ x in 𝓕, f (γ • x) ∂μ :=
     h𝓕.integral_eq_tsum'' f hf₁
-    _ = ∫ x in 𝓕, ∑' γ : (Subgroup.opposite Γ), f (γ • x) ∂μ := ?_
+    _ = ∫ x in 𝓕, ∑' γ : Γ.op, f (γ • x) ∂μ := ?_
     _ = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 :=
       (integral_map continuous_quotient_mk'.aemeasurable hf₂).symm
   rw [integral_tsum]
@@ -282,7 +282,7 @@ lemma QuotientAddGroup.integral_mul_eq_integral_automorphize_mul {K : Type*} [No
     (f_ℒ_1 : Integrable f μ') {g : G' ⧸ Γ' → K} (hg : AEStronglyMeasurable g μ_𝓕)
     (g_ℒ_infinity : essSup (fun x ↦ (‖g x‖₊ : ℝ≥0∞)) μ_𝓕 ≠ ∞)
     (F_ae_measurable : AEStronglyMeasurable (QuotientAddGroup.automorphize f) μ_𝓕)
-    (h𝓕 : IsAddFundamentalDomain (AddSubgroup.opposite Γ') 𝓕' μ') :
+    (h𝓕 : IsAddFundamentalDomain Γ'.op 𝓕' μ') :
     ∫ x : G', g (x : G' ⧸ Γ') * (f x) ∂μ'
       = ∫ x : G' ⧸ Γ', g x * (QuotientAddGroup.automorphize f x) ∂μ_𝓕 := by
   let π : G' → G' ⧸ Γ' := QuotientAddGroup.mk

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -1569,14 +1569,14 @@ to show that the quotient group `G ⧸ S` is Hausdorff. -/
   If `G` is Hausdorff, this can be combined with `t2Space_of_properlyDiscontinuousVAdd_of_t2Space`
   to show that the quotient group `G ⧸ S` is Hausdorff."]
 theorem Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite (S : Subgroup G)
-    (hS : Tendsto S.subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul (opposite S) G :=
+    (hS : Tendsto S.subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul S.op G :=
   { finite_disjoint_inter_image := by
       intro K L hK hL
       have : Continuous fun p : G × G => (p.1⁻¹, p.2) := continuous_inv.prod_map continuous_id
       have H : Set.Finite _ :=
         hS ((hK.prod hL).image (continuous_mul.comp this)).compl_mem_cocompact
       simp only [preimage_compl, compl_compl, coeSubtype, comp_apply] at H
-      apply Finite.of_preimage _ (oppositeEquiv S).surjective
+      apply Finite.of_preimage _ (equivOp S).surjective
       convert H using 1
       ext x
       simp only [image_smul, mem_setOf_eq, coeSubtype, mem_preimage, mem_image, Prod.exists]

Mathlib/Topology/Instances/AddCircle.lean

@@ -517,7 +517,7 @@ instance compactSpace [Fact (0 < p)] : CompactSpace <| AddCircle p := by
 
 /-- The action on `ℝ` by right multiplication of its the subgroup `zmultiples p` (the multiples of
 `p:ℝ`) is properly discontinuous. -/
-instance : ProperlyDiscontinuousVAdd (AddSubgroup.opposite (zmultiples p)) ℝ :=
+instance : ProperlyDiscontinuousVAdd (zmultiples p).op ℝ :=
   (zmultiples p).properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite
     (AddSubgroup.tendsto_zmultiples_subtype_cofinite p)