Inverse Semigroups

Stream: mathlib4

[Fabian Brenner]

Hello, during @Laurent Bartholdi 's seminar, I have formalised some basics about Inverse Semigroups. I chose the following definitions:

universe u

class RegularSemigroup (G : Type u) extends Semigroup G, Inv G where
  mul_inv_mul : ∀ s : G, s*s⁻¹*s = s
  inv_mul_inv : ∀ s : G, s⁻¹*s*s⁻¹ = s⁻¹

class InverseSemigroup (G : Type u) extends RegularSemigroup G where
  inv_unique: ∀ s t : G, s*t*s = s -> t*s*t = t -> s⁻¹ = t

structure PartialBij (X : Type u) where
hom : Pointed.Hom ⟨Option X, none⟩ ⟨Option X, none⟩
inv : Pointed.Hom ⟨Option X, none⟩ ⟨Option X, none⟩
hom_inv_id : ∀ x, (Pointed.Hom.comp hom inv).toFun x = x ∨ hom.toFun x = none
inv_hom_id : ∀ x, (Pointed.Hom.comp inv hom).toFun x = x ∨ inv.toFun x = none
hom_not_image_inv : ∀ x, (¬ ∃ x', inv.toFun x' = x) -> hom.toFun x = none
inv_not_image_hom : ∀ x, (¬ ∃ x', hom.toFun x' = x) -> inv.toFun x = none

The main theorems I proved are that a regular semigroup is an inverse semigroup iff the idempotents commute; and that the partial bijections I defined are an instance of inverse semigroups. I would be happy if I could contribute my work to mathlib. However, as I have just begun working with lean in April, I am sure my code is not yet ready to be added to mathlib and most probably needs to be refactored. Maybe even my definition of partial bijections isn't the most elegant. Therefore, I would be greatful if someone more experienced would review my code. Also, how should I provide my code to be reviewed, should I just copy it into this conversation or should I create a pull request to mathlib?

[Kim Morrison]

The best way to get review is definitely to open a PR!

[Kim Morrison]

https://leanprover-community.github.io/contribute/index.html

[Floris van Doorn]

Are you aware of docs#PartialEquiv ?

[Floris van Doorn]

Also, I'm wondering if the two new classes should be mixins. I would hate for type-class inference to get slower because of two very rarely used classes.