Group with zeros (DivisionMonoid thoughts)

Stream: maths

[Kevin Buzzard]

There was a lengthy discussion about division monoids at Xena today. It claims in the docstring for docs#DivisionMonoid that "This is the immediate common ancestor of Group and GroupWithZero". However in a "design note" earlier in the file here several examples are given which are neither groups nor groups with zero. A lively discussion ensued about whether statements such as $aa^{-1}=a^{-1}a$ or $a^2a^{-1}=a$ or $\forall a, (aa^{-1}=1)\lor(aa^{-1}=a=a^{-1})$ were true for division monoids; turns out that none of them were true. A key example is that Finset sends division monoids to division monoids; these examples seem to be far from Group union GroupWithZero: if G is the free group on generators x,y then Finset G is a counterexample to all three statements with a={x,y}, a^2={x^2,xy,yx,y^2},a^{-1}={x^{-1},y^{-1}} etc.

Another thing we learnt was that you can add as many zeros as you like to a group and get a division monoid, as long as the zeros are linearly ordered :-) (the ordering tells you how to multiply them: you take the min). Feels a bit tropical?

import Mathlib.Tactic

universe u v

def WithZeros (G : Type u) [Group G] (L : Type v) [LinearOrder L] : Type _ := L ⊕ G

variable {G : Type u} [Group G] {L : Type v} [LinearOrder L]

namespace WithZeros

def one : WithZeros G L := .inr 1

instance : One (WithZeros G L) := ⟨one⟩

def mul : WithZeros G L → WithZeros G L → WithZeros G L
  | .inl a, .inl b => .inl (min a b)
  | .inl a, .inr _g => .inl a
  | .inr _g, .inl b => .inl b
  | .inr g, .inr h => .inr (g * h)

instance : Mul (WithZeros G L) := ⟨mul⟩

lemma one_mul (x : WithZeros G L) : 1 * x = x := by
  match x with
  | .inl a => rfl
  | .inr b =>
    change Sum.inr _ = Sum.inr _
    rw [_root_.one_mul]

lemma mul_one (x : WithZeros G L) : x * 1 = x := by
  match x with
  | .inl a => rfl
  | .inr b =>
    change Sum.inr _ = Sum.inr _
    rw [_root_.mul_one]

lemma mul_assoc (x y z : WithZeros G L) : x * y * z = x * (y * z) := by
  match x, y, z with
  | .inl a, .inl b, .inl c =>
    change Sum.inl _ = .inl _
    rw [min_assoc]
  | .inl a, .inl b, .inr g => rfl
  | .inl a, .inr g, .inl c => rfl
  | .inl a, .inr g, .inr h => rfl
  | .inr g, .inl b, .inl c => rfl
  | .inr g, .inl b, .inr h => rfl
  | .inr g, .inr h, .inl c => rfl
  | .inr g, .inr h, .inr k =>
    change Sum.inr _ = Sum.inr _
    rw [_root_.mul_assoc]

def inv : WithZeros G L → WithZeros G L
| .inl a => .inl a
| .inr g => .inr g⁻¹

instance : Inv (WithZeros G L) := ⟨inv⟩

lemma inv_inv (x : WithZeros G L) : x⁻¹⁻¹ = x := by
  match x with
  | .inl a => rfl
  | .inr g =>
    change Sum.inr _ = Sum.inr _
    rw [_root_.inv_inv]

lemma mul_inv_rev (x y : WithZeros G L) : (x * y)⁻¹ = y⁻¹ * x⁻¹ := by
  match x, y with
  | .inl a, .inl b =>
    change Sum.inl _ = .inl _
    rw [min_comm]
  | .inl a, .inr g => rfl
  | .inr g, .inl b => rfl
  | .inr g, .inr h =>
    change Sum.inr _ = .inr _
    rw [_root_.mul_inv_rev]

lemma inv_eq_of_mul (x y : WithZeros G L) (h : x * y = 1) : x⁻¹ = y := by
  match x, y, h with
  | .inr g, .inr h, h₁ =>
    change Sum.inr (g * h) = .inr 1 at h₁
    simp at h₁
    change Sum.inr _ = _
    congr
    exact DivisionMonoid.inv_eq_of_mul g h h₁

instance : DivisionMonoid (WithZeros G L) where
  mul := (· * ·)
  mul_assoc := mul_assoc
  one := 1
  one_mul := one_mul
  mul_one := mul_one
  inv_inv := inv_inv
  mul_inv_rev := mul_inv_rev
  inv_eq_of_mul := inv_eq_of_mul

end WithZeros

[Jireh Loreaux]

I think this belongs in Counterexamples or something.