------------------------------------------------------------------------
-- 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

import Algebra.Properties.Loop as LoopProperties
import Algebra.Properties.Quasigroup as QuasigroupProperties
open import Data.Product.Base using (_,_)
open import Function.Base using (_$_)
open import Function.Definitions

open Group G
open import Algebra.Consequences.Setoid setoid
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup)
open import Relation.Binary.Reasoning.Setoid setoid

\\-cong₂ : Congruent₂ _\\_
\\-cong₂ x≈y u≈v = ∙-cong (⁻¹-cong x≈y) u≈v

//-cong₂ : Congruent₂ _//_
//-cong₂ x≈y u≈v = ∙-cong x≈y (⁻¹-cong u≈v)

------------------------------------------------------------------------
-- Groups are quasi-groups

\\-leftDividesˡ : LeftDividesˡ _∙_ _\\_
\\-leftDividesˡ x y = begin
  x  ∙ (x \\ y)  ≈⟨ assoc x (x ⁻¹) y ⟨
  x ∙ x ⁻¹ ∙ y   ≈⟨ ∙-congʳ (inverseʳ x) ⟩
  ε ∙ y          ≈⟨ identityˡ y ⟩
  y              ∎

\\-leftDividesʳ : LeftDividesʳ _∙_ _\\_
\\-leftDividesʳ x y = begin
  x \\ x ∙ y     ≈⟨ assoc (x ⁻¹) x y ⟨
  x ⁻¹ ∙ x ∙ y   ≈⟨ ∙-congʳ (inverseˡ x) ⟩
  ε ∙ y          ≈⟨ identityˡ y ⟩
  y              ∎


\\-leftDivides : LeftDivides _∙_ _\\_
\\-leftDivides = \\-leftDividesˡ , \\-leftDividesʳ

//-rightDividesˡ : RightDividesˡ _∙_ _//_
//-rightDividesˡ x y = begin
  (y // x) ∙ x    ≈⟨ assoc y (x ⁻¹) x ⟩
  y ∙ (x ⁻¹ ∙ x)  ≈⟨ ∙-congˡ (inverseˡ x) ⟩
  y ∙ ε           ≈⟨ identityʳ y ⟩
  y               ∎

//-rightDividesʳ : RightDividesʳ _∙_ _//_
//-rightDividesʳ x y = begin
  y ∙ x // x    ≈⟨ assoc y x (x ⁻¹) ⟩
  y ∙ (x // x)  ≈⟨ ∙-congˡ (inverseʳ x) ⟩
  y ∙ ε         ≈⟨ identityʳ y ⟩
  y             ∎

//-rightDivides : RightDivides _∙_ _//_
//-rightDivides = //-rightDividesˡ , //-rightDividesʳ

isQuasigroup : IsQuasigroup _∙_ _\\_ _//_
isQuasigroup = record
  { isMagma = isMagma
  ; \\-cong = \\-cong₂
  ; //-cong = //-cong₂
  ; leftDivides = \\-leftDivides
  ; rightDivides = //-rightDivides
  }

quasigroup : Quasigroup _ _
quasigroup = record { isQuasigroup = isQuasigroup }

open QuasigroupProperties quasigroup public
  using (x≈z//y; y≈x\\z)
  renaming (cancelˡ to ∙-cancelˡ; cancelʳ to ∙-cancelʳ; cancel to ∙-cancel)

------------------------------------------------------------------------
-- Groups are loops

isLoop : IsLoop _∙_ _\\_ _//_ ε
isLoop = record { isQuasigroup = isQuasigroup ; identity = identity }

loop : Loop _ _
loop = record { isLoop = isLoop }

open LoopProperties loop public
  using (identityˡ-unique; identityʳ-unique; identity-unique)

------------------------------------------------------------------------
-- Other properties

inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹
inverseˡ-unique x y eq = trans (x≈z//y x y ε eq) (identityˡ _)

inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹
inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _)

ε⁻¹≈ε : ε ⁻¹ ≈ ε
ε⁻¹≈ε = sym $ inverseˡ-unique _ _ (identityˡ ε)

⁻¹-selfInverse : SelfInverse _⁻¹
⁻¹-selfInverse {x} {y} eq = sym $ inverseˡ-unique x y $ begin
  x ∙ y    ≈⟨ ∙-congˡ eq ⟨
  x ∙ x ⁻¹ ≈⟨ inverseʳ x  ⟩
  ε        ∎

⁻¹-involutive : Involutive _⁻¹
⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse

x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y
x∙y⁻¹≈ε⇒x≈y x y x∙y⁻¹≈ε = begin
  x         ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
  y ⁻¹ ⁻¹   ≈⟨ ⁻¹-involutive y ⟩
  y         ∎

x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε
x≈y⇒x∙y⁻¹≈ε {x} {y} x≈y = begin
  x ∙ y ⁻¹ ≈⟨ ∙-congʳ x≈y ⟩
  y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
  ε        ∎

⁻¹-injective : Injective _≈_ _≈_ _⁻¹
⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse

⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹
⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ $ begin
  x ∙ y ∙ (x ∙ y) ⁻¹    ≈⟨ inverseʳ _ ⟩
  ε                     ≈⟨ inverseʳ _ ⟨
  x ∙ x ⁻¹              ≈⟨ ∙-congʳ (//-rightDividesʳ y x) ⟨
  (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
  x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎

⁻¹-anti-homo-// : ∀ x y → (x // y) ⁻¹ ≈ y // x
⁻¹-anti-homo-// x y = begin
  (x // y) ⁻¹      ≡⟨⟩
  (x ∙ y ⁻¹) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ x (y ⁻¹) ⟩
  (y ⁻¹) ⁻¹ ∙ x ⁻¹ ≈⟨ ∙-congʳ (⁻¹-involutive y) ⟩
  y ∙ x ⁻¹         ≡⟨⟩
  y // x ∎

⁻¹-anti-homo-\\ : ∀ x y → (x \\ y) ⁻¹ ≈ y \\ x
⁻¹-anti-homo-\\ x y = begin
  (x \\ y) ⁻¹      ≡⟨⟩
  (x ⁻¹ ∙ y) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ (x ⁻¹) y ⟩
  y ⁻¹ ∙ (x ⁻¹) ⁻¹ ≈⟨ ∙-congˡ (⁻¹-involutive x) ⟩
  y ⁻¹ ∙ x         ≡⟨⟩
  y \\ x ∎

\\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
\\≗flip-//⇒comm \\≗//ᵒ x y = begin
  x ∙ y                ≈⟨ ∙-congˡ (//-rightDividesˡ x y) ⟨
  x ∙ ((y // x) ∙ x)   ≈⟨ ∙-congˡ (∙-congʳ (\\≗//ᵒ x y)) ⟨
  x ∙ ((x \\ y) ∙ x)   ≈⟨ assoc x (x \\ y) x ⟨
  x ∙ (x \\ y) ∙ x     ≈⟨ ∙-congʳ (\\-leftDividesˡ x y) ⟩
  y ∙ x                ∎

comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
comm⇒\\≗flip-// comm x y = begin
  x \\ y    ≡⟨⟩
  x ⁻¹ ∙ y  ≈⟨ comm _ _ ⟩
  y ∙ x ⁻¹  ≡⟨⟩
  y // x    ∎