/usr/share/agda-stdlib/Algebra/Props/Group.agda is in agda-stdlib 0.7-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------
open import Algebra
module Algebra.Props.Group {g₁ g₂} (G : Group g₁ g₂) where
open Group G
import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Function
open import Data.Product
⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x
⁻¹-involutive x = begin
x ⁻¹ ⁻¹ ≈⟨ sym $ proj₂ identity _ ⟩
x ⁻¹ ⁻¹ ∙ ε ≈⟨ refl ⟨ ∙-cong ⟩ sym (proj₁ inverse _) ⟩
x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x) ≈⟨ sym $ assoc _ _ _ ⟩
x ⁻¹ ⁻¹ ∙ x ⁻¹ ∙ x ≈⟨ proj₁ inverse _ ⟨ ∙-cong ⟩ refl ⟩
ε ∙ x ≈⟨ proj₁ identity _ ⟩
x ∎
private
left-helper : ∀ x y → x ≈ (x ∙ y) ∙ y ⁻¹
left-helper x y = begin
x ≈⟨ sym (proj₂ identity x) ⟩
x ∙ ε ≈⟨ refl ⟨ ∙-cong ⟩ sym (proj₂ 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 (proj₁ identity y) ⟩
ε ∙ y ≈⟨ sym (proj₁ inverse x) ⟨ ∙-cong ⟩ refl ⟩
(x ⁻¹ ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
x ⁻¹ ∙ (x ∙ y) ∎
left-identity-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
left-identity-unique x y eq = begin
x ≈⟨ left-helper x y ⟩
(x ∙ y) ∙ y ⁻¹ ≈⟨ eq ⟨ ∙-cong ⟩ refl ⟩
y ∙ y ⁻¹ ≈⟨ proj₂ inverse y ⟩
ε ∎
right-identity-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε
right-identity-unique x y eq = begin
y ≈⟨ right-helper x y ⟩
x ⁻¹ ∙ (x ∙ y) ≈⟨ refl ⟨ ∙-cong ⟩ eq ⟩
x ⁻¹ ∙ x ≈⟨ proj₁ inverse x ⟩
ε ∎
identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
identity-unique {x} id = left-identity-unique x x (proj₂ id x)
left-inverse-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹
left-inverse-unique x y eq = begin
x ≈⟨ left-helper x y ⟩
(x ∙ y) ∙ y ⁻¹ ≈⟨ eq ⟨ ∙-cong ⟩ refl ⟩
ε ∙ y ⁻¹ ≈⟨ proj₁ identity (y ⁻¹) ⟩
y ⁻¹ ∎
right-inverse-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹
right-inverse-unique x y eq = begin
y ≈⟨ sym (⁻¹-involutive y) ⟩
y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (left-inverse-unique x y eq)) ⟩
x ⁻¹ ∎
|