{-# 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 ⁻¹ ∎