------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between group-like structures
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Bundles using (RawGroup)
open import Algebra.Morphism.Structures
  using (IsGroupMonomorphism; IsMonoidMonomorphism)
open import Function.Base using (_∘_)
open import Level using (_⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures using (IsEquivalence)

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
  using (Inverse; LeftInverse; RightInverse; Congruent₁)
open import Algebra.Structures
  using (IsMagma; IsGroup; IsAbelianGroup)
open import Data.Product.Base using (_,_)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

------------------------------------------------------------------------
-- Re-export all properties of monoid monomorphisms

open import Algebra.Morphism.MonoidMonomorphism
  isMonoidMonomorphism public

------------------------------------------------------------------------
-- Properties

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#1907}{\htmlId{1934}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{1936}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1019}{\htmlId{1940}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1907}{\htmlId{1942}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$     ≈⟨ ∙-homo (x ⁻¹₁ ) x ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1907}{\htmlId{1979}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{1981}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1907}{\htmlId{1991}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong (⁻¹-homo x) refl ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1907}{\htmlId{2030}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⁻¹₂ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1907}{\htmlId{2042}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ invˡ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1907}{\htmlId{2056}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
    ε₂                ≈⟨ ε-homo ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1042}{\htmlId{2102}{\htmlClass{Function}{\text{ε₁}}}}\, \end{pmatrix}$ ∎)

  inverseʳ : RightInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → RightInverse _≈₁_ ε₁ _⁻¹₁ _∙_
  inverseʳ invʳ x = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2202}{\htmlId{2229}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1019}{\htmlId{2231}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#2202}{\htmlId{2233}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{2235}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$     ≈⟨ ∙-homo x (x ⁻¹₁) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2202}{\htmlId{2273}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2202}{\htmlId{2281}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{2283}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ≈⟨ ◦-cong refl (⁻¹-homo x) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2202}{\htmlId{2324}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2202}{\htmlId{2332}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⁻¹₂ ≈⟨ invʳ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2202}{\htmlId{2350}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⟩
    ε₂                ≈⟨ ε-homo ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#1042}{\htmlId{2396}{\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#2601}{\htmlId{2637}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{2639}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ≈⟨ ⁻¹-homo x ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2601}{\htmlId{2666}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⁻¹₂ ≈⟨ ⁻¹-cong (⟦⟧-cong x≈y) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2605}{\htmlId{2707}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⁻¹₂ ≈⟨ ⁻¹-homo y ⟨
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#2605}{\htmlId{2736}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{2738}{\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} \,\htmlId{3094}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Morphism.GroupMonomorphism.html#3065}{\htmlId{3095}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1019}{\htmlId{3097}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#3067}{\htmlId{3099}{\htmlClass{Bound}{\text{y}}}}\,\,\htmlId{3100}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{3102}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$       ≈⟨ ⁻¹-homo (x ∙ y) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#3065}{\htmlId{3141}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1019}{\htmlId{3143}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#3067}{\htmlId{3145}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⁻¹₂         ≈⟨ ⁻¹₂-cong (∙-homo x y) ⟩
    ($\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#3065}{\htmlId{3195}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#3067}{\htmlId{3203}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$) ⁻¹₂   ≈⟨ ⁻¹-distrib-∙ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#3065}{\htmlId{3232}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#3067}{\htmlId{3238}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#3065}{\htmlId{3250}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⁻¹₂ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#3067}{\htmlId{3262}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⁻¹₂ ≈⟨ sym (◦-cong (⁻¹-homo x) (⁻¹-homo y)) ⟩
    $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#3065}{\htmlId{3318}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{3320}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ◦ $\begin{pmatrix} \,\href{Algebra.Morphism.GroupMonomorphism.html#3067}{\htmlId{3330}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{3332}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\, \end{pmatrix}$ ≈⟨ sym (∙-homo (x ⁻¹₁) (y ⁻¹₁)) ⟩
    $\begin{pmatrix} \,\htmlId{3378}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Morphism.GroupMonomorphism.html#3065}{\htmlId{3379}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{3381}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\,\,\htmlId{3384}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1019}{\htmlId{3386}{\htmlClass{Function Operator}{\text{∙}}}}\, \,\htmlId{3388}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Morphism.GroupMonomorphism.html#3067}{\htmlId{3389}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Morphism.GroupMonomorphism.html#1031}{\htmlId{3391}{\htmlClass{Function Operator}{\text{⁻¹₁}}}}\,\,\htmlId{3394}{\htmlClass{Symbol}{\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