Peter Davidson

Stream: new members

[Peter Davidson]

Hello everyone, my name is Peter Davidson. I've been a member of this channel for a while now, but this is my first post. I've ran into a problem while working on my first project (formalising Green's relations from semigroup theory) and I was hoping to get some help from the community.

Here is my code (including some sorry's to reduce its length):

import Mathlib.Tactic

variable {S : Type} [Semigroup S]

variable {a x y : S}

theorem left_principal_ideal.mem (hx : x ∈ {s : S | ∃ t, s = t * a} ∪ {a}) (hy : y ∈ {s : S | ∃ t, s = t * a} ∪ {a}) : x * y ∈ {s : S | ∃ t, s = t * a} ∪ {a} := by
  sorry

 def left_principal_ideal (a : S) : Subsemigroup S where
  carrier := {s : S | ∃ t, s = t * a} ∪ {a}
  mul_mem' := left_principal_ideal.mem

notation "S¹ " a => left_principal_ideal a

theorem mem_left_principal_ideal_iff (a s : S) : (s ∈ S¹ a) ↔ (∃ t, s = t * a) ∨ s = a := by
  sorry

def left_green_relation (a b : S) : Prop := (S¹ a) = (S¹ b)

infix:40 " L " => left_green_relation

theorem left_green_relation.refl (a : S) : a L a := rfl

theorem left_green_relation.symm (a b : S) (h : a L b) : b L a := Eq.symm h

theorem left_green_relation.trans (a b c : S) (h1 : a L b) (h2 : b L c) : a L c := Eq.trans h1 h2

theorem left_green_relation.equiv : Equivalence left_green_relation where
  refl := left_green_relation.refl
  symm := left_green_relation.symm
  trans := left_green_relation.trans

The infoview returns a typeclass instance problem for the theorem left_green_relation.equiv. I have a very basic understanding of this type of the problem and I don't know how to fix it. Is it down to the fact that Lean cannot infer that S is a semigroup from how I've set up my variables?

[Andrew Yang]

The issue is Lean cannot know which S you are referring to in the statement Equivalence left_green_relation. You need Equivalence fun a b : S ↦ left_green_relation a b or Equivalence (α := S) left_green_relation.

[Andrew Yang]

The confusion might stem from the fact that the variable command doesn't introduce a "global variable". It is just a syntax sugar to insert {S : Type} into every following declaration.

[Moritz Firsching]

theorem left_green_relation.symm {a b : S} (h : a L b) : b L a := Eq.symm h

theorem left_green_relation.trans {a b c : S} (h1 : a L b) (h2 : b L c) : a L c := Eq.trans h1 h2



theorem left_green_relation.equiv : Equivalence <| left_green_relation (S := S) where
  refl := left_green_relation.refl
  symm := left_green_relation.symm
  trans := left_green_relation.trans

This makes it work, but not sure if you want to provide the argument S this way

[Moritz Firsching]

note that left_green_relation.symm and left_green_relation.trans also needed implicit arguments in order to match what Equivalence expects.

[Peter Davidson]

Thank you both! I had an "a-ha" moment when I read Equivalence (α := S) left_green_relation

Moritz Firsching said:

note that left_green_relation.symm and left_green_relation.trans also needed implicit arguments in order to match what Equivalence expects.

I had overlooked that but I now see that it matches the documentation in Mathlib. Why does left_green_relation.refl need an explicit argument but not symm and trans ?

[Kevin Buzzard]

Thinking of proofs as functions: the input to refl doesn't have anything of the form x ~ y, the input is x and the output is a proof of x ~ x. But the inputs to symm contain a proof of x ~ y and from that input Lean can figure out what x and y are so you don't need to give them explicitly.

[Peter Davidson]

I'm now thinking how I would formalise the following result from John Howie's book "Fundamentals of Semigourp Theory".

Let $a$ and $b$ be elements of a semigroup $S$. Then $a$ L $b$ if and only if there exist $x$ and $y$ in $S^1$ such that $x a = b$ and $y b = a$.

Here, $S^1$ is the monoid obtained from $S$ by adjoining an identity. I've defined this in Lean using
class SemigroupWithOne (S : Type) extends Semigroup S, MulOneClass S
but I don't know how to work with $S$ and $S^1$ in the same theorem.

[Eric Wieser]

SemigroupWithOne is just Monoid, I think

[Eric Wieser]

Are you looking for WithOne S? (docs#WithOne)

[Edward van de Meent]

using this, you could formalize thestatement as

example {S : Type*} [Semigroup S] (a b : S) : a L b ↔ ∃ x y : WithOne S, x * a = b ∧ y * b = a := by
  sorry

[Peter Davidson]

Eric Wieser said:

Are you looking for WithOne S? (docs#WithOne)

That's exactly what I was looking for. Thanks!