← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Algebra/Properties/Group.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

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