Proofs of some linearity axioms.

CHANGELOG.md

@@ -833,7 +833,8 @@ New modules
   Algebra.Module.Morphism.Construct.Composition
   Algebra.Module.Morphism.Construct.Identity
   Algebra.Module.Morphism.Definitions
-  Algebra.Module.Morphism.Structures
+  Algebra.Module.Morphism.Structures  
+  Algebra.Module.Properties
   ```
 
 * Identity morphisms and composition of morphisms between algebraic structures:
@@ -987,6 +988,11 @@ New modules
   Data.Vec.Relation.Unary.Linked.Properties
   ```
 
+* Proofs of some axioms of linearity:
+  ```
+  Algebra.Module.Morphism.ModuleHomomorphism
+  Algebra.Module.Properties
+  ```
 
 Other minor changes
 -------------------

src/Algebra/Module/Bundles.agda

@@ -27,12 +27,15 @@ module Algebra.Module.Bundles where
 
 open import Algebra.Bundles
 open import Algebra.Core
+open import Algebra.Definitions using (Involutive)
 open import Algebra.Module.Core
 open import Algebra.Module.Structures
 open import Algebra.Module.Definitions
+open import Algebra.Properties.Group
 open import Function.Base
 open import Level
 open import Relation.Binary
+open import Relation.Nullary    using (¬_)
 import Relation.Binary.Reasoning.Setoid as SetR
 
 private
@@ -59,6 +62,10 @@ record LeftSemimodule (semiring : Semiring r ℓr) m ℓm
     0ᴹ : Carrierᴹ
     isLeftSemimodule : IsLeftSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_
 
+  infix 4 _≉ᴹ_
+  _≉ᴹ_ : Rel Carrierᴹ _
+  a ≉ᴹ b = ¬ (a ≈ᴹ b)
+
   open IsLeftSemimodule isLeftSemimodule public
 
   +ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
@@ -99,7 +106,7 @@ record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ 
 
   open LeftSemimodule leftSemimodule public
     using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
-          ; +ᴹ-rawMagma; +ᴹ-rawMonoid)
+          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
 
   +ᴹ-abelianGroup : AbelianGroup m ℓm
   +ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }
@@ -127,6 +134,10 @@ record RightSemimodule (semiring : Semiring r ℓr) m ℓm
     0ᴹ : Carrierᴹ
     isRightSemimodule : IsRightSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ᵣ_
 
+  infix 4 _≉ᴹ_
+  _≉ᴹ_ : Rel Carrierᴹ _
+  a ≉ᴹ b = ¬ (a ≈ᴹ b)
+
   open IsRightSemimodule isRightSemimodule public
 
   +ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
@@ -167,7 +178,7 @@ record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔
 
   open RightSemimodule rightSemimodule public
     using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
-          ; +ᴹ-rawMagma; +ᴹ-rawMonoid)
+          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
 
   +ᴹ-abelianGroup : AbelianGroup m ℓm
   +ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }
@@ -208,7 +219,7 @@ record Bisemimodule (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs
 
   open LeftSemimodule leftSemimodule public
     using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma
-          ; +ᴹ-rawMonoid)
+          ; +ᴹ-rawMonoid; _≉ᴹ_)
 
 record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
                 : Set (r ⊔ s ⊔ ℓr ⊔ ℓs ⊔ suc (m ⊔ ℓm)) where
@@ -240,7 +251,8 @@ record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
 
   open LeftModule leftModule public
     using ( +ᴹ-abelianGroup; +ᴹ-commutativeMonoid; +ᴹ-group; +ᴹ-monoid
-          ; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma; +ᴹ-rawMonoid; +ᴹ-rawGroup)
+          ; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma; +ᴹ-rawMonoid; +ᴹ-rawGroup
+          ; _≉ᴹ_)
 
   bisemimodule : Bisemimodule R.semiring S.semiring m ℓm
   bisemimodule = record { isBisemimodule = isBisemimodule }
@@ -282,7 +294,7 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
   open Bisemimodule bisemimodule public
     using ( leftSemimodule; rightSemimodule
           ; +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
-          ; +ᴹ-rawMagma; +ᴹ-rawMonoid)
+          ; +ᴹ-rawMagma; +ᴹ-rawMonoid; _≉ᴹ_)
 
   open SetR ≈ᴹ-setoid
 
@@ -315,8 +327,8 @@ record Module (commutativeRing : CommutativeRing r ℓr) m ℓm
     _+ᴹ_ : Op₂ Carrierᴹ
     _*ₗ_ : Opₗ Carrier Carrierᴹ
     _*ᵣ_ : Opᵣ Carrier Carrierᴹ
-    0ᴹ : Carrierᴹ
-    -ᴹ_ : Op₁ Carrierᴹ
+    0ᴹ   : Carrierᴹ
+    -ᴹ_  : Op₁ Carrierᴹ
     isModule : IsModule commutativeRing _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_
 
   open IsModule isModule public
@@ -327,7 +339,8 @@ record Module (commutativeRing : CommutativeRing r ℓr) m ℓm
   open Bimodule bimodule public
     using ( leftModule; rightModule; leftSemimodule; rightSemimodule
           ; +ᴹ-abelianGroup; +ᴹ-group; +ᴹ-commutativeMonoid; +ᴹ-monoid
-          ; +ᴹ-semigroup; +ᴹ-magma ; +ᴹ-rawMonoid; +ᴹ-rawMagma; +ᴹ-rawGroup)
+          ; +ᴹ-semigroup; +ᴹ-magma ; +ᴹ-rawMonoid; +ᴹ-rawMagma
+          ; +ᴹ-rawGroup; _≉ᴹ_)
 
   semimodule : Semimodule commutativeSemiring m ℓm
   semimodule = record { isSemimodule = isSemimodule }

src/Algebra/Module/Morphism/ModuleHomomorphism.agda

@@ -0,0 +1,117 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of linear maps.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+import Algebra.Module.Properties            as ModuleProperties
+import Algebra.Module.Morphism.Structures   as MorphismStructures
+
+open import Algebra                   using (CommutativeRing)
+open import Algebra.Module            using (Module)
+open import Level                     using (Level)
+
+module Algebra.Module.Morphism.ModuleHomomorphism
+  {r ℓr m ℓm : Level}
+  {ring      : CommutativeRing r ℓr}
+  (modA modB  : Module ring m ℓm)
+  (open Module modA using () renaming (Carrierᴹ to A))
+  (open Module modB using () renaming (Carrierᴹ to B))
+  {f : A → B}
+  (open MorphismStructures.ModuleMorphisms modA modB)
+  (isModuleHomomorphism : IsModuleHomomorphism f)
+  where
+
+open import Axiom.DoubleNegationElimination
+open import Data.Product
+open import Relation.Binary.Reasoning.MultiSetoid
+open import Relation.Nullary          using (¬_)
+open import Relation.Nullary.Negation using (contraposition)
+
+module A = Module modA
+module B = Module modB
+module PA = ModuleProperties modA
+module PB = ModuleProperties modB
+open CommutativeRing ring renaming (Carrier to S)
+
+open IsModuleHomomorphism isModuleHomomorphism
+
+-- Some of the lemmas below only hold for continously scalable,
+-- non-trivial functions, i.e., f x = f (s y) and f ≠ const 0.
+-- This is a handy abbreviation for that rather verbose term.
+NonTrivial : A → Set (r Level.⊔ m Level.⊔ ℓm)
+NonTrivial x = ∃₂ λ s y → (s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)
+
+x≈0⇒fx≈0 : ∀ {x} → x A.≈ᴹ A.0ᴹ → f x B.≈ᴹ B.0ᴹ
+x≈0⇒fx≈0 {x} x≈0 = begin⟨ B.≈ᴹ-setoid ⟩
+  f x    ≈⟨ ⟦⟧-cong x≈0 ⟩
+  f A.0ᴹ ≈⟨ 0ᴹ-homo ⟩
+  B.0ᴹ   ∎
+
+fx≉0⇒x≉0 : ∀ {x} → f x B.≉ᴹ B.0ᴹ → x A.≉ᴹ A.0ᴹ
+fx≉0⇒x≉0 = contraposition x≈0⇒fx≈0
+
+-- Zero is a unique output of non-trivial (i.e. - ≉ `const 0`) linear map.
+x≉0⇒f[x]≉0 : ∀ {x} → NonTrivial x → x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ
+x≉0⇒f[x]≉0 {x} (s , y , s·x≈y , fy≉0) x≉0 =
+  PB.x*y≉0⇒y≉0 ( λ s·fx≈0 → fy≉0 ( begin⟨ B.≈ᴹ-setoid ⟩
+                   f y          ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym s·x≈y) ⟩
+                   f (s A.*ₗ x) ≈⟨ *ₗ-homo s x ⟩
+                   s B.*ₗ f x   ≈⟨ s·fx≈0 ⟩
+                   B.0ᴹ         ∎ )
+               )
+
+-- f is odd (i.e. - f (-x) ≈ - (f x)).
+fx+f[-x]≈0 : (x : A) → f x B.+ᴹ f (A.-ᴹ x) B.≈ᴹ B.0ᴹ
+fx+f[-x]≈0 x = begin⟨ B.≈ᴹ-setoid ⟩
+  f x B.+ᴹ f (A.-ᴹ x) ≈⟨ B.≈ᴹ-sym (+ᴹ-homo x (A.-ᴹ x)) ⟩
+  f (x A.+ᴹ (A.-ᴹ x)) ≈⟨ ⟦⟧-cong (A.-ᴹ‿inverseʳ x) ⟩
+  f A.0ᴹ              ≈⟨ 0ᴹ-homo ⟩
+  B.0ᴹ                ∎
+
+f[-x]≈-fx : (x : A) → f (A.-ᴹ x) B.≈ᴹ B.-ᴹ f x
+f[-x]≈-fx x = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) (fx+f[-x]≈0 x)
+
+-- A non-trivial linear function is injective.
+fx≈fy⇒fx-fy≈0 : ∀ {x y} → f x B.≈ᴹ f y → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ
+fx≈fy⇒fx-fy≈0 {x} {y} fx≈fy = begin⟨ B.≈ᴹ-setoid ⟩
+  f x B.+ᴹ (B.-ᴹ f y) ≈⟨ B.+ᴹ-congˡ (B.-ᴹ‿cong (B.≈ᴹ-sym fx≈fy)) ⟩
+  f x B.+ᴹ (B.-ᴹ f x) ≈⟨ B.-ᴹ‿inverseʳ (f x) ⟩
+  B.0ᴹ                ∎
+
+fx≈fy⇒f[x-y]≈0 : ∀ {x y} → f x B.≈ᴹ f y → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ
+fx≈fy⇒f[x-y]≈0 {x} {y} fx≈fy = begin⟨ B.≈ᴹ-setoid ⟩
+  f (x A.+ᴹ (A.-ᴹ y)) ≈⟨ +ᴹ-homo x (A.-ᴹ y) ⟩
+  f x B.+ᴹ f (A.-ᴹ y) ≈⟨ B.+ᴹ-congˡ (f[-x]≈-fx y) ⟩
+  f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx≈fy⇒fx-fy≈0 fx≈fy ⟩
+  B.0ᴹ                ∎
+
+module _ {dne : DoubleNegationElimination _} where
+
+  fx≈0⇒x≈0 : ∀ {x} → NonTrivial x → f x B.≈ᴹ B.0ᴹ → x A.≈ᴹ A.0ᴹ
+  fx≈0⇒x≈0 {x} (s , y , s·x≈y , fy≉0) fx≈0 =
+    dne ¬x≉0
+    where
+    ¬x≉0 : ¬ (x A.≉ᴹ A.0ᴹ)
+    ¬x≉0 = λ x≉0 → x≉0⇒f[x]≉0 (s , y , s·x≈y , fy≉0) x≉0 fx≈0
+
+  inj-lm : ∀ {x y} →
+           (∃₂ λ s z → ((s A.*ₗ (x A.+ᴹ A.-ᴹ y) A.≈ᴹ z) × (f z B.≉ᴹ B.0ᴹ))) →
+           f x B.≈ᴹ f y → x A.≈ᴹ y
+  inj-lm {x} {y} (s , z , s·[x-y]≈z , fz≉0) fx≈fy =
+    begin⟨ A.≈ᴹ-setoid ⟩
+    x             ≈⟨ x≈--y ⟩
+    A.-ᴹ (A.-ᴹ y) ≈⟨ PA.-ᴹ-involutive y ⟩
+    y             ∎
+    where
+    x-y≈0 : x A.+ᴹ (A.-ᴹ y) A.≈ᴹ A.0ᴹ
+    x-y≈0 = fx≈0⇒x≈0 (s , z , s·[x-y]≈z , fz≉0) (fx≈fy⇒f[x-y]≈0 fx≈fy)
+    x≈--y : x A.≈ᴹ A.-ᴹ (A.-ᴹ y)
+    x≈--y = A.uniqueʳ‿-ᴹ (A.-ᴹ y) x
+      ( begin⟨ A.≈ᴹ-setoid ⟩
+        A.-ᴹ y A.+ᴹ x ≈⟨ A.+ᴹ-comm (A.-ᴹ y) x ⟩
+        x A.+ᴹ A.-ᴹ y ≈⟨ x-y≈0 ⟩
+        A.0ᴹ          ∎
+      )

src/Algebra/Module/Properties.agda

@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of modules.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra                using (CommutativeRing; Involutive)
+open import Algebra.Module.Bundles using (Module)
+open import Level                  using (Level)
+
+module Algebra.Module.Properties
+  {r ℓr m ℓm : Level}
+  {ring      : CommutativeRing r ℓr}
+  (mod       : Module ring m ℓm)
+  where
+
+open Module mod
+open import Algebra.Module.Properties.Semimodule semimodule public
+open import Algebra.Properties.Group using (⁻¹-involutive)
+
+-ᴹ-involutive : Involutive _≈ᴹ_ -ᴹ_
+-ᴹ-involutive = ⁻¹-involutive +ᴹ-group

src/Algebra/Module/Properties/Semimodule.agda

@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of semimodules.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra                using (CommutativeSemiring)
+open import Algebra.Module.Bundles using (Semimodule)
+open import Level                  using (Level)
+
+module Algebra.Module.Properties.Semimodule
+  {r ℓr m ℓm : Level}
+  {semiring  : CommutativeSemiring r ℓr}
+  (semimod   : Semimodule semiring m ℓm)
+  where
+
+open CommutativeSemiring semiring
+open Semimodule          semimod
+open import Relation.Nullary.Negation using (contraposition)
+open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid
+
+x≈0⇒x*y≈0 : ∀ {x y} → x ≈ 0# → x *ₗ y ≈ᴹ 0ᴹ
+x≈0⇒x*y≈0 {x} {y} x≈0 = begin
+  x  *ₗ y ≈⟨ *ₗ-congʳ x≈0 ⟩
+  0# *ₗ y ≈⟨ *ₗ-zeroˡ y ⟩
+  0ᴹ      ∎
+
+y≈0⇒x*y≈0 : ∀ {x y} → y ≈ᴹ 0ᴹ → x *ₗ y ≈ᴹ 0ᴹ
+y≈0⇒x*y≈0 {x} {y} y≈0 = begin
+  x *ₗ y  ≈⟨ *ₗ-congˡ y≈0 ⟩
+  x *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ x ⟩
+  0ᴹ      ∎
+
+x*y≉0⇒x≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → x ≉ 0#
+x*y≉0⇒x≉0 = contraposition x≈0⇒x*y≈0
+
+x*y≉0⇒y≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → y ≉ᴹ 0ᴹ
+x*y≉0⇒y≉0 = contraposition y≈0⇒x*y≈0