diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/src/Algebra/Module/Construct/DirectProduct.agda index c369983904..4cbf6c3972 100644 --- a/src/Algebra/Module/Construct/DirectProduct.agda +++ b/src/Algebra/Module/Construct/DirectProduct.agda @@ -184,7 +184,7 @@ leftModule : {R : Ring r ℓr} → LeftModule R m′ ℓm′ → LeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′) leftModule M N = record - { -ᴹ_ = map M.-ᴹ_ N.-ᴹ_ + { -ᴹ_ = map (M.-ᴹ_) (N.-ᴹ_) ; isLeftModule = record { isLeftSemimodule = LeftSemimodule.isLeftSemimodule (leftSemimodule M.leftSemimodule N.leftSemimodule) @@ -200,7 +200,7 @@ rightModule : {R : Ring r ℓr} → RightModule R m′ ℓm′ → RightModule R (m ⊔ m′) (ℓm ⊔ ℓm′) rightModule M N = record - { -ᴹ_ = map M.-ᴹ_ N.-ᴹ_ + { -ᴹ_ = map (M.-ᴹ_) (N.-ᴹ_) ; isRightModule = record { isRightSemimodule = RightSemimodule.isRightSemimodule (rightSemimodule M.rightSemimodule N.rightSemimodule) @@ -216,7 +216,7 @@ bimodule : {R : Ring r ℓr} {S : Ring s ℓs} → Bimodule R S m′ ℓm′ → Bimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′) bimodule M N = record - { -ᴹ_ = map M.-ᴹ_ N.-ᴹ_ + { -ᴹ_ = map (M.-ᴹ_) (N.-ᴹ_) ; isBimodule = record { isBisemimodule = Bisemimodule.isBisemimodule (bisemimodule M.bisemimodule N.bisemimodule) diff --git a/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda index 79d5cfff9c..cfed1ef629 100644 --- a/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/BimoduleMonomorphism.agda @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.BimoduleMonomorphism (isBimoduleMonomorphism : IsBimoduleMonomorphism M N ⟦_⟧) where -open IsBimoduleMonomorphism isBimoduleMonomorphism +open IsBimoduleMonomorphism M N isBimoduleMonomorphism private module M = RawBimodule M module N = RawBimodule N diff --git a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda index 3eaec2f788..105496accc 100644 --- a/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.BisemimoduleMonomorphism (isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M N ⟦_⟧) where -open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism +open IsBisemimoduleMonomorphism M N isBisemimoduleMonomorphism private module M = RawBisemimodule M module N = RawBisemimodule N diff --git a/src/Algebra/Module/Morphism/Construct/Composition.agda b/src/Algebra/Module/Morphism/Construct/Composition.agda index 6bee1497fa..1550933e31 100644 --- a/src/Algebra/Module/Morphism/Construct/Composition.agda +++ b/src/Algebra/Module/Morphism/Construct/Composition.agda @@ -39,7 +39,7 @@ module _ isLeftSemimoduleHomomorphism f-homo g-homo = record { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism ; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x)) - } where module F = IsLeftSemimoduleHomomorphism f-homo; module G = IsLeftSemimoduleHomomorphism g-homo + } where module F = IsLeftSemimoduleHomomorphism M₁ M₂ f-homo; module G = IsLeftSemimoduleHomomorphism M₂ M₃ g-homo isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ f → IsLeftSemimoduleMonomorphism M₂ M₃ g → @@ -47,7 +47,7 @@ module _ isLeftSemimoduleMonomorphism f-mono g-mono = record { isLeftSemimoduleHomomorphism = isLeftSemimoduleHomomorphism F.isLeftSemimoduleHomomorphism G.isLeftSemimoduleHomomorphism ; injective = F.injective ∘ G.injective - } where module F = IsLeftSemimoduleMonomorphism f-mono; module G = IsLeftSemimoduleMonomorphism g-mono + } where module F = IsLeftSemimoduleMonomorphism M₁ M₂ f-mono; module G = IsLeftSemimoduleMonomorphism M₂ M₃ g-mono isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism M₁ M₂ f → IsLeftSemimoduleIsomorphism M₂ M₃ g → @@ -55,7 +55,7 @@ module _ isLeftSemimoduleIsomorphism f-iso g-iso = record { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism F.isLeftSemimoduleMonomorphism G.isLeftSemimoduleMonomorphism ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective - } where module F = IsLeftSemimoduleIsomorphism f-iso; module G = IsLeftSemimoduleIsomorphism g-iso + } where module F = IsLeftSemimoduleIsomorphism M₁ M₂ f-iso; module G = IsLeftSemimoduleIsomorphism M₂ M₃ g-iso module _ {R : Set r} @@ -74,7 +74,7 @@ module _ isLeftModuleHomomorphism f-homo g-homo = record { +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism ; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x)) - } where module F = IsLeftModuleHomomorphism f-homo; module G = IsLeftModuleHomomorphism g-homo + } where module F = IsLeftModuleHomomorphism M₁ M₂ f-homo; module G = IsLeftModuleHomomorphism M₂ M₃ g-homo isLeftModuleMonomorphism : IsLeftModuleMonomorphism M₁ M₂ f → IsLeftModuleMonomorphism M₂ M₃ g → @@ -82,7 +82,7 @@ module _ isLeftModuleMonomorphism f-mono g-mono = record { isLeftModuleHomomorphism = isLeftModuleHomomorphism F.isLeftModuleHomomorphism G.isLeftModuleHomomorphism ; injective = F.injective ∘ G.injective - } where module F = IsLeftModuleMonomorphism f-mono; module G = IsLeftModuleMonomorphism g-mono + } where module F = IsLeftModuleMonomorphism M₁ M₂ f-mono; module G = IsLeftModuleMonomorphism M₂ M₃ g-mono isLeftModuleIsomorphism : IsLeftModuleIsomorphism M₁ M₂ f → IsLeftModuleIsomorphism M₂ M₃ g → @@ -90,7 +90,7 @@ module _ isLeftModuleIsomorphism f-iso g-iso = record { isLeftModuleMonomorphism = isLeftModuleMonomorphism F.isLeftModuleMonomorphism G.isLeftModuleMonomorphism ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective - } where module F = IsLeftModuleIsomorphism f-iso; module G = IsLeftModuleIsomorphism g-iso + } where module F = IsLeftModuleIsomorphism M₁ M₂ f-iso; module G = IsLeftModuleIsomorphism M₂ M₃ g-iso module _ {R : Set r} @@ -109,7 +109,7 @@ module _ isRightSemimoduleHomomorphism f-homo g-homo = record { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism ; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x)) - } where module F = IsRightSemimoduleHomomorphism f-homo; module G = IsRightSemimoduleHomomorphism g-homo + } where module F = IsRightSemimoduleHomomorphism M₁ M₂ f-homo; module G = IsRightSemimoduleHomomorphism M₂ M₃ g-homo isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism M₁ M₂ f → IsRightSemimoduleMonomorphism M₂ M₃ g → @@ -117,7 +117,7 @@ module _ isRightSemimoduleMonomorphism f-mono g-mono = record { isRightSemimoduleHomomorphism = isRightSemimoduleHomomorphism F.isRightSemimoduleHomomorphism G.isRightSemimoduleHomomorphism ; injective = F.injective ∘ G.injective - } where module F = IsRightSemimoduleMonomorphism f-mono; module G = IsRightSemimoduleMonomorphism g-mono + } where module F = IsRightSemimoduleMonomorphism M₁ M₂ f-mono; module G = IsRightSemimoduleMonomorphism M₂ M₃ g-mono isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism M₁ M₂ f → IsRightSemimoduleIsomorphism M₂ M₃ g → @@ -125,7 +125,7 @@ module _ isRightSemimoduleIsomorphism f-iso g-iso = record { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism F.isRightSemimoduleMonomorphism G.isRightSemimoduleMonomorphism ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective - } where module F = IsRightSemimoduleIsomorphism f-iso; module G = IsRightSemimoduleIsomorphism g-iso + } where module F = IsRightSemimoduleIsomorphism M₁ M₂ f-iso; module G = IsRightSemimoduleIsomorphism M₂ M₃ g-iso module _ {R : Set r} @@ -144,7 +144,7 @@ module _ isRightModuleHomomorphism f-homo g-homo = record { +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism ; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x)) - } where module F = IsRightModuleHomomorphism f-homo; module G = IsRightModuleHomomorphism g-homo + } where module F = IsRightModuleHomomorphism M₁ M₂ f-homo; module G = IsRightModuleHomomorphism M₂ M₃ g-homo isRightModuleMonomorphism : IsRightModuleMonomorphism M₁ M₂ f → IsRightModuleMonomorphism M₂ M₃ g → @@ -152,7 +152,7 @@ module _ isRightModuleMonomorphism f-mono g-mono = record { isRightModuleHomomorphism = isRightModuleHomomorphism F.isRightModuleHomomorphism G.isRightModuleHomomorphism ; injective = F.injective ∘ G.injective - } where module F = IsRightModuleMonomorphism f-mono; module G = IsRightModuleMonomorphism g-mono + } where module F = IsRightModuleMonomorphism M₁ M₂ f-mono; module G = IsRightModuleMonomorphism M₂ M₃ g-mono isRightModuleIsomorphism : IsRightModuleIsomorphism M₁ M₂ f → IsRightModuleIsomorphism M₂ M₃ g → @@ -160,7 +160,7 @@ module _ isRightModuleIsomorphism f-iso g-iso = record { isRightModuleMonomorphism = isRightModuleMonomorphism F.isRightModuleMonomorphism G.isRightModuleMonomorphism ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective - } where module F = IsRightModuleIsomorphism f-iso; module G = IsRightModuleIsomorphism g-iso + } where module F = IsRightModuleIsomorphism M₁ M₂ f-iso; module G = IsRightModuleIsomorphism M₂ M₃ g-iso module _ {R : Set r} @@ -181,7 +181,7 @@ module _ { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism ; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x)) ; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x)) - } where module F = IsBisemimoduleHomomorphism f-homo; module G = IsBisemimoduleHomomorphism g-homo + } where module F = IsBisemimoduleHomomorphism M₁ M₂ f-homo; module G = IsBisemimoduleHomomorphism M₂ M₃ g-homo isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M₁ M₂ f → IsBisemimoduleMonomorphism M₂ M₃ g → @@ -189,7 +189,7 @@ module _ isBisemimoduleMonomorphism f-mono g-mono = record { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism ; injective = F.injective ∘ G.injective - } where module F = IsBisemimoduleMonomorphism f-mono; module G = IsBisemimoduleMonomorphism g-mono + } where module F = IsBisemimoduleMonomorphism M₁ M₂ f-mono; module G = IsBisemimoduleMonomorphism M₂ M₃ g-mono isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism M₁ M₂ f → IsBisemimoduleIsomorphism M₂ M₃ g → @@ -197,7 +197,7 @@ module _ isBisemimoduleIsomorphism f-iso g-iso = record { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism F.isBisemimoduleMonomorphism G.isBisemimoduleMonomorphism ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective - } where module F = IsBisemimoduleIsomorphism f-iso; module G = IsBisemimoduleIsomorphism g-iso + } where module F = IsBisemimoduleIsomorphism M₁ M₂ f-iso; module G = IsBisemimoduleIsomorphism M₂ M₃ g-iso module _ {R : Set r} @@ -218,7 +218,7 @@ module _ { +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism ; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x)) ; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x)) - } where module F = IsBimoduleHomomorphism f-homo; module G = IsBimoduleHomomorphism g-homo + } where module F = IsBimoduleHomomorphism M₁ M₂ f-homo; module G = IsBimoduleHomomorphism M₂ M₃ g-homo isBimoduleMonomorphism : IsBimoduleMonomorphism M₁ M₂ f → IsBimoduleMonomorphism M₂ M₃ g → @@ -226,7 +226,7 @@ module _ isBimoduleMonomorphism f-mono g-mono = record { isBimoduleHomomorphism = isBimoduleHomomorphism F.isBimoduleHomomorphism G.isBimoduleHomomorphism ; injective = F.injective ∘ G.injective - } where module F = IsBimoduleMonomorphism f-mono; module G = IsBimoduleMonomorphism g-mono + } where module F = IsBimoduleMonomorphism M₁ M₂ f-mono; module G = IsBimoduleMonomorphism M₂ M₃ g-mono isBimoduleIsomorphism : IsBimoduleIsomorphism M₁ M₂ f → IsBimoduleIsomorphism M₂ M₃ g → @@ -234,7 +234,7 @@ module _ isBimoduleIsomorphism f-iso g-iso = record { isBimoduleMonomorphism = isBimoduleMonomorphism F.isBimoduleMonomorphism G.isBimoduleMonomorphism ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective - } where module F = IsBimoduleIsomorphism f-iso; module G = IsBimoduleIsomorphism g-iso + } where module F = IsBimoduleIsomorphism M₁ M₂ f-iso; module G = IsBimoduleIsomorphism M₂ M₃ g-iso module _ {R : Set r} @@ -252,7 +252,7 @@ module _ IsSemimoduleHomomorphism M₁ M₃ (g ∘ f) isSemimoduleHomomorphism f-homo g-homo = record { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism ≈ᴹ₃-trans F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism - } where module F = IsSemimoduleHomomorphism f-homo; module G = IsSemimoduleHomomorphism g-homo + } where module F = IsSemimoduleHomomorphism M₁ M₂ f-homo; module G = IsSemimoduleHomomorphism M₂ M₃ g-homo isSemimoduleMonomorphism : IsSemimoduleMonomorphism M₁ M₂ f → IsSemimoduleMonomorphism M₂ M₃ g → @@ -260,7 +260,7 @@ module _ isSemimoduleMonomorphism f-mono g-mono = record { isSemimoduleHomomorphism = isSemimoduleHomomorphism F.isSemimoduleHomomorphism G.isSemimoduleHomomorphism ; injective = F.injective ∘ G.injective - } where module F = IsSemimoduleMonomorphism f-mono; module G = IsSemimoduleMonomorphism g-mono + } where module F = IsSemimoduleMonomorphism M₁ M₂ f-mono; module G = IsSemimoduleMonomorphism M₂ M₃ g-mono isSemimoduleIsomorphism : IsSemimoduleIsomorphism M₁ M₂ f → IsSemimoduleIsomorphism M₂ M₃ g → @@ -268,7 +268,7 @@ module _ isSemimoduleIsomorphism f-iso g-iso = record { isSemimoduleMonomorphism = isSemimoduleMonomorphism F.isSemimoduleMonomorphism G.isSemimoduleMonomorphism ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective - } where module F = IsSemimoduleIsomorphism f-iso; module G = IsSemimoduleIsomorphism g-iso + } where module F = IsSemimoduleIsomorphism M₁ M₂ f-iso; module G = IsSemimoduleIsomorphism M₂ M₃ g-iso module _ {R : Set r} @@ -286,7 +286,7 @@ module _ IsModuleHomomorphism M₁ M₃ (g ∘ f) isModuleHomomorphism f-homo g-homo = record { isBimoduleHomomorphism = isBimoduleHomomorphism ≈ᴹ₃-trans F.isBimoduleHomomorphism G.isBimoduleHomomorphism - } where module F = IsModuleHomomorphism f-homo; module G = IsModuleHomomorphism g-homo + } where module F = IsModuleHomomorphism M₁ M₂ f-homo; module G = IsModuleHomomorphism M₂ M₃ g-homo isModuleMonomorphism : IsModuleMonomorphism M₁ M₂ f → IsModuleMonomorphism M₂ M₃ g → @@ -294,7 +294,7 @@ module _ isModuleMonomorphism f-mono g-mono = record { isModuleHomomorphism = isModuleHomomorphism F.isModuleHomomorphism G.isModuleHomomorphism ; injective = F.injective ∘ G.injective - } where module F = IsModuleMonomorphism f-mono; module G = IsModuleMonomorphism g-mono + } where module F = IsModuleMonomorphism M₁ M₂ f-mono; module G = IsModuleMonomorphism M₂ M₃ g-mono isModuleIsomorphism : IsModuleIsomorphism M₁ M₂ f → IsModuleIsomorphism M₂ M₃ g → @@ -302,4 +302,4 @@ module _ isModuleIsomorphism f-iso g-iso = record { isModuleMonomorphism = isModuleMonomorphism F.isModuleMonomorphism G.isModuleMonomorphism ; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective - } where module F = IsModuleIsomorphism f-iso; module G = IsModuleIsomorphism g-iso + } where module F = IsModuleIsomorphism M₁ M₂ f-iso; module G = IsModuleIsomorphism M₂ M₃ g-iso diff --git a/src/Algebra/Module/Morphism/Definitions.agda b/src/Algebra/Module/Morphism/Definitions.agda index 5ef3c53eee..98523b169b 100644 --- a/src/Algebra/Module/Morphism/Definitions.agda +++ b/src/Algebra/Module/Morphism/Definitions.agda @@ -9,7 +9,9 @@ open import Relation.Binary.Core using (Rel) module Algebra.Module.Morphism.Definitions - {r} (R : Set r) -- The underlying ring + {r} (R : Set r) -- The underlying ring of the domain + {s} (S : Set s) -- The underlying ring of the codomain + ([_] : R → S) -- The homomorphism between the underlying rings {a} (A : Set a) -- The domain of the morphism {b} (B : Set b) -- The codomain of the morphism {ℓ} (_≈_ : Rel B ℓ) -- The equality relation over the codomain @@ -18,8 +20,8 @@ module Algebra.Module.Morphism.Definitions open import Algebra.Module.Core using (Opₗ; Opᵣ) open import Algebra.Morphism.Definitions A B _≈_ public -Homomorphicₗ : (A → B) → Opₗ R A → Opₗ R B → Set _ -Homomorphicₗ ⟦_⟧ _∙_ _∘_ = ∀ r x → ⟦ r ∙ x ⟧ ≈ (r ∘ ⟦ x ⟧) +Homomorphicₗ : (A → B) → Opₗ R A → Opₗ S B → Set _ +Homomorphicₗ ⟦_⟧ _∙_ _∘_ = ∀ r x → ⟦ r ∙ x ⟧ ≈ ([ r ] ∘ ⟦ x ⟧) -Homomorphicᵣ : (A → B) → Opᵣ R A → Opᵣ R B → Set _ -Homomorphicᵣ ⟦_⟧ _∙_ _∘_ = ∀ r x → ⟦ x ∙ r ⟧ ≈ (⟦ x ⟧ ∘ r) +Homomorphicᵣ : (A → B) → Opᵣ R A → Opᵣ S B → Set _ +Homomorphicᵣ ⟦_⟧ _∙_ _∘_ = ∀ r x → ⟦ x ∙ r ⟧ ≈ (⟦ x ⟧ ∘ [ r ]) diff --git a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda index d1c6f9a848..c22b7f998b 100644 --- a/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.LeftModuleMonomorphism (isLeftModuleMonomorphism : IsLeftModuleMonomorphism M N ⟦_⟧) where -open IsLeftModuleMonomorphism isLeftModuleMonomorphism +open IsLeftModuleMonomorphism M N isLeftModuleMonomorphism private module M = RawLeftModule M module N = RawLeftModule N diff --git a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda index 8fa9f95e87..6a0eeffbca 100644 --- a/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.LeftSemimoduleMonomorphism (isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ ⟦_⟧) where -open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism +open IsLeftSemimoduleMonomorphism M₁ M₂ isLeftSemimoduleMonomorphism private module M = RawLeftSemimodule M₁ module N = RawLeftSemimodule M₂ diff --git a/src/Algebra/Module/Morphism/ModuleMonomorphism.agda b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda index 7bb629895a..719039aa4e 100644 --- a/src/Algebra/Module/Morphism/ModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/ModuleMonomorphism.agda @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.ModuleMonomorphism (isModuleMonomorphism : IsModuleMonomorphism M N ⟦_⟧) where -open IsModuleMonomorphism isModuleMonomorphism +open IsModuleMonomorphism M N isModuleMonomorphism private module M = RawModule M module N = RawModule N diff --git a/src/Algebra/Module/Morphism/Polymorphic/Structures.agda b/src/Algebra/Module/Morphism/Polymorphic/Structures.agda new file mode 100644 index 0000000000..0c021ca0a4 --- /dev/null +++ b/src/Algebra/Module/Morphism/Polymorphic/Structures.agda @@ -0,0 +1,621 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Morphisms between module-like algebraic structures over different ring structures +------------------------------------------------------------------------ +{-# OPTIONS --cubical-compatible --safe #-} + +module Algebra.Module.Morphism.Polymorphic.Structures where + +open import Algebra.Module.Bundles.Raw +import Algebra.Module.Morphism.Definitions as MorphismDefinitions +import Algebra.Morphism.Structures as MorphismStructures +open import Function.Definitions using (Injective; Surjective) +open import Level using (Level; _⊔_) + +private + variable + r s rl rr sl sr m₁ ℓm₁ m₂ ℓm₂ : Level + +module LeftSemimoduleMorphisms + {R : Set r} {S : Set s} + ([_] : R → S) + (M₁ : RawLeftSemimodule R m₁ ℓm₁) + (M₂ : RawLeftSemimodule S m₂ ℓm₂) + where + + open RawLeftSemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_) + open RawLeftSemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_) + open MorphismDefinitions R S [_] A B _≈ᴹ₂_ + open MorphismStructures.MonoidMorphisms (RawLeftSemimodule.+ᴹ-rawMonoid M₁) (RawLeftSemimodule.+ᴹ-rawMonoid M₂) + + record IsLeftSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + +ᴹ-isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ + *ₗ-homo : Homomorphicₗ ⟦_⟧ _*ₗ₁_ _*ₗ₂_ + + open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public + using (isRelHomomorphism; ⟦⟧-cong) + renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) + + record IsLeftSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsLeftSemimoduleHomomorphism isLeftSemimoduleHomomorphism public + + +ᴹ-isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧ + +ᴹ-isMonoidMonomorphism = record + { isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism + ; injective = injective + } + + open IsMonoidMonomorphism +ᴹ-isMonoidMonomorphism public + using (isRelMonomorphism) + renaming (isMagmaMonomorphism to +ᴹ-isMagmaMonomorphism) + + record IsLeftSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public + + +ᴹ-isMonoidIsomorphism : IsMonoidIsomorphism ⟦_⟧ + +ᴹ-isMonoidIsomorphism = record + { isMonoidMonomorphism = +ᴹ-isMonoidMonomorphism + ; surjective = surjective + } + + open IsMonoidIsomorphism +ᴹ-isMonoidIsomorphism public + using (isRelIsomorphism) + renaming (isMagmaIsomorphism to +ᴹ-isMagmaIsomorphism) + +module LeftModuleMorphisms + {R : Set r} {S : Set s} + ([_] : R → S) + (M₁ : RawLeftModule R m₁ ℓm₁) + (M₂ : RawLeftModule S m₂ ℓm₂) + where + + open RawLeftModule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_) + open RawLeftModule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_) + open MorphismDefinitions R S [_] A B _≈ᴹ₂_ + open MorphismStructures.GroupMorphisms (RawLeftModule.+ᴹ-rawGroup M₁) (RawLeftModule.+ᴹ-rawGroup M₂) + open LeftSemimoduleMorphisms [_] (RawLeftModule.rawLeftSemimodule M₁) (RawLeftModule.rawLeftSemimodule M₂) + + record IsLeftModuleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + +ᴹ-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧ + *ₗ-homo : Homomorphicₗ ⟦_⟧ _*ₗ₁_ _*ₗ₂_ + + open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public + using (isRelHomomorphism; ⟦⟧-cong) + renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism + ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo + ) + + isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧ + isLeftSemimoduleHomomorphism = record + { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism + ; *ₗ-homo = *ₗ-homo + } + + record IsLeftModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isLeftModuleHomomorphism : IsLeftModuleHomomorphism ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsLeftModuleHomomorphism isLeftModuleHomomorphism public + + isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism ⟦_⟧ + isLeftSemimoduleMonomorphism = record + { isLeftSemimoduleHomomorphism = isLeftSemimoduleHomomorphism + ; injective = injective + } + + open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public + using (isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism) + + +ᴹ-isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧ + +ᴹ-isGroupMonomorphism = record + { isGroupHomomorphism = +ᴹ-isGroupHomomorphism + ; injective = injective + } + + record IsLeftModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isLeftModuleMonomorphism : IsLeftModuleMonomorphism ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsLeftModuleMonomorphism isLeftModuleMonomorphism public + + isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism ⟦_⟧ + isLeftSemimoduleIsomorphism = record + { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism + ; surjective = surjective + } + + open IsLeftSemimoduleIsomorphism isLeftSemimoduleIsomorphism public + using (isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism) + + +ᴹ-isGroupIsomorphism : IsGroupIsomorphism ⟦_⟧ + +ᴹ-isGroupIsomorphism = record + { isGroupMonomorphism = +ᴹ-isGroupMonomorphism + ; surjective = surjective + } + +module RightSemimoduleMorphisms + {R : Set r} {S : Set s} + ([_] : R → S) + (M₁ : RawRightSemimodule R m₁ ℓm₁) + (M₂ : RawRightSemimodule S m₂ ℓm₂) + where + + open RawRightSemimodule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) + open RawRightSemimodule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) + open MorphismDefinitions R S [_] A B _≈ᴹ₂_ + open MorphismStructures.MonoidMorphisms (RawRightSemimodule.+ᴹ-rawMonoid M₁) (RawRightSemimodule.+ᴹ-rawMonoid M₂) + + record IsRightSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + +ᴹ-isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ + *ᵣ-homo : Homomorphicᵣ ⟦_⟧ _*ᵣ₁_ _*ᵣ₂_ + + open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public + using (isRelHomomorphism; ⟦⟧-cong) + renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) + + record IsRightSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsRightSemimoduleHomomorphism isRightSemimoduleHomomorphism public + + +ᴹ-isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧ + +ᴹ-isMonoidMonomorphism = record + { isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism + ; injective = injective + } + + open IsMonoidMonomorphism +ᴹ-isMonoidMonomorphism public + using (isRelMonomorphism) + renaming (isMagmaMonomorphism to +ᴹ-isMagmaMonomorphism) + + record IsRightSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism public + + +ᴹ-isMonoidIsomorphism : IsMonoidIsomorphism ⟦_⟧ + +ᴹ-isMonoidIsomorphism = record + { isMonoidMonomorphism = +ᴹ-isMonoidMonomorphism + ; surjective = surjective + } + + open IsMonoidIsomorphism +ᴹ-isMonoidIsomorphism public + using (isRelIsomorphism) + renaming (isMagmaIsomorphism to +ᴹ-isMagmaIsomorphism) + + +module RightModuleMorphisms + {R : Set r} {S : Set s} + ([_] : R → S) + (M₁ : RawRightModule R m₁ ℓm₁) + (M₂ : RawRightModule S m₂ ℓm₂) + where + + open RawRightModule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) + open RawRightModule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) + open MorphismDefinitions R S [_] A B _≈ᴹ₂_ + open MorphismStructures.GroupMorphisms (RawRightModule.+ᴹ-rawGroup M₁) (RawRightModule.+ᴹ-rawGroup M₂) + open RightSemimoduleMorphisms [_] (RawRightModule.rawRightSemimodule M₁) (RawRightModule.rawRightSemimodule M₂) + + record IsRightModuleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + +ᴹ-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧ + *ᵣ-homo : Homomorphicᵣ ⟦_⟧ _*ᵣ₁_ _*ᵣ₂_ + + open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public + using (isRelHomomorphism; ⟦⟧-cong) + renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism + ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo + ) + isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧ + isRightSemimoduleHomomorphism = record + { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism + ; *ᵣ-homo = *ᵣ-homo + } + + record IsRightModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isRightModuleHomomorphism : IsRightModuleHomomorphism ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsRightModuleHomomorphism isRightModuleHomomorphism public + + isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism ⟦_⟧ + isRightSemimoduleMonomorphism = record + { isRightSemimoduleHomomorphism = isRightSemimoduleHomomorphism + ; injective = injective + } + + open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism public + using (isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism) + + +ᴹ-isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧ + +ᴹ-isGroupMonomorphism = record + { isGroupHomomorphism = +ᴹ-isGroupHomomorphism + ; injective = injective + } + + record IsRightModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isRightModuleMonomorphism : IsRightModuleMonomorphism ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsRightModuleMonomorphism isRightModuleMonomorphism public + + isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism ⟦_⟧ + isRightSemimoduleIsomorphism = record + { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism + ; surjective = surjective + } + + open IsRightSemimoduleIsomorphism isRightSemimoduleIsomorphism public + using (isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism) + + +ᴹ-isGroupIsomorphism : IsGroupIsomorphism ⟦_⟧ + +ᴹ-isGroupIsomorphism = record + { isGroupMonomorphism = +ᴹ-isGroupMonomorphism + ; surjective = surjective + } + +module BisemimoduleMorphisms + {RL : Set rl} {SL : Set sl} ([_]ₗ : RL → SL) + {RR : Set rr} {SR : Set sr} ([_]ᵣ : RR → SR) + (M₁ : RawBisemimodule RL RR m₁ ℓm₁) + (M₂ : RawBisemimodule SL SR m₂ ℓm₂) + where + + open RawBisemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) + open RawBisemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) + open MorphismDefinitions RL SL [_]ₗ A B _≈ᴹ₂_ using (Homomorphicₗ) + open MorphismDefinitions RR SR [_]ᵣ A B _≈ᴹ₂_ using (Homomorphicᵣ) + open MorphismStructures.MonoidMorphisms (RawBisemimodule.+ᴹ-rawMonoid M₁) (RawBisemimodule.+ᴹ-rawMonoid M₂) + open LeftSemimoduleMorphisms [_]ₗ (RawBisemimodule.rawLeftSemimodule M₁) (RawBisemimodule.rawLeftSemimodule M₂) + open RightSemimoduleMorphisms [_]ᵣ (RawBisemimodule.rawRightSemimodule M₁) (RawBisemimodule.rawRightSemimodule M₂) + + record IsBisemimoduleHomomorphism (⟦_⟧ : A → B) : Set (rl ⊔ rr ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + +ᴹ-isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ + *ₗ-homo : Homomorphicₗ ⟦_⟧ _*ₗ₁_ _*ₗ₂_ + *ᵣ-homo : Homomorphicᵣ ⟦_⟧ _*ᵣ₁_ _*ᵣ₂_ + + isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧ + isLeftSemimoduleHomomorphism = record + { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism + ; *ₗ-homo = *ₗ-homo + } + + open IsLeftSemimoduleHomomorphism isLeftSemimoduleHomomorphism public + using (isRelHomomorphism; ⟦⟧-cong; +ᴹ-isMagmaHomomorphism; +ᴹ-homo; 0ᴹ-homo) + + isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧ + isRightSemimoduleHomomorphism = record + { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism + ; *ᵣ-homo = *ᵣ-homo + } + + record IsBisemimoduleMonomorphism (⟦_⟧ : A → B) : Set (rl ⊔ rr ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public + + isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism ⟦_⟧ + isLeftSemimoduleMonomorphism = record + { isLeftSemimoduleHomomorphism = isLeftSemimoduleHomomorphism + ; injective = injective + } + + open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public + using (isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism) + + isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism ⟦_⟧ + isRightSemimoduleMonomorphism = record + { isRightSemimoduleHomomorphism = isRightSemimoduleHomomorphism + ; injective = injective + } + + record IsBisemimoduleIsomorphism (⟦_⟧ : A → B) : Set (rl ⊔ rr ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism public + + isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism ⟦_⟧ + isLeftSemimoduleIsomorphism = record + { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism + ; surjective = surjective + } + + open IsLeftSemimoduleIsomorphism isLeftSemimoduleIsomorphism public + using (isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism) + + isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism ⟦_⟧ + isRightSemimoduleIsomorphism = record + { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism + ; surjective = surjective + } + +module BimoduleMorphisms + {RL : Set rl} {SL : Set sl} ([_]ₗ : RL → SL) + {RR : Set rr} {SR : Set sr} ([_]ᵣ : RR → SR) + (M₁ : RawBimodule RL RR m₁ ℓm₁) + (M₂ : RawBimodule SL SR m₂ ℓm₂) + where + + open RawBimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) + open RawBimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) + open MorphismDefinitions RL SL [_]ₗ A B _≈ᴹ₂_ using (Homomorphicₗ) + open MorphismDefinitions RR SR [_]ᵣ A B _≈ᴹ₂_ using (Homomorphicᵣ) + open MorphismStructures.GroupMorphisms (RawBimodule.+ᴹ-rawGroup M₁) (RawBimodule.+ᴹ-rawGroup M₂) + open LeftModuleMorphisms [_]ₗ (RawBimodule.rawLeftModule M₁) (RawBimodule.rawLeftModule M₂) + open RightModuleMorphisms [_]ᵣ (RawBimodule.rawRightModule M₁) (RawBimodule.rawRightModule M₂) + open BisemimoduleMorphisms [_]ₗ [_]ᵣ (RawBimodule.rawBisemimodule M₁) (RawBimodule.rawBisemimodule M₂) + + record IsBimoduleHomomorphism (⟦_⟧ : A → B) : Set (rl ⊔ rr ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + +ᴹ-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧ + *ₗ-homo : Homomorphicₗ ⟦_⟧ _*ₗ₁_ _*ₗ₂_ + *ᵣ-homo : Homomorphicᵣ ⟦_⟧ _*ᵣ₁_ _*ᵣ₂_ + + open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public + using (isRelHomomorphism; ⟦⟧-cong) + renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism + ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo + ) + + isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧ + isBisemimoduleHomomorphism = record + { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism + ; *ₗ-homo = *ₗ-homo + ; *ᵣ-homo = *ᵣ-homo + } + + open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public + using (isLeftSemimoduleHomomorphism; isRightSemimoduleHomomorphism) + + isLeftModuleHomomorphism : IsLeftModuleHomomorphism ⟦_⟧ + isLeftModuleHomomorphism = record + { +ᴹ-isGroupHomomorphism = +ᴹ-isGroupHomomorphism + ; *ₗ-homo = *ₗ-homo + } + + isRightModuleHomomorphism : IsRightModuleHomomorphism ⟦_⟧ + isRightModuleHomomorphism = record + { +ᴹ-isGroupHomomorphism = +ᴹ-isGroupHomomorphism + ; *ᵣ-homo = *ᵣ-homo + } + + record IsBimoduleMonomorphism (⟦_⟧ : A → B) : Set (rl ⊔ rr ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isBimoduleHomomorphism : IsBimoduleHomomorphism ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsBimoduleHomomorphism isBimoduleHomomorphism public + + +ᴹ-isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧ + +ᴹ-isGroupMonomorphism = record + { isGroupHomomorphism = +ᴹ-isGroupHomomorphism + ; injective = injective + } + + open IsGroupMonomorphism +ᴹ-isGroupMonomorphism public + using (isRelMonomorphism) + renaming (isMagmaMonomorphism to +ᴹ-isMagmaMonomorphism; isMonoidMonomorphism to +ᴹ-isMonoidMonomorphism) + + isLeftModuleMonomorphism : IsLeftModuleMonomorphism ⟦_⟧ + isLeftModuleMonomorphism = record + { isLeftModuleHomomorphism = isLeftModuleHomomorphism + ; injective = injective + } + + open IsLeftModuleMonomorphism isLeftModuleMonomorphism public + using (isLeftSemimoduleMonomorphism) + + isRightModuleMonomorphism : IsRightModuleMonomorphism ⟦_⟧ + isRightModuleMonomorphism = record + { isRightModuleHomomorphism = isRightModuleHomomorphism + ; injective = injective + } + + open IsRightModuleMonomorphism isRightModuleMonomorphism public + using (isRightSemimoduleMonomorphism) + + isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism ⟦_⟧ + isBisemimoduleMonomorphism = record + { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism + ; injective = injective + } + + record IsBimoduleIsomorphism (⟦_⟧ : A → B) : Set (rl ⊔ rr ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isBimoduleMonomorphism : IsBimoduleMonomorphism ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsBimoduleMonomorphism isBimoduleMonomorphism public + + +ᴹ-isGroupIsomorphism : IsGroupIsomorphism ⟦_⟧ + +ᴹ-isGroupIsomorphism = record + { isGroupMonomorphism = +ᴹ-isGroupMonomorphism + ; surjective = surjective + } + + open IsGroupIsomorphism +ᴹ-isGroupIsomorphism public + using (isRelIsomorphism) + renaming (isMagmaIsomorphism to +ᴹ-isMagmaIsomorphism; isMonoidIsomorphism to +ᴹ-isMonoidIsomorphism) + + isLeftModuleIsomorphism : IsLeftModuleIsomorphism ⟦_⟧ + isLeftModuleIsomorphism = record + { isLeftModuleMonomorphism = isLeftModuleMonomorphism + ; surjective = surjective + } + + open IsLeftModuleIsomorphism isLeftModuleIsomorphism public + using (isLeftSemimoduleIsomorphism) + + isRightModuleIsomorphism : IsRightModuleIsomorphism ⟦_⟧ + isRightModuleIsomorphism = record + { isRightModuleMonomorphism = isRightModuleMonomorphism + ; surjective = surjective + } + + open IsRightModuleIsomorphism isRightModuleIsomorphism public + using (isRightSemimoduleIsomorphism) + + isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism ⟦_⟧ + isBisemimoduleIsomorphism = record + { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism + ; surjective = surjective + } + +module SemimoduleMorphisms + {R : Set r} {S : Set s} ([_] : R → S) + (M₁ : RawSemimodule R m₁ ℓm₁) + (M₂ : RawSemimodule S m₂ ℓm₂) + where + + open RawSemimodule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_) + open RawSemimodule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_) + open BisemimoduleMorphisms [_] [_] (RawSemimodule.rawBisemimodule M₁) (RawSemimodule.rawBisemimodule M₂) + + record IsSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧ + + open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public + + record IsSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isSemimoduleHomomorphism : IsSemimoduleHomomorphism ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsSemimoduleHomomorphism isSemimoduleHomomorphism public + + isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism ⟦_⟧ + isBisemimoduleMonomorphism = record + { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism + ; injective = injective + } + + open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism public + using ( isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism + ; isLeftSemimoduleMonomorphism; isRightSemimoduleMonomorphism + ) + + record IsSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isSemimoduleMonomorphism : IsSemimoduleMonomorphism ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsSemimoduleMonomorphism isSemimoduleMonomorphism public + + isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism ⟦_⟧ + isBisemimoduleIsomorphism = record + { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism + ; surjective = surjective + } + + open IsBisemimoduleIsomorphism isBisemimoduleIsomorphism public + using ( isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism + ; isLeftSemimoduleIsomorphism; isRightSemimoduleIsomorphism + ) + +module ModuleMorphisms + {R : Set r} {S : Set s} ([_] : R → S) + (M₁ : RawModule R m₁ ℓm₁) + (M₂ : RawModule S m₂ ℓm₂) + where + + open RawModule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_) + open RawModule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_) + open BimoduleMorphisms [_] [_] (RawModule.rawBimodule M₁) (RawModule.rawBimodule M₂) + open SemimoduleMorphisms [_] (RawModule.rawBisemimodule M₁) (RawModule.rawBisemimodule M₂) + + record IsModuleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isBimoduleHomomorphism : IsBimoduleHomomorphism ⟦_⟧ + + open IsBimoduleHomomorphism isBimoduleHomomorphism public + + isSemimoduleHomomorphism : IsSemimoduleHomomorphism ⟦_⟧ + isSemimoduleHomomorphism = record + { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism + } + + record IsModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isModuleHomomorphism : IsModuleHomomorphism ⟦_⟧ + injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsModuleHomomorphism isModuleHomomorphism public + + isBimoduleMonomorphism : IsBimoduleMonomorphism ⟦_⟧ + isBimoduleMonomorphism = record + { isBimoduleHomomorphism = isBimoduleHomomorphism + ; injective = injective + } + + open IsBimoduleMonomorphism isBimoduleMonomorphism public + using ( isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism; +ᴹ-isGroupMonomorphism + ; isLeftSemimoduleMonomorphism; isRightSemimoduleMonomorphism; isBisemimoduleMonomorphism + ; isLeftModuleMonomorphism; isRightModuleMonomorphism + ) + + isSemimoduleMonomorphism : IsSemimoduleMonomorphism ⟦_⟧ + isSemimoduleMonomorphism = record + { isSemimoduleHomomorphism = isSemimoduleHomomorphism + ; injective = injective + } + + record IsModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where + field + isModuleMonomorphism : IsModuleMonomorphism ⟦_⟧ + surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ + + open IsModuleMonomorphism isModuleMonomorphism public + + isBimoduleIsomorphism : IsBimoduleIsomorphism ⟦_⟧ + isBimoduleIsomorphism = record + { isBimoduleMonomorphism = isBimoduleMonomorphism + ; surjective = surjective + } + + open IsBimoduleIsomorphism isBimoduleIsomorphism public + using ( isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism; +ᴹ-isGroupIsomorphism + ; isLeftSemimoduleIsomorphism; isRightSemimoduleIsomorphism; isBisemimoduleIsomorphism + ; isLeftModuleIsomorphism; isRightModuleIsomorphism + ) + + isSemimoduleIsomorphism : IsSemimoduleIsomorphism ⟦_⟧ + isSemimoduleIsomorphism = record + { isSemimoduleMonomorphism = isSemimoduleMonomorphism + ; surjective = surjective + } + +open LeftSemimoduleMorphisms public +open LeftModuleMorphisms public +open RightSemimoduleMorphisms public +open RightModuleMorphisms public +open BisemimoduleMorphisms public +open BimoduleMorphisms public +open SemimoduleMorphisms public +open ModuleMorphisms public diff --git a/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda index 555b918815..392f50b3b2 100644 --- a/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/RightModuleMonomorphism.agda @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.RightModuleMonomorphism (isRightModuleMonomorphism : IsRightModuleMonomorphism M N ⟦_⟧) where -open IsRightModuleMonomorphism isRightModuleMonomorphism +open IsRightModuleMonomorphism M N isRightModuleMonomorphism module M = RawRightModule M module N = RawRightModule N diff --git a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda index b77f0aed02..620ef9794d 100644 --- a/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.RightSemimoduleMonomorphism (isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism M N ⟦_⟧) where -open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism +open IsRightSemimoduleMonomorphism M N isRightSemimoduleMonomorphism private module M = RawRightSemimodule M module N = RawRightSemimodule N diff --git a/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda index 378cf164d2..6304ffeef7 100644 --- a/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda +++ b/src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda @@ -14,7 +14,7 @@ module Algebra.Module.Morphism.SemimoduleMonomorphism (isSemimoduleMonomorphism : IsSemimoduleMonomorphism M N ⟦_⟧) where -open IsSemimoduleMonomorphism isSemimoduleMonomorphism +open IsSemimoduleMonomorphism M N isSemimoduleMonomorphism private module M = RawSemimodule M module N = RawSemimodule N diff --git a/src/Algebra/Module/Morphism/Structures.agda b/src/Algebra/Module/Morphism/Structures.agda index 3ef580ebea..5d36410bb8 100644 --- a/src/Algebra/Module/Morphism/Structures.agda +++ b/src/Algebra/Module/Morphism/Structures.agda @@ -8,603 +8,32 @@ module Algebra.Module.Morphism.Structures where open import Algebra.Module.Bundles.Raw -import Algebra.Module.Morphism.Definitions as MorphismDefinitions -import Algebra.Morphism.Structures as MorphismStructures -open import Function.Definitions using (Injective; Surjective) -open import Level using (Level; _⊔_) +import Algebra.Module.Morphism.Polymorphic.Structures as Polymorphic +open import Function.Base using (id) -private - variable - r s m₁ m₂ ℓm₁ ℓm₂ : Level +module LeftSemimoduleMorphisms {r} {m₁} {ℓm₁} {m₂} {ℓm₂} {R : Set r} (M₁ : RawLeftSemimodule R m₁ ℓm₁) (M₂ : RawLeftSemimodule R m₂ ℓm₂) + = Polymorphic.LeftSemimoduleMorphisms {m₁ = m₁} {ℓm₁ = ℓm₁} {m₂ = m₂} {ℓm₂ = ℓm₂} (id {A = R}) M₁ M₂ -module LeftSemimoduleMorphisms - {R : Set r} - (M₁ : RawLeftSemimodule R m₁ ℓm₁) - (M₂ : RawLeftSemimodule R m₂ ℓm₂) - where +module LeftModuleMorphisms {r} {m₁} {ℓm₁} {m₂} {ℓm₂} {R : Set r} + = Polymorphic.LeftModuleMorphisms {m₁ = m₁} {ℓm₁ = ℓm₁} {m₂ = m₂} {ℓm₂ = ℓm₂} (id {A = R}) - open RawLeftSemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_) - open RawLeftSemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_) - open MorphismDefinitions R A B _≈ᴹ₂_ - open MorphismStructures.MonoidMorphisms (RawLeftSemimodule.+ᴹ-rawMonoid M₁) (RawLeftSemimodule.+ᴹ-rawMonoid M₂) +module RightSemimoduleMorphisms {r} {m₁} {ℓm₁} {m₂} {ℓm₂} {R : Set r} + = Polymorphic.RightSemimoduleMorphisms {m₁ = m₁} {ℓm₁ = ℓm₁} {m₂ = m₂} {ℓm₂ = ℓm₂} (id {A = R}) - record IsLeftSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - +ᴹ-isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ - *ₗ-homo : Homomorphicₗ ⟦_⟧ _*ₗ₁_ _*ₗ₂_ +module RightModuleMorphisms {r} {m₁} {ℓm₁} {m₂} {ℓm₂} {R : Set r} + = Polymorphic.RightModuleMorphisms {m₁ = m₁} {ℓm₁ = ℓm₁} {m₂ = m₂} {ℓm₂ = ℓm₂} (id {A = R}) - open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public - using (isRelHomomorphism; ⟦⟧-cong) - renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) +module BisemimoduleMorphisms {r} {s} {m₁} {ℓm₁} {m₂} {ℓm₂} {R : Set r} {S : Set s} + = Polymorphic.BisemimoduleMorphisms {m₁ = m₁} {ℓm₁ = ℓm₁} {m₂ = m₂} {ℓm₂ = ℓm₂} (id {A = R}) (id {A = S}) - record IsLeftSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧ - injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ +module BimoduleMorphisms {r} {s} {m₁} {ℓm₁} {m₂} {ℓm₂} {R : Set r} {S : Set s} + = Polymorphic.BimoduleMorphisms {m₁ = m₁} {ℓm₁ = ℓm₁} {m₂ = m₂} {ℓm₂ = ℓm₂} (id {A = R}) (id {A = S}) - open IsLeftSemimoduleHomomorphism isLeftSemimoduleHomomorphism public +module SemimoduleMorphisms {r} {m₁} {ℓm₁} {m₂} {ℓm₂} {R : Set r} + = Polymorphic.SemimoduleMorphisms {m₁ = m₁} {ℓm₁ = ℓm₁} {m₂ = m₂} {ℓm₂ = ℓm₂} (id {A = R}) - +ᴹ-isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧ - +ᴹ-isMonoidMonomorphism = record - { isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism - ; injective = injective - } - - open IsMonoidMonomorphism +ᴹ-isMonoidMonomorphism public - using (isRelMonomorphism) - renaming (isMagmaMonomorphism to +ᴹ-isMagmaMonomorphism) - - record IsLeftSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism ⟦_⟧ - surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public - - +ᴹ-isMonoidIsomorphism : IsMonoidIsomorphism ⟦_⟧ - +ᴹ-isMonoidIsomorphism = record - { isMonoidMonomorphism = +ᴹ-isMonoidMonomorphism - ; surjective = surjective - } - - open IsMonoidIsomorphism +ᴹ-isMonoidIsomorphism public - using (isRelIsomorphism) - renaming (isMagmaIsomorphism to +ᴹ-isMagmaIsomorphism) - -module LeftModuleMorphisms - {R : Set r} - (M₁ : RawLeftModule R m₁ ℓm₁) - (M₂ : RawLeftModule R m₂ ℓm₂) - where - - open RawLeftModule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _≈ᴹ_ to _≈ᴹ₁_) - open RawLeftModule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _≈ᴹ_ to _≈ᴹ₂_) - open MorphismDefinitions R A B _≈ᴹ₂_ - open MorphismStructures.GroupMorphisms (RawLeftModule.+ᴹ-rawGroup M₁) (RawLeftModule.+ᴹ-rawGroup M₂) - open LeftSemimoduleMorphisms (RawLeftModule.rawLeftSemimodule M₁) (RawLeftModule.rawLeftSemimodule M₂) - - record IsLeftModuleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - +ᴹ-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧ - *ₗ-homo : Homomorphicₗ ⟦_⟧ _*ₗ₁_ _*ₗ₂_ - - open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public - using (isRelHomomorphism; ⟦⟧-cong) - renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism - ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo - ) - - isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧ - isLeftSemimoduleHomomorphism = record - { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism - ; *ₗ-homo = *ₗ-homo - } - - record IsLeftModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isLeftModuleHomomorphism : IsLeftModuleHomomorphism ⟦_⟧ - injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsLeftModuleHomomorphism isLeftModuleHomomorphism public - - isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism ⟦_⟧ - isLeftSemimoduleMonomorphism = record - { isLeftSemimoduleHomomorphism = isLeftSemimoduleHomomorphism - ; injective = injective - } - - open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public - using (isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism) - - +ᴹ-isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧ - +ᴹ-isGroupMonomorphism = record - { isGroupHomomorphism = +ᴹ-isGroupHomomorphism - ; injective = injective - } - - record IsLeftModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isLeftModuleMonomorphism : IsLeftModuleMonomorphism ⟦_⟧ - surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsLeftModuleMonomorphism isLeftModuleMonomorphism public - - isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism ⟦_⟧ - isLeftSemimoduleIsomorphism = record - { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism - ; surjective = surjective - } - - open IsLeftSemimoduleIsomorphism isLeftSemimoduleIsomorphism public - using (isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism) - - +ᴹ-isGroupIsomorphism : IsGroupIsomorphism ⟦_⟧ - +ᴹ-isGroupIsomorphism = record - { isGroupMonomorphism = +ᴹ-isGroupMonomorphism - ; surjective = surjective - } - -module RightSemimoduleMorphisms - {R : Set r} - (M₁ : RawRightSemimodule R m₁ ℓm₁) - (M₂ : RawRightSemimodule R m₂ ℓm₂) - where - - open RawRightSemimodule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) - open RawRightSemimodule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) - open MorphismDefinitions R A B _≈ᴹ₂_ - open MorphismStructures.MonoidMorphisms (RawRightSemimodule.+ᴹ-rawMonoid M₁) (RawRightSemimodule.+ᴹ-rawMonoid M₂) - - record IsRightSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - +ᴹ-isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ - *ᵣ-homo : Homomorphicᵣ ⟦_⟧ _*ᵣ₁_ _*ᵣ₂_ - - open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public - using (isRelHomomorphism; ⟦⟧-cong) - renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo) - - record IsRightSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧ - injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsRightSemimoduleHomomorphism isRightSemimoduleHomomorphism public - - +ᴹ-isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧ - +ᴹ-isMonoidMonomorphism = record - { isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism - ; injective = injective - } - - open IsMonoidMonomorphism +ᴹ-isMonoidMonomorphism public - using (isRelMonomorphism) - renaming (isMagmaMonomorphism to +ᴹ-isMagmaMonomorphism) - - record IsRightSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism ⟦_⟧ - surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism public - - +ᴹ-isMonoidIsomorphism : IsMonoidIsomorphism ⟦_⟧ - +ᴹ-isMonoidIsomorphism = record - { isMonoidMonomorphism = +ᴹ-isMonoidMonomorphism - ; surjective = surjective - } - - open IsMonoidIsomorphism +ᴹ-isMonoidIsomorphism public - using (isRelIsomorphism) - renaming (isMagmaIsomorphism to +ᴹ-isMagmaIsomorphism) - -module RightModuleMorphisms - {R : Set r} - (M₁ : RawRightModule R m₁ ℓm₁) - (M₂ : RawRightModule R m₂ ℓm₂) - where - - open RawRightModule M₁ renaming (Carrierᴹ to A; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) - open RawRightModule M₂ renaming (Carrierᴹ to B; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) - open MorphismDefinitions R A B _≈ᴹ₂_ - open MorphismStructures.GroupMorphisms (RawRightModule.+ᴹ-rawGroup M₁) (RawRightModule.+ᴹ-rawGroup M₂) - open RightSemimoduleMorphisms (RawRightModule.rawRightSemimodule M₁) (RawRightModule.rawRightSemimodule M₂) - - record IsRightModuleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - +ᴹ-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧ - *ᵣ-homo : Homomorphicᵣ ⟦_⟧ _*ᵣ₁_ _*ᵣ₂_ - - open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public - using (isRelHomomorphism; ⟦⟧-cong) - renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism - ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo - ) - isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧ - isRightSemimoduleHomomorphism = record - { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism - ; *ᵣ-homo = *ᵣ-homo - } - - record IsRightModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isRightModuleHomomorphism : IsRightModuleHomomorphism ⟦_⟧ - injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsRightModuleHomomorphism isRightModuleHomomorphism public - - isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism ⟦_⟧ - isRightSemimoduleMonomorphism = record - { isRightSemimoduleHomomorphism = isRightSemimoduleHomomorphism - ; injective = injective - } - - open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism public - using (isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism) - - +ᴹ-isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧ - +ᴹ-isGroupMonomorphism = record - { isGroupHomomorphism = +ᴹ-isGroupHomomorphism - ; injective = injective - } - - record IsRightModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isRightModuleMonomorphism : IsRightModuleMonomorphism ⟦_⟧ - surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsRightModuleMonomorphism isRightModuleMonomorphism public - - isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism ⟦_⟧ - isRightSemimoduleIsomorphism = record - { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism - ; surjective = surjective - } - - open IsRightSemimoduleIsomorphism isRightSemimoduleIsomorphism public - using (isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism) - - +ᴹ-isGroupIsomorphism : IsGroupIsomorphism ⟦_⟧ - +ᴹ-isGroupIsomorphism = record - { isGroupMonomorphism = +ᴹ-isGroupMonomorphism - ; surjective = surjective - } - -module BisemimoduleMorphisms - {R : Set r} - {S : Set s} - (M₁ : RawBisemimodule R S m₁ ℓm₁) - (M₂ : RawBisemimodule R S m₂ ℓm₂) - where - - open RawBisemimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) - open RawBisemimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) - open MorphismDefinitions R A B _≈ᴹ₂_ using (Homomorphicₗ) - open MorphismDefinitions S A B _≈ᴹ₂_ using (Homomorphicᵣ) - open MorphismStructures.MonoidMorphisms (RawBisemimodule.+ᴹ-rawMonoid M₁) (RawBisemimodule.+ᴹ-rawMonoid M₂) - open LeftSemimoduleMorphisms (RawBisemimodule.rawLeftSemimodule M₁) (RawBisemimodule.rawLeftSemimodule M₂) - open RightSemimoduleMorphisms (RawBisemimodule.rawRightSemimodule M₁) (RawBisemimodule.rawRightSemimodule M₂) - - record IsBisemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - +ᴹ-isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ - *ₗ-homo : Homomorphicₗ ⟦_⟧ _*ₗ₁_ _*ₗ₂_ - *ᵣ-homo : Homomorphicᵣ ⟦_⟧ _*ᵣ₁_ _*ᵣ₂_ - - isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧ - isLeftSemimoduleHomomorphism = record - { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism - ; *ₗ-homo = *ₗ-homo - } - - open IsLeftSemimoduleHomomorphism isLeftSemimoduleHomomorphism public - using (isRelHomomorphism; ⟦⟧-cong; +ᴹ-isMagmaHomomorphism; +ᴹ-homo; 0ᴹ-homo) - - isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧ - isRightSemimoduleHomomorphism = record - { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism - ; *ᵣ-homo = *ᵣ-homo - } - - record IsBisemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧ - injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public - - isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism ⟦_⟧ - isLeftSemimoduleMonomorphism = record - { isLeftSemimoduleHomomorphism = isLeftSemimoduleHomomorphism - ; injective = injective - } - - open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public - using (isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism) - - isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism ⟦_⟧ - isRightSemimoduleMonomorphism = record - { isRightSemimoduleHomomorphism = isRightSemimoduleHomomorphism - ; injective = injective - } - - record IsBisemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism ⟦_⟧ - surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism public - - isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism ⟦_⟧ - isLeftSemimoduleIsomorphism = record - { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism - ; surjective = surjective - } - - open IsLeftSemimoduleIsomorphism isLeftSemimoduleIsomorphism public - using (isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism) - - isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism ⟦_⟧ - isRightSemimoduleIsomorphism = record - { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism - ; surjective = surjective - } - -module BimoduleMorphisms - {R : Set r} - {S : Set s} - (M₁ : RawBimodule R S m₁ ℓm₁) - (M₂ : RawBimodule R S m₂ ℓm₂) - where - - open RawBimodule M₁ renaming (Carrierᴹ to A; _*ₗ_ to _*ₗ₁_; _*ᵣ_ to _*ᵣ₁_; _≈ᴹ_ to _≈ᴹ₁_) - open RawBimodule M₂ renaming (Carrierᴹ to B; _*ₗ_ to _*ₗ₂_; _*ᵣ_ to _*ᵣ₂_; _≈ᴹ_ to _≈ᴹ₂_) - open MorphismDefinitions R A B _≈ᴹ₂_ using (Homomorphicₗ) - open MorphismDefinitions S A B _≈ᴹ₂_ using (Homomorphicᵣ) - open MorphismStructures.GroupMorphisms (RawBimodule.+ᴹ-rawGroup M₁) (RawBimodule.+ᴹ-rawGroup M₂) - open LeftModuleMorphisms (RawBimodule.rawLeftModule M₁) (RawBimodule.rawLeftModule M₂) - open RightModuleMorphisms (RawBimodule.rawRightModule M₁) (RawBimodule.rawRightModule M₂) - open BisemimoduleMorphisms (RawBimodule.rawBisemimodule M₁) (RawBimodule.rawBisemimodule M₂) - - record IsBimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - +ᴹ-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧ - *ₗ-homo : Homomorphicₗ ⟦_⟧ _*ₗ₁_ _*ₗ₂_ - *ᵣ-homo : Homomorphicᵣ ⟦_⟧ _*ᵣ₁_ _*ᵣ₂_ - - open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public - using (isRelHomomorphism; ⟦⟧-cong) - renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism - ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo - ) - - isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧ - isBisemimoduleHomomorphism = record - { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism - ; *ₗ-homo = *ₗ-homo - ; *ᵣ-homo = *ᵣ-homo - } - - open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public - using (isLeftSemimoduleHomomorphism; isRightSemimoduleHomomorphism) - - isLeftModuleHomomorphism : IsLeftModuleHomomorphism ⟦_⟧ - isLeftModuleHomomorphism = record - { +ᴹ-isGroupHomomorphism = +ᴹ-isGroupHomomorphism - ; *ₗ-homo = *ₗ-homo - } - - isRightModuleHomomorphism : IsRightModuleHomomorphism ⟦_⟧ - isRightModuleHomomorphism = record - { +ᴹ-isGroupHomomorphism = +ᴹ-isGroupHomomorphism - ; *ᵣ-homo = *ᵣ-homo - } - - record IsBimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isBimoduleHomomorphism : IsBimoduleHomomorphism ⟦_⟧ - injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsBimoduleHomomorphism isBimoduleHomomorphism public - - +ᴹ-isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧ - +ᴹ-isGroupMonomorphism = record - { isGroupHomomorphism = +ᴹ-isGroupHomomorphism - ; injective = injective - } - - open IsGroupMonomorphism +ᴹ-isGroupMonomorphism public - using (isRelMonomorphism) - renaming (isMagmaMonomorphism to +ᴹ-isMagmaMonomorphism; isMonoidMonomorphism to +ᴹ-isMonoidMonomorphism) - - isLeftModuleMonomorphism : IsLeftModuleMonomorphism ⟦_⟧ - isLeftModuleMonomorphism = record - { isLeftModuleHomomorphism = isLeftModuleHomomorphism - ; injective = injective - } - - open IsLeftModuleMonomorphism isLeftModuleMonomorphism public - using (isLeftSemimoduleMonomorphism) - - isRightModuleMonomorphism : IsRightModuleMonomorphism ⟦_⟧ - isRightModuleMonomorphism = record - { isRightModuleHomomorphism = isRightModuleHomomorphism - ; injective = injective - } - - open IsRightModuleMonomorphism isRightModuleMonomorphism public - using (isRightSemimoduleMonomorphism) - - isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism ⟦_⟧ - isBisemimoduleMonomorphism = record - { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism - ; injective = injective - } - - record IsBimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ s ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isBimoduleMonomorphism : IsBimoduleMonomorphism ⟦_⟧ - surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsBimoduleMonomorphism isBimoduleMonomorphism public - - +ᴹ-isGroupIsomorphism : IsGroupIsomorphism ⟦_⟧ - +ᴹ-isGroupIsomorphism = record - { isGroupMonomorphism = +ᴹ-isGroupMonomorphism - ; surjective = surjective - } - - open IsGroupIsomorphism +ᴹ-isGroupIsomorphism public - using (isRelIsomorphism) - renaming (isMagmaIsomorphism to +ᴹ-isMagmaIsomorphism; isMonoidIsomorphism to +ᴹ-isMonoidIsomorphism) - - isLeftModuleIsomorphism : IsLeftModuleIsomorphism ⟦_⟧ - isLeftModuleIsomorphism = record - { isLeftModuleMonomorphism = isLeftModuleMonomorphism - ; surjective = surjective - } - - open IsLeftModuleIsomorphism isLeftModuleIsomorphism public - using (isLeftSemimoduleIsomorphism) - - isRightModuleIsomorphism : IsRightModuleIsomorphism ⟦_⟧ - isRightModuleIsomorphism = record - { isRightModuleMonomorphism = isRightModuleMonomorphism - ; surjective = surjective - } - - open IsRightModuleIsomorphism isRightModuleIsomorphism public - using (isRightSemimoduleIsomorphism) - - isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism ⟦_⟧ - isBisemimoduleIsomorphism = record - { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism - ; surjective = surjective - } - -module SemimoduleMorphisms - {R : Set r} - (M₁ : RawSemimodule R m₁ ℓm₁) - (M₂ : RawSemimodule R m₂ ℓm₂) - where - - open RawSemimodule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_) - open RawSemimodule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_) - open BisemimoduleMorphisms (RawSemimodule.rawBisemimodule M₁) (RawSemimodule.rawBisemimodule M₂) - - record IsSemimoduleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧ - - open IsBisemimoduleHomomorphism isBisemimoduleHomomorphism public - - record IsSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isSemimoduleHomomorphism : IsSemimoduleHomomorphism ⟦_⟧ - injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsSemimoduleHomomorphism isSemimoduleHomomorphism public - - isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism ⟦_⟧ - isBisemimoduleMonomorphism = record - { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism - ; injective = injective - } - - open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism public - using ( isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism - ; isLeftSemimoduleMonomorphism; isRightSemimoduleMonomorphism - ) - - record IsSemimoduleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isSemimoduleMonomorphism : IsSemimoduleMonomorphism ⟦_⟧ - surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsSemimoduleMonomorphism isSemimoduleMonomorphism public - - isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism ⟦_⟧ - isBisemimoduleIsomorphism = record - { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism - ; surjective = surjective - } - - open IsBisemimoduleIsomorphism isBisemimoduleIsomorphism public - using ( isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism - ; isLeftSemimoduleIsomorphism; isRightSemimoduleIsomorphism - ) - -module ModuleMorphisms - {R : Set r} - (M₁ : RawModule R m₁ ℓm₁) - (M₂ : RawModule R m₂ ℓm₂) - where - - open RawModule M₁ renaming (Carrierᴹ to A; _≈ᴹ_ to _≈ᴹ₁_) - open RawModule M₂ renaming (Carrierᴹ to B; _≈ᴹ_ to _≈ᴹ₂_) - open BimoduleMorphisms (RawModule.rawBimodule M₁) (RawModule.rawBimodule M₂) - open SemimoduleMorphisms (RawModule.rawBisemimodule M₁) (RawModule.rawBisemimodule M₂) - - record IsModuleHomomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isBimoduleHomomorphism : IsBimoduleHomomorphism ⟦_⟧ - - open IsBimoduleHomomorphism isBimoduleHomomorphism public - - isSemimoduleHomomorphism : IsSemimoduleHomomorphism ⟦_⟧ - isSemimoduleHomomorphism = record - { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism - } - - record IsModuleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isModuleHomomorphism : IsModuleHomomorphism ⟦_⟧ - injective : Injective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsModuleHomomorphism isModuleHomomorphism public - - isBimoduleMonomorphism : IsBimoduleMonomorphism ⟦_⟧ - isBimoduleMonomorphism = record - { isBimoduleHomomorphism = isBimoduleHomomorphism - ; injective = injective - } - - open IsBimoduleMonomorphism isBimoduleMonomorphism public - using ( isRelMonomorphism; +ᴹ-isMagmaMonomorphism; +ᴹ-isMonoidMonomorphism; +ᴹ-isGroupMonomorphism - ; isLeftSemimoduleMonomorphism; isRightSemimoduleMonomorphism; isBisemimoduleMonomorphism - ; isLeftModuleMonomorphism; isRightModuleMonomorphism - ) - - isSemimoduleMonomorphism : IsSemimoduleMonomorphism ⟦_⟧ - isSemimoduleMonomorphism = record - { isSemimoduleHomomorphism = isSemimoduleHomomorphism - ; injective = injective - } - - record IsModuleIsomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ m₂ ⊔ ℓm₁ ⊔ ℓm₂) where - field - isModuleMonomorphism : IsModuleMonomorphism ⟦_⟧ - surjective : Surjective _≈ᴹ₁_ _≈ᴹ₂_ ⟦_⟧ - - open IsModuleMonomorphism isModuleMonomorphism public - - isBimoduleIsomorphism : IsBimoduleIsomorphism ⟦_⟧ - isBimoduleIsomorphism = record - { isBimoduleMonomorphism = isBimoduleMonomorphism - ; surjective = surjective - } - - open IsBimoduleIsomorphism isBimoduleIsomorphism public - using ( isRelIsomorphism; +ᴹ-isMagmaIsomorphism; +ᴹ-isMonoidIsomorphism; +ᴹ-isGroupIsomorphism - ; isLeftSemimoduleIsomorphism; isRightSemimoduleIsomorphism; isBisemimoduleIsomorphism - ; isLeftModuleIsomorphism; isRightModuleIsomorphism - ) - - isSemimoduleIsomorphism : IsSemimoduleIsomorphism ⟦_⟧ - isSemimoduleIsomorphism = record - { isSemimoduleMonomorphism = isSemimoduleMonomorphism - ; surjective = surjective - } +module ModuleMorphisms {r} {m₁} {ℓm₁} {m₂} {ℓm₂} {R : Set r} + = Polymorphic.ModuleMorphisms {m₁ = m₁} {ℓm₁ = ℓm₁} {m₂ = m₂} {ℓm₂ = ℓm₂} (id {A = R}) open LeftSemimoduleMorphisms public open LeftModuleMorphisms public diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 0084b33d90..7d82d46a7f 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -215,6 +215,7 @@ module _ (ring : Ring r ℓr) ; inverseʳ to -ᴹ‿inverseʳ ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ + ; _-_ to _-ᴹ_ ) {-# WARNING_ON_USAGE uniqueˡ‿-ᴹ "Warning: uniqueˡ‿-ᴹ was deprecated in v2.3. @@ -252,6 +253,7 @@ module _ (ring : Ring r ℓr) ; inverseʳ to -ᴹ‿inverseʳ ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ + ; _-_ to _-ᴹ_ ) {-# WARNING_ON_USAGE uniqueˡ‿-ᴹ "Warning: uniqueˡ‿-ᴹ was deprecated in v2.3. @@ -289,9 +291,9 @@ module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) open IsLeftModule isLeftModule public using ( +ᴹ-isAbelianGroup; +ᴹ-isGroup; -ᴹ‿inverseˡ; -ᴹ‿inverseʳ - ; uniqueˡ‿-ᴹ; uniqueʳ‿-ᴹ) + ; uniqueˡ‿-ᴹ; uniqueʳ‿-ᴹ; _-ᴹ_) - isRightModule : IsRightModule S-ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ᵣ + isRightModule : IsRightModule S-ring ≈ᴹ +ᴹ 0ᴹ (-ᴹ) *ᵣ isRightModule = record { isRightSemimodule = isRightSemimodule ; -ᴹ‿cong = -ᴹ‿cong diff --git a/src/Algebra/Module/Structures/Biased.agda b/src/Algebra/Module/Structures/Biased.agda index 9459874f0f..08d6e28f79 100644 --- a/src/Algebra/Module/Structures/Biased.agda +++ b/src/Algebra/Module/Structures/Biased.agda @@ -113,7 +113,7 @@ module _ (commutativeRing : CommutativeRing r ℓr) where open IsLeftModule isLeftModule - isModule : IsModule commutativeRing ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ (flip *ₗ) + isModule : IsModule commutativeRing ≈ᴹ +ᴹ 0ᴹ (-ᴹ) *ₗ (flip *ₗ) isModule = record { isBimodule = record { isBisemimodule = IsSemimoduleFromLeft.isBisemimodule @@ -135,7 +135,7 @@ module _ (commutativeRing : CommutativeRing r ℓr) where open IsRightModule isRightModule - isModule : IsModule commutativeRing ≈ᴹ +ᴹ 0ᴹ -ᴹ (flip *ᵣ) *ᵣ + isModule : IsModule commutativeRing ≈ᴹ +ᴹ 0ᴹ (-ᴹ) (flip *ᵣ) *ᵣ isModule = record { isBimodule = record { isBisemimodule = IsSemimoduleFromRight.isBisemimodule