algebra_groups_defs.lean

-- Stuff that's not there yet

class One (α : Type u) where
  one : α

instance [One α] : OfNat α (natLit! 1) where
  ofNat := One.one

class Inv (α : Type u) where
  inv : α → α

postfix:max "⁻¹" => Inv.inv

-- where is `u` coming from?
def Function.injective {α : Sort u} {β : Sort v} (f : α → β) : Prop :=
  ∀ a₁ a₂ : α, f a₁ = f a₂ → a₁ = a₂

theorem Function.injective.eqIff {α : Sort u} {β : Sort v} {f : α → β} (I : Function.injective f) {a b : α} :
  f a = f b ↔ a = b :=
⟨I a b, λ h => congrArg _ h⟩

-- Actual File from mathlib

universe u

section Mul

variables {G : Type u} [Mul G]

def leftMul : G → G → G := λ g : G => λ x : G => g * x 

def rightMul : G → G → G := λ g : G => λ x : G => x * g

end Mul

class Semigroup (G : Type u) extends Mul G where
  mulAssoc : ∀ a b c : G, (a * b) * c = a * (b * c)

section Semigroup

variables {G : Type u} [Semigroup G]

theorem mulAssoc : ∀ a b c : G, (a * b) * c = a * (b * c) := Semigroup.mulAssoc

end Semigroup

class CommSemigroup (G : Type u) extends Semigroup G where
  mulComm : ∀ a b : G, a * b = b * a

section CommSemigroup

variables {G : Type u} [CommSemigroup G]

theorem mulComm : ∀ a b : G, a * b = b * a := CommSemigroup.mulComm

end CommSemigroup

class LeftCancelSemigroup (G : Type u) extends Semigroup G where
  mulLeftCancel : ∀ a b c : G, a * b = a * c → b = c

section LeftCancelSemigroup

variables {G : Type u} [LeftCancelSemigroup G] {a b c : G}

theorem mulLeftCancel : a * b = a * c → b = c := LeftCancelSemigroup.mulLeftCancel a b c

theorem mulLeftCancelIff : a * b = a * c ↔ b = c :=
⟨mulLeftCancel, congrArg _⟩

-- It's \centerdot
theorem mulRightInjective (a : G) : Function.injective ((a * ·)) :=
λ b c => mulLeftCancel

theorem mulRightInj (a : G) {b c : G} : a * b = a * c ↔ b = c :=
(mulRightInjective a).eqIff

end LeftCancelSemigroup

class RightCancelSemigroup (G : Type u) extends Semigroup G where
  mulRightCancel : ∀ a b c : G, a * b = c * b → a = c

section RightCancelSemigroup

variables {G : Type u} [RightCancelSemigroup G] {a b c : G}

theorem mulRightCancel : a * b = c * b → a = c := RightCancelSemigroup.mulRightCancel a b c

theorem mulRightCancelIff : a * b = c * b ↔ a = c :=
⟨mulRightCancel, congrArg (· * b)⟩ -- mathlib Lean 3 proof is ⟨mul_right_cancel, congr_arg _⟩

theorem mulLeftInjective (a : G) : Function.injective (· * a) :=
λ b c => mulRightCancel

theorem mulLeftInj (a : G) {b c : G} : b * a = c * a ↔ b = c :=
(mulLeftInjective a).eqIff

end RightCancelSemigroup

class Monoid (M : Type u) extends Semigroup M, One M where
  oneMul : ∀ a : M, 1 * a = a
  mulOne : ∀ a : M, a * 1 = a

section Monoid

variables {M : Type u} [Monoid M]

theorem oneMul : ∀ a : M, 1 * a = a := Monoid.oneMul

theorem mulOne : ∀ a : M, a * 1 = a := Monoid.mulOne

theorem leftInvEqRightInv {a b c : M} (hba : b * a = 1) (hac : a * c = 1) : b = c := by
  rw [←oneMul c, ←hba, mulAssoc, hac, mulOne]

end Monoid

-- This no longer `extends` `CommSemigroup`
class CommMonoid (M : Type u) extends Monoid M where
  mulComm : ∀ a b : M, a * b = b * a

-- Instead, we have an instance going from `CommMonoid` to `CommSemigroup`
instance {M : Type u} [CommMonoid M] : CommSemigroup M where
  mulComm := CommMonoid.mulComm

section LeftCancelMonoid

-- Again, we only extend one `class` and we provide an instance to the other
class LeftCancelMonoid (M : Type u) extends Monoid M where
  mulLeftCancel : ∀ a b c : M, a * b = a * c → b = c

instance {M : Type u} [LeftCancelMonoid M] : LeftCancelSemigroup M where
  mulLeftCancel := LeftCancelMonoid.mulLeftCancel

class LeftCancelCommMonoid (M : Type u) extends LeftCancelMonoid M where
  mulComm : ∀ a b : M, a * b = b * a

instance {M : Type u} [LeftCancelCommMonoid M] : CommMonoid M where
  mulComm := LeftCancelCommMonoid.mulComm

end LeftCancelMonoid

section RightCancelMonoid 

class RightCancelMonoid (M : Type u) extends Monoid M where
  mulRightCancel : ∀ a b c : M, a * b = c * b → a = c

instance {M : Type u} [RightCancelMonoid M] : RightCancelSemigroup M where
  mulRightCancel := RightCancelMonoid.mulRightCancel

class RightCancelCommMonoid (M : Type u) extends RightCancelMonoid M where
  mulComm : ∀ a b : M, a * b = b * a

instance {M : Type u} [RightCancelCommMonoid M] : CommMonoid M where
  mulComm := RightCancelCommMonoid.mulComm

end RightCancelMonoid

section CancelMonoid

class CancelMonoid (M : Type u) extends LeftCancelMonoid M where
  mulRightCancel : ∀ a b c : M, a * b = c * b → a = c

instance {M : Type u} [CancelMonoid M] : RightCancelMonoid M where
  mulRightCancel := CancelMonoid.mulRightCancel

class CancelCommMonoid (M : Type u) extends LeftCancelCommMonoid M where
  mulRightCancel : ∀ a b c : M, a * b = c * b → a = c

instance {M : Type u} [CancelCommMonoid M] : RightCancelCommMonoid M where
  mulRightCancel := CancelCommMonoid.mulRightCancel
  mulComm := λ a b => mulComm a b -- why is the λ necessary?

end CancelMonoid

class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
  div := λ a b => a * b⁻¹
  divEqMulInv : ∀ a b : G, a / b = a * b⁻¹

theorem divEqMulInv {G : Type u} [DivInvMonoid G] :
  ∀ a b : G, a / b = a * b⁻¹ :=
DivInvMonoid.divEqMulInv

class Group (G : Type u) extends DivInvMonoid G where
  mulLeftInv : ∀ a : G, a⁻¹ * a = 1

def Group.toMonoid (G : Type u) [Group G] : Monoid G :=
  (Group.toDivInvMonoid (G := G)).toMonoid -- no more underscores!

section Group

variables {G : Type u} [Group G] {a b c : G}

@[simp]
theorem mulLeftInv : ∀ a : G, a⁻¹ * a = 1 := Group.mulLeftInv

@[simp]
theorem invMulCancelLeft (a b : G) : a⁻¹ * (a * b) = b := by
  rw [←mulAssoc, mulLeftInv, oneMul]

@[simp]
theorem invEqOfMulEqOne (h : a * b = 1) : a⁻¹ = b :=
  leftInvEqRightInv (mulLeftInv _) h

@[simp]
theorem invInv (a : G) : a⁻¹⁻¹ = a :=
  invEqOfMulEqOne (mulLeftInv _)

@[simp]
theorem mulRightInv (a : G) : a * a⁻¹ = 1 :=
  have a⁻¹⁻¹ * a⁻¹ = 1 := mulLeftInv a⁻¹
  by rw invInv at this
     assumption

theorem mulInvSelf (a : G) : a * a⁻¹ = 1 := mulRightInv a

theorem mulInvCancelRight (a b : G) : a * b * b⁻¹ = a := by
  rw [mulAssoc, mulRightInv, mulOne]

instance : CancelMonoid G where 
  mulLeftCancel := λ a b c h => by rw [←invMulCancelLeft a b, h, invMulCancelLeft]
  mulRightCancel := λ a b c h => by rw [←mulInvCancelRight a b, h, mulInvCancelRight]

end Group

class CommGroup (G : Type u) extends Group G where
  mulComm : ∀ a b : G, a * b = b * a

instance (G : Type u) [CommGroup G] : CommMonoid G where
  mulComm := CommGroup.mulComm

Re the comment on line 15:
https://leanprover.github.io/lean4/doc/autobound.html?highlight=lower#auto-bound-implict-arguments

Re the comment on line 15:
https://leanprover.github.io/lean4/doc/autobound.html?highlight=lower#auto-bound-implict-arguments

Thanks! I knew it could generate variables and types, but I didn't know it could synthesize universes as well.