Green's Lemma

This file proves Green's lemma, which is the following: Let x 𝓡 y such that y * u = x and x * v = y. Then the map x ↦ x * v is a bijection from the 𝓛-class of x to the 𝓛-class of y, and the map x → x * u is its inverse. Additionally, these bijections preserve 𝓗 classes.

We also prove the dual version of this lemma.

Main Theorems

Let x 𝓡 y such that y * u = x and x * v = y.

• REquiv.invOn_lClass - the map x ↦ x * u is the inverse of x ↦ x * v on the 𝓛-class of x.
• REquiv.bijOn_lClass - the map x ↦ x * v is a bijection from the 𝓛-class of x to the 𝓛-class of y.
• REquiv.bijOn_lClass_pres_hClass - this bijection preserves 𝓗 classes.

Let x 𝓛 y such that u * y = x and v * x = y.

• LEquiv.invOn_rClass - the map x ↦ u * x is the inverse of x ↦ v * x on the 𝓡-class of x.
• LEquiv.bijOn_rClass - the map x ↦ v * x is a bijection from the 𝓡-class of x to the 𝓡-class of y.
• LEquiv.bijOn_rClass_pres_hClass - this bijection preserves 𝓗 classes.

References

TODO

Blueprint

• One lemma entry for the 𝓡-class bijection and its properties. label : lem:greens-lemma Lean lemmas to tag :
  • Semigroup.REquiv.bijOn_lClass
  • Semigroup.REquiv.bijOn_lClass_pres_hClass
  • Semigroup.LEquiv.bijOn_rClass
  • Semigroup.LEquiv.bijOn_rClass_pres_hClass dependencies :
  • lem:greens-relations-mul-compat

theorem Semigroup.REquiv.translation_id {S : Type u_1} [Semigroup S] {x y u v w : S} (hv : x * v = y) (hu : y * u = x) (hw : w 𝓛 x) : w * v * u = w

If x 𝓡 y such that x * v = y and y * u = x, then right translation by v * u on any element 𝓛-equivalent to x is the identity.

theorem Semigroup.RPreorder.mapsTo_lClass {S : Type u_1} [Semigroup S] {x y v : S} (hv : x * v = y) : Set.MapsTo (fun (w : S) => w * v) ⟦x⟧𝓛 ⟦y⟧𝓛

If x * v = y, then the map w ↦ w * v maps the 𝓛-class of x to that of y

theorem Semigroup.REquiv.injOn_lClass {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓡 y) (hv : x * v = y) : Set.InjOn (fun (w : S) => w * v) ⟦x⟧𝓛

If x 𝓡 y such that x * v = y then the map w ↦ w * v is injective on the 𝓛-class of x.

theorem Semigroup.REquiv.surjOn_lClass {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓡 y) (hv : x * v = y) : Set.SurjOn (fun (w : S) => w * v) ⟦x⟧𝓛 ⟦y⟧𝓛

If x 𝓡 y such that x * v = y, then the map w ↦ w * v is surjective from the 𝓛-class of x to that of y.

theorem Semigroup.REquiv.invOn_lClass {S : Type u_1} [Semigroup S] {x y u v : S} (hv : x * v = y) (hu : y * u = x) : Set.InvOn (fun (w : S) => w * u) (fun (w : S) => w * v) ⟦x⟧𝓛 ⟦y⟧𝓛

If x * v = y and y * u = x, then the map w ↦ w * u is the inverse of w ↦ w * v when restricted to the 𝓛-classes of x and y

theorem Semigroup.REquiv.bijOn_lClass {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓡 y) (hv : x * v = y) : Set.BijOn (fun (w : S) => w * v) ⟦x⟧𝓛 ⟦y⟧𝓛

If x 𝓡 y such that x * v = y, then the map w ↦ w * v is a bijection from the 𝓛-class of x to that of y.

theorem Semigroup.REquiv.exists_bij_on_lClass {S : Type u_1} [Semigroup S] {x y : S} (hr : x 𝓡 y) : ∃ (f : S → S), Set.BijOn f ⟦x⟧𝓛 ⟦y⟧𝓛

theorem Semigroup.REquiv.bijOn_lClass_pres_hClass {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓡 y) (hv : x * v = y) {a b : S} (hw : a 𝓛 x) (hz : b 𝓛 x) : a 𝓗 b ↔ (fun (w : S) => w * v) a 𝓗 (fun (w : S) => w * v) b

If x 𝓡 y such that x * v = y, then the map w ↦ w * v preserves 𝓗-classes.

theorem Semigroup.REquiv.bijOn_lClass_rEquiv {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓡 y) (hv : x * v = y) {z : S} (hz : z 𝓛 x) : z 𝓡 z * v

If x 𝓡 y such that x * v = y, then for all z 𝓛 x, z 𝓡 z * v.

theorem Semigroup.REquiv.mapsTo_hClass {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓡 y) (hv : x * v = y) : Set.MapsTo (fun (w : S) => w * v) ⟦x⟧𝓗 ⟦y⟧𝓗

theorem Semigroup.REquiv.surjOn_hClass {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓡 y) (hv : x * v = y) : Set.SurjOn (fun (w : S) => w * v) ⟦x⟧𝓗 ⟦y⟧𝓗

theorem Semigroup.REquiv.injOn_hClass {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓡 y) (hv : x * v = y) : Set.InjOn (fun (w : S) => w * v) ⟦x⟧𝓗

theorem Semigroup.REquiv.invOn_hClass {S : Type u_1} [Semigroup S] {x y u v : S} (hv : x * v = y) (hu : y * u = x) : Set.InvOn (fun (w : S) => w * u) (fun (w : S) => w * v) ⟦x⟧𝓗 ⟦y⟧𝓗

theorem Semigroup.REquiv.bijOn_hClass {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓡 y) (hv : x * v = y) : Set.BijOn (fun (w : S) => w * v) ⟦x⟧𝓗 ⟦y⟧𝓗

If x 𝓡 y such that x * v = y, then the map w ↦ w * v is a bijection from the 𝓗-class of x to that of y.

theorem Semigroup.REquiv.exists_bij_on_hClass {S : Type u_1} [Semigroup S] {x y : S} (hr : x 𝓡 y) : ∃ (f : S → S), Set.BijOn f ⟦x⟧𝓗 ⟦y⟧𝓗

Dual proofs

theorem Semigroup.LEquiv.translation_id {S : Type u_1} [Semigroup S] {x y u v w : S} (hv : v * x = y) (hu : u * y = x) (hw : w 𝓡 x) : u * v * w = w

If x 𝓛 y such that u * y = x and v * x = y, then left translation by u * v on any element 𝓡-equivalent to x is the identity.

theorem Semigroup.LPreorder.mapsTo_rClass {S : Type u_1} [Semigroup S] {x y v : S} (hy : v * x = y) : Set.MapsTo (fun (w : S) => v * w) ⟦x⟧𝓡 ⟦y⟧𝓡

If v * x = y, then the map w ↦ v * w maps the 𝓡-class of x to that of y

theorem Semigroup.LEquiv.injOn_rClass {S : Type u_1} [Semigroup S] {x y v : S} (hl : x 𝓛 y) (hv : v * x = y) : Set.InjOn (fun (w : S) => v * w) ⟦x⟧𝓡

If x 𝓛 y such that v * x = y then the map w ↦ v * w is injective on the 𝓡-class of x.

theorem Semigroup.LEquiv.surjOn_rClass {S : Type u_1} [Semigroup S] {x y v : S} (hl : x 𝓛 y) (hv : v * x = y) : Set.SurjOn (fun (w : S) => v * w) ⟦x⟧𝓡 ⟦y⟧𝓡

If x 𝓛 y such that v * x = y, then the map w ↦ v * w is surjective from the 𝓡-class of x to that of y.

theorem Semigroup.LEquiv.invOn_rClass {S : Type u_1} [Semigroup S] {x y u v : S} (hv : v * x = y) (hu : u * y = x) : Set.InvOn (fun (w : S) => u * w) (fun (w : S) => v * w) ⟦x⟧𝓡 ⟦y⟧𝓡

If u * y = x and v * x = y, then the map w ↦ u * w is the inverse of w ↦ v * w when restricted to the 𝓡-classes of x and y

theorem Semigroup.LEquiv.bijOn_rClass {S : Type u_1} [Semigroup S] {x y v : S} (hl : x 𝓛 y) (hv : v * x = y) : Set.BijOn (fun (w : S) => v * w) ⟦x⟧𝓡 ⟦y⟧𝓡

If x 𝓛 y such that v * x = y, then the map w ↦ v * w is a bijection from the 𝓡-class of x to that of y.

theorem Semigroup.LEquiv.exists_bijOn_rClass {S : Type u_1} [Semigroup S] {x y : S} (hl : x 𝓛 y) : ∃ (f : S → S), Set.BijOn f ⟦x⟧𝓡 ⟦y⟧𝓡

theorem Semigroup.LEquiv.bijOn_rClass_lEquiv {S : Type u_1} [Semigroup S] {x y v : S} (hr : x 𝓛 y) (hv : v * x = y) {z : S} (hz : z 𝓡 x) : z 𝓛 v * z

If x 𝓛 y such that v * x = y, then for all z 𝓡 x, z 𝓛 v * z.

theorem Semigroup.LEquiv.mapsTo_hClass {S : Type u_1} [Semigroup S] {x y v : S} (hl : x 𝓛 y) (hv : v * x = y) : Set.MapsTo (fun (w : S) => v * w) ⟦x⟧𝓗 ⟦y⟧𝓗

theorem Semigroup.LEquiv.surjOn_hClass {S : Type u_1} [Semigroup S] {x y v : S} (hl : x 𝓛 y) (hv : v * x = y) : Set.SurjOn (fun (w : S) => v * w) ⟦x⟧𝓗 ⟦y⟧𝓗

theorem Semigroup.LEquiv.injOn_hClass {S : Type u_1} [Semigroup S] {x y v : S} (hl : x 𝓛 y) (hv : v * x = y) : Set.InjOn (fun (w : S) => v * w) ⟦x⟧𝓗

theorem Semigroup.LEquiv.invOn_hClass {S : Type u_1} [Semigroup S] {x y u v : S} (hv : v * x = y) (hu : u * y = x) : Set.InvOn (fun (w : S) => u * w) (fun (w : S) => v * w) ⟦x⟧𝓗 ⟦y⟧𝓗

theorem Semigroup.LEquiv.bijOn_hClass {S : Type u_1} [Semigroup S] {x y v : S} (hl : x 𝓛 y) (hv : v * x = y) : Set.BijOn (fun (w : S) => v * w) ⟦x⟧𝓗 ⟦y⟧𝓗

If x 𝓛 y such that v * x = y, then the map w ↦ v * w is a bijection from the 𝓗-class of x to that of y.

theorem Semigroup.LEquiv.exists_bijOn_hClass {S : Type u_1} [Semigroup S] {x y : S} (hl : x 𝓛 y) : ∃ (f : S → S), Set.BijOn f ⟦x⟧𝓗 ⟦y⟧𝓗