------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Bundles

module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where

open Group G
open import Algebra.Definitions _≈_
open import Relation.Binary.Reasoning.Setoid setoid
open import Function.Base using (_$_; _⟨_⟩_)
open import Data.Product.Base using (_,_; proj₂)

ε⁻¹≈ε : ε ⁻¹  ε
ε⁻¹≈ε = begin
  ε ⁻¹      ≈⟨ sym $ identityʳ (ε ⁻¹) 
  ε ⁻¹  ε  ≈⟨ inverseˡ ε 
  ε         

private

  left-helper :  x y  x  (x  y)  y ⁻¹
  left-helper x y = begin
    x              ≈⟨ sym (identityʳ x) 
    x  ε          ≈⟨ ∙-congˡ $ sym (inverseʳ y) 
    x  (y  y ⁻¹) ≈⟨ sym (assoc x y (y ⁻¹)) 
    (x  y)  y ⁻¹ 

  right-helper :  x y  y  x ⁻¹  (x  y)
  right-helper x y = begin
    y              ≈⟨ sym (identityˡ y) 
    ε           y ≈⟨ ∙-congʳ $ sym (inverseˡ x) 
    (x ⁻¹  x)  y ≈⟨ assoc (x ⁻¹) x y 
    x ⁻¹  (x  y) 

∙-cancelˡ : LeftCancellative _∙_
∙-cancelˡ x y z eq = begin
              y  ≈⟨ right-helper x y 
  x ⁻¹  (x  y) ≈⟨ ∙-congˡ eq 
  x ⁻¹  (x  z) ≈⟨ right-helper x z 
              z  

∙-cancelʳ : RightCancellative _∙_
∙-cancelʳ x y z eq = begin
  y            ≈⟨ left-helper y x 
  y  x  x ⁻¹ ≈⟨ ∙-congʳ eq 
  z  x  x ⁻¹ ≈⟨ left-helper z x 
  z            

∙-cancel : Cancellative _∙_
∙-cancel = ∙-cancelˡ , ∙-cancelʳ

⁻¹-involutive :  x  x ⁻¹ ⁻¹  x
⁻¹-involutive x = begin
  x ⁻¹ ⁻¹              ≈⟨ identityʳ _ 
  x ⁻¹ ⁻¹  ε          ≈⟨ ∙-congˡ $ inverseˡ _ 
  x ⁻¹ ⁻¹  (x ⁻¹  x) ≈⟨ right-helper (x ⁻¹) x 
  x                    

⁻¹-injective :  {x y}  x ⁻¹  y ⁻¹  x  y
⁻¹-injective {x} {y} eq = ∙-cancelʳ _ _ _ ( begin
  x  x ⁻¹ ≈⟨ inverseʳ x 
  ε        ≈⟨ inverseʳ y 
  y  y ⁻¹ ≈⟨ ∙-congˡ eq 
  y  x ⁻¹  )

⁻¹-anti-homo-∙ :  x y  (x  y) ⁻¹  y ⁻¹  x ⁻¹
⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ ( begin
  x  y  (x  y) ⁻¹    ≈⟨ inverseʳ _ 
  ε                     ≈⟨ inverseʳ _ 
  x  x ⁻¹              ≈⟨ ∙-congʳ (left-helper x y) 
  (x  y)  y ⁻¹  x ⁻¹ ≈⟨ assoc (x  y) (y ⁻¹) (x ⁻¹) 
  x  y  (y ⁻¹  x ⁻¹)  )

identityˡ-unique :  x y  x  y  y  x  ε
identityˡ-unique x y eq = begin
  x              ≈⟨ left-helper x y 
  (x  y)  y ⁻¹ ≈⟨ ∙-congʳ eq 
       y   y ⁻¹ ≈⟨ inverseʳ y 
  ε              

identityʳ-unique :  x y  x  y  x  y  ε
identityʳ-unique x y eq = begin
  y              ≈⟨ right-helper x y 
  x ⁻¹  (x  y) ≈⟨ refl  ∙-cong  eq 
  x ⁻¹   x      ≈⟨ inverseˡ x 
  ε              

identity-unique :  {x}  Identity x _∙_  x  ε
identity-unique {x} id = identityˡ-unique x x (proj₂ id x)

inverseˡ-unique :  x y  x  y  ε  x  y ⁻¹
inverseˡ-unique x y eq = begin
  x              ≈⟨ left-helper x y 
  (x  y)  y ⁻¹ ≈⟨ ∙-congʳ eq 
       ε   y ⁻¹ ≈⟨ identityˡ (y ⁻¹) 
            y ⁻¹ 

inverseʳ-unique :  x y  x  y  ε  y  x ⁻¹
inverseʳ-unique x y eq = begin
  y       ≈⟨ sym (⁻¹-involutive y) 
  y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (inverseˡ-unique x y eq)) 
  x ⁻¹