Skip to content

Commit c3a32e9

Browse files
ReemMelamedReemMelamed
committed
feat(Algebra/Group/GreensRelations): add definitions for Green's relations
1 parent 3eb1a69 commit c3a32e9

2 files changed

Lines changed: 317 additions & 0 deletions

File tree

‎Mathlib/Algebra/Group/GreensRelations/Basic.lean‎

Lines changed: 246 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,246 @@
1+
/-
2+
Copyright (c) 2026 Re'em Melamed-Katz. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Re'em Melamed-Katz
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.Group.GreensRelations.Defs
9+
public import Mathlib.Data.Setoid.Basic
10+
public import Mathlib.Algebra.Group.Opposite
11+
12+
/-!
13+
# Basic Properties of Green's Relations
14+
15+
This file proves the foundational equivalences and duality properties of Green's relations,
16+
establishing them as setoids over a semigroup.
17+
18+
## References
19+
* [T. Colcombet, *The Factorization Forest Theorem*][colombet2008]
20+
-/
21+
22+
public section
23+
24+
variable {S : Type*} [Semigroup S]
25+
26+
27+
section Duality
28+
29+
open MulOpposite
30+
31+
lemma op_rightDvd_op_iff {a b : S} : RightDvd (op a) (op b) ↔ a ∣ b :=
32+
⟨fun ⟨c, hc⟩ ↦ ⟨unop c, op_injective (by simp [hc])⟩,
33+
fun ⟨c, hc⟩ ↦ ⟨op c, by simp [hc]⟩⟩
34+
35+
lemma op_dvd_op_iff {a b : S} : op a ∣ op b ↔ RightDvd a b :=
36+
⟨fun ⟨c, hc⟩ ↦ ⟨unop c, op_injective (by simp [hc])⟩,
37+
fun ⟨c, hc⟩ ↦ ⟨op c, by simp [hc]⟩⟩
38+
39+
lemma isGreenRightDvd_iff_isGreenLeftDvd_op {a b : S} :
40+
IsGreenRightDvd a b ↔ IsGreenLeftDvd (op a) (op b) := by
41+
simp only [IsGreenRightDvd, IsGreenLeftDvd, op_rightDvd_op_iff, op_inj]
42+
43+
lemma isGreenLeftDvd_iff_isGreenRightDvd_op {a b : S} :
44+
IsGreenLeftDvd a b ↔ IsGreenRightDvd (op a) (op b) := by
45+
simp only [IsGreenRightDvd, IsGreenLeftDvd, op_dvd_op_iff, op_inj]
46+
47+
lemma isGreenR_iff_isGreenL_op {a b : S} : IsGreenR a b ↔ IsGreenL (op a) (op b) := by
48+
simp only [IsGreenR, IsGreenL, isGreenRightDvd_iff_isGreenLeftDvd_op]
49+
50+
lemma isGreenL_iff_isGreenR_op {a b : S} : IsGreenL a b ↔ IsGreenR (op a) (op b) := by
51+
simp only [IsGreenL, IsGreenR, isGreenLeftDvd_iff_isGreenRightDvd_op]
52+
53+
end Duality
54+
55+
section Equivalences
56+
57+
namespace IsGreenLeftDvd
58+
59+
/-- Left divisibility is reflexive. -/
60+
@[refl] theorem refl (a : S) : IsGreenLeftDvd a a := Or.inl rfl
61+
62+
/-- Left divisibility is transitive. -/
63+
@[trans] theorem trans {a b c : S} : IsGreenLeftDvd a b → IsGreenLeftDvd b c → IsGreenLeftDvd a c
64+
| .inl rfl, hbc => hbc
65+
| hab, .inl rfl => hab
66+
| .inr ⟨x, hx⟩, .inr ⟨y, hy⟩ => .inr ⟨x * y, by rw [hx, hy, mul_assoc]⟩
67+
68+
end IsGreenLeftDvd
69+
70+
namespace IsGreenRightDvd
71+
72+
/-- Right divisibility is reflexive. -/
73+
@[refl] theorem refl (a : S) : IsGreenRightDvd a a := Or.inl rfl
74+
75+
open MulOpposite in
76+
/-- Right divisibility is transitive. -/
77+
@[trans] theorem trans {a b c : S} (hab : IsGreenRightDvd a b)
78+
(hbc : IsGreenRightDvd b c) : IsGreenRightDvd a c := by
79+
rw [isGreenRightDvd_iff_isGreenLeftDvd_op] at hab hbc ⊢
80+
exact IsGreenLeftDvd.trans hab hbc
81+
82+
end IsGreenRightDvd
83+
84+
namespace IsGreenJRel
85+
86+
/-- The basic J-relation step is reflexive. -/
87+
@[refl] theorem refl (a : S) : IsGreenJRel a a := of_eq rfl
88+
89+
/-- The basic J-relation step is transitive. -/
90+
@[trans] theorem trans {a b c : S} (hab : IsGreenJRel a b)
91+
(hbc : IsGreenJRel b c) : IsGreenJRel a c := by
92+
rcases hab, hbc with
93+
⟨(h | ⟨_, h⟩ | ⟨_, h⟩ | ⟨_, _, h⟩), (h' | ⟨_, h'⟩ | ⟨_, h'⟩ | ⟨_, _, h'⟩)⟩ <;>
94+
(simp [← mul_assoc, h' ▸ h]; grind [mul_assoc, IsGreenJRel])
95+
96+
end IsGreenJRel
97+
98+
namespace IsGreenL
99+
100+
/-- Green's L relation is reflexive. -/
101+
@[refl] theorem refl (a : S) : IsGreenL a a := ⟨IsGreenLeftDvd.refl a, IsGreenLeftDvd.refl a⟩
102+
103+
/-- Green's L relation is symmetric. -/
104+
@[symm] theorem symm {a b : S} (h : IsGreenL a b) : IsGreenL b a := ⟨h.right, h.left⟩
105+
106+
/-- Green's L relation is transitive. -/
107+
@[trans] theorem trans {a b c : S} (hab : IsGreenL a b) (hbc : IsGreenL b c) : IsGreenL a c :=
108+
⟨IsGreenLeftDvd.trans hab.left hbc.left, IsGreenLeftDvd.trans hbc.right hab.right⟩
109+
110+
/-- Green's L relation defines a setoid on `S`. -/
111+
protected def setoid (S : Type*) [Semigroup S] : Setoid S where
112+
r := IsGreenL
113+
iseqv := { refl := refl, symm := symm, trans := trans }
114+
115+
/-- Green's L relation is preserved by right multiplication. -/
116+
theorem mul_right (c : S) {a b : S} (h : IsGreenL a b) : IsGreenL (a * c) (b * c) := by
117+
grind [mul_assoc, RightDvd]
118+
119+
/-- Right cancellation property for elements related by Green's L relation. -/
120+
theorem cancellation {a x u v : S} (hx : IsGreenL x a) (h_cancel : a * u * v = a) :
121+
x * u * v = x := by
122+
rcases hx.left with rfl | ⟨k, rfl⟩ <;> simp [mul_assoc, h_cancel]
123+
124+
end IsGreenL
125+
126+
namespace IsGreenR
127+
128+
/-- Green's R relation is reflexive. -/
129+
@[refl] theorem refl (a : S) : IsGreenR a a :=
130+
⟨IsGreenRightDvd.refl a, IsGreenRightDvd.refl a⟩
131+
132+
/-- Green's R relation is symmetric. -/
133+
@[symm] theorem symm {a b : S} (h : IsGreenR a b) : IsGreenR b a := ⟨h.right, h.left⟩
134+
135+
/-- Green's R relation is transitive. -/
136+
@[trans] theorem trans {a b c : S} (hab : IsGreenR a b) (hbc : IsGreenR b c) : IsGreenR a c :=
137+
⟨IsGreenRightDvd.trans hab.left hbc.left, IsGreenRightDvd.trans hbc.right hab.right⟩
138+
139+
/-- Green's R relation defines a setoid on `S`. -/
140+
protected def setoid (S : Type*) [Semigroup S] : Setoid S where
141+
r := IsGreenR
142+
iseqv := { refl := refl, symm := symm, trans := trans }
143+
144+
open MulOpposite in
145+
/-- Green's R relation is preserved by left multiplication. -/
146+
theorem mul_left (c : S) {a b : S} (h : IsGreenR a b) : IsGreenR (c * a) (c * b) := by
147+
rw [isGreenR_iff_isGreenL_op] at h ⊢
148+
exact IsGreenL.mul_right (op c) h
149+
150+
/-- Left cancellation property for elements related by Green's R relation. -/
151+
theorem cancellation {a x u v : S} (hx : IsGreenR x a) (h_cancel : v * u * a = a) :
152+
v * u * x = x := by
153+
rcases hx.left with rfl | ⟨k, rfl⟩ <;> simp [← mul_assoc, h_cancel]
154+
155+
end IsGreenR
156+
157+
namespace IsGreenH
158+
159+
/-- Green's H relation is reflexive. -/
160+
@[refl] theorem refl (a : S) : IsGreenH a a := ⟨IsGreenL.refl a, IsGreenR.refl a⟩
161+
162+
/-- Green's H relation is symmetric. -/
163+
@[symm] theorem symm {a b : S} (hab : IsGreenH a b) : IsGreenH b a :=
164+
⟨hab.left.symm, hab.right.symm⟩
165+
166+
/-- Green's H relation is transitive. -/
167+
@[trans] theorem trans {a b c : S} (hab : IsGreenH a b) (hbc : IsGreenH b c) : IsGreenH a c :=
168+
⟨hab.left.trans hbc.left, hab.right.trans hbc.right⟩
169+
170+
/-- Green's H relation defines a setoid on `S`. -/
171+
protected def setoid (S : Type*) [Semigroup S] : Setoid S where
172+
r := IsGreenH
173+
iseqv := { refl := refl, symm := symm, trans := trans }
174+
175+
open MulOpposite in
176+
/-- Green's H relation is self-dual under the opposite semigroup. -/
177+
lemma isGreenH_iff_isGreenH_op {a b : S} : IsGreenH a b ↔ IsGreenH (op a) (op b) :=
178+
⟨fun ⟨hL, hR⟩ ↦ ⟨isGreenR_iff_isGreenL_op.mp hR, isGreenL_iff_isGreenR_op.mp hL⟩,
179+
fun ⟨hL, hR⟩ ↦ ⟨isGreenL_iff_isGreenR_op.mpr hR, isGreenR_iff_isGreenL_op.mpr hL⟩⟩
180+
181+
end IsGreenH
182+
183+
/-- Green's L and R relations commute: `L ∘ R = R ∘ L`. -/
184+
lemma isGreenL_commutes_isGreenR {a b z : S} (hL : IsGreenL a z) (hR : IsGreenR z b) :
185+
∃ z', IsGreenR a z' ∧ IsGreenL z' b :=
186+
match hL, hR with
187+
| ⟨.inl rfl, _⟩, hR' | ⟨_, .inl rfl⟩, hR' => ⟨b, hR', IsGreenL.refl b⟩
188+
| hL', ⟨.inl rfl, _⟩ | hL', ⟨_, .inl rfl⟩ => ⟨a, IsGreenR.refl a, hL'⟩
189+
| ⟨.inr ⟨u, hu⟩, .inr ⟨v, hv⟩⟩, ⟨.inr ⟨x, hx⟩, .inr ⟨y, hy⟩⟩ =>
190+
⟨a * y,
191+
⟨.inr ⟨x, by simp [hu, ← hy, ← hx, mul_assoc]⟩, .inr ⟨y, rfl⟩⟩,
192+
⟨.inr ⟨u, by simp [hu, ← hy, mul_assoc]⟩, .inr ⟨v, by simp [← hv, hy, ← mul_assoc]⟩⟩⟩
193+
194+
namespace IsGreenD
195+
196+
/-- Green's D relation is reflexive. -/
197+
@[refl] theorem refl (a : S) : IsGreenD a a := ⟨a, IsGreenL.refl a, IsGreenR.refl a⟩
198+
199+
/-- Green's D relation is symmetric. -/
200+
@[symm] theorem symm {a b : S} : IsGreenD a b → IsGreenD b a
201+
| ⟨_, hL, hR⟩ => let ⟨y, hyR, hyL⟩ := isGreenL_commutes_isGreenR hL hR; ⟨y, hyL.symm, hyR.symm⟩
202+
203+
/-- Green's D relation is transitive. -/
204+
@[trans] theorem trans {a b c : S} : IsGreenD a b → IsGreenD b c → IsGreenD a c
205+
| ⟨_, hL1, hR1⟩, ⟨_, hL2, hR2⟩ =>
206+
let ⟨z, hR3, hL3⟩ := isGreenL_commutes_isGreenR hL2.symm hR1.symm
207+
⟨z, hL1.trans hL3.symm, hR3.symm.trans hR2⟩
208+
209+
/-- Green's D relation defines a setoid on `S`. -/
210+
protected def setoid (S : Type*) [Semigroup S] : Setoid S where
211+
r := IsGreenD
212+
iseqv := { refl := refl, symm := symm, trans := trans }
213+
214+
open MulOpposite in
215+
/-- Green's D relation is self-dual under the opposite semigroup. -/
216+
lemma isGreenD_iff_isGreenD_op {a b : S} : IsGreenD a b ↔ IsGreenD (op a) (op b) :=
217+
⟨fun ⟨_, hL, hR⟩ ↦
218+
let ⟨y, hyR, hyL⟩ := isGreenL_commutes_isGreenR hL hR
219+
⟨op y, isGreenR_iff_isGreenL_op.mp hyR, isGreenL_iff_isGreenR_op.mp hyL⟩,
220+
fun ⟨_, hL, hR⟩ ↦
221+
let ⟨y, hyR, hyL⟩ := isGreenL_commutes_isGreenR (isGreenL_iff_isGreenR_op.mpr hR).symm
222+
(isGreenR_iff_isGreenL_op.mpr hL).symm
223+
⟨y, hyL.symm, hyR.symm⟩⟩
224+
225+
end IsGreenD
226+
227+
namespace IsGreenJ
228+
229+
/-- Green's J relation is reflexive. -/
230+
@[refl] theorem refl (a : S) : IsGreenJ a a := ⟨IsGreenJRel.refl a, IsGreenJRel.refl a⟩
231+
232+
/-- Green's J relation is symmetric. -/
233+
@[symm] theorem symm {a b : S} (h : IsGreenJ a b) : IsGreenJ b a := ⟨h.right, h.left⟩
234+
235+
/-- Green's J relation is transitive. -/
236+
@[trans] theorem trans {a b c : S} (hab : IsGreenJ a b) (hbc : IsGreenJ b c) : IsGreenJ a c :=
237+
⟨hab.left.trans hbc.left, hbc.right.trans hab.right⟩
238+
239+
/-- Green's J relation defines a setoid on `S`. -/
240+
protected def setoid (S : Type*) [Semigroup S] : Setoid S where
241+
r := IsGreenJ
242+
iseqv := { refl := refl, symm := symm, trans := trans }
243+
244+
end IsGreenJ
245+
246+
end Equivalences

‎Mathlib/Algebra/Group/GreensRelations/Defs.lean‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
/-
2+
Copyright (c) 2026 Re'em Melamed-Katz. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Re'em Melamed-Katz
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.Divisibility.Basic
9+
public import Mathlib.Algebra.Group.Basic
10+
11+
/-!
12+
# Green's Relations Definitions
13+
14+
This file contains the fundamental definitions of Green's relations (L, R, H, D, and J)
15+
on a general semigroup.
16+
17+
## Main definitions
18+
19+
* `IsGreenLeftDvd`: Left divisibility in a semigroup.
20+
* `IsGreenRightDvd`: Right divisibility in a semigroup.
21+
* `IsGreenJRel`: The basic step of being a two-sided multiple.
22+
* `IsGreenL`: Green's L relation (generating the same left ideal).
23+
* `IsGreenR`: Green's R relation (generating the same right ideal).
24+
* `IsGreenH`: Green's H relation (the intersection of L and R).
25+
* `IsGreenD`: Green's D relation (the composition of L and R).
26+
* `IsGreenJ`: Green's J relation (generating the same two-sided ideal).
27+
28+
## References
29+
30+
* [T. Colcombet, *The Factorization Forest Theorem*][colcombet2008]
31+
-/
32+
33+
public section
34+
35+
variable {S : Type*} [Semigroup S]
36+
37+
/-- `IsGreenLeftDvd a b` means that `a` is a left multiple of `b`,
38+
i.e., `a = b` or `a = z * b`. -/
39+
abbrev IsGreenLeftDvd (a b : S) : Prop := a = b ∨ RightDvd b a
40+
41+
/-- `IsGreenRightDvd a b` means that `a` is a right multiple of `b`,
42+
i.e., `a = b` or `a = b * z`. -/
43+
abbrev IsGreenRightDvd (a b : S) : Prop := a = b ∨ b ∣ a
44+
45+
/-- `IsGreenJRel a b` represents the basic step of being a two-sided multiple.
46+
`a` is related to `b` if `a = b`, `a = u * b`, `a = b * v`, or `a = u * b * v`. -/
47+
inductive IsGreenJRel (a b : S) : Prop
48+
/-- `a` and `b` are equal. -/
49+
| of_eq (h : a = b)
50+
/-- `a` is a left multiple of `b`. -/
51+
| mul_left (u : S) (h : a = u * b)
52+
/-- `a` is a right multiple of `b`. -/
53+
| mul_right (v : S) (h : a = b * v)
54+
/-- `a` is a two-sided multiple of `b`. -/
55+
| mul_both (u v : S) (h : a = u * b * v)
56+
57+
/-- Green's L relation: `a` and `b` generate the same left ideal. -/
58+
abbrev IsGreenL (a b : S) : Prop := IsGreenLeftDvd a b ∧ IsGreenLeftDvd b a
59+
60+
/-- Green's R relation: `a` and `b` generate the same right ideal. -/
61+
abbrev IsGreenR (a b : S) : Prop := IsGreenRightDvd a b ∧ IsGreenRightDvd b a
62+
63+
/-- Green's H relation: the intersection of Green's L and Green's R relations. -/
64+
abbrev IsGreenH (a b : S) : Prop := IsGreenL a b ∧ IsGreenR a b
65+
66+
/-- Green's D relation: the composition of Green's L and Green's R relations.
67+
Here defined explicitly as the existence of an intermediate element `z`. -/
68+
abbrev IsGreenD (a b : S) : Prop := ∃ z, IsGreenL a z ∧ IsGreenR z b
69+
70+
/-- Green's J relation: `a` and `b` generate the same two-sided ideal. -/
71+
abbrev IsGreenJ (a b : S) : Prop := IsGreenJRel a b ∧ IsGreenJRel b a

0 commit comments

Comments
 (0)