------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties ------------------------------------------------------------------------ {-# OPTIONS --without-K --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 open import Data.Product ε⁻¹≈ε : ε ⁻¹ ≈ ε ε⁻¹≈ε = 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ʳ x y ( 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 ⁻¹ ∎ ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version 1.1 left-identity-unique = identityˡ-unique {-# WARNING_ON_USAGE left-identity-unique "Warning: left-identity-unique was deprecated in v1.1. Please use identityˡ-unique instead." #-} right-identity-unique = identityʳ-unique {-# WARNING_ON_USAGE right-identity-unique "Warning: right-identity-unique was deprecated in v1.1. Please use identityʳ-unique instead." #-} left-inverse-unique = inverseˡ-unique {-# WARNING_ON_USAGE left-inverse-unique "Warning: left-inverse-unique was deprecated in v1.1. Please use inverseˡ-unique instead." #-} right-inverse-unique = inverseʳ-unique {-# WARNING_ON_USAGE right-inverse-unique "Warning: right-inverse-unique was deprecated in v1.1. Please use inverseʳ-unique instead." #-}