/- Basics on monoids

   Clara L\"oh, 10/2025
-/

universe u -- fixing a background universe

-- Definition: monoids (unital, associative)
class monoid 
  (a : Type u) [BEq a] 
where
  -- structure
  comp : a -> a -> a
  e : a
  -- properties
  is_associative : ∀ (x : a) (y : a) (z : a), comp x (comp y z) = comp (comp x y) z
  is_neutral : ∀ (x : a), comp x e = x ∧ comp e x = x
  
-- inverses of elements in monoids  
def is_inverse_of 
  (a : Type u) [BEq a] [m : monoid a]
  (x : a)
  (y : a)
:= m.comp x y = m.e ∧ m.comp y x = m.e  

-- an element of a monoid is invertible if there exists an inverse element
def is_invertible
  (a : Type u) [BEq a] [m : monoid a]
  (x : a)
:= ∃ y : a, is_inverse_of a x y 

-- elements in monoids that behave like the neutral element
-- are equal to the neutral element
theorem neutral_element_is_unique
  (a : Type u) [BEq a] [m : monoid a]
  (e' : a)
  (is_neutral_e' : ∀ x : a, m.comp x e' = x ∧ m.comp e' x = x)
: m.e = e'
:=
calc
  m.e = m.comp m.e e' := by exact (is_neutral_e' m.e).1.symm
  _   = e'            := by exact (m.is_neutral e').2

-- Definition: monoid homomorphism
class monoid_hom 
  (a : Type u) [BEq a] [ma : monoid a] 
  (b : Type u) [BEq b] [mb : monoid b] 
where
  -- structure
  map : a -> b
  -- properties
  is_multiplicative : ∀ (x : a) (y : a), mb.comp (map x) (map y) = map (ma.comp x y) 
  preserves_neutral_elt : map (ma.e) = mb.e

-- applying a monoid homomorphism to an invertible element
-- results in an invertible element
theorem monoid_hom_of_invertible_element 
  (a : Type u) [BEq a] [ma : monoid a] 
  (b : Type u) [BEq b] [mb : monoid b] 
  (f : monoid_hom a b)
  (x : a)
  (is_inv_x : is_invertible a x)
: is_invertible b (f.map x)
:= 
by 
  -- because x is invertible, there is an inverse, called y
  have ⟨y, y_is_inv_of_x⟩ := is_inv_x

  -- we show that f(y) is the inverse of f(x),
  -- by verifying the two relevant equations
  have fy_is_inverse_of_fx : is_inverse_of b (f.map x) (f.map y)
  := by 
    have fxfy_is_e : mb.comp (f.map x) (f.map y) = mb.e 
    := calc mb.comp (f.map x) (f.map y) 
          = f.map (ma.comp x y) := by exact f.is_multiplicative x y  
        _ = f.map ma.e          := by rw[y_is_inv_of_x.1]
        _ = mb.e                := by exact f.preserves_neutral_elt 

    have fyfx_is_e : mb.comp (f.map y) (f.map x) = mb.e 
    := calc mb.comp (f.map y) (f.map x)
          = f.map (ma.comp y x) := by exact f.is_multiplicative y x 
        _ = f.map ma.e          := by rw[y_is_inv_of_x.2]
        _ = mb.e                := by exact f.preserves_neutral_elt

    exact And.intro fxfy_is_e fyfx_is_e

  -- the element f(y) witnesses that f(x) is invertible 
  show is_invertible b (f.map x) 
  exact Exists.intro (f.map y) fy_is_inverse_of_fx