Skip to content

Commit c31d2fb

Browse files
sven-manthesven-manthe
committed
feat(Algebra): add Subsemigroup.op (#32428)
the file Subsemigroup.MulOpposite is analogous to Submonoid.MulOpposite. Also add trivial lemmas on relation with monoids and groups in the corresponding file
1 parent 2bf8d4b commit c31d2fb

File tree

4 files changed

+199
-4
lines changed

4 files changed

+199
-4
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -451,6 +451,7 @@ public import Mathlib.Algebra.Group.Submonoid.Units
451451
public import Mathlib.Algebra.Group.Subsemigroup.Basic
452452
public import Mathlib.Algebra.Group.Subsemigroup.Defs
453453
public import Mathlib.Algebra.Group.Subsemigroup.Membership
454+
public import Mathlib.Algebra.Group.Subsemigroup.MulOpposite
454455
public import Mathlib.Algebra.Group.Subsemigroup.Operations
455456
public import Mathlib.Algebra.Group.Support
456457
public import Mathlib.Algebra.Group.Torsion

‎Mathlib/Algebra/Group/Subgroup/MulOpposite.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,10 @@ theorem mem_op {x : Gᵐᵒᵖ} {S : Subgroup G} : x ∈ S.op ↔ x.unop ∈ S :
3838
H.op.toSubmonoid = H.toSubmonoid.op :=
3939
rfl
4040

41+
@[to_additive] lemma op_toSubsemigroup (H : Subgroup G) :
42+
H.op.toSubsemigroup = H.toSubsemigroup.op := by
43+
dsimp
44+
4145
/-- Pull an opposite subgroup back to a subgroup along `MulOpposite.op` -/
4246
@[to_additive (attr := simps)
4347
/-- Pull an opposite additive subgroup back to an additive subgroup along `AddOpposite.op` -/]
@@ -54,6 +58,10 @@ theorem mem_unop {x : G} {S : Subgroup Gᵐᵒᵖ} : x ∈ S.unop ↔ MulOpposit
5458
H.unop.toSubmonoid = H.toSubmonoid.unop :=
5559
rfl
5660

61+
@[to_additive] lemma unop_toSubsemigroup (H : Subgroup Gᵐᵒᵖ) :
62+
H.unop.toSubsemigroup = H.toSubsemigroup.unop := by
63+
dsimp
64+
5765
@[to_additive (attr := simp)]
5866
theorem unop_op (S : Subgroup G) : S.op.unop = S := rfl
5967

‎Mathlib/Algebra/Group/Submonoid/MulOpposite.lean‎

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Eric Wieser, Jujian Zhang
55
-/
66
module
77

8-
public import Mathlib.Algebra.Group.Opposite
8+
public import Mathlib.Algebra.Group.Subsemigroup.MulOpposite
99
public import Mathlib.Algebra.Group.Submonoid.Basic
1010

1111
/-!
@@ -34,6 +34,10 @@ protected def op (x : Submonoid M) : Submonoid Mᵐᵒᵖ where
3434
@[to_additive (attr := simp)]
3535
theorem mem_op {x : Mᵐᵒᵖ} {S : Submonoid M} : x ∈ S.op ↔ x.unop ∈ S := Iff.rfl
3636

37+
@[to_additive (attr := simp)] lemma op_toSubsemigroup (H : Submonoid M) :
38+
H.op.toSubsemigroup = H.toSubsemigroup.op :=
39+
rfl
40+
3741
/-- Pull an opposite submonoid back to a submonoid along `MulOpposite.op` -/
3842
@[to_additive (attr := simps) /-- Pull an opposite additive submonoid back to a submonoid along
3943
`AddOpposite.op` -/]
@@ -45,6 +49,10 @@ protected def unop (x : Submonoid Mᵐᵒᵖ) : Submonoid M where
4549
@[to_additive (attr := simp)]
4650
theorem mem_unop {x : M} {S : Submonoid Mᵐᵒᵖ} : x ∈ S.unop ↔ MulOpposite.op x ∈ S := Iff.rfl
4751

52+
@[to_additive (attr := simp)] lemma unop_toSubsemigroup (H : Submonoid Mᵐᵒᵖ) :
53+
H.unop.toSubsemigroup = H.toSubsemigroup.unop :=
54+
rfl
55+
4856
@[to_additive (attr := simp)]
4957
theorem unop_op (S : Submonoid M) : S.op.unop = S := rfl
5058

@@ -69,9 +77,9 @@ theorem op_le_op_iff {S₁ S₂ : Submonoid M} : S₁.op ≤ S₂.op ↔ S₁
6977
theorem unop_le_unop_iff {S₁ S₂ : Submonoid Mᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂ :=
7078
MulOpposite.unop_surjective.forall
7179

72-
/-- A submonoid `H` of `G` determines a submonoid `H.op` of the opposite group `Gᵐᵒᵖ`. -/
73-
@[to_additive (attr := simps) /-- An additive submonoid `H` of `G` determines an additive submonoid
74-
`H.op` of the opposite group `Gᵐᵒᵖ`. -/]
80+
/-- A submonoid `H` of `M` determines a submonoid `H.op` of the opposite monoid `Mᵐᵒᵖ`. -/
81+
@[to_additive (attr := simps) /-- An additive submonoid `H` of `M` determines an additive submonoid
82+
`H.op` of the opposite monoid `Mᵐᵒᵖ`. -/]
7583
def opEquiv : Submonoid M ≃o Submonoid Mᵐᵒᵖ where
7684
toFun := Submonoid.op
7785
invFun := Submonoid.unop

‎Mathlib/Algebra/Group/Subsemigroup/MulOpposite.lean‎

Lines changed: 178 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,178 @@
1+
/-
2+
Copyright (c) 2025 Sven Manthe. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Sven Manthe
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.Group.Opposite
9+
public import Mathlib.Algebra.Group.Subsemigroup.Basic
10+
11+
/-!
12+
# Subsemigroup of opposite semigroups
13+
14+
For every semigroup `M`, we construct an equivalence between subsemigroups of `M` and that of
15+
`Mᵐᵒᵖ`.
16+
17+
-/
18+
19+
@[expose] public section
20+
21+
assert_not_exists MonoidWithZero
22+
23+
variable {ι : Sort*} {M : Type*} [Mul M]
24+
25+
namespace Subsemigroup
26+
27+
/-- Pull a subsemigroup back to an opposite subsemigroup along `MulOpposite.unop` -/
28+
@[to_additive (attr := simps) /-- Pull an additive subsemigroup back to an opposite subsemigroup
29+
along `AddOpposite.unop` -/]
30+
protected def op (x : Subsemigroup M) : Subsemigroup Mᵐᵒᵖ where
31+
carrier := MulOpposite.unop ⁻¹' x
32+
mul_mem' ha hb := x.mul_mem hb ha
33+
34+
@[to_additive (attr := simp)]
35+
theorem mem_op {x : Mᵐᵒᵖ} {S : Subsemigroup M} : x ∈ S.op ↔ x.unop ∈ S := Iff.rfl
36+
37+
/-- Pull an opposite subsemigroup back to a subsemigroup along `MulOpposite.op` -/
38+
@[to_additive (attr := simps) /-- Pull an opposite additive subsemigroup back to a subsemigroup
39+
along `AddOpposite.op` -/]
40+
protected def unop (x : Subsemigroup Mᵐᵒᵖ) : Subsemigroup M where
41+
carrier := MulOpposite.op ⁻¹' x
42+
mul_mem' ha hb := x.mul_mem hb ha
43+
44+
@[to_additive (attr := simp)]
45+
theorem mem_unop {x : M} {S : Subsemigroup Mᵐᵒᵖ} : x ∈ S.unop ↔ MulOpposite.op x ∈ S := Iff.rfl
46+
47+
@[to_additive (attr := simp)]
48+
theorem unop_op (S : Subsemigroup M) : S.op.unop = S := rfl
49+
50+
@[to_additive (attr := simp)]
51+
theorem op_unop (S : Subsemigroup Mᵐᵒᵖ) : S.unop.op = S := rfl
52+
53+
/-! ### Lattice results -/
54+
55+
@[to_additive]
56+
theorem op_le_iff {S₁ : Subsemigroup M} {S₂ : Subsemigroup Mᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop :=
57+
MulOpposite.op_surjective.forall
58+
59+
@[to_additive]
60+
theorem le_op_iff {S₁ : Subsemigroup Mᵐᵒᵖ} {S₂ : Subsemigroup M} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂ :=
61+
MulOpposite.op_surjective.forall
62+
63+
@[to_additive (attr := simp)]
64+
theorem op_le_op_iff {S₁ S₂ : Subsemigroup M} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂ :=
65+
MulOpposite.op_surjective.forall
66+
67+
@[to_additive (attr := simp)]
68+
theorem unop_le_unop_iff {S₁ S₂ : Subsemigroup Mᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂ :=
69+
MulOpposite.unop_surjective.forall
70+
71+
/-- A subsemigroup `H` of `M` determines a subsemigroup `H.op` of the opposite semigroup `Mᵐᵒᵖ`. -/
72+
@[to_additive (attr := simps) /-- An additive subsemigroup `H` of `M` determines an additive
73+
subsemigroup `H.op` of the opposite semigroup `Mᵐᵒᵖ`. -/]
74+
def opEquiv : Subsemigroup M ≃o Subsemigroup Mᵐᵒᵖ where
75+
toFun := Subsemigroup.op
76+
invFun := Subsemigroup.unop
77+
left_inv := unop_op
78+
right_inv := op_unop
79+
map_rel_iff' := op_le_op_iff
80+
81+
@[to_additive]
82+
theorem op_injective : (@Subsemigroup.op M _).Injective := opEquiv.injective
83+
84+
@[to_additive]
85+
theorem unop_injective : (@Subsemigroup.unop M _).Injective := opEquiv.symm.injective
86+
87+
@[to_additive (attr := simp)]
88+
theorem op_inj {S T : Subsemigroup M} : S.op = T.op ↔ S = T := opEquiv.eq_iff_eq
89+
90+
@[to_additive (attr := simp)]
91+
theorem unop_inj {S T : Subsemigroup Mᵐᵒᵖ} : S.unop = T.unop ↔ S = T := opEquiv.symm.eq_iff_eq
92+
93+
@[to_additive (attr := simp)]
94+
theorem op_bot : (⊥ : Subsemigroup M).op = ⊥ := opEquiv.map_bot
95+
96+
@[to_additive (attr := simp)]
97+
theorem op_eq_bot {S : Subsemigroup M} : S.op = ⊥ ↔ S = ⊥ := op_injective.eq_iff' op_bot
98+
99+
@[to_additive (attr := simp)]
100+
theorem unop_bot : (⊥ : Subsemigroup Mᵐᵒᵖ).unop = ⊥ := opEquiv.symm.map_bot
101+
102+
@[to_additive (attr := simp)]
103+
theorem unop_eq_bot {S : Subsemigroup Mᵐᵒᵖ} : S.unop = ⊥ ↔ S = ⊥ := unop_injective.eq_iff' unop_bot
104+
105+
@[to_additive (attr := simp)]
106+
theorem op_top : (⊤ : Subsemigroup M).op = ⊤ := rfl
107+
108+
@[to_additive (attr := simp)]
109+
theorem op_eq_top {S : Subsemigroup M} : S.op = ⊤ ↔ S = ⊤ := op_injective.eq_iff' op_top
110+
111+
@[to_additive (attr := simp)]
112+
theorem unop_top : (⊤ : Subsemigroup Mᵐᵒᵖ).unop = ⊤ := rfl
113+
114+
@[to_additive (attr := simp)]
115+
theorem unop_eq_top {S : Subsemigroup Mᵐᵒᵖ} : S.unop = ⊤ ↔ S = ⊤ := unop_injective.eq_iff' unop_top
116+
117+
@[to_additive]
118+
theorem op_sup (S₁ S₂ : Subsemigroup M) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op :=
119+
opEquiv.map_sup _ _
120+
121+
@[to_additive]
122+
theorem unop_sup (S₁ S₂ : Subsemigroup Mᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop :=
123+
opEquiv.symm.map_sup _ _
124+
125+
@[to_additive]
126+
theorem op_inf (S₁ S₂ : Subsemigroup M) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op := rfl
127+
128+
@[to_additive]
129+
theorem unop_inf (S₁ S₂ : Subsemigroup Mᵐᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop := rfl
130+
131+
@[to_additive]
132+
theorem op_sSup (S : Set (Subsemigroup M)) : (sSup S).op = sSup (.unop ⁻¹' S) :=
133+
opEquiv.map_sSup_eq_sSup_symm_preimage _
134+
135+
@[to_additive]
136+
theorem unop_sSup (S : Set (Subsemigroup Mᵐᵒᵖ)) : (sSup S).unop = sSup (.op ⁻¹' S) :=
137+
opEquiv.symm.map_sSup_eq_sSup_symm_preimage _
138+
139+
@[to_additive]
140+
theorem op_sInf (S : Set (Subsemigroup M)) : (sInf S).op = sInf (.unop ⁻¹' S) :=
141+
opEquiv.map_sInf_eq_sInf_symm_preimage _
142+
143+
@[to_additive]
144+
theorem unop_sInf (S : Set (Subsemigroup Mᵐᵒᵖ)) : (sInf S).unop = sInf (.op ⁻¹' S) :=
145+
opEquiv.symm.map_sInf_eq_sInf_symm_preimage _
146+
147+
@[to_additive]
148+
theorem op_iSup (S : ι → Subsemigroup M) : (iSup S).op = ⨆ i, (S i).op := opEquiv.map_iSup _
149+
150+
@[to_additive]
151+
theorem unop_iSup (S : ι → Subsemigroup Mᵐᵒᵖ) : (iSup S).unop = ⨆ i, (S i).unop :=
152+
opEquiv.symm.map_iSup _
153+
154+
@[to_additive]
155+
theorem op_iInf (S : ι → Subsemigroup M) : (iInf S).op = ⨅ i, (S i).op := opEquiv.map_iInf _
156+
157+
@[to_additive]
158+
theorem unop_iInf (S : ι → Subsemigroup Mᵐᵒᵖ) : (iInf S).unop = ⨅ i, (S i).unop :=
159+
opEquiv.symm.map_iInf _
160+
161+
@[to_additive]
162+
theorem op_closure (s : Set M) : (closure s).op = closure (MulOpposite.unop ⁻¹' s) := by
163+
simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Subsemigroup.coe_unop]
164+
congr with a
165+
exact MulOpposite.unop_surjective.forall
166+
167+
@[to_additive]
168+
theorem unop_closure (s : Set Mᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s) := by
169+
rw [← op_inj, op_unop, op_closure]
170+
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']
171+
172+
/-- Bijection between a subsemigroup `H` and its opposite. -/
173+
@[to_additive (attr := simps!) /-- Bijection between an additive subsemigroup `H` and its opposite.
174+
-/]
175+
def equivOp (H : Subsemigroup M) : H ≃ H.op :=
176+
MulOpposite.opEquiv.subtypeEquiv fun _ => Iff.rfl
177+
178+
end Subsemigroup

0 commit comments

Comments
 (0)