binary.lean for arbitrary groupoid-like structures

binary.lean

/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Module: algebra.binary
Authors: Leonardo de Moura, Jeremy Avigad

General properties of binary operations.
-/

import logic.eq
open eq.ops

namespace binary
  section
    variable {ob : Type}
    variable {mor : ob → ob → Type}
    variable (op₁ : Π {a b c : ob}, mor a b → mor b c → mor a c)
    variable (inv : Π {a b : ob}, mor a b → mor b a)
    variable (one : Π {a : ob}, mor a a)

    notation [local] a * b := op₁ a b
    notation [local] a ⁻¹  := inv a
    notation [local] 1     := one

    definition commutative := Π {x} (a : mor x x) (b : mor x x), a*b = b*a
    definition associative := Π {x y z w} (a : mor x y) (b : mor y z) (c : mor z w), (a*b)*c = a*(b*c)
    definition left_identity := Π {x y} (a : mor x y), 1 * a = a
    definition right_identity := Π {x y} (a : mor x y), a * 1 = a
    definition left_inverse := Π {x y} (a : mor x y), a⁻¹ * a = 1
    definition right_inverse := Π {x y} (a : mor x y), a * a⁻¹ = 1
    definition left_cancelative := Π {x y z} (a : mor x y) (b c : mor y z), a * b = a * c → b = c
    definition right_cancelative := Π {x y z} (a c : mor x y) (b : mor y z), a * b = c * b → a = c

    definition inv_op_cancel_left := Π {x y z} (a : mor x y) (b : mor y z), a⁻¹ * (a * b) = b
    definition op_inv_cancel_left := Π {x y z} (a : mor x y) (b : mor x z) , a * (a⁻¹ * b) = b
    definition inv_op_cancel_right := Π {x y z} (a : mor x z) (b : mor y z), a * b⁻¹ * b =  a
    definition op_inv_cancel_right := Π {x y z} (a : mor x y) (b : mor y z), a * b * b⁻¹ = a

    variable (op₂ : Π {x y : ob}, mor x y → mor x y → mor x y)

    notation [local] a + b := op₂ a b

    definition left_distributive := Π {x y z} (a : mor x y) (b c : mor y z), a * (b + c) = a * b + a * c
    definition right_distributive := Π {x y z} (a b : mor x y) (c : mor y z), (a + b) * c = a * c + b * c
  end

  context
    variable {ob : Type}
    variable {mor : ob → ob → Type}
    variable {f : Π {x y z : ob}, mor x y → mor y z → mor x z}
    variable H_comm : commutative @f
    variable H_assoc : associative @f
    infixl `*` := f
    theorem left_comm : Π {x} (a b c : mor x x), a*(b*c) = b*(a*c) :=
    take x a b c, calc
      a*(b*c) = (a*b)*c  : H_assoc
        ...   = (b*a)*c  : H_comm
        ...   = b*(a*c)  : H_assoc

    theorem right_comm : Π {x} (a b c : mor x x), (a*b)*c = (a*c)*b :=
    take x a b c, calc
      (a*b)*c = a*(b*c) : H_assoc
        ...   = a*(c*b) : H_comm
        ...   = (a*c)*b : H_assoc
  end

  context
    variable {ob : Type}
    variable {mor : ob → ob → Type}
    variable {f : Π {x y z : ob}, mor x y → mor y z → mor x z}
    variable H_assoc : associative @f
    infixl `*` := f
    theorem assoc4helper {x y z w q} (a : mor x y) (b : mor y z) (c : mor z w) (d : mor w q)
        : (a*b)*(c*d) = a*((b*c)*d) :=
    calc
      (a*b)*(c*d) = a*(b*(c*d)) : H_assoc
              ... = a*((b*c)*d) : H_assoc
  end

end binary