{-# OPTIONS --safe --cubical-compatible #-}
module Algebra.Morphism.Construct.Composition where
open import Algebra.Bundles
open import Algebra.Morphism.Structures
open import Function.Base using (_∘_)
import Function.Construct.Composition as Func
open import Level using (Level)
open import Relation.Binary.Morphism.Construct.Composition
open import Relation.Binary.Definitions using (Transitive)
private
variable
a b c ℓ₁ ℓ₂ ℓ₃ : Level
module _ {M₁ : RawMagma a ℓ₁}
{M₂ : RawMagma b ℓ₂}
{M₃ : RawMagma c ℓ₃}
(open RawMagma)
(≈₃-trans : Transitive (_≈_ M₃))
{f : Carrier M₁ → Carrier M₂}
{g : Carrier M₂ → Carrier M₃}
where
isMagmaHomomorphism
: IsMagmaHomomorphism M₁ M₂ f
→ IsMagmaHomomorphism M₂ M₃ g
→ IsMagmaHomomorphism M₁ M₃ (g ∘ f)
isMagmaHomomorphism f-homo g-homo = record
{ isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism
; homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.homo x y)) (G.homo (f x) (f y))
} where module F = IsMagmaHomomorphism f-homo; module G = IsMagmaHomomorphism g-homo
isMagmaMonomorphism
: IsMagmaMonomorphism M₁ M₂ f
→ IsMagmaMonomorphism M₂ M₃ g
→ IsMagmaMonomorphism M₁ M₃ (g ∘ f)
isMagmaMonomorphism f-mono g-mono = record
{ isMagmaHomomorphism = isMagmaHomomorphism F.isMagmaHomomorphism G.isMagmaHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsMagmaMonomorphism f-mono; module G = IsMagmaMonomorphism g-mono
isMagmaIsomorphism
: IsMagmaIsomorphism M₁ M₂ f
→ IsMagmaIsomorphism M₂ M₃ g
→ IsMagmaIsomorphism M₁ M₃ (g ∘ f)
isMagmaIsomorphism f-iso g-iso = record
{ isMagmaMonomorphism = isMagmaMonomorphism F.isMagmaMonomorphism G.isMagmaMonomorphism
; surjective = Func.surjective _ _ (_≈_ M₃) F.surjective G.surjective
} where module F = IsMagmaIsomorphism f-iso; module G = IsMagmaIsomorphism g-iso
module _ {M₁ : RawMonoid a ℓ₁}
{M₂ : RawMonoid b ℓ₂}
{M₃ : RawMonoid c ℓ₃}
(open RawMonoid)
(≈₃-trans : Transitive (_≈_ M₃))
{f : Carrier M₁ → Carrier M₂}
{g : Carrier M₂ → Carrier M₃}
where
isMonoidHomomorphism
: IsMonoidHomomorphism M₁ M₂ f
→ IsMonoidHomomorphism M₂ M₃ g
→ IsMonoidHomomorphism M₁ M₃ (g ∘ f)
isMonoidHomomorphism f-homo g-homo = record
{ isMagmaHomomorphism = isMagmaHomomorphism ≈₃-trans F.isMagmaHomomorphism G.isMagmaHomomorphism
; ε-homo = ≈₃-trans (G.⟦⟧-cong F.ε-homo) G.ε-homo
} where module F = IsMonoidHomomorphism f-homo; module G = IsMonoidHomomorphism g-homo
isMonoidMonomorphism
: IsMonoidMonomorphism M₁ M₂ f
→ IsMonoidMonomorphism M₂ M₃ g
→ IsMonoidMonomorphism M₁ M₃ (g ∘ f)
isMonoidMonomorphism f-mono g-mono = record
{ isMonoidHomomorphism = isMonoidHomomorphism F.isMonoidHomomorphism G.isMonoidHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsMonoidMonomorphism f-mono; module G = IsMonoidMonomorphism g-mono
isMonoidIsomorphism
: IsMonoidIsomorphism M₁ M₂ f
→ IsMonoidIsomorphism M₂ M₃ g
→ IsMonoidIsomorphism M₁ M₃ (g ∘ f)
isMonoidIsomorphism f-iso g-iso = record
{ isMonoidMonomorphism = isMonoidMonomorphism F.isMonoidMonomorphism G.isMonoidMonomorphism
; surjective = Func.surjective _ _(_≈_ M₃) F.surjective G.surjective
} where module F = IsMonoidIsomorphism f-iso; module G = IsMonoidIsomorphism g-iso
module _ {G₁ : RawGroup a ℓ₁}
{G₂ : RawGroup b ℓ₂}
{G₃ : RawGroup c ℓ₃}
(open RawGroup)
(≈₃-trans : Transitive (_≈_ G₃))
{f : Carrier G₁ → Carrier G₂}
{g : Carrier G₂ → Carrier G₃}
where
isGroupHomomorphism
: IsGroupHomomorphism G₁ G₂ f
→ IsGroupHomomorphism G₂ G₃ g
→ IsGroupHomomorphism G₁ G₃ (g ∘ f)
isGroupHomomorphism f-homo g-homo = record
{ isMonoidHomomorphism = isMonoidHomomorphism ≈₃-trans F.isMonoidHomomorphism G.isMonoidHomomorphism
; ⁻¹-homo = λ x → ≈₃-trans (G.⟦⟧-cong (F.⁻¹-homo x)) (G.⁻¹-homo (f x))
} where module F = IsGroupHomomorphism f-homo; module G = IsGroupHomomorphism g-homo
isGroupMonomorphism
: IsGroupMonomorphism G₁ G₂ f
→ IsGroupMonomorphism G₂ G₃ g
→ IsGroupMonomorphism G₁ G₃ (g ∘ f)
isGroupMonomorphism f-mono g-mono = record
{ isGroupHomomorphism = isGroupHomomorphism F.isGroupHomomorphism G.isGroupHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsGroupMonomorphism f-mono; module G = IsGroupMonomorphism g-mono
isGroupIsomorphism
: IsGroupIsomorphism G₁ G₂ f
→ IsGroupIsomorphism G₂ G₃ g
→ IsGroupIsomorphism G₁ G₃ (g ∘ f)
isGroupIsomorphism f-iso g-iso = record
{ isGroupMonomorphism = isGroupMonomorphism F.isGroupMonomorphism G.isGroupMonomorphism
; surjective = Func.surjective _ _ (_≈_ G₃) F.surjective G.surjective
} where module F = IsGroupIsomorphism f-iso; module G = IsGroupIsomorphism g-iso
module _ {R₁ : RawNearSemiring a ℓ₁}
{R₂ : RawNearSemiring b ℓ₂}
{R₃ : RawNearSemiring c ℓ₃}
(open RawNearSemiring)
(≈₃-trans : Transitive (_≈_ R₃))
{f : Carrier R₁ → Carrier R₂}
{g : Carrier R₂ → Carrier R₃}
where
isNearSemiringHomomorphism
: IsNearSemiringHomomorphism R₁ R₂ f
→ IsNearSemiringHomomorphism R₂ R₃ g
→ IsNearSemiringHomomorphism R₁ R₃ (g ∘ f)
isNearSemiringHomomorphism f-homo g-homo = record
{ +-isMonoidHomomorphism = isMonoidHomomorphism ≈₃-trans F.+-isMonoidHomomorphism G.+-isMonoidHomomorphism
; *-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.*-homo x y)) (G.*-homo (f x) (f y))
} where module F = IsNearSemiringHomomorphism f-homo; module G = IsNearSemiringHomomorphism g-homo
isNearSemiringMonomorphism
: IsNearSemiringMonomorphism R₁ R₂ f
→ IsNearSemiringMonomorphism R₂ R₃ g
→ IsNearSemiringMonomorphism R₁ R₃ (g ∘ f)
isNearSemiringMonomorphism f-mono g-mono = record
{ isNearSemiringHomomorphism = isNearSemiringHomomorphism F.isNearSemiringHomomorphism G.isNearSemiringHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsNearSemiringMonomorphism f-mono; module G = IsNearSemiringMonomorphism g-mono
isNearSemiringIsomorphism
: IsNearSemiringIsomorphism R₁ R₂ f
→ IsNearSemiringIsomorphism R₂ R₃ g
→ IsNearSemiringIsomorphism R₁ R₃ (g ∘ f)
isNearSemiringIsomorphism f-iso g-iso = record
{ isNearSemiringMonomorphism = isNearSemiringMonomorphism F.isNearSemiringMonomorphism G.isNearSemiringMonomorphism
; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
} where module F = IsNearSemiringIsomorphism f-iso; module G = IsNearSemiringIsomorphism g-iso
module _
{R₁ : RawSemiring a ℓ₁}
{R₂ : RawSemiring b ℓ₂}
{R₃ : RawSemiring c ℓ₃}
(open RawSemiring)
(≈₃-trans : Transitive (_≈_ R₃))
{f : Carrier R₁ → Carrier R₂}
{g : Carrier R₂ → Carrier R₃}
where
isSemiringHomomorphism
: IsSemiringHomomorphism R₁ R₂ f
→ IsSemiringHomomorphism R₂ R₃ g
→ IsSemiringHomomorphism R₁ R₃ (g ∘ f)
isSemiringHomomorphism f-homo g-homo = record
{ isNearSemiringHomomorphism = isNearSemiringHomomorphism ≈₃-trans F.isNearSemiringHomomorphism G.isNearSemiringHomomorphism
; 1#-homo = ≈₃-trans (G.⟦⟧-cong F.1#-homo) G.1#-homo
} where module F = IsSemiringHomomorphism f-homo; module G = IsSemiringHomomorphism g-homo
isSemiringMonomorphism
: IsSemiringMonomorphism R₁ R₂ f
→ IsSemiringMonomorphism R₂ R₃ g
→ IsSemiringMonomorphism R₁ R₃ (g ∘ f)
isSemiringMonomorphism f-mono g-mono = record
{ isSemiringHomomorphism = isSemiringHomomorphism F.isSemiringHomomorphism G.isSemiringHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsSemiringMonomorphism f-mono; module G = IsSemiringMonomorphism g-mono
isSemiringIsomorphism
: IsSemiringIsomorphism R₁ R₂ f
→ IsSemiringIsomorphism R₂ R₃ g
→ IsSemiringIsomorphism R₁ R₃ (g ∘ f)
isSemiringIsomorphism f-iso g-iso = record
{ isSemiringMonomorphism = isSemiringMonomorphism F.isSemiringMonomorphism G.isSemiringMonomorphism
; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
} where module F = IsSemiringIsomorphism f-iso; module G = IsSemiringIsomorphism g-iso
module _ {R₁ : RawRingWithoutOne a ℓ₁}
{R₂ : RawRingWithoutOne b ℓ₂}
{R₃ : RawRingWithoutOne c ℓ₃}
(open RawRingWithoutOne)
(≈₃-trans : Transitive (_≈_ R₃))
{f : Carrier R₁ → Carrier R₂}
{g : Carrier R₂ → Carrier R₃}
where
isRingWithoutOneHomomorphism
: IsRingWithoutOneHomomorphism R₁ R₂ f
→ IsRingWithoutOneHomomorphism R₂ R₃ g
→ IsRingWithoutOneHomomorphism R₁ R₃ (g ∘ f)
isRingWithoutOneHomomorphism f-homo g-homo = record
{ +-isGroupHomomorphism = isGroupHomomorphism ≈₃-trans F.+-isGroupHomomorphism G.+-isGroupHomomorphism
; *-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.*-homo x y)) (G.*-homo (f x) (f y))
} where module F = IsRingWithoutOneHomomorphism f-homo; module G = IsRingWithoutOneHomomorphism g-homo
isRingWithoutOneMonomorphism
: IsRingWithoutOneMonomorphism R₁ R₂ f
→ IsRingWithoutOneMonomorphism R₂ R₃ g
→ IsRingWithoutOneMonomorphism R₁ R₃ (g ∘ f)
isRingWithoutOneMonomorphism f-mono g-mono = record
{ isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism F.isRingWithoutOneHomomorphism G.isRingWithoutOneHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsRingWithoutOneMonomorphism f-mono; module G = IsRingWithoutOneMonomorphism g-mono
isRingWithoutOneIsoMorphism
: IsRingWithoutOneIsoMorphism R₁ R₂ f
→ IsRingWithoutOneIsoMorphism R₂ R₃ g
→ IsRingWithoutOneIsoMorphism R₁ R₃ (g ∘ f)
isRingWithoutOneIsoMorphism f-iso g-iso = record
{ isRingWithoutOneMonomorphism = isRingWithoutOneMonomorphism F.isRingWithoutOneMonomorphism G.isRingWithoutOneMonomorphism
; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
} where module F = IsRingWithoutOneIsoMorphism f-iso; module G = IsRingWithoutOneIsoMorphism g-iso
module _ {R₁ : RawRing a ℓ₁}
{R₂ : RawRing b ℓ₂}
{R₃ : RawRing c ℓ₃}
(open RawRing)
(≈₃-trans : Transitive (_≈_ R₃))
{f : Carrier R₁ → Carrier R₂}
{g : Carrier R₂ → Carrier R₃}
where
isRingHomomorphism
: IsRingHomomorphism R₁ R₂ f
→ IsRingHomomorphism R₂ R₃ g
→ IsRingHomomorphism R₁ R₃ (g ∘ f)
isRingHomomorphism f-homo g-homo = record
{ isSemiringHomomorphism = isSemiringHomomorphism ≈₃-trans F.isSemiringHomomorphism G.isSemiringHomomorphism
; -‿homo = λ x → ≈₃-trans (G.⟦⟧-cong (F.-‿homo x)) (G.-‿homo (f x))
} where module F = IsRingHomomorphism f-homo; module G = IsRingHomomorphism g-homo
isRingMonomorphism
: IsRingMonomorphism R₁ R₂ f
→ IsRingMonomorphism R₂ R₃ g
→ IsRingMonomorphism R₁ R₃ (g ∘ f)
isRingMonomorphism f-mono g-mono = record
{ isRingHomomorphism = isRingHomomorphism F.isRingHomomorphism G.isRingHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsRingMonomorphism f-mono; module G = IsRingMonomorphism g-mono
isRingIsomorphism
: IsRingIsomorphism R₁ R₂ f
→ IsRingIsomorphism R₂ R₃ g
→ IsRingIsomorphism R₁ R₃ (g ∘ f)
isRingIsomorphism f-iso g-iso = record
{ isRingMonomorphism = isRingMonomorphism F.isRingMonomorphism G.isRingMonomorphism
; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
} where module F = IsRingIsomorphism f-iso; module G = IsRingIsomorphism g-iso
module _ {Q₁ : RawQuasigroup a ℓ₁}
{Q₂ : RawQuasigroup b ℓ₂}
{Q₃ : RawQuasigroup c ℓ₃}
(open RawQuasigroup)
(≈₃-trans : Transitive (_≈_ Q₃))
{f : Carrier Q₁ → Carrier Q₂}
{g : Carrier Q₂ → Carrier Q₃}
where
isQuasigroupHomomorphism
: IsQuasigroupHomomorphism Q₁ Q₂ f
→ IsQuasigroupHomomorphism Q₂ Q₃ g
→ IsQuasigroupHomomorphism Q₁ Q₃ (g ∘ f)
isQuasigroupHomomorphism f-homo g-homo = record
{ isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism
; ∙-homo = λ x y → ≈₃-trans (G.⟦⟧-cong ( F.∙-homo x y )) ( G.∙-homo (f x) (f y) )
; \\-homo = λ x y → ≈₃-trans (G.⟦⟧-cong ( F.\\-homo x y )) ( G.\\-homo (f x) (f y) )
; //-homo = λ x y → ≈₃-trans (G.⟦⟧-cong ( F.//-homo x y )) ( G.//-homo (f x) (f y) )
} where module F = IsQuasigroupHomomorphism f-homo; module G = IsQuasigroupHomomorphism g-homo
isQuasigroupMonomorphism
: IsQuasigroupMonomorphism Q₁ Q₂ f
→ IsQuasigroupMonomorphism Q₂ Q₃ g
→ IsQuasigroupMonomorphism Q₁ Q₃ (g ∘ f)
isQuasigroupMonomorphism f-mono g-mono = record
{ isQuasigroupHomomorphism = isQuasigroupHomomorphism F.isQuasigroupHomomorphism G.isQuasigroupHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsQuasigroupMonomorphism f-mono; module G = IsQuasigroupMonomorphism g-mono
isQuasigroupIsomorphism
: IsQuasigroupIsomorphism Q₁ Q₂ f
→ IsQuasigroupIsomorphism Q₂ Q₃ g
→ IsQuasigroupIsomorphism Q₁ Q₃ (g ∘ f)
isQuasigroupIsomorphism f-iso g-iso = record
{ isQuasigroupMonomorphism = isQuasigroupMonomorphism F.isQuasigroupMonomorphism G.isQuasigroupMonomorphism
; surjective = Func.surjective _ _ (_≈_ Q₃) F.surjective G.surjective
} where module F = IsQuasigroupIsomorphism f-iso; module G = IsQuasigroupIsomorphism g-iso
module _ {L₁ : RawLoop a ℓ₁}
{L₂ : RawLoop b ℓ₂}
{L₃ : RawLoop c ℓ₃}
(open RawLoop)
(≈₃-trans : Transitive (_≈_ L₃))
{f : Carrier L₁ → Carrier L₂}
{g : Carrier L₂ → Carrier L₃}
where
isLoopHomomorphism
: IsLoopHomomorphism L₁ L₂ f
→ IsLoopHomomorphism L₂ L₃ g
→ IsLoopHomomorphism L₁ L₃ (g ∘ f)
isLoopHomomorphism f-homo g-homo = record
{ isQuasigroupHomomorphism = isQuasigroupHomomorphism ≈₃-trans F.isQuasigroupHomomorphism G.isQuasigroupHomomorphism
; ε-homo = ≈₃-trans (G.⟦⟧-cong F.ε-homo) G.ε-homo
} where module F = IsLoopHomomorphism f-homo; module G = IsLoopHomomorphism g-homo
isLoopMonomorphism
: IsLoopMonomorphism L₁ L₂ f
→ IsLoopMonomorphism L₂ L₃ g
→ IsLoopMonomorphism L₁ L₃ (g ∘ f)
isLoopMonomorphism f-mono g-mono = record
{ isLoopHomomorphism = isLoopHomomorphism F.isLoopHomomorphism G.isLoopHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsLoopMonomorphism f-mono; module G = IsLoopMonomorphism g-mono
isLoopIsomorphism
: IsLoopIsomorphism L₁ L₂ f
→ IsLoopIsomorphism L₂ L₃ g
→ IsLoopIsomorphism L₁ L₃ (g ∘ f)
isLoopIsomorphism f-iso g-iso = record
{ isLoopMonomorphism = isLoopMonomorphism F.isLoopMonomorphism G.isLoopMonomorphism
; surjective = Func.surjective _ _ (_≈_ L₃) F.surjective G.surjective
} where module F = IsLoopIsomorphism f-iso; module G = IsLoopIsomorphism g-iso
module _ {K₁ : RawKleeneAlgebra a ℓ₁}
{K₂ : RawKleeneAlgebra b ℓ₂}
{K₃ : RawKleeneAlgebra c ℓ₃}
(open RawKleeneAlgebra)
(≈₃-trans : Transitive (_≈_ K₃))
{f : Carrier K₁ → Carrier K₂}
{g : Carrier K₂ → Carrier K₃}
where
isKleeneAlgebraHomomorphism
: IsKleeneAlgebraHomomorphism K₁ K₂ f
→ IsKleeneAlgebraHomomorphism K₂ K₃ g
→ IsKleeneAlgebraHomomorphism K₁ K₃ (g ∘ f)
isKleeneAlgebraHomomorphism f-homo g-homo = record
{ isSemiringHomomorphism = isSemiringHomomorphism ≈₃-trans F.isSemiringHomomorphism G.isSemiringHomomorphism
; ⋆-homo = λ x → ≈₃-trans (G.⟦⟧-cong (F.⋆-homo x)) (G.⋆-homo (f x))
} where module F = IsKleeneAlgebraHomomorphism f-homo; module G = IsKleeneAlgebraHomomorphism g-homo
isKleeneAlgebraMonomorphism
: IsKleeneAlgebraMonomorphism K₁ K₂ f
→ IsKleeneAlgebraMonomorphism K₂ K₃ g
→ IsKleeneAlgebraMonomorphism K₁ K₃ (g ∘ f)
isKleeneAlgebraMonomorphism f-mono g-mono = record
{ isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism F.isKleeneAlgebraHomomorphism G.isKleeneAlgebraHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsKleeneAlgebraMonomorphism f-mono; module G = IsKleeneAlgebraMonomorphism g-mono
isKleeneAlgebraIsomorphism
: IsKleeneAlgebraIsomorphism K₁ K₂ f
→ IsKleeneAlgebraIsomorphism K₂ K₃ g
→ IsKleeneAlgebraIsomorphism K₁ K₃ (g ∘ f)
isKleeneAlgebraIsomorphism f-iso g-iso = record
{ isKleeneAlgebraMonomorphism = isKleeneAlgebraMonomorphism F.isKleeneAlgebraMonomorphism G.isKleeneAlgebraMonomorphism
; surjective = Func.surjective (_≈_ K₁) (_≈_ K₂) (_≈_ K₃) F.surjective G.surjective
} where module F = IsKleeneAlgebraIsomorphism f-iso; module G = IsKleeneAlgebraIsomorphism g-iso