------------------------------------------------------------------------
-- 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
⟦ x ⁻¹₁ ∙ x ⟧ ≈⟨ ∙-homo (x ⁻¹₁ ) x ⟩
⟦ x ⁻¹₁ ⟧ ◦ ⟦ x ⟧ ≈⟨ ◦-cong (⁻¹-homo x) refl ⟩
⟦ x ⟧ ⁻¹₂ ◦ ⟦ x ⟧ ≈⟨ invˡ ⟦ x ⟧ ⟩
ε₂ ≈⟨ ε-homo ⟨
⟦ ε₁ ⟧ ∎)
inverseʳ : RightInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → RightInverse _≈₁_ ε₁ _⁻¹₁ _∙_
inverseʳ invʳ x = injective (begin
⟦ x ∙ x ⁻¹₁ ⟧ ≈⟨ ∙-homo x (x ⁻¹₁) ⟩
⟦ x ⟧ ◦ ⟦ x ⁻¹₁ ⟧ ≈⟨ ◦-cong refl (⁻¹-homo x) ⟩
⟦ x ⟧ ◦ ⟦ x ⟧ ⁻¹₂ ≈⟨ invʳ ⟦ x ⟧ ⟩
ε₂ ≈⟨ ε-homo ⟨
⟦ ε₁ ⟧ ∎)
inverse : Inverse _≈₂_ ε₂ _⁻¹₂ _◦_ → Inverse _≈₁_ ε₁ _⁻¹₁ _∙_
inverse (invˡ , invʳ) = inverseˡ invˡ , inverseʳ invʳ
⁻¹-cong : Congruent₁ _≈₂_ _⁻¹₂ → Congruent₁ _≈₁_ _⁻¹₁
⁻¹-cong ⁻¹-cong {x} {y} x≈y = injective (begin
⟦ x ⁻¹₁ ⟧ ≈⟨ ⁻¹-homo x ⟩
⟦ x ⟧ ⁻¹₂ ≈⟨ ⁻¹-cong (⟦⟧-cong x≈y) ⟩
⟦ y ⟧ ⁻¹₂ ≈⟨ ⁻¹-homo y ⟨
⟦ y ⁻¹₁ ⟧ ∎)
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
⟦ (x ∙ y) ⁻¹₁ ⟧ ≈⟨ ⁻¹-homo (x ∙ y) ⟩
⟦ x ∙ y ⟧ ⁻¹₂ ≈⟨ ⁻¹₂-cong (∙-homo x y) ⟩
(⟦ x ⟧ ◦ ⟦ y ⟧) ⁻¹₂ ≈⟨ ⁻¹-distrib-∙ ⟦ x ⟧ ⟦ y ⟧ ⟩
⟦ x ⟧ ⁻¹₂ ◦ ⟦ y ⟧ ⁻¹₂ ≈⟨ sym (◦-cong (⁻¹-homo x) (⁻¹-homo y)) ⟩
⟦ x ⁻¹₁ ⟧ ◦ ⟦ y ⁻¹₁ ⟧ ≈⟨ sym (∙-homo (x ⁻¹₁) (y ⁻¹₁)) ⟩
⟦ (x ⁻¹₁) ∙ (y ⁻¹₁) ⟧ ∎)
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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4