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