how to specify an identity for a semigroup ?

Stream: maths

[cairunze cairunze]

I want to formalize this result in lean4, https://planetmath.org/acharacterizationofgroups
basically to show a certain semigroup is a group.
I think I have all the ingredients, but I cannot put them together in an instance.
The main difficulty for me is to produce an identity (instead of using an existing one) for the group, see near bottom part of the following code.
The problem seems to be that I can produce the wanted identity in tactic mode, but I don't know a way to put it in term mode.
thanks for the help~

import Mathlib.Tactic

variable {S : Type*} [Semigroup S]

namespace regsemigp

-- https://planetmath.org/acharacterizationofgroups
lemma idem_imp_left_id (i x: S) (h : ∀ (x : S), ∃! y, x * y * x = x) :
  i * i = i → i * x = x := by
  intro hi
  rcases h (i * x) with ⟨ix',hix',hixu'⟩
  rcases h ix' with ⟨ix'',hix'',hixu''⟩
  -- ix = (ix)''
  have h0 : i * x = ix'' := by
    apply hixu''
    apply hixu'
    rw [← mul_assoc (i * x), ← mul_assoc (i * x),hix',hix']
  -- i^2=i => ix=ix(ix)'ix=ix(ix)'iix => (ix)'i=(ix)'
  have h1 : ix' * i = ix' := by
    apply hixu'
    rw [mul_assoc,← mul_assoc (ix' * i),mul_assoc ix',hi]
    nth_rw 2 [← hix']
    group
  -- (ix)'=(ix)'(ix)''(ix)'=(ix)'(ix)(ix)'=((ix)'i)x(ix)'=(ix)'x(ix)'
  have h2 : x = ix'' := by
    apply hixu''
    nth_rw 3 [← hix'']
    rw [← h0,← mul_assoc,h1]
  rw [h0,h2]

lemma idem_imp_right_id (i x: S) (h : ∀ (x : S), ∃! y, x * y * x = x) :
  i * i = i → x * i = x := by
  intro hi
  rcases h (x * i) with ⟨xi',hxi',hxiu'⟩
  rcases h xi' with ⟨xi'',hxi'',hxiu''⟩
  -- ix = (ix)''
  have h0 : x * i = xi'' := by
    apply hxiu''
    apply hxiu'
    calc x * i * (xi' * (x * i) * xi') * (x * i) =
        x * i * xi' * (x * i) * xi' * (x * i) := by group
      _ = x * i := by rw [hxi',hxi']
  -- i^2=i => xi=xi(xi)'xi=xii(xi)'xi => i(ix)'=(xi)'
  have h1 : i * xi' = xi' := by
    apply hxiu'
    calc x * i * (i * xi') * (x * i) =
        (x * (i * i) * xi') * (x * i) := by group
      _ = x * i := by rw [hi,hxi']
  -- (xi)'=(xi)'(xi)''(xi)'=(xi)'(xi)(xi)'=(xi)'x(i(xi)')=(xi)'x(xi)'
  have h2 : x = xi'' := by
    apply hxiu''
    calc xi' * x * xi' = xi' * x * (i * xi') := by rw [h1]
      _ = xi' * (x * i) * xi' := by group
      _ = xi' * xi'' * xi' := by rw [h0]
      _ = xi' := by rw [hxi'']
  rw [h0,h2]

lemma exists_one {x : S} (h : ∀ (x : S), ∃! y, x * y * x = x) :
  ∃! (e : S), ∀ x, e * x = x ∧ x * e = x := by
  rcases h x with ⟨x',hx',hxu'⟩
  have idem : (x * x') * (x * x') = x * x' := by
    calc x * x' * (x * x') = (x * x' * x) * x' := by group
      _ = x * x' := by rw [hx']
  use x * x'
  constructor
  intro y
  exact ⟨idem_imp_left_id _ _ h idem,idem_imp_right_id _ _ h idem⟩
  intro e he
  rw [← idem_imp_left_id (x * x') e h idem,(he (x * x')).2]


lemma exists_inv {x e: S} (h : ∀ (x : S), ∃! y, x * y * x = x)
  (h1 : ∀ x, e * x = x ∧ x * e = x) :
  ∃ (y : S), x * y = e ∧ y * x = e := by
  rcases h x with ⟨x',hx',hxu'⟩
  use x'
  have ideml : (x * x') * (x * x') = x * x' := by rw [← mul_assoc,hx']
  have idemr : (x' * x) * (x' * x) = x' * x := by
    rw [mul_assoc x',← mul_assoc x,hx']
  constructor
  · rw [← idem_imp_left_id (x * x') e h ideml, (h1 (x * x')).2]
  · rw [← idem_imp_right_id (x' * x) e h idemr,(h1 (x' * x)).1]


instance (h0 : Nonempty S)  -- not sure this is the correct way to specify nonemptiness
  (h : ∀ (x : S), ∃! y, x * y * x = x) : Group S where
    mul := (· * ·)
    mul_assoc := mul_assoc
    one := sorry -- don't know how proceed here
    one_mul := by
      cases h0 with -- this will obtain an element in S, but looks unnatural to me
      | _ x =>
        rcases h x with ⟨x',hx',hxu'⟩
        have ideml : (x * x') * (x * x') = x * x' := by rw [← mul_assoc,hx']
        intro y
        apply idem_imp_left_id _ _ h
        -- ⊢ 1 * 1 = 1
        sorry
    mul_one := sorry
    inv := sorry
    mul_left_inv := sorry


end regsemigp

[Edward van de Meent]

Since you're choosing the identity by making use of a term from an exists-statement, you will need some sort of axiom of choice, which in this case will most likely take the form of docs#Exists.choose

[Edward van de Meent]

I'm not sure that this will make for great defEq though. I think that this at most should be a def, or maybe should be stated in a reduced form, stating that a unit and inverse exist rather than giving the terms.

[cairunze cairunze]

Edward van de Meent said:

Since you're choosing the identity by making use of a term from an exists-statement, you will need some sort of axiom of choice, which in this case will most likely take the form of docs#Exists.choose

Ah this is helpful, I did not realize that I have to use both Classical.choice and Classical.choose (maybe?). So the definition checks out, and I can provide a candidate for the identity. The instance (or I defined elsewhere) has to be made noncomputable.

Now, however, in the subsequent parts, Lean does not recognize the identity I defined is the same as 1. Any way to salvage this? Thanks.

noncomputable instance (h0 : Nonempty S)
  (h : ∀ (x : S), ∃! y, x * y * x = x) : Group S where
    mul := (· * ·)
    mul_assoc := mul_assoc
    one :=
      let x : S := Classical.choice h0
      let y : S := Classical.choose (h x)
      x * y
    one_mul := by
      let x : S := Classical.choice h0
      rcases h x with ⟨x',hx',hxu'⟩
      have ideml : (x * x') * (x * x') = x * x' := by rw [← mul_assoc,hx']
      intro y
      apply idem_imp_left_id _ _ h
      -- ⊢ 1 * 1 = 1    <-- this `1` seems unrelated to the `one` prescribed above
      sorry
    mul_one := sorry
    inv := sorry
    mul_left_inv := sorry

[cairunze cairunze]

It turns out that the 1 and the one are indeed not unrelated. I hover the mouse over the 1 in the tactic state and get that it follows the definition. So I made some changes to the ingredients.

lemma exists_one (h0 : Nonempty S) (h : ∀ (x : S), ∃! y, x * y * x = x) :
  ∃! (e : S), ∀ x, e * x = x ∧ x * e = x := by
  let x : S := Classical.choice h0
  rcases h x with ⟨x',hx',hxu'⟩
  have idem : (x * x') * (x * x') = x * x' := by
    calc x * x' * (x * x') = (x * x' * x) * x' := by group
      _ = x * x' := by rw [hx']
  use x * x'
  constructor
  intro y
  exact ⟨idem_imp_left_id _ _ h idem,idem_imp_right_id _ _ h idem⟩
  intro e he
  rw [← idem_imp_left_id (x * x') e h idem,(he (x * x')).2]

noncomputable example (h0 : Nonempty S)
  (h : ∀ (x : S), ∃! y, x * y * x = x) : Group S where
    mul := (· * ·)
    mul_assoc := mul_assoc
    one := Classical.choose (exists_one h0 h)
    one_mul := λ y ↦ ((Classical.choose_spec (exists_one h0 h)).1 y).1
    mul_one := λ y ↦ ((Classical.choose_spec (exists_one h0 h)).1 y).2
    inv := sorry
    mul_left_inv := sorry

So far everything compiles and at least the monoid part is done, only a bit ugly though.
Maybe there's a better way to this?

[cairunze cairunze]

I think finally the following (with other parts above together) works.
The final part on the inverse is creating similar problem as before of not seemingly to have the 1 in the goal showing anything obvious related to the rest. I have to modify the identity 1 in the lemma to resolve this nesting.
The overall Classical.choose thing is making the code less readable, I hope there's a better way to present this.
(I realized that there are redundancies in the lemmas, for example, the uniqueness of identity is not needed, and so on.)

lemma exists_inv'' (h0 : Nonempty S) (h : ∀ (x : S), ∃! y, x * y * x = x)
  : ∀ (x : S), ∃ y, y * x = Classical.choose (exists_one h0 h) := by
  intro x
  rcases h x with ⟨x',hx',hxu'⟩
  use x'
  have h1 :=(Classical.choose_spec (exists_one h0 h)).1
  have idemr : (x' * x) * (x' * x) = x' * x := by
    rw [mul_assoc x',← mul_assoc x,hx']
  rw [← idem_imp_right_id (x' * x) (Classical.choose (exists_one h0 h)) h idemr,(h1 (x' * x)).1]

noncomputable example (h0 : Nonempty S)
  (h : ∀ (x : S), ∃! y, x * y * x = x) : Group S where
    mul := (· * ·)
    mul_assoc := mul_assoc
    one := Classical.choose (exists_one h0 h)
    one_mul :=  λ y ↦ ((Classical.choose_spec (exists_one h0 h)).1 y).1
    mul_one :=  λ y ↦ ((Classical.choose_spec (exists_one h0 h)).1 y).2
    inv := λ x ↦ Classical.choose (exists_inv'' h0 h x)
    mul_left_inv := λ x ↦ Classical.choose_spec (exists_inv'' h0 h x)

[Edward van de Meent]

one approach is to use h to define a function f : S -> S with the property that x * f x * x = x and x * y * x = x -> y = f x using AoC, and (where necessary) assume Inhabited S rather than Nonempty S so you (constructively) have access to default : S as a generic element of S. If you do this, you will be able to construct all of the rest of the argument without AoC, and because you're proving things about constructions using this f rather than Exists.Choose for a specific lemma, it will look nice too. the only question then is "what is a nice name for this function f that carries its intuition?"

[cairunze cairunze]

Edward van de Meent said:

one approach is to use h to define a function f : S -> S with the property that x * f x * x = x and x * y * x = x -> y = f x using AoC, and (where necessary) assume Inhabited S rather than Nonempty S so you (constructively) have access to default : S as a generic element of S. If you do this, you will be able to construct all of the rest of the argument without AoC, and because you're proving things about constructions using this f rather than Exists.Choose for a specific lemma, it will look nice too. the only question then is "what is a nice name for this function f that carries its intuition?"

Wow, this is a nice way to extract the element, by semigroup theory jargon, probably f should be called weak inverse or something, cf, https://en.wikipedia.org/wiki/Weak_inverse

However, I cannot work it out in the proof, since it only provide the element but not its properties (maybe need to write it in another lemma?). So instead, I just defined the identity and inverse, along with some lemmas about their property.
So the final bundled instance seems a little bit cleaner...

-- noncomputable def weak_inv [Inhabited S]
--   (h : ∀ (x : S), ∃! y, x * y * x = x) : S → S :=
--   λ x ↦ Classical.choose (h x)

lemma exists_one [Inhabited S] (h : ∀ (x : S), ∃! y, x * y * x = x) :
  ∃ (e : S), ∀ x, e * x = x ∧ x * e = x := by
  let x : S := (default : S)
  -- let x' : S := weak_inv h x
  rcases h x with ⟨x',hx',hxu'⟩
  have idem : (x * x') * (x * x') = x * x' := by
    calc x * x' * (x * x') = (x * x' * x) * x' := by group
      _ = x * x' := by rw [hx']
  use x * x'
  intro y
  exact ⟨idem_imp_left_id _ _ h idem,idem_imp_right_id _ _ h idem⟩

noncomputable def one_S [Inhabited S]
  (h : ∀ (x : S), ∃! y, x * y * x = x) : S
  := Classical.choose (exists_one h)

lemma exists_inv [Inhabited S]
  (h : ∀ (x : S), ∃! y, x * y * x = x)
  : ∀ (x : S), ∃ y, y * x = one_S h := by
  intro x
  rcases h x with ⟨x',hx',hxu'⟩
  use x' -- = weak_inv h x
  have h1 := Classical.choose_spec (exists_one h)
  have idemr : (x' * x) * (x' * x) = x' * x := by
    rw [mul_assoc x',← mul_assoc x,hx']
  rw [← idem_imp_right_id (x' * x) (one_S h) h idemr,one_S,(h1 (x' * x)).1]

noncomputable def inv_S [Inhabited S]
  (h : ∀ (x : S), ∃! y, x * y * x = x) : S → S
  := λ x ↦ Classical.choose (exists_inv h x)

lemma one_S_left_spec [Inhabited S]
  (h : ∀ (x : S), ∃! y, x * y * x = x)
  : ∀ x, (one_S h) * x = x
  := λ x ↦ (Classical.choose_spec (exists_one h) x).1

lemma one_S_right_spec [Inhabited S]
  (h : ∀ (x : S), ∃! y, x * y * x = x)
  : ∀ x, x * (one_S h) = x
  := λ x ↦ (Classical.choose_spec (exists_one h) x).2

lemma inv_S_spec [Inhabited S]
  (h : ∀ (x : S), ∃! y, x * y * x = x)
  : ∀ x, (inv_S h x) * x = one_S h
  := λ x ↦ Classical.choose_spec (exists_inv h x)

noncomputable instance [Inhabited S]
  (h : ∀ (x : S), ∃! y, x * y * x = x) : Group S where
  mul := (· * ·)
  mul_assoc := mul_assoc
  one := one_S h
  one_mul := one_S_left_spec h
  mul_one := one_S_right_spec h
  inv := λ x ↦ inv_S h x
  mul_left_inv := inv_S_spec h

[Edward van de Meent]

As a small note, you don't need to specify mul or mul_assoc, those can be filled automatically since you're assuming Semigroup S

[Edward van de Meent]

here is how to get the properties for such a definition:

variable {S:Type*} [Semigroup S]

noncomputable def weak_inv (h : ∀ (x : S), ∃! y, x * y * x = x) : S → S :=
  λ x ↦ (h x).exists.choose

lemma weak_inv_prop (h : ∀ (x : S), ∃! y, x * y * x = x) :
    ∀ x, x * weak_inv h x * x = x := by
  intro x
  exact (h x).exists.choose_spec

lemma weak_inv_unique (h : ∀ (x : S), ∃! y, x * y * x = x) :
    ∀ y x, x * y * x = x → y = weak_inv h x := by
  intro y x hy
  exact (h x).unique hy (weak_inv_prop h x)

[cairunze cairunze]

Edward van de Meent said:

here is how to get the properties for such a definition:

variable {S:Type*} [Semigroup S]

noncomputable def weak_inv (h : ∀ (x : S), ∃! y, x * y * x = x) : S → S :=
  λ x ↦ (h x).exists.choose

lemma weak_inv_prop (h : ∀ (x : S), ∃! y, x * y * x = x) :
    ∀ x, x * weak_inv h x * x = x := by
  intro x
  exact (h x).exists.choose_spec

lemma weak_inv_unique (h : ∀ (x : S), ∃! y, x * y * x = x) :
    ∀ y x, x * y * x = x → y = weak_inv h x := by
  intro y x hy
  exact (h x).unique hy (weak_inv_prop h x)

This seems more civilized! Thanks a lot for the various suggestions!
I get to get the rid of a lot of the rcases.
I think for better presentation, I need to write some small lemmas tagged with @[simp], and then see what happens.

example (i x: S) : i * i = i → i * x = x := by
  intro hi
  set ix' := weak_inv h (i * x) with hix'
  set ix'' := weak_inv h ix' with hix''
  -- ix = (ix)''
  have h0 : i * x = ix'' := by
    apply weak_inv_unique
    apply weak_inv_unique
    rw [← mul_assoc (i * x), ← mul_assoc (i * x),weak_inv_prop,weak_inv_prop]
  -- i^2=i => ix=ix(ix)'ix=ix(ix)'iix => (ix)'i=(ix)'
  have h1 : ix' * i = ix' := by
    apply weak_inv_unique
    rw [mul_assoc,← mul_assoc (ix' * i),mul_assoc ix',hi,mul_assoc ix',← mul_assoc (i*x)]
    apply weak_inv_prop h (i * x)
  -- (ix)'=(ix)'(ix)''(ix)'=(ix)'(ix)(ix)'=((ix)'i)x(ix)'=(ix)'x(ix)'
  have h2 : x = ix'' := by
    apply weak_inv_unique
    nth_rw 3 [← weak_inv_prop h ix']
    rw [← hix'',← h0,← mul_assoc,h1]
  rw [h0,h2]

lemma exists_one : ∃ (e : S), ∀ x, e * x = x ∧ x * e = x := by
  let x : S := (default : S)
  let x' := weak_inv h x
  have idem : (x * x') * (x * x') = x * x' := by
    calc x * x' * (x * x') = (x * x' * x) * x' := by group
      _ = x * x' := by rw [weak_inv_prop]
  use x * x'
  intro y
  exact ⟨idem_imp_left_id h _ _ idem,idem_imp_right_id h _ _ idem⟩

lemma exists_inv : ∀ (x : S), ∃ y, y * x = one_S h := by
  intro x
  let x' := weak_inv h x
  use x'
  have h1 := Classical.choose_spec (exists_one h)
  have idemr : (x' * x) * (x' * x) = x' * x := by
    rw [mul_assoc x',← mul_assoc x,weak_inv_prop]
  rw [← idem_imp_right_id h (x' * x) (one_S h)  idemr,one_S,(h1 (x' * x)).1]