{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles
open import Algebra.Morphism.Structures
open import Relation.Binary.Core
module Algebra.Morphism.GroupMonomorphism
{a b ℓ₁ ℓ₂} {G₁ : RawGroup a ℓ₁} {G₂ : RawGroup b ℓ₂} {⟦_⟧}
(isGroupMonomorphism : IsGroupMonomorphism G₁ G₂ ⟦_⟧)
where
open IsGroupMonomorphism isGroupMonomorphism
open RawGroup G₁ renaming
(Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; _⁻¹ to _⁻¹₁; ε to ε₁)
open RawGroup G₂ renaming
(Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)
open import Algebra.Definitions
open import Algebra.Structures
open import Data.Product.Base using (_,_)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
open import Algebra.Morphism.MonoidMonomorphism
isMonoidMonomorphism public
module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
open ≈-Reasoning setoid
inverseˡ : LeftInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → LeftInverse _≈₁_ ε₁ _⁻¹₁ _∙_
inverseˡ invˡ x = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1597}{\htmlId{1624}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{1626}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#809}{\htmlId{1630}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1597}{\htmlId{1632}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ∙-homo (x ⁻¹₁ ) x ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1597}{\htmlId{1669}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{1671}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1597}{\htmlId{1681}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong (⁻¹-homo x) refl ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1597}{\htmlId{1720}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⁻¹₂ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1597}{\htmlId{1732}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ invˡ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1597}{\htmlId{1746}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
ε₂ ≈⟨ ε-homo ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#832}{\htmlId{1792}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ∎)
inverseʳ : RightInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → RightInverse _≈₁_ ε₁ _⁻¹₁ _∙_
inverseʳ invʳ x = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1892}{\htmlId{1919}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#809}{\htmlId{1921}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1892}{\htmlId{1923}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{1925}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ≈⟨ ∙-homo x (x ⁻¹₁) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1892}{\htmlId{1963}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1892}{\htmlId{1971}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{1973}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong refl (⁻¹-homo x) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1892}{\htmlId{2014}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1892}{\htmlId{2022}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⁻¹₂ ≈⟨ invʳ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1892}{\htmlId{2040}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
ε₂ ≈⟨ ε-homo ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#832}{\htmlId{2086}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ∎)
inverse : Inverse _≈₂_ ε₂ _⁻¹₂ _◦_ → Inverse _≈₁_ ε₁ _⁻¹₁ _∙_
inverse (invˡ , invʳ) = inverseˡ invˡ , inverseʳ invʳ
⁻¹-cong : Congruent₁ _≈₂_ _⁻¹₂ → Congruent₁ _≈₁_ _⁻¹₁
⁻¹-cong ⁻¹-cong {x} {y} x≈y = injective (begin
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2291}{\htmlId{2327}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{2329}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ≈⟨ ⁻¹-homo x ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2291}{\htmlId{2356}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⁻¹₂ ≈⟨ ⁻¹-cong (⟦⟧-cong x≈y) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2295}{\htmlId{2397}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⁻¹₂ ≈⟨ ⁻¹-homo y ⟨
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2295}{\htmlId{2426}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{2428}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ∎)
module _ (◦-isAbelianGroup : IsAbelianGroup _≈₂_ _◦_ ε₂ _⁻¹₂) where
open IsAbelianGroup ◦-isAbelianGroup renaming (∙-cong to ◦-cong; ⁻¹-cong to ⁻¹₂-cong)
open ≈-Reasoning setoid
⁻¹-distrib-∙ : (∀ x y → (x ◦ y) ⁻¹₂ ≈₂ (x ⁻¹₂) ◦ (y ⁻¹₂)) → (∀ x y → (x ∙ y) ⁻¹₁ ≈₁ (x ⁻¹₁) ∙ (y ⁻¹₁))
⁻¹-distrib-∙ ⁻¹-distrib-∙ x y = injective (begin
$\begin{pmatrix} (\,\href{Algebra.Morphism.GroupMonomorphism.html#2755}{\htmlId{2785}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#809}{\htmlId{2787}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#2757}{\htmlId{2789}{\htmlClass{Bound}{\text{y}}}}\,) \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{2792}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ≈⟨ ⁻¹-homo (x ∙ y) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2755}{\htmlId{2831}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#809}{\htmlId{2833}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#2757}{\htmlId{2835}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⁻¹₂ ≈⟨ ⁻¹₂-cong (∙-homo x y) ⟩
($\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2755}{\htmlId{2885}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2757}{\htmlId{2893}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$) ⁻¹₂ ≈⟨ ⁻¹-distrib-∙ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2755}{\htmlId{2922}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2757}{\htmlId{2928}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2755}{\htmlId{2940}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⁻¹₂ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2757}{\htmlId{2952}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⁻¹₂ ≈⟨ sym (◦-cong (⁻¹-homo x) (⁻¹-homo y)) ⟩
$\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2755}{\htmlId{3008}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{3010}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2757}{\htmlId{3020}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{3022}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ≈⟨ sym (∙-homo (x ⁻¹₁) (y ⁻¹₁)) ⟩
$\begin{pmatrix} (\,\href{Algebra.Morphism.GroupMonomorphism.html#2755}{\htmlId{3069}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{3071}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\,) \,\href{Algebra.Morphism.GroupMonomorphism.html#809}{\htmlId{3076}{\htmlClass{Function Operator}{\text{∙}}}}\, (\,\href{Algebra.Morphism.GroupMonomorphism.html#2757}{\htmlId{3079}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#821}{\htmlId{3081}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\,) \end{pmatrix}$ ∎)
isGroup : IsGroup _≈₂_ _◦_ ε₂ _⁻¹₂ → IsGroup _≈₁_ _∙_ ε₁ _⁻¹₁
isGroup isGroup = record
{ isMonoid = isMonoid G.isMonoid
; inverse = inverse G.isMagma G.inverse
; ⁻¹-cong = ⁻¹-cong G.isMagma G.⁻¹-cong
} where module G = IsGroup isGroup
isAbelianGroup : IsAbelianGroup _≈₂_ _◦_ ε₂ _⁻¹₂ → IsAbelianGroup _≈₁_ _∙_ ε₁ _⁻¹₁
isAbelianGroup isAbelianGroup = record
{ isGroup = isGroup G.isGroup
; comm = comm G.isMagma G.comm
} where module G = IsAbelianGroup isAbelianGroup