@@ -10,99 +10,133 @@ open import Algebra.Bundles
1010
1111module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where
1212
13+ import Algebra.Properties.Loop as LoopProperties
14+ import Algebra.Properties.Quasigroup as QuasigroupProperties
15+ open import Data.Product.Base using (_,_)
16+ open import Function.Base using (_$_)
17+ open import Function.Definitions
18+
1319open Group G
20+ open import Algebra.Consequences.Setoid setoid
1421open import Algebra.Definitions _≈_
22+ open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup)
1523open import Relation.Binary.Reasoning.Setoid setoid
16- open import Function.Base using (_$_; _⟨_⟩_)
17- open import Data.Product.Base using (_,_; proj₂)
1824
19- ε⁻¹≈ε : ε ⁻¹ ≈ ε
20- ε⁻¹≈ε = begin
21- ε ⁻¹ ≈⟨ sym $ identityʳ (ε ⁻¹) ⟩
22- ε ⁻¹ ∙ ε ≈⟨ inverseˡ ε ⟩
23- ε ∎
24-
25- private
26-
27- left-helper : ∀ x y → x ≈ (x ∙ y) ∙ y ⁻¹
28- left-helper x y = begin
29- x ≈⟨ sym (identityʳ x) ⟩
30- x ∙ ε ≈⟨ ∙-congˡ $ sym (inverseʳ y) ⟩
31- x ∙ (y ∙ y ⁻¹) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
32- (x ∙ y) ∙ y ⁻¹ ∎
33-
34- right-helper : ∀ x y → y ≈ x ⁻¹ ∙ (x ∙ y)
35- right-helper x y = begin
36- y ≈⟨ sym (identityˡ y) ⟩
37- ε ∙ y ≈⟨ ∙-congʳ $ sym (inverseˡ x) ⟩
38- (x ⁻¹ ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
39- x ⁻¹ ∙ (x ∙ y) ∎
40-
41- ∙-cancelˡ : LeftCancellative _∙_
42- ∙-cancelˡ x y z eq = begin
43- y ≈⟨ right-helper x y ⟩
44- x ⁻¹ ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
45- x ⁻¹ ∙ (x ∙ z) ≈⟨ right-helper x z ⟨
46- z ∎
47-
48- ∙-cancelʳ : RightCancellative _∙_
49- ∙-cancelʳ x y z eq = begin
50- y ≈⟨ left-helper y x ⟩
51- y ∙ x ∙ x ⁻¹ ≈⟨ ∙-congʳ eq ⟩
52- z ∙ x ∙ x ⁻¹ ≈⟨ left-helper z x ⟨
53- z ∎
54-
55- ∙-cancel : Cancellative _∙_
56- ∙-cancel = ∙-cancelˡ , ∙-cancelʳ
57-
58- ⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x
59- ⁻¹-involutive x = begin
60- x ⁻¹ ⁻¹ ≈⟨ identityʳ _ ⟨
61- x ⁻¹ ⁻¹ ∙ ε ≈⟨ ∙-congˡ $ inverseˡ _ ⟨
62- x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x) ≈⟨ right-helper (x ⁻¹) x ⟨
63- x ∎
64-
65- ⁻¹-injective : ∀ {x y} → x ⁻¹ ≈ y ⁻¹ → x ≈ y
66- ⁻¹-injective {x} {y} eq = ∙-cancelʳ _ _ _ ( begin
67- x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩
68- ε ≈⟨ inverseʳ y ⟨
69- y ∙ y ⁻¹ ≈⟨ ∙-congˡ eq ⟨
70- y ∙ x ⁻¹ ∎ )
25+ \\-cong₂ : Congruent₂ _\\_
26+ \\-cong₂ x≈y u≈v = ∙-cong (⁻¹-cong x≈y) u≈v
7127
72- ⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹
73- ⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ ( begin
74- x ∙ y ∙ (x ∙ y) ⁻¹ ≈⟨ inverseʳ _ ⟩
75- ε ≈⟨ inverseʳ _ ⟨
76- x ∙ x ⁻¹ ≈⟨ ∙-congʳ (left-helper x y) ⟩
77- (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
78- x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎ )
28+ //-cong₂ : Congruent₂ _//_
29+ //-cong₂ x≈y u≈v = ∙-cong x≈y (⁻¹-cong u≈v)
30+
31+ ------------------------------------------------------------------------
32+ -- Groups are quasi-groups
33+
34+ \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_
35+ \\-leftDividesˡ x y = begin
36+ x ∙ (x \\ y) ≈⟨ assoc x (x ⁻¹) y ⟨
37+ x ∙ x ⁻¹ ∙ y ≈⟨ ∙-congʳ (inverseʳ x) ⟩
38+ ε ∙ y ≈⟨ identityˡ y ⟩
39+ y ∎
40+
41+ \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_
42+ \\-leftDividesʳ x y = begin
43+ x \\ x ∙ y ≈⟨ assoc (x ⁻¹) x y ⟨
44+ x ⁻¹ ∙ x ∙ y ≈⟨ ∙-congʳ (inverseˡ x) ⟩
45+ ε ∙ y ≈⟨ identityˡ y ⟩
46+ y ∎
47+
48+
49+ \\-leftDivides : LeftDivides _∙_ _\\_
50+ \\-leftDivides = \\-leftDividesˡ , \\-leftDividesʳ
51+
52+ //-rightDividesˡ : RightDividesˡ _∙_ _//_
53+ //-rightDividesˡ x y = begin
54+ (y // x) ∙ x ≈⟨ assoc y (x ⁻¹) x ⟩
55+ y ∙ (x ⁻¹ ∙ x) ≈⟨ ∙-congˡ (inverseˡ x) ⟩
56+ y ∙ ε ≈⟨ identityʳ y ⟩
57+ y ∎
58+
59+ //-rightDividesʳ : RightDividesʳ _∙_ _//_
60+ //-rightDividesʳ x y = begin
61+ y ∙ x // x ≈⟨ assoc y x (x ⁻¹) ⟩
62+ y ∙ (x // x) ≈⟨ ∙-congˡ (inverseʳ x) ⟩
63+ y ∙ ε ≈⟨ identityʳ y ⟩
64+ y ∎
65+
66+ //-rightDivides : RightDivides _∙_ _//_
67+ //-rightDivides = //-rightDividesˡ , //-rightDividesʳ
68+
69+ isQuasigroup : IsQuasigroup _∙_ _\\_ _//_
70+ isQuasigroup = record
71+ { isMagma = isMagma
72+ ; \\-cong = \\-cong₂
73+ ; //-cong = //-cong₂
74+ ; leftDivides = \\-leftDivides
75+ ; rightDivides = //-rightDivides
76+ }
77+
78+ quasigroup : Quasigroup _ _
79+ quasigroup = record { isQuasigroup = isQuasigroup }
80+
81+ open QuasigroupProperties quasigroup public
82+ using (x≈z//y; y≈x\\z)
83+ renaming (cancelˡ to ∙-cancelˡ; cancelʳ to ∙-cancelʳ; cancel to ∙-cancel)
84+
85+ ------------------------------------------------------------------------
86+ -- Groups are loops
87+
88+ isLoop : IsLoop _∙_ _\\_ _//_ ε
89+ isLoop = record { isQuasigroup = isQuasigroup ; identity = identity }
7990
80- identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
81- identityˡ-unique x y eq = begin
82- x ≈⟨ left-helper x y ⟩
83- (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩
84- y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
85- ε ∎
91+ loop : Loop _ _
92+ loop = record { isLoop = isLoop }
8693
87- identityʳ-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε
88- identityʳ-unique x y eq = begin
89- y ≈⟨ right-helper x y ⟩
90- x ⁻¹ ∙ (x ∙ y) ≈⟨ refl ⟨ ∙-cong ⟩ eq ⟩
91- x ⁻¹ ∙ x ≈⟨ inverseˡ x ⟩
92- ε ∎
94+ open LoopProperties loop public
95+ using (identityˡ-unique; identityʳ-unique; identity-unique)
9396
94- identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
95- identity-unique {x} id = identityˡ-unique x x (proj₂ id x)
97+ ------------------------------------------------------------------------
98+ -- Other properties
9699
97100inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹
98- inverseˡ-unique x y eq = begin
99- x ≈⟨ left-helper x y ⟩
100- (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩
101- ε ∙ y ⁻¹ ≈⟨ identityˡ (y ⁻¹) ⟩
102- y ⁻¹ ∎
101+ inverseˡ-unique x y eq = trans (x≈z//y x y ε eq) (identityˡ _)
103102
104103inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹
105- inverseʳ-unique x y eq = begin
106- y ≈⟨ sym (⁻¹-involutive y) ⟩
107- y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (inverseˡ-unique x y eq)) ⟩
108- x ⁻¹ ∎
104+ inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _)
105+
106+ ε⁻¹≈ε : ε ⁻¹ ≈ ε
107+ ε⁻¹≈ε = sym $ inverseˡ-unique _ _ (identityˡ ε)
108+
109+ ⁻¹-selfInverse : SelfInverse _⁻¹
110+ ⁻¹-selfInverse {x} {y} eq = sym $ inverseˡ-unique x y $ begin
111+ x ∙ y ≈⟨ ∙-congˡ eq ⟨
112+ x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩
113+ ε ∎
114+
115+ ⁻¹-involutive : Involutive _⁻¹
116+ ⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse
117+
118+ ⁻¹-injective : Injective _≈_ _≈_ _⁻¹
119+ ⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse
120+
121+ ⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹
122+ ⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ $ begin
123+ x ∙ y ∙ (x ∙ y) ⁻¹ ≈⟨ inverseʳ _ ⟩
124+ ε ≈⟨ inverseʳ _ ⟨
125+ x ∙ x ⁻¹ ≈⟨ ∙-congʳ (//-rightDividesʳ y x) ⟨
126+ (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
127+ x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎
128+
129+ \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
130+ \\≗flip-//⇒comm \\≗//ᵒ x y = begin
131+ x ∙ y ≈⟨ ∙-congˡ (//-rightDividesˡ x y) ⟨
132+ x ∙ ((y // x) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (\\≗//ᵒ x y)) ⟨
133+ x ∙ ((x \\ y) ∙ x) ≈⟨ assoc x (x \\ y) x ⟨
134+ x ∙ (x \\ y) ∙ x ≈⟨ ∙-congʳ (\\-leftDividesˡ x y) ⟩
135+ y ∙ x ∎
136+
137+ comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
138+ comm⇒\\≗flip-// comm x y = begin
139+ x \\ y ≡⟨⟩
140+ x ⁻¹ ∙ y ≈⟨ comm _ _ ⟩
141+ y ∙ x ⁻¹ ≡⟨⟩
142+ y // x ∎
0 commit comments