From 05dbfcc6768435ca7272126efde52112995eed57 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 3 Feb 2024 18:28:53 +0100 Subject: [PATCH 01/22] First shot at left semimodule monomorphism consequences --- .../Morphism/LeftSemimoduleMonomorphism.agda | 143 ++++++++++++++++++ 1 file changed, 143 insertions(+) create mode 100644 src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda diff --git a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda new file mode 100644 index 0000000000..5f4211acd1 --- /dev/null +++ b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda @@ -0,0 +1,143 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between left semimodules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.LeftSemimoduleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M₁ : RawLeftSemimodule R a ℓ₁} {M₂ : RawLeftSemimodule R b ℓ₂} {⟦_⟧} + (isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ ⟦_⟧) + where + +open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism +open RawLeftSemimodule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_; _+ᴹ_ to _+ᴹ_; 0ᴹ to 0ᴹ₁; _*ₗ_ to _*ₗ_) +open RawLeftSemimodule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_; _+ᴹ_ to _⊕ᴹ_; 0ᴹ to 0ᴹ₂; _*ₗ_ to _⊛ₗ_) + +open import Algebra.Core +open import Algebra.Module.Definitions.Left R _≈ᴹ₁_ +open import Algebra.Module.Structures +open import Algebra.Structures +open import Function.Base +open import Level +open import Relation.Binary.Core +import Relation.Binary.Reasoning.Setoid as SetoidReasoning + +private + variable + ℓr : Level + _≈_ : Rel R ℓr + _+_ _*_ : Op₂ R + 0# 1# : R + +------------------------------------------------------------------------ +-- Re-export most properties of monoid monomorphisms + +open import Algebra.Morphism.MonoidMonomorphism + +ᴹ-isMonoidMonomorphism public + using () + renaming + ( cong to +ᴹ-cong + ; assoc to +ᴹ-assoc + ; comm to +ᴹ-comm + ; identityˡ to +ᴹ-identityˡ + ; identityʳ to +ᴹ-identityʳ + ; identity to +ᴹ-identity + ; isMagma to +ᴹ-isMagma + ; isSemigroup to +ᴹ-isSemigroup + ; isMonoid to +ᴹ-isMonoid + ; isCommutativeMonoid to +ᴹ-isCommutativeMonoid + ) + +---------------------------------------------------------------------------------- +-- Properties + +module _ + {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} {0# 1# : R} + (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) + (let R-semiring = record { isSemiring = R-isSemiring }) + (⊕-isLeftSemimodule : IsLeftSemimodule R-semiring _≈ᴹ₂_ _⊕ᴹ_ 0ᴹ₂ _⊛ₗ_) + where + + open IsLeftSemimodule ⊕-isLeftSemimodule + renaming (*ₗ-cong to ⊛ₗ-cong; *ₗ-congˡ to ⊛ₗ-congˡ; *ₗ-zeroˡ to ⊛ₗ-zeroˡ; *ₗ-distribʳ to ⊛ₗ-distribʳ; *ₗ-identityˡ to ⊛ₗ-identityˡ; *ₗ-assoc to ⊛ₗ-assoc; *ₗ-zeroʳ to ⊛ₗ-zeroʳ; *ₗ-distribˡ to ⊛ₗ-distribˡ; +ᴹ-cong to ⊕ᴹ-cong) + open SetoidReasoning ≈ᴹ-setoid + + *ₗ-cong : Congruent _≈_ _*ₗ_ + *ₗ-cong {x} {y} {u} {v} x≈y u≈ᴹv = injective $ begin + ⟦ x *ₗ u ⟧ ≈⟨ *ₗ-homo x u ⟩ + x ⊛ₗ ⟦ u ⟧ ≈⟨ ⊛ₗ-cong x≈y (⟦⟧-cong u≈ᴹv) ⟩ + y ⊛ₗ ⟦ v ⟧ ≈˘⟨ *ₗ-homo y v ⟩ + ⟦ y *ₗ v ⟧ ∎ + + *ₗ-zeroˡ : LeftZero 0# 0ᴹ₁ _*ₗ_ + *ₗ-zeroˡ x = injective $ begin + ⟦ 0# *ₗ x ⟧ ≈⟨ *ₗ-homo 0# x ⟩ + 0# ⊛ₗ ⟦ x ⟧ ≈⟨ ⊛ₗ-zeroˡ ⟦ x ⟧ ⟩ + 0ᴹ₂ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ 0ᴹ₁ ⟧ ∎ + + *ₗ-distribʳ : _*ₗ_ DistributesOverʳ _+_ ⟶ _+ᴹ_ + *ₗ-distribʳ x m n = injective $ begin + ⟦ (m + n) *ₗ x ⟧ ≈⟨ *ₗ-homo (m + n) x ⟩ + (m + n) ⊛ₗ ⟦ x ⟧ ≈⟨ ⊛ₗ-distribʳ ⟦ x ⟧ m n ⟩ + m ⊛ₗ ⟦ x ⟧ ⊕ᴹ n ⊛ₗ ⟦ x ⟧ ≈˘⟨ ⊕ᴹ-cong (*ₗ-homo m x) (*ₗ-homo n x) ⟩ + ⟦ m *ₗ x ⟧ ⊕ᴹ ⟦ n *ₗ x ⟧ ≈˘⟨ +ᴹ-homo (m *ₗ x) (n *ₗ x) ⟩ + ⟦ m *ₗ x +ᴹ n *ₗ x ⟧ ∎ + + *ₗ-identityˡ : LeftIdentity 1# _*ₗ_ + *ₗ-identityˡ m = injective $ begin + ⟦ 1# *ₗ m ⟧ ≈⟨ *ₗ-homo 1# m ⟩ + 1# ⊛ₗ ⟦ m ⟧ ≈⟨ ⊛ₗ-identityˡ ⟦ m ⟧ ⟩ + ⟦ m ⟧ ∎ + + *ₗ-assoc : Associative _*_ _*ₗ_ + *ₗ-assoc x y m = injective $ begin + ⟦ (x * y) *ₗ m ⟧ ≈⟨ *ₗ-homo (x * y) m ⟩ + (x * y) ⊛ₗ ⟦ m ⟧ ≈⟨ ⊛ₗ-assoc x y ⟦ m ⟧ ⟩ + x ⊛ₗ y ⊛ₗ ⟦ m ⟧ ≈˘⟨ ⊛ₗ-congˡ (*ₗ-homo y m) ⟩ + x ⊛ₗ ⟦ y *ₗ m ⟧ ≈˘⟨ *ₗ-homo x (y *ₗ m) ⟩ + ⟦ x *ₗ y *ₗ m ⟧ ∎ + + *ₗ-zeroʳ : RightZero 0ᴹ₁ _*ₗ_ + *ₗ-zeroʳ x = injective $ begin + ⟦ x *ₗ 0ᴹ₁ ⟧ ≈⟨ *ₗ-homo x 0ᴹ₁ ⟩ + x ⊛ₗ ⟦ 0ᴹ₁ ⟧ ≈⟨ ⊛ₗ-congˡ 0ᴹ-homo ⟩ + x ⊛ₗ 0ᴹ₂ ≈⟨ ⊛ₗ-zeroʳ x ⟩ + 0ᴹ₂ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ 0ᴹ₁ ⟧ ∎ + + *ₗ-distribˡ : _*ₗ_ DistributesOverˡ _+ᴹ_ + *ₗ-distribˡ x m n = injective $ begin + ⟦ x *ₗ (m +ᴹ n) ⟧ ≈⟨ *ₗ-homo x (m +ᴹ n) ⟩ + x ⊛ₗ ⟦ m +ᴹ n ⟧ ≈⟨ ⊛ₗ-congˡ (+ᴹ-homo m n) ⟩ + x ⊛ₗ (⟦ m ⟧ ⊕ᴹ ⟦ n ⟧) ≈⟨ ⊛ₗ-distribˡ x ⟦ m ⟧ ⟦ n ⟧ ⟩ + x ⊛ₗ ⟦ m ⟧ ⊕ᴹ x ⊛ₗ ⟦ n ⟧ ≈˘⟨ ⊕ᴹ-cong (*ₗ-homo x m) (*ₗ-homo x n) ⟩ + ⟦ x *ₗ m ⟧ ⊕ᴹ ⟦ x *ₗ n ⟧ ≈˘⟨ +ᴹ-homo (x *ₗ m) (x *ₗ n) ⟩ + ⟦ x *ₗ m +ᴹ x *ₗ n ⟧ ∎ + +------------------------------------------------------------------------ +-- Structures + +isLeftSemimodule : + {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} {0# 1# : R} + (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) + (let R-semiring = record { isSemiring = R-isSemiring }) + → IsLeftSemimodule R-semiring _≈ᴹ₂_ _⊕ᴹ_ 0ᴹ₂ _⊛ₗ_ + → IsLeftSemimodule R-semiring _≈ᴹ₁_ _+ᴹ_ 0ᴹ₁ _*ₗ_ +isLeftSemimodule isSemiring isLeftSemimodule = record + { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid M.+ᴹ-isCommutativeMonoid + ; isPreleftSemimodule = record + { *ₗ-cong = *ₗ-cong isSemiring isLeftSemimodule + ; *ₗ-zeroˡ = *ₗ-zeroˡ isSemiring isLeftSemimodule + ; *ₗ-distribʳ = *ₗ-distribʳ isSemiring isLeftSemimodule + ; *ₗ-identityˡ = *ₗ-identityˡ isSemiring isLeftSemimodule + ; *ₗ-assoc = *ₗ-assoc isSemiring isLeftSemimodule + ; *ₗ-zeroʳ = *ₗ-zeroʳ isSemiring isLeftSemimodule + ; *ₗ-distribˡ = *ₗ-distribˡ isSemiring isLeftSemimodule + } + } where module M = IsLeftSemimodule isLeftSemimodule From 0d8421b57e21fe86d28d155654ab4d0524650a6c Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 3 Feb 2024 18:49:44 +0100 Subject: [PATCH 02/22] Weaken arguments of properties --- .../Morphism/LeftSemimoduleMonomorphism.agda | 60 +++++++++---------- 1 file changed, 28 insertions(+), 32 deletions(-) diff --git a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda index 5f4211acd1..c3ac7583ea 100644 --- a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda @@ -19,7 +19,7 @@ open RawLeftSemimodule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_; open RawLeftSemimodule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_; _+ᴹ_ to _⊕ᴹ_; 0ᴹ to 0ᴹ₂; _*ₗ_ to _⊛ₗ_) open import Algebra.Core -open import Algebra.Module.Definitions.Left R _≈ᴹ₁_ +open import Algebra.Module.Definitions.Left open import Algebra.Module.Structures open import Algebra.Structures open import Function.Base @@ -56,70 +56,66 @@ open import Algebra.Morphism.MonoidMonomorphism ---------------------------------------------------------------------------------- -- Properties -module _ - {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} {0# 1# : R} - (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) - (let R-semiring = record { isSemiring = R-isSemiring }) - (⊕-isLeftSemimodule : IsLeftSemimodule R-semiring _≈ᴹ₂_ _⊕ᴹ_ 0ᴹ₂ _⊛ₗ_) - where +module _ (⊕ᴹ-isMonoid : IsMonoid _≈ᴹ₂_ _⊕ᴹ_ 0ᴹ₂) where - open IsLeftSemimodule ⊕-isLeftSemimodule - renaming (*ₗ-cong to ⊛ₗ-cong; *ₗ-congˡ to ⊛ₗ-congˡ; *ₗ-zeroˡ to ⊛ₗ-zeroˡ; *ₗ-distribʳ to ⊛ₗ-distribʳ; *ₗ-identityˡ to ⊛ₗ-identityˡ; *ₗ-assoc to ⊛ₗ-assoc; *ₗ-zeroʳ to ⊛ₗ-zeroʳ; *ₗ-distribˡ to ⊛ₗ-distribˡ; +ᴹ-cong to ⊕ᴹ-cong) - open SetoidReasoning ≈ᴹ-setoid + open IsMonoid ⊕ᴹ-isMonoid + using (setoid) + renaming (∙-cong to ⊕ᴹ-cong) + open SetoidReasoning setoid - *ₗ-cong : Congruent _≈_ _*ₗ_ - *ₗ-cong {x} {y} {u} {v} x≈y u≈ᴹv = injective $ begin + *ₗ-cong : Congruent R _≈ᴹ₂_ _≈_ _⊛ₗ_ → Congruent R _≈ᴹ₁_ _≈_ _*ₗ_ + *ₗ-cong ⊛ₗ-cong {x} {y} {u} {v} x≈y u≈ᴹv = injective $ begin ⟦ x *ₗ u ⟧ ≈⟨ *ₗ-homo x u ⟩ x ⊛ₗ ⟦ u ⟧ ≈⟨ ⊛ₗ-cong x≈y (⟦⟧-cong u≈ᴹv) ⟩ y ⊛ₗ ⟦ v ⟧ ≈˘⟨ *ₗ-homo y v ⟩ ⟦ y *ₗ v ⟧ ∎ - *ₗ-zeroˡ : LeftZero 0# 0ᴹ₁ _*ₗ_ - *ₗ-zeroˡ x = injective $ begin + *ₗ-zeroˡ : LeftZero R _≈ᴹ₂_ 0# 0ᴹ₂ _⊛ₗ_ → LeftZero R _≈ᴹ₁_ 0# 0ᴹ₁ _*ₗ_ + *ₗ-zeroˡ {0# = 0#} ⊛ₗ-zeroˡ x = injective $ begin ⟦ 0# *ₗ x ⟧ ≈⟨ *ₗ-homo 0# x ⟩ 0# ⊛ₗ ⟦ x ⟧ ≈⟨ ⊛ₗ-zeroˡ ⟦ x ⟧ ⟩ 0ᴹ₂ ≈˘⟨ 0ᴹ-homo ⟩ ⟦ 0ᴹ₁ ⟧ ∎ - *ₗ-distribʳ : _*ₗ_ DistributesOverʳ _+_ ⟶ _+ᴹ_ - *ₗ-distribʳ x m n = injective $ begin + *ₗ-distribʳ : _DistributesOverʳ_⟶_ R _≈ᴹ₂_ _⊛ₗ_ _+_ _⊕ᴹ_ → _DistributesOverʳ_⟶_ R _≈ᴹ₁_ _*ₗ_ _+_ _+ᴹ_ + *ₗ-distribʳ {_+_ = _+_} ⊛ₗ-distribʳ x m n = injective $ begin ⟦ (m + n) *ₗ x ⟧ ≈⟨ *ₗ-homo (m + n) x ⟩ (m + n) ⊛ₗ ⟦ x ⟧ ≈⟨ ⊛ₗ-distribʳ ⟦ x ⟧ m n ⟩ m ⊛ₗ ⟦ x ⟧ ⊕ᴹ n ⊛ₗ ⟦ x ⟧ ≈˘⟨ ⊕ᴹ-cong (*ₗ-homo m x) (*ₗ-homo n x) ⟩ ⟦ m *ₗ x ⟧ ⊕ᴹ ⟦ n *ₗ x ⟧ ≈˘⟨ +ᴹ-homo (m *ₗ x) (n *ₗ x) ⟩ ⟦ m *ₗ x +ᴹ n *ₗ x ⟧ ∎ - *ₗ-identityˡ : LeftIdentity 1# _*ₗ_ - *ₗ-identityˡ m = injective $ begin + *ₗ-identityˡ : LeftIdentity R _≈ᴹ₂_ 1# _⊛ₗ_ → LeftIdentity R _≈ᴹ₁_ 1# _*ₗ_ + *ₗ-identityˡ {1# = 1#} ⊛ₗ-identityˡ m = injective $ begin ⟦ 1# *ₗ m ⟧ ≈⟨ *ₗ-homo 1# m ⟩ 1# ⊛ₗ ⟦ m ⟧ ≈⟨ ⊛ₗ-identityˡ ⟦ m ⟧ ⟩ ⟦ m ⟧ ∎ - *ₗ-assoc : Associative _*_ _*ₗ_ - *ₗ-assoc x y m = injective $ begin + *ₗ-assoc : LeftCongruent R _≈ᴹ₂_ _⊛ₗ_ → Associative R _≈ᴹ₂_ _*_ _⊛ₗ_ → Associative R _≈ᴹ₁_ _*_ _*ₗ_ + *ₗ-assoc {_*_ = _*_} ⊛ₗ-congˡ ⊛ₗ-assoc x y m = injective $ begin ⟦ (x * y) *ₗ m ⟧ ≈⟨ *ₗ-homo (x * y) m ⟩ (x * y) ⊛ₗ ⟦ m ⟧ ≈⟨ ⊛ₗ-assoc x y ⟦ m ⟧ ⟩ x ⊛ₗ y ⊛ₗ ⟦ m ⟧ ≈˘⟨ ⊛ₗ-congˡ (*ₗ-homo y m) ⟩ x ⊛ₗ ⟦ y *ₗ m ⟧ ≈˘⟨ *ₗ-homo x (y *ₗ m) ⟩ ⟦ x *ₗ y *ₗ m ⟧ ∎ - *ₗ-zeroʳ : RightZero 0ᴹ₁ _*ₗ_ - *ₗ-zeroʳ x = injective $ begin + *ₗ-zeroʳ : LeftCongruent R _≈ᴹ₂_ _⊛ₗ_ → RightZero R _≈ᴹ₂_ 0ᴹ₂ _⊛ₗ_ → RightZero R _≈ᴹ₁_ 0ᴹ₁ _*ₗ_ + *ₗ-zeroʳ ⊛ₗ-congˡ ⊛ₗ-zeroʳ x = injective $ begin ⟦ x *ₗ 0ᴹ₁ ⟧ ≈⟨ *ₗ-homo x 0ᴹ₁ ⟩ x ⊛ₗ ⟦ 0ᴹ₁ ⟧ ≈⟨ ⊛ₗ-congˡ 0ᴹ-homo ⟩ x ⊛ₗ 0ᴹ₂ ≈⟨ ⊛ₗ-zeroʳ x ⟩ 0ᴹ₂ ≈˘⟨ 0ᴹ-homo ⟩ ⟦ 0ᴹ₁ ⟧ ∎ - *ₗ-distribˡ : _*ₗ_ DistributesOverˡ _+ᴹ_ - *ₗ-distribˡ x m n = injective $ begin + *ₗ-distribˡ : LeftCongruent R _≈ᴹ₂_ _⊛ₗ_ → _DistributesOverˡ_ R _≈ᴹ₂_ _⊛ₗ_ _⊕ᴹ_ → _DistributesOverˡ_ R _≈ᴹ₁_ _*ₗ_ _+ᴹ_ + *ₗ-distribˡ ⊛ₗ-congˡ ⊛ₗ-distribˡ x m n = injective $ begin ⟦ x *ₗ (m +ᴹ n) ⟧ ≈⟨ *ₗ-homo x (m +ᴹ n) ⟩ x ⊛ₗ ⟦ m +ᴹ n ⟧ ≈⟨ ⊛ₗ-congˡ (+ᴹ-homo m n) ⟩ x ⊛ₗ (⟦ m ⟧ ⊕ᴹ ⟦ n ⟧) ≈⟨ ⊛ₗ-distribˡ x ⟦ m ⟧ ⟦ n ⟧ ⟩ x ⊛ₗ ⟦ m ⟧ ⊕ᴹ x ⊛ₗ ⟦ n ⟧ ≈˘⟨ ⊕ᴹ-cong (*ₗ-homo x m) (*ₗ-homo x n) ⟩ ⟦ x *ₗ m ⟧ ⊕ᴹ ⟦ x *ₗ n ⟧ ≈˘⟨ +ᴹ-homo (x *ₗ m) (x *ₗ n) ⟩ ⟦ x *ₗ m +ᴹ x *ₗ n ⟧ ∎ - + ------------------------------------------------------------------------ -- Structures @@ -132,12 +128,12 @@ isLeftSemimodule : isLeftSemimodule isSemiring isLeftSemimodule = record { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid M.+ᴹ-isCommutativeMonoid ; isPreleftSemimodule = record - { *ₗ-cong = *ₗ-cong isSemiring isLeftSemimodule - ; *ₗ-zeroˡ = *ₗ-zeroˡ isSemiring isLeftSemimodule - ; *ₗ-distribʳ = *ₗ-distribʳ isSemiring isLeftSemimodule - ; *ₗ-identityˡ = *ₗ-identityˡ isSemiring isLeftSemimodule - ; *ₗ-assoc = *ₗ-assoc isSemiring isLeftSemimodule - ; *ₗ-zeroʳ = *ₗ-zeroʳ isSemiring isLeftSemimodule - ; *ₗ-distribˡ = *ₗ-distribˡ isSemiring isLeftSemimodule + { *ₗ-cong = *ₗ-cong M.+ᴹ-isMonoid M.*ₗ-cong + ; *ₗ-zeroˡ = *ₗ-zeroˡ M.+ᴹ-isMonoid M.*ₗ-zeroˡ + ; *ₗ-distribʳ = *ₗ-distribʳ M.+ᴹ-isMonoid M.*ₗ-distribʳ + ; *ₗ-identityˡ = *ₗ-identityˡ M.+ᴹ-isMonoid M.*ₗ-identityˡ + ; *ₗ-assoc = *ₗ-assoc M.+ᴹ-isMonoid M.*ₗ-congˡ M.*ₗ-assoc + ; *ₗ-zeroʳ = *ₗ-zeroʳ M.+ᴹ-isMonoid M.*ₗ-congˡ M.*ₗ-zeroʳ + ; *ₗ-distribˡ = *ₗ-distribˡ M.+ᴹ-isMonoid M.*ₗ-congˡ M.*ₗ-distribˡ } } where module M = IsLeftSemimodule isLeftSemimodule From 51938b2eb423380020db85f4e65947101fbd3eda Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 3 Feb 2024 18:54:46 +0100 Subject: [PATCH 03/22] Remember I made a variable declaration for this --- src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda index c3ac7583ea..d9b8718eae 100644 --- a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda @@ -120,7 +120,6 @@ module _ (⊕ᴹ-isMonoid : IsMonoid _≈ᴹ₂_ _⊕ᴹ_ 0ᴹ₂) where -- Structures isLeftSemimodule : - {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} {0# 1# : R} (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) (let R-semiring = record { isSemiring = R-isSemiring }) → IsLeftSemimodule R-semiring _≈ᴹ₂_ _⊕ᴹ_ 0ᴹ₂ _⊛ₗ_ From f59ce63271dce03c15fa5cba9003aa3a3260af0a Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 3 Feb 2024 21:53:18 +0100 Subject: [PATCH 04/22] Left module monomorphisms --- .../Morphism/LeftModuleMonomorphism.agda | 58 +++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda diff --git a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda new file mode 100644 index 0000000000..a29111572c --- /dev/null +++ b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda @@ -0,0 +1,58 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between left modules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.LeftModuleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawLeftModule R a ℓ₁} {N : RawLeftModule R b ℓ₂} {⟦_⟧} + (isLeftModuleMonomorphism : IsLeftModuleMonomorphism M N ⟦_⟧) + where + +open IsLeftModuleMonomorphism isLeftModuleMonomorphism +module M = RawLeftModule M +module N = RawLeftModule N + +open import Algebra.Bundles +open import Algebra.Core +open import Algebra.Module.Structures +open import Algebra.Structures +open import Relation.Binary.Core + +------------------------------------------------------------------------ +-- Rexports + +open import Algebra.Morphism.GroupMonomorphism +ᴹ-isGroupMonomorphism public + using () renaming + ( inverseˡ to -ᴹ‿inverseˡ + ; inverseʳ to -ᴹ‿inverseʳ + ; inverse to -ᴹ‿inverse + ; ⁻¹-cong to -ᴹ‿cong + ; ⁻¹-distrib-∙ to -ᴹ‿distrib-+ᴹ + ; isGroup to +ᴹ-isGroup + ; isAbelianGroup to +ᴹ-isAbelianGroup + ) +open import Algebra.Module.Morphism.LeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public + +------------------------------------------------------------------------ +-- Structures + +isLeftModule : + ∀ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} { -_ : Op₁ R} {0# 1# : R} + (R-isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) + (let R-ring = record { isRing = R-isRing }) + → IsLeftModule R-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ + → IsLeftModule R-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ +isLeftModule R-isRing isLeftModule = record + { isLeftSemimodule = isLeftSemimodule R.isSemiring NN.isLeftSemimodule + ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse + } + where + module R = IsRing R-isRing + module NN = IsLeftModule isLeftModule From 1c02b7ca19e6b64d7b4ebf260b961764c0c236cb Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 13 Feb 2024 12:16:27 +0100 Subject: [PATCH 05/22] Attempt using qualified names rather than renaming --- .../Morphism/LeftSemimoduleMonomorphism.agda | 139 +++++++++--------- 1 file changed, 71 insertions(+), 68 deletions(-) diff --git a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda index d9b8718eae..bfb9e61e44 100644 --- a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda @@ -15,11 +15,11 @@ module Algebra.Module.Morphism.LeftSemimoduleMonomorphism where open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism -open RawLeftSemimodule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_; _+ᴹ_ to _+ᴹ_; 0ᴹ to 0ᴹ₁; _*ₗ_ to _*ₗ_) -open RawLeftSemimodule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_; _+ᴹ_ to _⊕ᴹ_; 0ᴹ to 0ᴹ₂; _*ₗ_ to _⊛ₗ_) +module M = RawLeftSemimodule M₁ +module N = RawLeftSemimodule M₂ open import Algebra.Core -open import Algebra.Module.Definitions.Left +import Algebra.Module.Definitions.Left as LeftDefs open import Algebra.Module.Structures open import Algebra.Structures open import Function.Base @@ -56,65 +56,68 @@ open import Algebra.Morphism.MonoidMonomorphism ---------------------------------------------------------------------------------- -- Properties -module _ (⊕ᴹ-isMonoid : IsMonoid _≈ᴹ₂_ _⊕ᴹ_ 0ᴹ₂) where +module _ (⊕ᴹ-isMonoid : IsMonoid N._≈ᴹ_ N._+ᴹ_ N.0ᴹ) where open IsMonoid ⊕ᴹ-isMonoid using (setoid) - renaming (∙-cong to ⊕ᴹ-cong) + renaming (∙-cong to +ᴹ-cong′) open SetoidReasoning setoid - *ₗ-cong : Congruent R _≈ᴹ₂_ _≈_ _⊛ₗ_ → Congruent R _≈ᴹ₁_ _≈_ _*ₗ_ - *ₗ-cong ⊛ₗ-cong {x} {y} {u} {v} x≈y u≈ᴹv = injective $ begin - ⟦ x *ₗ u ⟧ ≈⟨ *ₗ-homo x u ⟩ - x ⊛ₗ ⟦ u ⟧ ≈⟨ ⊛ₗ-cong x≈y (⟦⟧-cong u≈ᴹv) ⟩ - y ⊛ₗ ⟦ v ⟧ ≈˘⟨ *ₗ-homo y v ⟩ - ⟦ y *ₗ v ⟧ ∎ - - *ₗ-zeroˡ : LeftZero R _≈ᴹ₂_ 0# 0ᴹ₂ _⊛ₗ_ → LeftZero R _≈ᴹ₁_ 0# 0ᴹ₁ _*ₗ_ - *ₗ-zeroˡ {0# = 0#} ⊛ₗ-zeroˡ x = injective $ begin - ⟦ 0# *ₗ x ⟧ ≈⟨ *ₗ-homo 0# x ⟩ - 0# ⊛ₗ ⟦ x ⟧ ≈⟨ ⊛ₗ-zeroˡ ⟦ x ⟧ ⟩ - 0ᴹ₂ ≈˘⟨ 0ᴹ-homo ⟩ - ⟦ 0ᴹ₁ ⟧ ∎ - - *ₗ-distribʳ : _DistributesOverʳ_⟶_ R _≈ᴹ₂_ _⊛ₗ_ _+_ _⊕ᴹ_ → _DistributesOverʳ_⟶_ R _≈ᴹ₁_ _*ₗ_ _+_ _+ᴹ_ - *ₗ-distribʳ {_+_ = _+_} ⊛ₗ-distribʳ x m n = injective $ begin - ⟦ (m + n) *ₗ x ⟧ ≈⟨ *ₗ-homo (m + n) x ⟩ - (m + n) ⊛ₗ ⟦ x ⟧ ≈⟨ ⊛ₗ-distribʳ ⟦ x ⟧ m n ⟩ - m ⊛ₗ ⟦ x ⟧ ⊕ᴹ n ⊛ₗ ⟦ x ⟧ ≈˘⟨ ⊕ᴹ-cong (*ₗ-homo m x) (*ₗ-homo n x) ⟩ - ⟦ m *ₗ x ⟧ ⊕ᴹ ⟦ n *ₗ x ⟧ ≈˘⟨ +ᴹ-homo (m *ₗ x) (n *ₗ x) ⟩ - ⟦ m *ₗ x +ᴹ n *ₗ x ⟧ ∎ - - *ₗ-identityˡ : LeftIdentity R _≈ᴹ₂_ 1# _⊛ₗ_ → LeftIdentity R _≈ᴹ₁_ 1# _*ₗ_ - *ₗ-identityˡ {1# = 1#} ⊛ₗ-identityˡ m = injective $ begin - ⟦ 1# *ₗ m ⟧ ≈⟨ *ₗ-homo 1# m ⟩ - 1# ⊛ₗ ⟦ m ⟧ ≈⟨ ⊛ₗ-identityˡ ⟦ m ⟧ ⟩ - ⟦ m ⟧ ∎ - - *ₗ-assoc : LeftCongruent R _≈ᴹ₂_ _⊛ₗ_ → Associative R _≈ᴹ₂_ _*_ _⊛ₗ_ → Associative R _≈ᴹ₁_ _*_ _*ₗ_ - *ₗ-assoc {_*_ = _*_} ⊛ₗ-congˡ ⊛ₗ-assoc x y m = injective $ begin - ⟦ (x * y) *ₗ m ⟧ ≈⟨ *ₗ-homo (x * y) m ⟩ - (x * y) ⊛ₗ ⟦ m ⟧ ≈⟨ ⊛ₗ-assoc x y ⟦ m ⟧ ⟩ - x ⊛ₗ y ⊛ₗ ⟦ m ⟧ ≈˘⟨ ⊛ₗ-congˡ (*ₗ-homo y m) ⟩ - x ⊛ₗ ⟦ y *ₗ m ⟧ ≈˘⟨ *ₗ-homo x (y *ₗ m) ⟩ - ⟦ x *ₗ y *ₗ m ⟧ ∎ - - *ₗ-zeroʳ : LeftCongruent R _≈ᴹ₂_ _⊛ₗ_ → RightZero R _≈ᴹ₂_ 0ᴹ₂ _⊛ₗ_ → RightZero R _≈ᴹ₁_ 0ᴹ₁ _*ₗ_ - *ₗ-zeroʳ ⊛ₗ-congˡ ⊛ₗ-zeroʳ x = injective $ begin - ⟦ x *ₗ 0ᴹ₁ ⟧ ≈⟨ *ₗ-homo x 0ᴹ₁ ⟩ - x ⊛ₗ ⟦ 0ᴹ₁ ⟧ ≈⟨ ⊛ₗ-congˡ 0ᴹ-homo ⟩ - x ⊛ₗ 0ᴹ₂ ≈⟨ ⊛ₗ-zeroʳ x ⟩ - 0ᴹ₂ ≈˘⟨ 0ᴹ-homo ⟩ - ⟦ 0ᴹ₁ ⟧ ∎ - - *ₗ-distribˡ : LeftCongruent R _≈ᴹ₂_ _⊛ₗ_ → _DistributesOverˡ_ R _≈ᴹ₂_ _⊛ₗ_ _⊕ᴹ_ → _DistributesOverˡ_ R _≈ᴹ₁_ _*ₗ_ _+ᴹ_ - *ₗ-distribˡ ⊛ₗ-congˡ ⊛ₗ-distribˡ x m n = injective $ begin - ⟦ x *ₗ (m +ᴹ n) ⟧ ≈⟨ *ₗ-homo x (m +ᴹ n) ⟩ - x ⊛ₗ ⟦ m +ᴹ n ⟧ ≈⟨ ⊛ₗ-congˡ (+ᴹ-homo m n) ⟩ - x ⊛ₗ (⟦ m ⟧ ⊕ᴹ ⟦ n ⟧) ≈⟨ ⊛ₗ-distribˡ x ⟦ m ⟧ ⟦ n ⟧ ⟩ - x ⊛ₗ ⟦ m ⟧ ⊕ᴹ x ⊛ₗ ⟦ n ⟧ ≈˘⟨ ⊕ᴹ-cong (*ₗ-homo x m) (*ₗ-homo x n) ⟩ - ⟦ x *ₗ m ⟧ ⊕ᴹ ⟦ x *ₗ n ⟧ ≈˘⟨ +ᴹ-homo (x *ₗ m) (x *ₗ n) ⟩ - ⟦ x *ₗ m +ᴹ x *ₗ n ⟧ ∎ + module MDefs = LeftDefs R M._≈ᴹ_ + module NDefs = LeftDefs R N._≈ᴹ_ + + *ₗ-cong : NDefs.Congruent _≈_ N._*ₗ_ → MDefs.Congruent _≈_ M._*ₗ_ + *ₗ-cong *ₗ-cong {x} {y} {u} {v} x≈y u≈ᴹv = injective $ begin + ⟦ x M.*ₗ u ⟧ ≈⟨ *ₗ-homo x u ⟩ + x N.*ₗ ⟦ u ⟧ ≈⟨ *ₗ-cong x≈y (⟦⟧-cong u≈ᴹv) ⟩ + y N.*ₗ ⟦ v ⟧ ≈˘⟨ *ₗ-homo y v ⟩ + ⟦ y M.*ₗ v ⟧ ∎ + + *ₗ-zeroˡ : NDefs.LeftZero 0# N.0ᴹ N._*ₗ_ → MDefs.LeftZero 0# M.0ᴹ M._*ₗ_ + *ₗ-zeroˡ {0# = 0#} *ₗ-zeroˡ x = injective $ begin + ⟦ 0# M.*ₗ x ⟧ ≈⟨ *ₗ-homo 0# x ⟩ + 0# N.*ₗ ⟦ x ⟧ ≈⟨ *ₗ-zeroˡ ⟦ x ⟧ ⟩ + N.0ᴹ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ M.0ᴹ ⟧ ∎ + + *ₗ-distribʳ : N._*ₗ_ NDefs.DistributesOverʳ _+_ ⟶ N._+ᴹ_ → M._*ₗ_ MDefs.DistributesOverʳ _+_ ⟶ M._+ᴹ_ + *ₗ-distribʳ {_+_ = _+_} *ₗ-distribʳ x m n = injective $ begin + ⟦ (m + n) M.*ₗ x ⟧ ≈⟨ *ₗ-homo (m + n) x ⟩ + (m + n) N.*ₗ ⟦ x ⟧ ≈⟨ *ₗ-distribʳ ⟦ x ⟧ m n ⟩ + m N.*ₗ ⟦ x ⟧ N.+ᴹ n N.*ₗ ⟦ x ⟧ ≈˘⟨ +ᴹ-cong′ (*ₗ-homo m x) (*ₗ-homo n x) ⟩ + ⟦ m M.*ₗ x ⟧ N.+ᴹ ⟦ n M.*ₗ x ⟧ ≈˘⟨ +ᴹ-homo (m M.*ₗ x) (n M.*ₗ x) ⟩ + ⟦ m M.*ₗ x M.+ᴹ n M.*ₗ x ⟧ ∎ + + *ₗ-identityˡ : NDefs.LeftIdentity 1# N._*ₗ_ → MDefs.LeftIdentity 1# M._*ₗ_ + *ₗ-identityˡ {1# = 1#} *ₗ-identityˡ m = injective $ begin + ⟦ 1# M.*ₗ m ⟧ ≈⟨ *ₗ-homo 1# m ⟩ + 1# N.*ₗ ⟦ m ⟧ ≈⟨ *ₗ-identityˡ ⟦ m ⟧ ⟩ + ⟦ m ⟧ ∎ + + *ₗ-assoc : NDefs.LeftCongruent N._*ₗ_ → NDefs.Associative _*_ N._*ₗ_ → MDefs.Associative _*_ M._*ₗ_ + *ₗ-assoc {_*_ = _*_} *ₗ-congˡ *ₗ-assoc x y m = injective $ begin + ⟦ (x * y) M.*ₗ m ⟧ ≈⟨ *ₗ-homo (x * y) m ⟩ + (x * y) N.*ₗ ⟦ m ⟧ ≈⟨ *ₗ-assoc x y ⟦ m ⟧ ⟩ + x N.*ₗ y N.*ₗ ⟦ m ⟧ ≈˘⟨ *ₗ-congˡ (*ₗ-homo y m) ⟩ + x N.*ₗ ⟦ y M.*ₗ m ⟧ ≈˘⟨ *ₗ-homo x (y M.*ₗ m) ⟩ + ⟦ x M.*ₗ y M.*ₗ m ⟧ ∎ + + *ₗ-zeroʳ : NDefs.LeftCongruent N._*ₗ_ → NDefs.RightZero N.0ᴹ N._*ₗ_ → MDefs.RightZero M.0ᴹ M._*ₗ_ + *ₗ-zeroʳ *ₗ-congˡ *ₗ-zeroʳ x = injective $ begin + ⟦ x M.*ₗ M.0ᴹ ⟧ ≈⟨ *ₗ-homo x M.0ᴹ ⟩ + x N.*ₗ ⟦ M.0ᴹ ⟧ ≈⟨ *ₗ-congˡ 0ᴹ-homo ⟩ + x N.*ₗ N.0ᴹ ≈⟨ *ₗ-zeroʳ x ⟩ + N.0ᴹ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ M.0ᴹ ⟧ ∎ + + *ₗ-distribˡ : NDefs.LeftCongruent N._*ₗ_ → N._*ₗ_ NDefs.DistributesOverˡ N._+ᴹ_ → M._*ₗ_ MDefs.DistributesOverˡ M._+ᴹ_ + *ₗ-distribˡ *ₗ-congˡ *ₗ-distribˡ x m n = injective $ begin + ⟦ x M.*ₗ (m M.+ᴹ n) ⟧ ≈⟨ *ₗ-homo x (m M.+ᴹ n) ⟩ + x N.*ₗ ⟦ m M.+ᴹ n ⟧ ≈⟨ *ₗ-congˡ (+ᴹ-homo m n) ⟩ + x N.*ₗ (⟦ m ⟧ N.+ᴹ ⟦ n ⟧) ≈⟨ *ₗ-distribˡ x ⟦ m ⟧ ⟦ n ⟧ ⟩ + x N.*ₗ ⟦ m ⟧ N.+ᴹ x N.*ₗ ⟦ n ⟧ ≈˘⟨ +ᴹ-cong′ (*ₗ-homo x m) (*ₗ-homo x n) ⟩ + ⟦ x M.*ₗ m ⟧ N.+ᴹ ⟦ x M.*ₗ n ⟧ ≈˘⟨ +ᴹ-homo (x M.*ₗ m) (x M.*ₗ n) ⟩ + ⟦ x M.*ₗ m M.+ᴹ x M.*ₗ n ⟧ ∎ ------------------------------------------------------------------------ -- Structures @@ -122,17 +125,17 @@ module _ (⊕ᴹ-isMonoid : IsMonoid _≈ᴹ₂_ _⊕ᴹ_ 0ᴹ₂) where isLeftSemimodule : (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) (let R-semiring = record { isSemiring = R-isSemiring }) - → IsLeftSemimodule R-semiring _≈ᴹ₂_ _⊕ᴹ_ 0ᴹ₂ _⊛ₗ_ - → IsLeftSemimodule R-semiring _≈ᴹ₁_ _+ᴹ_ 0ᴹ₁ _*ₗ_ + → IsLeftSemimodule R-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ + → IsLeftSemimodule R-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ isLeftSemimodule isSemiring isLeftSemimodule = record - { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid M.+ᴹ-isCommutativeMonoid + { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid ; isPreleftSemimodule = record - { *ₗ-cong = *ₗ-cong M.+ᴹ-isMonoid M.*ₗ-cong - ; *ₗ-zeroˡ = *ₗ-zeroˡ M.+ᴹ-isMonoid M.*ₗ-zeroˡ - ; *ₗ-distribʳ = *ₗ-distribʳ M.+ᴹ-isMonoid M.*ₗ-distribʳ - ; *ₗ-identityˡ = *ₗ-identityˡ M.+ᴹ-isMonoid M.*ₗ-identityˡ - ; *ₗ-assoc = *ₗ-assoc M.+ᴹ-isMonoid M.*ₗ-congˡ M.*ₗ-assoc - ; *ₗ-zeroʳ = *ₗ-zeroʳ M.+ᴹ-isMonoid M.*ₗ-congˡ M.*ₗ-zeroʳ - ; *ₗ-distribˡ = *ₗ-distribˡ M.+ᴹ-isMonoid M.*ₗ-congˡ M.*ₗ-distribˡ + { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMonoid NN.*ₗ-cong + ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMonoid NN.*ₗ-zeroˡ + ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMonoid NN.*ₗ-distribʳ + ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMonoid NN.*ₗ-identityˡ + ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-assoc + ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-zeroʳ + ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-distribˡ } - } where module M = IsLeftSemimodule isLeftSemimodule + } where module NN = IsLeftSemimodule isLeftSemimodule From bc5ee42c436784f97167bdaf9bfa58ebb61c37e5 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 13 Feb 2024 14:09:50 +0100 Subject: [PATCH 06/22] Mark modules as private --- src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda index bfb9e61e44..38a7548cba 100644 --- a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda @@ -15,8 +15,9 @@ module Algebra.Module.Morphism.LeftSemimoduleMonomorphism where open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism -module M = RawLeftSemimodule M₁ -module N = RawLeftSemimodule M₂ +private + module M = RawLeftSemimodule M₁ + module N = RawLeftSemimodule M₂ open import Algebra.Core import Algebra.Module.Definitions.Left as LeftDefs From 9db52ac7fa6895ab6b1976fa3862fe75fb411282 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 8 Jun 2024 16:26:23 +0200 Subject: [PATCH 07/22] Typo --- src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda index a29111572c..f5281e21ad 100644 --- a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda @@ -25,7 +25,7 @@ open import Algebra.Structures open import Relation.Binary.Core ------------------------------------------------------------------------ --- Rexports +-- Re-exports open import Algebra.Morphism.GroupMonomorphism +ᴹ-isGroupMonomorphism public using () renaming From b2ea2d995c512f5c933cf8e410c1e24e3f27c9a8 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 8 Jun 2024 16:30:09 +0200 Subject: [PATCH 08/22] These modules should be private --- src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda index f5281e21ad..710b71b1a2 100644 --- a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda @@ -15,8 +15,9 @@ module Algebra.Module.Morphism.LeftModuleMonomorphism where open IsLeftModuleMonomorphism isLeftModuleMonomorphism -module M = RawLeftModule M -module N = RawLeftModule N +private + module M = RawLeftModule M + module N = RawLeftModule N open import Algebra.Bundles open import Algebra.Core From 1a3107b4a40cdf33df57fb0620538dccd07b380d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 14:46:37 +0200 Subject: [PATCH 09/22] Monomorphisms over right semimodules --- .../Morphism/RightSemimoduleMonomorphism.agda | 139 ++++++++++++++++++ 1 file changed, 139 insertions(+) create mode 100644 src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda diff --git a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda new file mode 100644 index 0000000000..bab54b4bf9 --- /dev/null +++ b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda @@ -0,0 +1,139 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomomorphism between right semimodules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.RightSemimoduleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawRightSemimodule R a ℓ₁} {N : RawRightSemimodule R b ℓ₂} {⟦_⟧} + (isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism M N ⟦_⟧) + where + +open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism +private + module M = RawRightSemimodule M + module N = RawRightSemimodule N + +open import Algebra.Core +import Algebra.Module.Definitions.Right as RightDefs +open import Algebra.Module.Structures +open import Algebra.Structures +open import Function.Base +open import Level +open import Relation.Binary.Core +import Relation.Binary.Reasoning.Setoid as SetoidReasoning + +private + variable + ℓr : Level + _≈_ : Rel R ℓr + _+_ _*_ : Op₂ R + 0# 1# : R + +open import Algebra.Morphism.MonoidMonomorphism + +ᴹ-isMonoidMonomorphism public + using () + renaming + ( cong to +ᴹ-cong + ; assoc to +ᴹ-assoc + ; comm to +ᴹ-comm + ; identityˡ to +ᴹ-identityˡ + ; identityʳ to +ᴹ-identityʳ + ; identity to +ᴹ-identity + ; isMagma to +ᴹ-isMagma + ; isSemigroup to +ᴹ-isSemigroup + ; isMonoid to +ᴹ-isMonoid + ; isCommutativeMonoid to +ᴹ-isCommutativeMonoid + ) + +------------------------------------------------------------------------ +-- Properties + +module _ (+ᴹ-isMonoid : IsMonoid N._≈ᴹ_ N._+ᴹ_ N.0ᴹ) where + + open IsMonoid +ᴹ-isMonoid + using (setoid) + renaming (∙-cong to +ᴹ-cong′) + open SetoidReasoning setoid + + module MDefs = RightDefs R M._≈ᴹ_ + module NDefs = RightDefs R N._≈ᴹ_ + + *ᵣ-cong : NDefs.Congruent _≈_ N._*ᵣ_ → MDefs.Congruent _≈_ M._*ᵣ_ + *ᵣ-cong *ᵣ-cong {x} {y} {u} {v} x≈ᴹy u≈v = injective $ begin + ⟦ x M.*ᵣ u ⟧ ≈⟨ *ᵣ-homo u x ⟩ + ⟦ x ⟧ N.*ᵣ u ≈⟨ *ᵣ-cong (⟦⟧-cong x≈ᴹy) u≈v ⟩ + ⟦ y ⟧ N.*ᵣ v ≈˘⟨ *ᵣ-homo v y ⟩ + ⟦ y M.*ᵣ v ⟧ ∎ + + *ᵣ-zeroʳ : NDefs.RightZero 0# N.0ᴹ N._*ᵣ_ → MDefs.RightZero 0# M.0ᴹ M._*ᵣ_ + *ᵣ-zeroʳ {0# = 0#} *ᵣ-zeroʳ x = injective $ begin + ⟦ x M.*ᵣ 0# ⟧ ≈⟨ *ᵣ-homo 0# x ⟩ + ⟦ x ⟧ N.*ᵣ 0# ≈⟨ *ᵣ-zeroʳ ⟦ x ⟧ ⟩ + N.0ᴹ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ M.0ᴹ ⟧ ∎ + + *ᵣ-distribˡ : N._*ᵣ_ NDefs.DistributesOverˡ _+_ ⟶ N._+ᴹ_ → M._*ᵣ_ MDefs.DistributesOverˡ _+_ ⟶ M._+ᴹ_ + *ᵣ-distribˡ {_+_ = _+_} *ᵣ-distribˡ x m n = injective $ begin + ⟦ x M.*ᵣ (m + n) ⟧ ≈⟨ *ᵣ-homo (m + n) x ⟩ + ⟦ x ⟧ N.*ᵣ (m + n) ≈⟨ *ᵣ-distribˡ ⟦ x ⟧ m n ⟩ + ⟦ x ⟧ N.*ᵣ m N.+ᴹ ⟦ x ⟧ N.*ᵣ n ≈˘⟨ +ᴹ-cong′ (*ᵣ-homo m x) (*ᵣ-homo n x) ⟩ + ⟦ x M.*ᵣ m ⟧ N.+ᴹ ⟦ x M.*ᵣ n ⟧ ≈˘⟨ +ᴹ-homo (x M.*ᵣ m) (x M.*ᵣ n) ⟩ + ⟦ x M.*ᵣ m M.+ᴹ x M.*ᵣ n ⟧ ∎ + + *ᵣ-identityʳ : NDefs.RightIdentity 1# N._*ᵣ_ → MDefs.RightIdentity 1# M._*ᵣ_ + *ᵣ-identityʳ {1# = 1#} *ᵣ-identityʳ m = injective $ begin + ⟦ m M.*ᵣ 1# ⟧ ≈⟨ *ᵣ-homo 1# m ⟩ + ⟦ m ⟧ N.*ᵣ 1# ≈⟨ *ᵣ-identityʳ ⟦ m ⟧ ⟩ + ⟦ m ⟧ ∎ + + *ᵣ-assoc : NDefs.RightCongruent N._*ᵣ_ → NDefs.Associative _*_ N._*ᵣ_ → MDefs.Associative _*_ M._*ᵣ_ + *ᵣ-assoc {_*_ = _*_} *ᵣ-congʳ *ᵣ-assoc m x y = injective $ begin + ⟦ m M.*ᵣ x M.*ᵣ y ⟧ ≈⟨ *ᵣ-homo y (m M.*ᵣ x) ⟩ + ⟦ m M.*ᵣ x ⟧ N.*ᵣ y ≈⟨ *ᵣ-congʳ (*ᵣ-homo x m) ⟩ + ⟦ m ⟧ N.*ᵣ x N.*ᵣ y ≈⟨ *ᵣ-assoc ⟦ m ⟧ x y ⟩ + ⟦ m ⟧ N.*ᵣ (x * y) ≈˘⟨ *ᵣ-homo (x * y) m ⟩ + ⟦ m M.*ᵣ (x * y) ⟧ ∎ + + *ᵣ-zeroˡ : NDefs.RightCongruent N._*ᵣ_ → NDefs.LeftZero N.0ᴹ N._*ᵣ_ → MDefs.LeftZero M.0ᴹ M._*ᵣ_ + *ᵣ-zeroˡ *ᵣ-congʳ *ᵣ-zeroˡ x = injective $ begin + ⟦ M.0ᴹ M.*ᵣ x ⟧ ≈⟨ *ᵣ-homo x M.0ᴹ ⟩ + ⟦ M.0ᴹ ⟧ N.*ᵣ x ≈⟨ *ᵣ-congʳ 0ᴹ-homo ⟩ + N.0ᴹ N.*ᵣ x ≈⟨ *ᵣ-zeroˡ x ⟩ + N.0ᴹ ≈˘⟨ 0ᴹ-homo ⟩ + ⟦ M.0ᴹ ⟧ ∎ + + *ᵣ-distribʳ : NDefs.RightCongruent N._*ᵣ_ → N._*ᵣ_ NDefs.DistributesOverʳ N._+ᴹ_ → M._*ᵣ_ MDefs.DistributesOverʳ M._+ᴹ_ + *ᵣ-distribʳ *ᵣ-congʳ *ᵣ-distribʳ x m n = injective $ begin + ⟦ (m M.+ᴹ n) M.*ᵣ x ⟧ ≈⟨ *ᵣ-homo x (m M.+ᴹ n) ⟩ + ⟦ m M.+ᴹ n ⟧ N.*ᵣ x ≈⟨ *ᵣ-congʳ (+ᴹ-homo m n) ⟩ + (⟦ m ⟧ N.+ᴹ ⟦ n ⟧) N.*ᵣ x ≈⟨ *ᵣ-distribʳ x ⟦ m ⟧ ⟦ n ⟧ ⟩ + ⟦ m ⟧ N.*ᵣ x N.+ᴹ ⟦ n ⟧ N.*ᵣ x ≈˘⟨ +ᴹ-cong′ (*ᵣ-homo x m) (*ᵣ-homo x n) ⟩ + ⟦ m M.*ᵣ x ⟧ N.+ᴹ ⟦ n M.*ᵣ x ⟧ ≈˘⟨ +ᴹ-homo (m M.*ᵣ x) (n M.*ᵣ x) ⟩ + ⟦ m M.*ᵣ x M.+ᴹ n M.*ᵣ x ⟧ ∎ + +------------------------------------------------------------------------ +-- Structures + +isRightSemimodule : + (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) + (let R-semiring = record { isSemiring = R-isSemiring }) + → IsRightSemimodule R-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ᵣ_ + → IsRightSemimodule R-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ᵣ_ +isRightSemimodule isSemiring isRightSemimodule = record + { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid + ; isPrerightSemimodule = record + { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMonoid NN.*ᵣ-cong + ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMonoid NN.*ᵣ-zeroʳ + ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMonoid NN.*ᵣ-distribˡ + ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMonoid NN.*ᵣ-identityʳ + ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-assoc + ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ + ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-distribʳ + } + } where module NN = IsRightSemimodule isRightSemimodule From 169e3ae3fea880a96eb218552b4db8073f046047 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 14:46:48 +0200 Subject: [PATCH 10/22] Monomorphisms over right modules --- .../Morphism/RightModuleMonomorphism.agda | 58 +++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 src/Algebra/Module/Morphism/RightModuleMonomorphism.agda diff --git a/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda new file mode 100644 index 0000000000..26835d3a30 --- /dev/null +++ b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda @@ -0,0 +1,58 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between right modules +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.RightModuleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawRightModule R a ℓ₁} {N : RawRightModule R b ℓ₂} {⟦_⟧} + (isRightModuleMonomorphism : IsRightModuleMonomorphism M N ⟦_⟧) + where + +open IsRightModuleMonomorphism isRightModuleMonomorphism +module M = RawRightModule M +module N = RawRightModule N + +open import Algebra.Bundles +open import Algebra.Core +open import Algebra.Module.Structures +open import Algebra.Structures +open import Relation.Binary.Core + +------------------------------------------------------------------------ +-- Reexports + +open import Algebra.Morphism.GroupMonomorphism +ᴹ-isGroupMonomorphism public + using () renaming + ( inverseˡ to -ᴹ‿inverseˡ + ; inverseʳ to -ᴹ‿inverseʳ + ; inverse to -ᴹ‿inverse + ; ⁻¹-cong to -ᴹ‿cong + ; ⁻¹-distrib-∙ to -ᴹ‿distrib-+ᴹ + ; isGroup to +ᴹ-isGroup + ; isAbelianGroup to +ᴹ-isAbelianGroup + ) +open import Algebra.Module.Morphism.RightSemimoduleMonomorphism isRightSemimoduleMonomorphism public + +------------------------------------------------------------------------ +-- Structures + +isRightModule : + ∀ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} { -_ : Op₁ R} {0# 1# : R} + (R-isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) + (let R-ring = record { isRing = R-isRing }) + → IsRightModule R-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ᵣ_ + → IsRightModule R-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ᵣ_ +isRightModule isRing isRightModule = record + { isRightSemimodule = isRightSemimodule R.isSemiring NN.isRightSemimodule + ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse + } + where + module R = IsRing isRing + module NN = IsRightModule isRightModule From 5350002fbf59c416644fac1c0cb691b82c98cf4b Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 16:41:16 +0200 Subject: [PATCH 11/22] Add properties of bisemimodule monomorphisms --- .../Morphism/BisemimoduleMonomorphism.agda | 139 ++++++++++++++++++ 1 file changed, 139 insertions(+) create mode 100644 src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda diff --git a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda new file mode 100644 index 0000000000..255ed1ecae --- /dev/null +++ b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda @@ -0,0 +1,139 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between bisemimodules +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.BisemimoduleMonomorphism + {r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBisemimodule R S a ℓ₁} {N : RawBisemimodule R S b ℓ₂} {⟦_⟧} + (isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M N ⟦_⟧) + where + +open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism +module M = RawBisemimodule M +module N = RawBisemimodule N + +open import Algebra.Core +import Algebra.Module.Definitions.Bi as BiDefs +import Algebra.Module.Definitions.Left as LeftDefs +import Algebra.Module.Definitions.Right as RightDefs +open import Algebra.Module.Structures +open import Algebra.Structures +open import Function.Base +open import Relation.Binary.Core +import Relation.Binary.Reasoning.Setoid as SetoidReasoning + +------------------------------------------------------------------------ +-- Reexports + +open import Algebra.Morphism.MonoidMonomorphism + +ᴹ-isMonoidMonomorphism public + using () + renaming + ( cong to +ᴹ-cong + ; assoc to +ᴹ-assoc + ; comm to +ᴹ-comm + ; identityˡ to +ᴹ-identityˡ + ; identityʳ to +ᴹ-identityʳ + ; identity to +ᴹ-identity + ; isMagma to +ᴹ-isMagma + ; isSemigroup to +ᴹ-isSemigroup + ; isMonoid to +ᴹ-isMonoid + ; isCommutativeMonoid to +ᴹ-isCommutativeMonoid + ) + +open import Algebra.Module.Morphism.LeftSemimoduleMonomorphism + isLeftSemimoduleMonomorphism public + using + ( *ₗ-cong + ; *ₗ-zeroˡ + ; *ₗ-distribʳ + ; *ₗ-identityˡ + ; *ₗ-assoc + ; *ₗ-zeroʳ + ; *ₗ-distribˡ + ; isLeftSemimodule + ) + +open import Algebra.Module.Morphism.RightSemimoduleMonomorphism + isRightSemimoduleMonomorphism public + using + ( *ᵣ-cong + ; *ᵣ-zeroʳ + ; *ᵣ-distribˡ + ; *ᵣ-identityʳ + ; *ᵣ-assoc + ; *ᵣ-zeroˡ + ; *ᵣ-distribʳ + ; isRightSemimodule + ) + +------------------------------------------------------------------------ +-- Properties + +module _ (+ᴹ-isMonoid : IsMonoid N._≈ᴹ_ N._+ᴹ_ N.0ᴹ) where + + open IsMonoid +ᴹ-isMonoid + using (setoid) + renaming (∙-cong to +ᴹ-cong) + open SetoidReasoning setoid + + private + module MDefs = BiDefs R S M._≈ᴹ_ + module NDefs = BiDefs R S N._≈ᴹ_ + module LDefs = LeftDefs R N._≈ᴹ_ + module RDefs = RightDefs S N._≈ᴹ_ + + *ₗ-*ᵣ-assoc + : LDefs.LeftCongruent N._*ₗ_ → RDefs.RightCongruent N._*ᵣ_ + → NDefs.Associative N._*ₗ_ N._*ᵣ_ + → MDefs.Associative M._*ₗ_ M._*ᵣ_ + *ₗ-*ᵣ-assoc *ₗ-congˡ *ᵣ-congʳ *ₗ-*ᵣ-assoc x m y = injective $ begin + ⟦ (x M.*ₗ m) M.*ᵣ y ⟧ ≈⟨ *ᵣ-homo y (x M.*ₗ m) ⟩ + ⟦ x M.*ₗ m ⟧ N.*ᵣ y ≈⟨ *ᵣ-congʳ (*ₗ-homo x m) ⟩ + (x N.*ₗ ⟦ m ⟧) N.*ᵣ y ≈⟨ *ₗ-*ᵣ-assoc x ⟦ m ⟧ y ⟩ + x N.*ₗ (⟦ m ⟧ N.*ᵣ y) ≈˘⟨ *ₗ-congˡ (*ᵣ-homo y m) ⟩ + x N.*ₗ ⟦ m M.*ᵣ y ⟧ ≈˘⟨ *ₗ-homo x (m M.*ᵣ y) ⟩ + ⟦ x M.*ₗ (m M.*ᵣ y) ⟧ ∎ + +------------------------------------------------------------------------ +-- Structures + +isBisemimodule : + ∀ {ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ : Op₂ R} {0r 1r : R} + {ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ : Op₂ S} {0s 1s : S} + (R-isSemiring : IsSemiring _≈r_ _+r_ _*r_ 0r 1r) + (S-isSemiring : IsSemiring _≈s_ _+s_ _*s_ 0s 1s) + (let R-semiring = record { isSemiring = R-isSemiring }) + (let S-semiring = record { isSemiring = S-isSemiring }) + → IsBisemimodule R-semiring S-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_ + → IsBisemimodule R-semiring S-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_ +isBisemimodule R-semiring S-semiring isBisemimodule = record + { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid + ; isPreleftSemimodule = record + { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMonoid NN.*ₗ-cong + ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMonoid NN.*ₗ-zeroˡ + ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMonoid NN.*ₗ-distribʳ + ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMonoid NN.*ₗ-identityˡ + ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-assoc + ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-zeroʳ + ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-distribˡ + } + ; isPrerightSemimodule = record + { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMonoid NN.*ᵣ-cong + ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMonoid NN.*ᵣ-zeroʳ + ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMonoid NN.*ᵣ-distribˡ + ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMonoid NN.*ᵣ-identityʳ + ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-assoc + ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ + ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-distribʳ + } + ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ᵣ-congʳ NN.*ₗ-*ᵣ-assoc + } + where + module NN = IsBisemimodule isBisemimodule From 9edd0349d44f7173608027cc4295fdce89dcf023 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 17:29:28 +0200 Subject: [PATCH 12/22] Make these modules private --- src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda index 255ed1ecae..b48e3554b5 100644 --- a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda @@ -15,8 +15,9 @@ module Algebra.Module.Morphism.BisemimoduleMonomorphism where open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism -module M = RawBisemimodule M -module N = RawBisemimodule N +private + module M = RawBisemimodule M + module N = RawBisemimodule N open import Algebra.Core import Algebra.Module.Definitions.Bi as BiDefs From 5f72cb540622cba4d37394962d0a6be9f58463f4 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 17:29:40 +0200 Subject: [PATCH 13/22] Properties of bimodule monomorphisms --- src/Algebra/Module/Morphism/Bimodule.agda | 64 +++++++++++++++++++++++ 1 file changed, 64 insertions(+) create mode 100644 src/Algebra/Module/Morphism/Bimodule.agda diff --git a/src/Algebra/Module/Morphism/Bimodule.agda b/src/Algebra/Module/Morphism/Bimodule.agda new file mode 100644 index 0000000000..3035066c6b --- /dev/null +++ b/src/Algebra/Module/Morphism/Bimodule.agda @@ -0,0 +1,64 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of a monomorphism between bimodules +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.Bimodule + {r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBimodule R S a ℓ₁} {N : RawBimodule R S b ℓ₂} {⟦_⟧} + (isBimoduleMonomorphism : IsBimoduleMonomorphism M N ⟦_⟧) + where + +open IsBimoduleMonomorphism isBimoduleMonomorphism +private + module M = RawBimodule M + module N = RawBimodule N + +open import Algebra.Bundles +open import Algebra.Core +open import Algebra.Module.Structures +open import Algebra.Structures +open import Relation.Binary.Core + +------------------------------------------------------------------------ +-- Re-exports + +open import Algebra.Morphism.GroupMonomorphism +ᴹ-isGroupMonomorphism public + using () renaming + ( inverseˡ to -ᴹ‿inverseˡ + ; inverseʳ to -ᴹ‿inverseʳ + ; inverse to -ᴹ‿inverse + ; ⁻¹-cong to -ᴹ‿cong + ; ⁻¹-distrib-∙ to -ᴹ‿distrib-+ᴹ + ; isGroup to +ᴹ-isGroup + ; isAbelianGroup to +ᴹ-isAbelianGroup + ) +open import Algebra.Module.Morphism.BisemimoduleMonomorphism isBisemimoduleMonomorphism public + +------------------------------------------------------------------------ +-- Structures + +isBimodule : + ∀ {ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ : Op₂ R} { -r_ : Op₁ R} {0r 1r : R} + {ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ : Op₂ S} { -s_ : Op₁ S} {0s 1s : S} + (R-isRing : IsRing _≈r_ _+r_ _*r_ -r_ 0r 1r) + (S-isRing : IsRing _≈s_ _+s_ _*s_ -s_ 0s 1s) + (let R-ring = record { isRing = R-isRing }) + (let S-ring = record { isRing = S-isRing }) + → IsBimodule R-ring S-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ + → IsBimodule R-ring S-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_ +isBimodule R-isRing S-isRing isBimodule = record + { isBisemimodule = isBisemimodule R-isRing.isSemiring S-isRing.isSemiring NN.isBisemimodule + ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse + } + where + module R-isRing = IsRing R-isRing + module S-isRing = IsRing S-isRing + module NN = IsBimodule isBimodule + From 9fe0efd1e5d848d7fd24a91d091844c8f00804fc Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 17:58:19 +0200 Subject: [PATCH 14/22] Properties of semimodule monomorphisms --- src/Algebra/Module/Morphism/Semimodule.agda | 69 +++++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 src/Algebra/Module/Morphism/Semimodule.agda diff --git a/src/Algebra/Module/Morphism/Semimodule.agda b/src/Algebra/Module/Morphism/Semimodule.agda new file mode 100644 index 0000000000..343943e07a --- /dev/null +++ b/src/Algebra/Module/Morphism/Semimodule.agda @@ -0,0 +1,69 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of a monomorphism between semimodules +------------------------------------------------------------------------ + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.Semimodule + {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawSemimodule R a ℓ₁} {N : RawSemimodule R b ℓ₂} {⟦_⟧} + (isSemimoduleMonomorphism : IsSemimoduleMonomorphism M N ⟦_⟧) + where + +open IsSemimoduleMonomorphism isSemimoduleMonomorphism +private + module M = RawSemimodule M + module N = RawSemimodule N + +open import Algebra.Bundles +open import Algebra.Core +import Algebra.Module.Definitions.Bi.Simultaneous as SimulDefs +open import Algebra.Module.Structures +open import Algebra.Structures +open import Function.Base +open import Relation.Binary.Core +import Relation.Binary.Reasoning.Setoid as SetoidReasoning + +------------------------------------------------------------------------ +-- Re-exports + +open import Algebra.Module.Morphism.BisemimoduleMonomorphism isBisemimoduleMonomorphism public + +------------------------------------------------------------------------ +-- Properties + +module _ (+ᴹ-isMonoid : IsMonoid N._≈ᴹ_ N._+ᴹ_ N.0ᴹ) where + open IsMonoid +ᴹ-isMonoid + using (setoid) + renaming (∙-cong to +ᴹ-cong) + open SetoidReasoning setoid + + private + module MDefs = SimulDefs R M._≈ᴹ_ + module NDefs = SimulDefs R N._≈ᴹ_ + + *ₗ-*ᵣ-coincident : NDefs.Coincident N._*ₗ_ N._*ᵣ_ → MDefs.Coincident M._*ₗ_ M._*ᵣ_ + *ₗ-*ᵣ-coincident *ₗ-*ᵣ-coincident x m = injective $ begin + ⟦ x M.*ₗ m ⟧ ≈⟨ *ₗ-homo x m ⟩ + x N.*ₗ ⟦ m ⟧ ≈⟨ *ₗ-*ᵣ-coincident x ⟦ m ⟧ ⟩ + ⟦ m ⟧ N.*ᵣ x ≈˘⟨ *ᵣ-homo x m ⟩ + ⟦ m M.*ᵣ x ⟧ ∎ + +------------------------------------------------------------------------ +-- Structures + +isSemimodule : + ∀ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} {0# 1# : R} + (R-isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#) + (let R-commutativeSemiring = record { isCommutativeSemiring = R-isCommutativeSemiring }) + → IsSemimodule R-commutativeSemiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_ + → IsSemimodule R-commutativeSemiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_ +isSemimodule R-isCommutativeSemiring isSemimodule = record + { isBisemimodule = isBisemimodule R.isSemiring R.isSemiring NN.isBisemimodule + ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMonoid NN.*ₗ-*ᵣ-coincident + } + where + module R = IsCommutativeSemiring R-isCommutativeSemiring + module NN = IsSemimodule isSemimodule From ef48161d8d0fb2d80654e169efcfb49450785bbf Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 18:03:57 +0200 Subject: [PATCH 15/22] Move modules to the right location --- .../Morphism/{Bimodule.agda => BimoduleMonomorphism.agda} | 2 +- .../Morphism/{Semimodule.agda => SemimoduleMonomorphism.agda} | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) rename src/Algebra/Module/Morphism/{Bimodule.agda => BimoduleMonomorphism.agda} (97%) rename src/Algebra/Module/Morphism/{Semimodule.agda => SemimoduleMonomorphism.agda} (98%) diff --git a/src/Algebra/Module/Morphism/Bimodule.agda b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda similarity index 97% rename from src/Algebra/Module/Morphism/Bimodule.agda rename to src/Algebra/Module/Morphism/BimoduleMonomorphism.agda index 3035066c6b..f97006ff9a 100644 --- a/src/Algebra/Module/Morphism/Bimodule.agda +++ b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda @@ -9,7 +9,7 @@ open import Algebra.Module.Bundles.Raw open import Algebra.Module.Morphism.Structures -module Algebra.Module.Morphism.Bimodule +module Algebra.Module.Morphism.BimoduleMonomorphism {r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBimodule R S a ℓ₁} {N : RawBimodule R S b ℓ₂} {⟦_⟧} (isBimoduleMonomorphism : IsBimoduleMonomorphism M N ⟦_⟧) where diff --git a/src/Algebra/Module/Morphism/Semimodule.agda b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda similarity index 98% rename from src/Algebra/Module/Morphism/Semimodule.agda rename to src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda index 343943e07a..613f1698f1 100644 --- a/src/Algebra/Module/Morphism/Semimodule.agda +++ b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda @@ -7,7 +7,7 @@ open import Algebra.Module.Bundles.Raw open import Algebra.Module.Morphism.Structures -module Algebra.Module.Morphism.Semimodule +module Algebra.Module.Morphism.SemimoduleMonomorphism {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawSemimodule R a ℓ₁} {N : RawSemimodule R b ℓ₂} {⟦_⟧} (isSemimoduleMonomorphism : IsSemimoduleMonomorphism M N ⟦_⟧) where From b58ecd8dbb66761ee1c421cf8956ac32fadf9d37 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 20:41:56 +0200 Subject: [PATCH 16/22] Add missing options --- src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda index 613f1698f1..45ed2aa60f 100644 --- a/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda @@ -4,6 +4,8 @@ -- Properties of a monomorphism between semimodules ------------------------------------------------------------------------ +{-# OPTIONS --safe --cubical-compatible #-} + open import Algebra.Module.Bundles.Raw open import Algebra.Module.Morphism.Structures From bbac769c61237370b0ca9e8ef4fccc4088fef04f Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 20:42:07 +0200 Subject: [PATCH 17/22] Properties of module monomorphisms --- .../Module/Morphism/ModuleMonomorphism.agda | 50 +++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 src/Algebra/Module/Morphism/ModuleMonomorphism.agda diff --git a/src/Algebra/Module/Morphism/ModuleMonomorphism.agda b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda new file mode 100644 index 0000000000..971cb36e7e --- /dev/null +++ b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda @@ -0,0 +1,50 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Consequences of a monomorphism between modules +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +open import Algebra.Module.Bundles.Raw +open import Algebra.Module.Morphism.Structures + +module Algebra.Module.Morphism.ModuleMonomorphism + {r a b ℓ₁ ℓ₂} {R : Set r} {M : RawModule R a ℓ₁} {N : RawModule R b ℓ₂} {⟦_⟧} + (isModuleMonomorphism : IsModuleMonomorphism M N ⟦_⟧) + where + +open IsModuleMonomorphism isModuleMonomorphism +private + module M = RawModule M + module N = RawModule N + +open import Algebra.Bundles +open import Algebra.Core +open import Algebra.Module.Structures +open import Algebra.Structures +open import Relation.Binary.Core + +------------------------------------------------------------------------ +-- Re-exports + +open import Algebra.Module.Morphism.BimoduleMonomorphism isBimoduleMonomorphism public +open import Algebra.Module.Morphism.SemimoduleMonomorphism isSemimoduleMonomorphism public + using (*ₗ-*ᵣ-coincident; isSemimodule) + +------------------------------------------------------------------------ +-- Structures + +isModule : + ∀ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} { -_ : Op₁ R} {0# 1# : R} + (R-isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#) + (let R-commutativeRing = record { isCommutativeRing = R-isCommutativeRing }) + → IsModule R-commutativeRing N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ + → IsModule R-commutativeRing M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_ +isModule R-isCommutativeRing isModule = record + { isBimodule = isBimodule R.isRing R.isRing NN.isBimodule + ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMonoid NN.*ₗ-*ᵣ-coincident + } + where + module R = IsCommutativeRing R-isCommutativeRing + module NN = IsModule isModule From 1d0f48266cf8e2e8ef9aa9710d8fd23fb3bf1731 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 20:43:40 +0200 Subject: [PATCH 18/22] Fix somewhitespace --- src/Algebra/Module/Bundles/Raw.agda | 2 +- src/Algebra/Module/Morphism/BimoduleMonomorphism.agda | 2 +- src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda | 2 +- src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Module/Bundles/Raw.agda b/src/Algebra/Module/Bundles/Raw.agda index b9cc108915..2eb280875f 100644 --- a/src/Algebra/Module/Bundles/Raw.agda +++ b/src/Algebra/Module/Bundles/Raw.agda @@ -200,7 +200,7 @@ record RawBimodule (R : Set r) (S : Set s) m ℓm : Set (r ⊔ s ⊔ suc (m ⊔ ; 0ᴹ = 0ᴹ ; -ᴹ_ = -ᴹ_ } - + rawRightModule : RawRightModule S m ℓm rawRightModule = record { _≈ᴹ_ = _≈ᴹ_ diff --git a/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda index f97006ff9a..6b1de42335 100644 --- a/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda @@ -50,7 +50,7 @@ isBimodule : (S-isRing : IsRing _≈s_ _+s_ _*s_ -s_ 0s 1s) (let R-ring = record { isRing = R-isRing }) (let S-ring = record { isRing = S-isRing }) - → IsBimodule R-ring S-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ + → IsBimodule R-ring S-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ → IsBimodule R-ring S-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_ isBimodule R-isRing S-isRing isBimodule = record { isBisemimodule = isBisemimodule R-isRing.isSemiring S-isRing.isSemiring NN.isBisemimodule diff --git a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda index b48e3554b5..d853e5e0f6 100644 --- a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda @@ -113,7 +113,7 @@ isBisemimodule : (let R-semiring = record { isSemiring = R-isSemiring }) (let S-semiring = record { isSemiring = S-isSemiring }) → IsBisemimodule R-semiring S-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_ - → IsBisemimodule R-semiring S-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_ + → IsBisemimodule R-semiring S-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_ isBisemimodule R-semiring S-semiring isBisemimodule = record { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid ; isPreleftSemimodule = record diff --git a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda index bab54b4bf9..7de597c03d 100644 --- a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda @@ -60,7 +60,7 @@ module _ (+ᴹ-isMonoid : IsMonoid N._≈ᴹ_ N._+ᴹ_ N.0ᴹ) where using (setoid) renaming (∙-cong to +ᴹ-cong′) open SetoidReasoning setoid - + module MDefs = RightDefs R M._≈ᴹ_ module NDefs = RightDefs R N._≈ᴹ_ From ae20eacbc2ca03f4b287b42a6feb069acacd1f67 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 20:47:39 +0200 Subject: [PATCH 19/22] Use IsMagma rather than IsMonoid in several places --- .../Morphism/BisemimoduleMonomorphism.agda | 34 +++++++++---------- .../Morphism/LeftSemimoduleMonomorphism.agda | 18 +++++----- .../Module/Morphism/ModuleMonomorphism.agda | 2 +- .../Morphism/RightSemimoduleMonomorphism.agda | 18 +++++----- .../Morphism/SemimoduleMonomorphism.agda | 6 ++-- 5 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda index d853e5e0f6..b8e5f61d82 100644 --- a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda @@ -77,9 +77,9 @@ open import Algebra.Module.Morphism.RightSemimoduleMonomorphism ------------------------------------------------------------------------ -- Properties -module _ (+ᴹ-isMonoid : IsMonoid N._≈ᴹ_ N._+ᴹ_ N.0ᴹ) where +module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where - open IsMonoid +ᴹ-isMonoid + open IsMagma +ᴹ-isMagma using (setoid) renaming (∙-cong to +ᴹ-cong) open SetoidReasoning setoid @@ -117,24 +117,24 @@ isBisemimodule : isBisemimodule R-semiring S-semiring isBisemimodule = record { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid ; isPreleftSemimodule = record - { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMonoid NN.*ₗ-cong - ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMonoid NN.*ₗ-zeroˡ - ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMonoid NN.*ₗ-distribʳ - ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMonoid NN.*ₗ-identityˡ - ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-assoc - ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-zeroʳ - ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-distribˡ + { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong + ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ + ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ + ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ + ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc + ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ + ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ } ; isPrerightSemimodule = record - { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMonoid NN.*ᵣ-cong - ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMonoid NN.*ᵣ-zeroʳ - ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMonoid NN.*ᵣ-distribˡ - ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMonoid NN.*ᵣ-identityʳ - ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-assoc - ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ - ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-distribʳ + { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong + ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ + ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ + ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ + ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc + ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ + ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ } - ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ᵣ-congʳ NN.*ₗ-*ᵣ-assoc + ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ᵣ-congʳ NN.*ₗ-*ᵣ-assoc } where module NN = IsBisemimodule isBisemimodule diff --git a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda index 38a7548cba..b4f9cee75b 100644 --- a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda @@ -57,9 +57,9 @@ open import Algebra.Morphism.MonoidMonomorphism ---------------------------------------------------------------------------------- -- Properties -module _ (⊕ᴹ-isMonoid : IsMonoid N._≈ᴹ_ N._+ᴹ_ N.0ᴹ) where +module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where - open IsMonoid ⊕ᴹ-isMonoid + open IsMagma +ᴹ-isMagma using (setoid) renaming (∙-cong to +ᴹ-cong′) open SetoidReasoning setoid @@ -131,12 +131,12 @@ isLeftSemimodule : isLeftSemimodule isSemiring isLeftSemimodule = record { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid ; isPreleftSemimodule = record - { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMonoid NN.*ₗ-cong - ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMonoid NN.*ₗ-zeroˡ - ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMonoid NN.*ₗ-distribʳ - ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMonoid NN.*ₗ-identityˡ - ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-assoc - ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-zeroʳ - ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMonoid NN.*ₗ-congˡ NN.*ₗ-distribˡ + { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong + ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ + ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ + ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ + ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc + ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ + ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ } } where module NN = IsLeftSemimodule isLeftSemimodule diff --git a/src/Algebra/Module/Morphism/ModuleMonomorphism.agda b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda index 971cb36e7e..40204d8052 100644 --- a/src/Algebra/Module/Morphism/ModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda @@ -43,7 +43,7 @@ isModule : → IsModule R-commutativeRing M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_ isModule R-isCommutativeRing isModule = record { isBimodule = isBimodule R.isRing R.isRing NN.isBimodule - ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMonoid NN.*ₗ-*ᵣ-coincident + ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMagma NN.*ₗ-*ᵣ-coincident } where module R = IsCommutativeRing R-isCommutativeRing diff --git a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda index 7de597c03d..4fd63e0e4b 100644 --- a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda @@ -54,9 +54,9 @@ open import Algebra.Morphism.MonoidMonomorphism ------------------------------------------------------------------------ -- Properties -module _ (+ᴹ-isMonoid : IsMonoid N._≈ᴹ_ N._+ᴹ_ N.0ᴹ) where +module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where - open IsMonoid +ᴹ-isMonoid + open IsMagma +ᴹ-isMagma using (setoid) renaming (∙-cong to +ᴹ-cong′) open SetoidReasoning setoid @@ -128,12 +128,12 @@ isRightSemimodule : isRightSemimodule isSemiring isRightSemimodule = record { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid ; isPrerightSemimodule = record - { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMonoid NN.*ᵣ-cong - ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMonoid NN.*ᵣ-zeroʳ - ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMonoid NN.*ᵣ-distribˡ - ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMonoid NN.*ᵣ-identityʳ - ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-assoc - ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ - ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMonoid NN.*ᵣ-congʳ NN.*ᵣ-distribʳ + { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong + ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ + ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ + ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ + ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc + ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ + ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ } } where module NN = IsRightSemimodule isRightSemimodule diff --git a/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda index 45ed2aa60f..3c8d69c3de 100644 --- a/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda @@ -36,8 +36,8 @@ open import Algebra.Module.Morphism.BisemimoduleMonomorphism isBisemimoduleMonom ------------------------------------------------------------------------ -- Properties -module _ (+ᴹ-isMonoid : IsMonoid N._≈ᴹ_ N._+ᴹ_ N.0ᴹ) where - open IsMonoid +ᴹ-isMonoid +module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where + open IsMagma +ᴹ-isMagma using (setoid) renaming (∙-cong to +ᴹ-cong) open SetoidReasoning setoid @@ -64,7 +64,7 @@ isSemimodule : → IsSemimodule R-commutativeSemiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_ isSemimodule R-isCommutativeSemiring isSemimodule = record { isBisemimodule = isBisemimodule R.isSemiring R.isSemiring NN.isBisemimodule - ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMonoid NN.*ₗ-*ᵣ-coincident + ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMagma NN.*ₗ-*ᵣ-coincident } where module R = IsCommutativeSemiring R-isCommutativeSemiring From be46a21aade3f405f995e494a517ca2207000dbd Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 9 Jun 2024 20:49:03 +0200 Subject: [PATCH 20/22] Spell re-exports consistently --- src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda | 2 +- src/Algebra/Module/Morphism/RightModuleMonomorphism.agda | 2 +- src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda | 3 +++ 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda index b8e5f61d82..8f9e00c91c 100644 --- a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda @@ -30,7 +30,7 @@ open import Relation.Binary.Core import Relation.Binary.Reasoning.Setoid as SetoidReasoning ------------------------------------------------------------------------ --- Reexports +-- Re-exports open import Algebra.Morphism.MonoidMonomorphism +ᴹ-isMonoidMonomorphism public diff --git a/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda index 26835d3a30..41086803ec 100644 --- a/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda @@ -25,7 +25,7 @@ open import Algebra.Structures open import Relation.Binary.Core ------------------------------------------------------------------------ --- Reexports +-- Re-exports open import Algebra.Morphism.GroupMonomorphism +ᴹ-isGroupMonomorphism public using () renaming diff --git a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda index 4fd63e0e4b..f6b2ebe55c 100644 --- a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda @@ -35,6 +35,9 @@ private _+_ _*_ : Op₂ R 0# 1# : R +------------------------------------------------------------------------ +-- Re-exports + open import Algebra.Morphism.MonoidMonomorphism +ᴹ-isMonoidMonomorphism public using () From 5fe2637f724a1b6c4fb29dd08f48d160c8ce840f Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 17 Jun 2024 09:38:44 +0200 Subject: [PATCH 21/22] Use modules to make type signatures of structures clearer --- .../Module/Morphism/BimoduleMonomorphism.agda | 39 +++++++---- .../Morphism/BisemimoduleMonomorphism.agda | 69 +++++++++++-------- .../Morphism/LeftModuleMonomorphism.agda | 31 +++++---- .../Morphism/LeftSemimoduleMonomorphism.agda | 39 ++++++----- .../Module/Morphism/ModuleMonomorphism.agda | 30 ++++---- .../Morphism/RightModuleMonomorphism.agda | 31 +++++---- .../Morphism/RightSemimoduleMonomorphism.agda | 39 ++++++----- .../Morphism/SemimoduleMonomorphism.agda | 30 ++++---- 8 files changed, 175 insertions(+), 133 deletions(-) diff --git a/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda index 6b1de42335..6cbdb5d8ba 100644 --- a/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda @@ -43,22 +43,31 @@ open import Algebra.Module.Morphism.BisemimoduleMonomorphism isBisemimoduleMonom ------------------------------------------------------------------------ -- Structures -isBimodule : - ∀ {ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ : Op₂ R} { -r_ : Op₁ R} {0r 1r : R} - {ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ : Op₂ S} { -s_ : Op₁ S} {0s 1s : S} +module _ + {ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ -r_ 0r 1r} + {ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ -s_ 0s 1s} (R-isRing : IsRing _≈r_ _+r_ _*r_ -r_ 0r 1r) (S-isRing : IsRing _≈s_ _+s_ _*s_ -s_ 0s 1s) - (let R-ring = record { isRing = R-isRing }) - (let S-ring = record { isRing = S-isRing }) - → IsBimodule R-ring S-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ - → IsBimodule R-ring S-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_ -isBimodule R-isRing S-isRing isBimodule = record - { isBisemimodule = isBisemimodule R-isRing.isSemiring S-isRing.isSemiring NN.isBisemimodule - ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong - ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse - } where - module R-isRing = IsRing R-isRing - module S-isRing = IsRing S-isRing - module NN = IsBimodule isBimodule + + private + R-ring : Ring _ _ + R-ring = record { isRing = R-isRing } + + S-ring : Ring _ _ + S-ring = record { isRing = S-isRing } + + module R = IsRing R-isRing + module S = IsRing S-isRing + + isBimodule + : IsBimodule R-ring S-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ + → IsBimodule R-ring S-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_ + isBimodule isBimodule = record + { isBisemimodule = isBisemimodule R.isSemiring S.isSemiring NN.isBisemimodule + ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse + } + where + module NN = IsBimodule isBimodule diff --git a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda index 8f9e00c91c..1a1142732b 100644 --- a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda @@ -19,6 +19,7 @@ private module M = RawBisemimodule M module N = RawBisemimodule N +open import Algebra.Bundles open import Algebra.Core import Algebra.Module.Definitions.Bi as BiDefs import Algebra.Module.Definitions.Left as LeftDefs @@ -105,36 +106,44 @@ module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where ------------------------------------------------------------------------ -- Structures -isBisemimodule : - ∀ {ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ : Op₂ R} {0r 1r : R} - {ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ : Op₂ S} {0s 1s : S} +module _ + {ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ 0r 1r} + {ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ 0s 1s} (R-isSemiring : IsSemiring _≈r_ _+r_ _*r_ 0r 1r) (S-isSemiring : IsSemiring _≈s_ _+s_ _*s_ 0s 1s) - (let R-semiring = record { isSemiring = R-isSemiring }) - (let S-semiring = record { isSemiring = S-isSemiring }) - → IsBisemimodule R-semiring S-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_ - → IsBisemimodule R-semiring S-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_ -isBisemimodule R-semiring S-semiring isBisemimodule = record - { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid - ; isPreleftSemimodule = record - { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong - ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ - ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ - ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ - ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc - ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ - ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ - } - ; isPrerightSemimodule = record - { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong - ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ - ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ - ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ - ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc - ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ - ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ - } - ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ᵣ-congʳ NN.*ₗ-*ᵣ-assoc - } where - module NN = IsBisemimodule isBisemimodule + + private + R-semiring : Semiring _ _ + R-semiring = record { isSemiring = R-isSemiring } + + S-semiring : Semiring _ _ + S-semiring = record { isSemiring = S-isSemiring } + + isBisemimodule + : IsBisemimodule R-semiring S-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_ + → IsBisemimodule R-semiring S-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_ + isBisemimodule isBisemimodule = record + { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid + ; isPreleftSemimodule = record + { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong + ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ + ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ + ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ + ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc + ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ + ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ + } + ; isPrerightSemimodule = record + { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong + ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ + ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ + ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ + ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc + ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ + ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ + } + ; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ᵣ-congʳ NN.*ₗ-*ᵣ-assoc + } + where + module NN = IsBisemimodule isBisemimodule diff --git a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda index 710b71b1a2..8aa4307fa6 100644 --- a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda @@ -43,17 +43,20 @@ open import Algebra.Module.Morphism.LeftSemimoduleMonomorphism isLeftSemimoduleM ------------------------------------------------------------------------ -- Structures -isLeftModule : - ∀ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} { -_ : Op₁ R} {0# 1# : R} - (R-isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) - (let R-ring = record { isRing = R-isRing }) - → IsLeftModule R-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ - → IsLeftModule R-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ -isLeftModule R-isRing isLeftModule = record - { isLeftSemimodule = isLeftSemimodule R.isSemiring NN.isLeftSemimodule - ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong - ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse - } - where - module R = IsRing R-isRing - module NN = IsLeftModule isLeftModule +module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ -_ 0# 1#} (R-isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) where + + private + R-ring : Ring _ _ + R-ring = record { isRing = R-isRing } + open IsRing R-isRing + + isLeftModule + : IsLeftModule R-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ + → IsLeftModule R-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ + isLeftModule isLeftModule = record + { isLeftSemimodule = isLeftSemimodule isSemiring NN.isLeftSemimodule + ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse + } + where + module NN = IsLeftModule isLeftModule diff --git a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda index b4f9cee75b..1976dc226c 100644 --- a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda @@ -19,6 +19,7 @@ private module M = RawLeftSemimodule M₁ module N = RawLeftSemimodule M₂ +open import Algebra.Bundles open import Algebra.Core import Algebra.Module.Definitions.Left as LeftDefs open import Algebra.Module.Structures @@ -123,20 +124,24 @@ module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where ------------------------------------------------------------------------ -- Structures -isLeftSemimodule : - (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) - (let R-semiring = record { isSemiring = R-isSemiring }) - → IsLeftSemimodule R-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ - → IsLeftSemimodule R-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ -isLeftSemimodule isSemiring isLeftSemimodule = record - { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid - ; isPreleftSemimodule = record - { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong - ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ - ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ - ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ - ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc - ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ - ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ - } - } where module NN = IsLeftSemimodule isLeftSemimodule +module _ (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) where + + private + R-semiring : Semiring _ _ + R-semiring = record { isSemiring = R-isSemiring } + + isLeftSemimodule + : IsLeftSemimodule R-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ + → IsLeftSemimodule R-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ + isLeftSemimodule isLeftSemimodule = record + { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid + ; isPreleftSemimodule = record + { *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong + ; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ + ; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ + ; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ + ; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc + ; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ + ; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ + } + } where module NN = IsLeftSemimodule isLeftSemimodule diff --git a/src/Algebra/Module/Morphism/ModuleMonomorphism.agda b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda index 40204d8052..29b9f68311 100644 --- a/src/Algebra/Module/Morphism/ModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda @@ -35,16 +35,20 @@ open import Algebra.Module.Morphism.SemimoduleMonomorphism isSemimoduleMonomorph ------------------------------------------------------------------------ -- Structures -isModule : - ∀ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} { -_ : Op₁ R} {0# 1# : R} - (R-isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#) - (let R-commutativeRing = record { isCommutativeRing = R-isCommutativeRing }) - → IsModule R-commutativeRing N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ - → IsModule R-commutativeRing M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_ -isModule R-isCommutativeRing isModule = record - { isBimodule = isBimodule R.isRing R.isRing NN.isBimodule - ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMagma NN.*ₗ-*ᵣ-coincident - } - where - module R = IsCommutativeRing R-isCommutativeRing - module NN = IsModule isModule +module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ -_ 0# 1#} (R-isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#) where + + private + R-commutativeRing : CommutativeRing _ _ + R-commutativeRing = record { isCommutativeRing = R-isCommutativeRing } + + open IsCommutativeRing R-isCommutativeRing + + isModule + : IsModule R-commutativeRing N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_ + → IsModule R-commutativeRing M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_ + isModule isModule = record + { isBimodule = isBimodule isRing isRing NN.isBimodule + ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMagma NN.*ₗ-*ᵣ-coincident + } + where + module NN = IsModule isModule diff --git a/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda index 41086803ec..23a6f68248 100644 --- a/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda @@ -42,17 +42,20 @@ open import Algebra.Module.Morphism.RightSemimoduleMonomorphism isRightSemimodul ------------------------------------------------------------------------ -- Structures -isRightModule : - ∀ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} { -_ : Op₁ R} {0# 1# : R} - (R-isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) - (let R-ring = record { isRing = R-isRing }) - → IsRightModule R-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ᵣ_ - → IsRightModule R-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ᵣ_ -isRightModule isRing isRightModule = record - { isRightSemimodule = isRightSemimodule R.isSemiring NN.isRightSemimodule - ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong - ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse - } - where - module R = IsRing isRing - module NN = IsRightModule isRightModule +module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ -_ 0# 1#} (R-isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) where + + private + R-ring : Ring _ _ + R-ring = record { isRing = R-isRing} + open IsRing R-isRing + + isRightModule + : IsRightModule R-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ᵣ_ + → IsRightModule R-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ᵣ_ + isRightModule isRightModule = record + { isRightSemimodule = isRightSemimodule isSemiring NN.isRightSemimodule + ; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse + } + where + module NN = IsRightModule isRightModule diff --git a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda index f6b2ebe55c..b3d0c312a0 100644 --- a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda @@ -19,6 +19,7 @@ private module M = RawRightSemimodule M module N = RawRightSemimodule N +open import Algebra.Bundles open import Algebra.Core import Algebra.Module.Definitions.Right as RightDefs open import Algebra.Module.Structures @@ -123,20 +124,24 @@ module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where ------------------------------------------------------------------------ -- Structures -isRightSemimodule : - (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) - (let R-semiring = record { isSemiring = R-isSemiring }) - → IsRightSemimodule R-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ᵣ_ - → IsRightSemimodule R-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ᵣ_ -isRightSemimodule isSemiring isRightSemimodule = record - { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid - ; isPrerightSemimodule = record - { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong - ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ - ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ - ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ - ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc - ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ - ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ - } - } where module NN = IsRightSemimodule isRightSemimodule +module _ (R-isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#) where + + private + R-semiring : Semiring _ _ + R-semiring = record { isSemiring = R-isSemiring } + + isRightSemimodule + : IsRightSemimodule R-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ᵣ_ + → IsRightSemimodule R-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ᵣ_ + isRightSemimodule isRightSemimodule = record + { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid + ; isPrerightSemimodule = record + { *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong + ; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ + ; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ + ; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ + ; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc + ; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ + ; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ + } + } where module NN = IsRightSemimodule isRightSemimodule diff --git a/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda index 3c8d69c3de..396230bee3 100644 --- a/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda @@ -56,16 +56,20 @@ module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where ------------------------------------------------------------------------ -- Structures -isSemimodule : - ∀ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ : Op₂ R} {0# 1# : R} - (R-isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#) - (let R-commutativeSemiring = record { isCommutativeSemiring = R-isCommutativeSemiring }) - → IsSemimodule R-commutativeSemiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_ - → IsSemimodule R-commutativeSemiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_ -isSemimodule R-isCommutativeSemiring isSemimodule = record - { isBisemimodule = isBisemimodule R.isSemiring R.isSemiring NN.isBisemimodule - ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMagma NN.*ₗ-*ᵣ-coincident - } - where - module R = IsCommutativeSemiring R-isCommutativeSemiring - module NN = IsSemimodule isSemimodule +module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ 0# 1#} (R-isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#) where + + private + R-commutativeSemiring : CommutativeSemiring _ _ + R-commutativeSemiring = record { isCommutativeSemiring = R-isCommutativeSemiring } + + open IsCommutativeSemiring R-isCommutativeSemiring + + isSemimodule + : IsSemimodule R-commutativeSemiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_ + → IsSemimodule R-commutativeSemiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_ + isSemimodule isSemimodule = record + { isBisemimodule = isBisemimodule isSemiring isSemiring NN.isBisemimodule + ; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident NN.+ᴹ-isMagma NN.*ₗ-*ᵣ-coincident + } + where + module NN = IsSemimodule isSemimodule From f57cbbd5bd6633125d5fa4e1d6fde9d3b92a2a56 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 6 Dec 2024 15:32:37 +0000 Subject: [PATCH 22/22] [ changelog ] listing the new modules --- CHANGELOG.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9f8d6de9bd..fb0eaa3740 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -126,6 +126,19 @@ New modules Algebra.Module.Construct.Idealization ``` +* Consequences of module monomorphisms + ```agda + Algebra.Module.Morphism.BimoduleMonomorphism + Algebra.Module.Morphism.BisemimoduleMonomorphism + Algebra.Module.Morphism.LeftModuleMonomorphism + Algebra.Module.Morphism.LeftSemimoduleMonomorphism + Algebra.Module.Morphism.ModuleMonomorphism + Algebra.Module.Morphism.RightModuleMonomorphism + Algebra.Module.Morphism.RightSemimoduleMonomorphism + Algebra.Module.Morphism.SemimoduleMonomorphism + ``` + + * The unique morphism from the initial, resp. terminal, algebra: ```agda Algebra.Morphism.Construct.Initial