------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties of Magma homomorphisms
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Morphism.Consequences where
open import Algebra using (Magma)
open import Algebra.Morphism.Definitions using (Homomorphic₂)
open import Data.Product.Base using (_,_)
open import Function.Base using (id; _∘_)
open import Function.Definitions
using (Injective; Congruent; Inverseᵇ; Inverseˡ)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
------------------------------------------------------------------------
-- If f and g are mutually inverse maps between A and B, g is congruent,
-- f is a homomorphism, then g is a homomorphism.
module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where
private
open module M₁ = Magma M₁ using () renaming (_≈_ to _≈₁_; _∙_ to _∙₁_)
open module M₂ = Magma M₂ using () renaming (_≈_ to _≈₂_; _∙_ to _∙₂_)
homomorphic₂-inv : ∀ {f g} → Congruent _≈₂_ _≈₁_ g →
Inverseᵇ _≈₁_ _≈₂_ f g →
Homomorphic₂ _ _ _≈₂_ f _∙₁_ _∙₂_ →
Homomorphic₂ _ _ _≈₁_ g _∙₂_ _∙₁_
homomorphic₂-inv {f} {g} g-cong (invˡ , invʳ) homo x y = begin
g (x ∙₂ y) ≈⟨ g-cong (M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl)) ⟨
g (f (g x) ∙₂ f (g y)) ≈⟨ g-cong (homo (g x) (g y)) ⟨
g (f (g x ∙₁ g y)) ≈⟨ invʳ M₂.refl ⟩
g x ∙₁ g y ∎
where open ≈-Reasoning M₁.setoid
homomorphic₂-inj : ∀ {f g} → Injective _≈₁_ _≈₂_ f →
Inverseˡ _≈₁_ _≈₂_ f g →
Homomorphic₂ _ _ _≈₂_ f _∙₁_ _∙₂_ →
Homomorphic₂ _ _ _≈₁_ g _∙₂_ _∙₁_
homomorphic₂-inj {f} {g} inj invˡ homo x y = inj (begin
f (g (x ∙₂ y)) ≈⟨ invˡ M₁.refl ⟩
x ∙₂ y ≈⟨ M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl) ⟨
f (g x) ∙₂ f (g y) ≈⟨ homo (g x) (g y) ⟨
f (g x ∙₁ g y) ∎)
where open ≈-Reasoning M₂.setoid
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