------------------------------------------------------------------------ -- 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." #-}