From 27746d83e2f11dcd795ce615a3ff338009596aa0 Mon Sep 17 00:00:00 2001 From: David Banas Date: Thu, 5 May 2022 12:50:52 -0700 Subject: [PATCH 01/19] Temporary check-in. --- .gitignore | 2 + src/Algebra/Module.agda | 2 + src/Algebra/Module/Morphism/Linear/Core.agda | 96 +++++++++++++++++++ .../Module/Morphism/Linear/Properties.agda | 79 +++++++++++++++ src/Algebra/Module/Properties.agda | 61 ++++++++++++ 5 files changed, 240 insertions(+) create mode 100644 src/Algebra/Module/Morphism/Linear/Core.agda create mode 100644 src/Algebra/Module/Morphism/Linear/Properties.agda create mode 100644 src/Algebra/Module/Properties.agda diff --git a/.gitignore b/.gitignore index d3516eb0f2..99f960e19f 100644 --- a/.gitignore +++ b/.gitignore @@ -11,6 +11,8 @@ *.vim *~ .*.swp +.#* +\#* ./_build/* .DS_Store .vscode/* diff --git a/src/Algebra/Module.agda b/src/Algebra/Module.agda index 5cc1379acc..e16b8999f9 100644 --- a/src/Algebra/Module.agda +++ b/src/Algebra/Module.agda @@ -14,3 +14,5 @@ open import Algebra.Module.Structures public open import Algebra.Module.Structures.Biased public open import Algebra.Module.Bundles public open import Algebra.Module.Definitions public +open import Algebra.Module.Properties public + diff --git a/src/Algebra/Module/Morphism/Linear/Core.agda b/src/Algebra/Module/Morphism/Linear/Core.agda new file mode 100644 index 0000000000..4c3ae96343 --- /dev/null +++ b/src/Algebra/Module/Morphism/Linear/Core.agda @@ -0,0 +1,96 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Core definitions for linear maps. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Algebra.Module.Morphism.Linear.Core where + +import Function.Definitions +import Relation.Binary.Reasoning.Setoid + +open import Algebra using (CommutativeRing) +open import Algebra.Module using (Module) +open import Level using (Level; _⊔_; suc) +open import Relation.Binary using (Rel; Setoid; IsEquivalence) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; trans; sym) +open import Relation.Nullary using (¬_) + +module _ + {r ℓr m ℓm : Level} + {ring : CommutativeRing r ℓr} + (modA : Module ring m ℓm) + (modB : Module ring m ℓm) + where + + lm = suc (ℓm ⊔ m ⊔ r) + record LinMap : Set lm where + + constructor mkLM + open Module modA public + using () renaming + ( Carrierᴹ to A + ; _+ᴹ_ to _+ᴬ_ + ; _*ₗ_ to _·ᴬ_ + ; _≈ᴹ_ to _≈ᴬ_ + ; 0ᴹ to 0ᴬ + ; ≈ᴹ-setoid to ≈ᴬ-setoid + ; *ₗ-zeroˡ to ·ᴬ-zeroˡ + ; ≈ᴹ-sym to symᴬ + ; non-zeroʳ to non-zeroʳᴬ + ; non-zeroˡ to non-zeroˡᴬ + ) + open Module modB public + using () renaming + ( Carrierᴹ to B + ; _+ᴹ_ to _+ᴮ_ + ; _*ₗ_ to _·ᴮ_ + ; _≈ᴹ_ to _≈ᴮ_ + ; 0ᴹ to 0ᴮ + ; ≈ᴹ-setoid to ≈ᴮ-setoid + ; *ₗ-zeroˡ to ·ᴮ-zeroˡ + ; ≈ᴹ-sym to symᴮ + ; non-zeroʳ to non-zeroʳᴮ + ; non-zeroˡ to non-zeroˡᴮ + ) + open CommutativeRing ring public + using () renaming + ( Carrier to S + ; 0# to 𝟘 + ) + -- open Relation.Binary.Setoid ≈ᴬ-setoid public + -- using () renaming (_≈_ to _≈ᴬ_) + -- open Relation.Binary.Setoid ≈ᴮ-setoid public + -- using (_≈_) + open Relation.Binary.Reasoning.Setoid ≈ᴮ-setoid public + open Function.Definitions _≈ᴬ_ _≈ᴮ_ + field + f : A → B + adds : ∀ {a₁ a₂ : A} → f (a₁ +ᴬ a₂) ≈ᴮ f a₁ +ᴮ f a₂ + scales : ∀ {s : S} {a : A} → f (s ·ᴬ a) ≈ᴮ s ·ᴮ f a + f-cong : Congruent f + + _≉ᴬ_ : A → A → Set ℓm + x ≉ᴬ y = ¬ (x ≈ᴬ y) + + _≉ᴮ_ : B → B → Set ℓm + x ≉ᴮ y = ¬ (x ≈ᴮ y) + + _≈ᴸᴹ_ : Rel LinMap m + lm₁ ≈ᴸᴹ lm₂ = f ≡ f + + isEquivalence : IsEquivalence _≈ᴸᴹ_ + isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + + open IsEquivalence isEquivalence public + + ≈ᴸᴹ-setoid : Setoid lm m + ≈ᴸᴹ-setoid = record { isEquivalence = isEquivalence } + -- open LinMap public diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda new file mode 100644 index 0000000000..6cb5401a01 --- /dev/null +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -0,0 +1,79 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of linear maps. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K #-} + +module Algebra.Module.Morphism.Linear.Properties where + +open import Agda.Builtin.Sigma +open import Algebra using (CommutativeRing) +open import Algebra.Module using (Module) +open import Algebra.Module.Morphism.Linear.Core +open import Axiom.Extensionality.Propositional using (Extensionality) +open import Data.List +open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax) +open import Function using (_↔_; mk↔; id; const) +open import Level using (Level; _⊔_) +open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (contraposition) + +private + variable + ℓ₁ ℓ₂ r ℓr m ℓm : Level + ring : CommutativeRing r ℓr + modA modB : Module ring m ℓm + +postulate + extensionality : Extensionality ℓ₁ ℓ₂ + -- excluded-middle : ∀ {A : Set ℓ₁} → ¬ (¬ A) ≡ A + -- ≡-involutive : ∀ {A : Set ℓ₁} → {x y : A} → ¬ (x ≢ y) → x ≡ y + +module _ (lm : LinMap modA modB) where + + open LinMap lm + + -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f + f𝟘≈𝟘 : {x : A} → f 0ᴬ ≈ᴮ 0ᴮ + f𝟘≈𝟘 {x = x} = begin + f 0ᴬ ≈⟨ f-cong (symᴬ (·ᴬ-zeroˡ x)) ⟩ + f (𝟘 ·ᴬ x) ≈⟨ scales ⟩ + 𝟘 ·ᴮ f x ≈⟨ ·ᴮ-zeroˡ (f x) ⟩ + 0ᴮ ∎ + + x≈𝟘→fx≈𝟘 : {x : A} → x ≈ᴬ 0ᴬ → f x ≈ᴮ 0ᴮ + x≈𝟘→fx≈𝟘 {x = x} x≈𝟘 = begin + f x ≈⟨ f-cong x≈𝟘 ⟩ + f 0ᴬ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ + 0ᴮ ∎ + + fx≉𝟘→x≉𝟘 : {x : A} → f x ≉ᴮ 0ᴮ → x ≉ᴬ 0ᴬ + fx≉𝟘→x≉𝟘 = contraposition x≈𝟘→fx≈𝟘 + + -- Zero is unique output of linear map ≉ `const 𝟘`. + zero-unique : {x : A} → Σ[ y ∈ A ] f y ≉ᴮ 0ᴮ → x ≉ᴬ 𝟘 → f x ≉ᴮ 𝟘 + zero-unique {x = x} (y , fy≉𝟘) x≉𝟘 = + let y≉𝟘 : y ≉ᴬ 0ᴬ + y≉𝟘 = fx≉𝟘→x≉𝟘 fy≉𝟘 + Σs→s·x≈y : Σ[ s ∈ S ] s ·ᴬ x ≈ᴬ y + -- Σs→s·x≈y = cont x y + Σs→s·x≈y = ? + Σs→fs·x≈fy : Σ[ s ∈ S ] f (s ·ᴬ x) ≈ᴮ f y + Σs→fs·x≈fy = let (s , g) = Σs→s·x≈y + in (s , f-cong g) + Σs→s·fx≈fy : Σ[ s ∈ S ] s ·ᴮ f x ≈ᴮ f y + Σs→s·fx≈fy = let (s , g) = Σs→fs·x≈fy + in (s , (begin + s ·ᴮ f x + ≈⟨ sym scales ⟩ + f (s ·ᴬ x) + ≈⟨ g ⟩ + f y + ∎)) + s·fx≉𝟘 : Σ[ s ∈ S ] s ·ᴮ f x ≉ᴮ 0ᴮ + s·fx≉𝟘 = let (s , g) = Σs→s·fx≈fy + in (s , λ s·fx≈𝟘 → fy≉𝟘 (step-≈ (f y) s·fx≈𝟘 (sym g))) + in non-zeroʳ (snd s·fx≉𝟘) + diff --git a/src/Algebra/Module/Properties.agda b/src/Algebra/Module/Properties.agda new file mode 100644 index 0000000000..34a54f7d78 --- /dev/null +++ b/src/Algebra/Module/Properties.agda @@ -0,0 +1,61 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of scaling. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Algebra.Module.Properties where + +open import Algebra using (Semiring) +open import Algebra.Module.Bundles using (LeftSemimodule) +open import Level using (Level) +open import Relation.Nullary using (¬_) + +private + variable + r ℓr : Level + m ℓm : Level + semiring : Semiring r ℓr + +module _ (lsmod : LeftSemimodule semiring m ℓm) where + + open LeftSemimodule lsmod + using (*ₗ-zeroˡ; *ₗ-zeroʳ; ≈ᴹ-setoid; _≈ᴹ_; *ₗ-congˡ; *ₗ-congʳ) + renaming + ( Carrierᴹ to M + ; _*ₗ_ to _·_ + ; 0ᴹ to 𝟘 + ) + infix 3 _≉ᴹ_ + _≉ᴹ_ : M → M → Set ℓm + x ≉ᴹ y = ¬ (x ≈ᴹ y) + + open Semiring semiring + using (_≉_) renaming + ( Carrier to R + ; 0# to 0ᴿ + ) + + open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid + + non-zeroˡ : {s : R} {v : M} → s · v ≉ᴹ 𝟘 → s ≉ 0ᴿ + non-zeroˡ {s = s} {v = v} s·v≉𝟘 = λ { s≈0ᴿ → + let s·v≈𝟘 : s · v ≈ᴹ 𝟘 + s·v≈𝟘 = begin + s · v ≈⟨ *ₗ-congʳ s≈0ᴿ ⟩ + 0ᴿ · v ≈⟨ *ₗ-zeroˡ v ⟩ + 𝟘 ∎ + in s·v≉𝟘 s·v≈𝟘 + } + + non-zeroʳ : {s : R} {v : M} → s · v ≉ᴹ 𝟘 → v ≉ᴹ 𝟘 + non-zeroʳ {s = s} {v = v} s·v≉𝟘 = λ { v≈𝟘 → + let s·v≈𝟘 : s · v ≈ᴹ 𝟘 + s·v≈𝟘 = begin + s · v ≈⟨ *ₗ-congˡ v≈𝟘 ⟩ + s · 𝟘 ≈⟨ *ₗ-zeroʳ s ⟩ + 𝟘 ∎ + in s·v≉𝟘 s·v≈𝟘 + } From 65989fdb0cb2e006fabad10debe479322db3efb2 Mon Sep 17 00:00:00 2001 From: David Banas Date: Sun, 8 May 2022 10:40:17 -0700 Subject: [PATCH 02/19] Last linearity axiom proved. --- src/Algebra/Module.agda | 1 - src/Algebra/Module/Morphism/Linear/Core.agda | 86 +++++++++++----- .../Module/Morphism/Linear/Properties.agda | 98 ++++++++++++++----- src/Algebra/Module/Properties.agda | 92 +++++++++-------- 4 files changed, 178 insertions(+), 99 deletions(-) diff --git a/src/Algebra/Module.agda b/src/Algebra/Module.agda index e16b8999f9..b7f6e52a21 100644 --- a/src/Algebra/Module.agda +++ b/src/Algebra/Module.agda @@ -14,5 +14,4 @@ open import Algebra.Module.Structures public open import Algebra.Module.Structures.Biased public open import Algebra.Module.Bundles public open import Algebra.Module.Definitions public -open import Algebra.Module.Properties public diff --git a/src/Algebra/Module/Morphism/Linear/Core.agda b/src/Algebra/Module/Morphism/Linear/Core.agda index 4c3ae96343..04c1c2431e 100644 --- a/src/Algebra/Module/Morphism/Linear/Core.agda +++ b/src/Algebra/Module/Morphism/Linear/Core.agda @@ -8,8 +8,9 @@ module Algebra.Module.Morphism.Linear.Core where +import Algebra.Module.Properties as Properties import Function.Definitions -import Relation.Binary.Reasoning.Setoid +import Relation.Binary.Reasoning.Setoid as Reasoning open import Algebra using (CommutativeRing) open import Algebra.Module using (Module) @@ -30,49 +31,84 @@ module _ record LinMap : Set lm where constructor mkLM + open Module modA public using () renaming - ( Carrierᴹ to A - ; _+ᴹ_ to _+ᴬ_ - ; _*ₗ_ to _·ᴬ_ - ; _≈ᴹ_ to _≈ᴬ_ - ; 0ᴹ to 0ᴬ - ; ≈ᴹ-setoid to ≈ᴬ-setoid - ; *ₗ-zeroˡ to ·ᴬ-zeroˡ - ; ≈ᴹ-sym to symᴬ - ; non-zeroʳ to non-zeroʳᴬ + ( Carrierᴹ to A + ; _+ᴹ_ to _+ᴬ_ + ; _*ₗ_ to _·ᴬ_ + ; -ᴹ_ to -ᴬ_ + ; _≈ᴹ_ to _≈ᴬ_ + ; 0ᴹ to 0ᴬ + ; +ᴹ-comm to +ᴬ-comm + ; +ᴹ-congˡ to +ᴬ-congˡ + ; +ᴹ-congʳ to +ᴬ-congʳ + ; *ₗ-zeroˡ to ·ᴬ-zeroˡ + ; -ᴹ‿cong to -ᴬ‿cong + ; -ᴹ‿inverseʳ to -ᴬ‿inverseʳ + ; uniqueʳ‿-ᴹ to uniqueʳ‿-ᴬ + ; ≈ᴹ-setoid to ≈ᴬ-setoid + ; ≈ᴹ-sym to symᴬ + ; leftSemimodule to leftSemimoduleᴬ + ) + open Properties leftSemimoduleᴬ public + using () renaming + ( non-zeroʳ to non-zeroʳᴬ ; non-zeroˡ to non-zeroˡᴬ ) + open Module modB public using () renaming - ( Carrierᴹ to B - ; _+ᴹ_ to _+ᴮ_ - ; _*ₗ_ to _·ᴮ_ - ; _≈ᴹ_ to _≈ᴮ_ - ; 0ᴹ to 0ᴮ - ; ≈ᴹ-setoid to ≈ᴮ-setoid - ; *ₗ-zeroˡ to ·ᴮ-zeroˡ - ; ≈ᴹ-sym to symᴮ - ; non-zeroʳ to non-zeroʳᴮ + ( Carrierᴹ to B + ; _+ᴹ_ to _+ᴮ_ + ; _*ₗ_ to _·ᴮ_ + ; -ᴹ_ to -ᴮ_ + ; _≈ᴹ_ to _≈ᴮ_ + ; 0ᴹ to 0ᴮ + ; +ᴹ-comm to +ᴮ-comm + ; +ᴹ-congˡ to +ᴮ-congˡ + ; +ᴹ-congʳ to +ᴮ-congʳ + ; *ₗ-zeroˡ to ·ᴮ-zeroˡ + ; -ᴹ‿cong to -ᴮ‿cong + ; -ᴹ‿inverseʳ to -ᴮ‿inverseʳ + ; uniqueʳ‿-ᴹ to uniqueʳ‿-ᴮ + ; ≈ᴹ-setoid to ≈ᴮ-setoid + ; ≈ᴹ-sym to symᴮ + ; leftSemimodule to leftSemimoduleᴮ + ) + open Properties leftSemimoduleᴮ public + using () renaming + ( non-zeroʳ to non-zeroʳᴮ ; non-zeroˡ to non-zeroˡᴮ ) + open CommutativeRing ring public using () renaming ( Carrier to S ; 0# to 𝟘 + ; 1# to 𝟙 + ) + open module Reasoningᴬ = Reasoning ≈ᴬ-setoid public + using () renaming + ( begin_ to beginᴬ_ + ; _∎ to _∎ᴬ ) - -- open Relation.Binary.Setoid ≈ᴬ-setoid public - -- using () renaming (_≈_ to _≈ᴬ_) - -- open Relation.Binary.Setoid ≈ᴮ-setoid public - -- using (_≈_) - open Relation.Binary.Reasoning.Setoid ≈ᴮ-setoid public + infixr 2 step-≈ᴬ + step-≈ᴬ = Reasoningᴬ.step-≈ + syntax step-≈ᴬ x y≈z x≈y = x ≈ᴬ⟨ x≈y ⟩ y≈z + open module Reasoningᴮ = Reasoning ≈ᴮ-setoid public open Function.Definitions _≈ᴬ_ _≈ᴮ_ + field f : A → B adds : ∀ {a₁ a₂ : A} → f (a₁ +ᴬ a₂) ≈ᴮ f a₁ +ᴮ f a₂ scales : ∀ {s : S} {a : A} → f (s ·ᴬ a) ≈ᴮ s ·ᴮ f a f-cong : Congruent f - + ¬-involutive-≈ᴬ : {a₁ a₂ : A} → ¬ (¬ (a₁ ≈ᴬ a₂)) → a₁ ≈ᴬ a₂ + ¬-involutive-≈ᴮ : {b₁ b₂ : B} → ¬ (¬ (b₁ ≈ᴮ b₂)) → b₁ ≈ᴮ b₂ + -ᴬ‿involutive : {a : A} → -ᴬ (-ᴬ a) ≈ᴬ a + -ᴮ‿involutive : {b : B} → -ᴮ (-ᴮ b) ≈ᴮ b + _≉ᴬ_ : A → A → Set ℓm x ≉ᴬ y = ¬ (x ≈ᴬ y) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index 6cb5401a01..cc9897e49a 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -10,11 +10,12 @@ module Algebra.Module.Morphism.Linear.Properties where open import Agda.Builtin.Sigma open import Algebra using (CommutativeRing) +-- open import Algebra.Lattice.Properties.BooleanAlgebra using (¬-involutive) open import Algebra.Module using (Module) open import Algebra.Module.Morphism.Linear.Core open import Axiom.Extensionality.Propositional using (Extensionality) open import Data.List -open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax) +open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax; _×_) open import Function using (_↔_; mk↔; id; const) open import Level using (Level; _⊔_) open import Relation.Nullary using (¬_) @@ -28,13 +29,12 @@ private postulate extensionality : Extensionality ℓ₁ ℓ₂ - -- excluded-middle : ∀ {A : Set ℓ₁} → ¬ (¬ A) ≡ A -- ≡-involutive : ∀ {A : Set ℓ₁} → {x y : A} → ¬ (x ≢ y) → x ≡ y module _ (lm : LinMap modA modB) where open LinMap lm - + -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f f𝟘≈𝟘 : {x : A} → f 0ᴬ ≈ᴮ 0ᴮ f𝟘≈𝟘 {x = x} = begin @@ -52,28 +52,76 @@ module _ (lm : LinMap modA modB) where fx≉𝟘→x≉𝟘 : {x : A} → f x ≉ᴮ 0ᴮ → x ≉ᴬ 0ᴬ fx≉𝟘→x≉𝟘 = contraposition x≈𝟘→fx≈𝟘 - -- Zero is unique output of linear map ≉ `const 𝟘`. - zero-unique : {x : A} → Σ[ y ∈ A ] f y ≉ᴮ 0ᴮ → x ≉ᴬ 𝟘 → f x ≉ᴮ 𝟘 - zero-unique {x = x} (y , fy≉𝟘) x≉𝟘 = + -- Zero is a unique output of linear map ≉ `const 𝟘`. + zero-unique : {x : A} → + Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (f y ≉ᴮ 0ᴮ)) → + x ≉ᴬ 0ᴬ → f x ≉ᴮ 0ᴮ + zero-unique {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 = let y≉𝟘 : y ≉ᴬ 0ᴬ y≉𝟘 = fx≉𝟘→x≉𝟘 fy≉𝟘 - Σs→s·x≈y : Σ[ s ∈ S ] s ·ᴬ x ≈ᴬ y - -- Σs→s·x≈y = cont x y - Σs→s·x≈y = ? - Σs→fs·x≈fy : Σ[ s ∈ S ] f (s ·ᴬ x) ≈ᴮ f y - Σs→fs·x≈fy = let (s , g) = Σs→s·x≈y - in (s , f-cong g) - Σs→s·fx≈fy : Σ[ s ∈ S ] s ·ᴮ f x ≈ᴮ f y - Σs→s·fx≈fy = let (s , g) = Σs→fs·x≈fy - in (s , (begin - s ·ᴮ f x - ≈⟨ sym scales ⟩ - f (s ·ᴬ x) - ≈⟨ g ⟩ - f y - ∎)) - s·fx≉𝟘 : Σ[ s ∈ S ] s ·ᴮ f x ≉ᴮ 0ᴮ - s·fx≉𝟘 = let (s , g) = Σs→s·fx≈fy - in (s , λ s·fx≈𝟘 → fy≉𝟘 (step-≈ (f y) s·fx≈𝟘 (sym g))) - in non-zeroʳ (snd s·fx≉𝟘) + fs·x≈fy : f (s ·ᴬ x) ≈ᴮ f y + fs·x≈fy = f-cong s·x≈y + s·fx≈fy : s ·ᴮ f x ≈ᴮ f y + s·fx≈fy = begin + s ·ᴮ f x ≈⟨ symᴮ scales ⟩ + f (s ·ᴬ x) ≈⟨ fs·x≈fy ⟩ + f y ∎ + s·fx≉𝟘 : (s ·ᴮ f x) ≉ᴮ 0ᴮ + s·fx≉𝟘 = λ s·fx≈𝟘 → + fy≉𝟘 ( begin + f y ≈⟨ f-cong (symᴬ s·x≈y) ⟩ + f (s ·ᴬ x) ≈⟨ scales ⟩ + s ·ᴮ f x ≈⟨ s·fx≈𝟘 ⟩ + 0ᴮ ∎ + ) + in non-zeroʳᴮ s·fx≉𝟘 + + fx≈𝟘⇒x≈𝟘 : {x : A} → + Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (f y ≉ᴮ 0ᴮ)) → + f x ≈ᴮ 0ᴮ → x ≈ᴬ 0ᴬ + fx≈𝟘⇒x≈𝟘 {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) fx≈𝟘 = + let ¬x≉𝟘 : ¬ (x ≉ᴬ 0ᴬ) + ¬x≉𝟘 = λ x≉𝟘 → zero-unique ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 fx≈𝟘 + in ¬-involutive-≈ᴬ ¬x≉𝟘 + + -- f is odd (i.e. - f (-x) ≈ - (f x)). + fx+f-x≈𝟘 : {x : A} → f x +ᴮ f (-ᴬ x) ≈ᴮ 0ᴮ + fx+f-x≈𝟘 {x = x} = begin + f x +ᴮ f (-ᴬ x) ≈⟨ symᴮ adds ⟩ + f (x +ᴬ (-ᴬ x)) ≈⟨ f-cong (-ᴬ‿inverseʳ x) ⟩ + f 0ᴬ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ + 0ᴮ ∎ + + f-x≈-fx : {x : A} → f (-ᴬ x) ≈ᴮ -ᴮ (f x) + f-x≈-fx {x = x} = uniqueʳ‿-ᴮ (f x) (f (-ᴬ x)) fx+f-x≈𝟘 + + -- A non-trivial linear function is injective. + inj-lm : {x y : A} → + Σ[ (s , z) ∈ S × A ] ((s ·ᴬ (x +ᴬ -ᴬ y) ≈ᴬ z) × (f z ≉ᴮ 0ᴮ)) → + f x ≈ᴮ f y → x ≈ᴬ y + inj-lm {x = x} {y = y} ((s , z) , (s·[x-y]≈z , fz≉𝟘)) fx≈fy = + let fx-fy≈𝟘 : f x +ᴮ (-ᴮ f y) ≈ᴮ 0ᴮ + fx-fy≈𝟘 = begin + f x +ᴮ (-ᴮ f y) ≈⟨ +ᴮ-congˡ (-ᴮ‿cong (symᴮ fx≈fy)) ⟩ + f x +ᴮ (-ᴮ f x) ≈⟨ -ᴮ‿inverseʳ (f x) ⟩ + 0ᴮ ∎ + fx-y≈𝟘 : f (x +ᴬ (-ᴬ y)) ≈ᴮ 0ᴮ + fx-y≈𝟘 = begin + f (x +ᴬ (-ᴬ y)) ≈⟨ adds ⟩ + f x +ᴮ f (-ᴬ y) ≈⟨ +ᴮ-congˡ f-x≈-fx ⟩ + f x +ᴮ (-ᴮ (f y)) ≈⟨ fx-fy≈𝟘 ⟩ + 0ᴮ ∎ + x-y≈𝟘 : x +ᴬ (-ᴬ y) ≈ᴬ 0ᴬ + x-y≈𝟘 = fx≈𝟘⇒x≈𝟘 {x = x +ᴬ (-ᴬ y)} ((s , z) , s·[x-y]≈z , fz≉𝟘) fx-y≈𝟘 + x≈--y : x ≈ᴬ -ᴬ (-ᴬ y) + x≈--y = uniqueʳ‿-ᴬ (-ᴬ y) x + ( beginᴬ + -ᴬ y +ᴬ x ≈ᴬ⟨ +ᴬ-comm (-ᴬ y) x ⟩ + x +ᴬ -ᴬ y ≈ᴬ⟨ x-y≈𝟘 ⟩ + 0ᴬ ∎ᴬ + ) + in beginᴬ + x ≈ᴬ⟨ x≈--y ⟩ + -ᴬ (-ᴬ y) ≈ᴬ⟨ -ᴬ‿involutive ⟩ + y ∎ᴬ diff --git a/src/Algebra/Module/Properties.agda b/src/Algebra/Module/Properties.agda index 34a54f7d78..59a5f4ec59 100644 --- a/src/Algebra/Module/Properties.agda +++ b/src/Algebra/Module/Properties.agda @@ -6,56 +6,52 @@ {-# OPTIONS --without-K --safe #-} -module Algebra.Module.Properties where - open import Algebra using (Semiring) open import Algebra.Module.Bundles using (LeftSemimodule) open import Level using (Level) + +module Algebra.Module.Properties + {r ℓr m ℓm : Level} {semiring : Semiring r ℓr} + (lsmod : LeftSemimodule semiring m ℓm) + where + open import Relation.Nullary using (¬_) -private - variable - r ℓr : Level - m ℓm : Level - semiring : Semiring r ℓr - -module _ (lsmod : LeftSemimodule semiring m ℓm) where - - open LeftSemimodule lsmod - using (*ₗ-zeroˡ; *ₗ-zeroʳ; ≈ᴹ-setoid; _≈ᴹ_; *ₗ-congˡ; *ₗ-congʳ) - renaming - ( Carrierᴹ to M - ; _*ₗ_ to _·_ - ; 0ᴹ to 𝟘 - ) - infix 3 _≉ᴹ_ - _≉ᴹ_ : M → M → Set ℓm - x ≉ᴹ y = ¬ (x ≈ᴹ y) - - open Semiring semiring - using (_≉_) renaming - ( Carrier to R - ; 0# to 0ᴿ - ) - - open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid - - non-zeroˡ : {s : R} {v : M} → s · v ≉ᴹ 𝟘 → s ≉ 0ᴿ - non-zeroˡ {s = s} {v = v} s·v≉𝟘 = λ { s≈0ᴿ → - let s·v≈𝟘 : s · v ≈ᴹ 𝟘 - s·v≈𝟘 = begin - s · v ≈⟨ *ₗ-congʳ s≈0ᴿ ⟩ - 0ᴿ · v ≈⟨ *ₗ-zeroˡ v ⟩ - 𝟘 ∎ - in s·v≉𝟘 s·v≈𝟘 - } - - non-zeroʳ : {s : R} {v : M} → s · v ≉ᴹ 𝟘 → v ≉ᴹ 𝟘 - non-zeroʳ {s = s} {v = v} s·v≉𝟘 = λ { v≈𝟘 → - let s·v≈𝟘 : s · v ≈ᴹ 𝟘 - s·v≈𝟘 = begin - s · v ≈⟨ *ₗ-congˡ v≈𝟘 ⟩ - s · 𝟘 ≈⟨ *ₗ-zeroʳ s ⟩ - 𝟘 ∎ - in s·v≉𝟘 s·v≈𝟘 - } +open LeftSemimodule lsmod + using (*ₗ-zeroˡ; *ₗ-zeroʳ; ≈ᴹ-setoid; _≈ᴹ_; *ₗ-congˡ; *ₗ-congʳ) + renaming + ( Carrierᴹ to M + ; _*ₗ_ to _·_ + ; 0ᴹ to 𝟘 + ) +infix 3 _≉ᴹ_ +_≉ᴹ_ : M → M → Set ℓm +x ≉ᴹ y = ¬ (x ≈ᴹ y) + +open Semiring semiring + using (_≉_) renaming + ( Carrier to R + ; 0# to 0ᴿ + ) + +open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid + +non-zeroˡ : {s : R} {v : M} → s · v ≉ᴹ 𝟘 → s ≉ 0ᴿ +non-zeroˡ {s = s} {v = v} s·v≉𝟘 = λ { s≈0ᴿ → + let s·v≈𝟘 : s · v ≈ᴹ 𝟘 + s·v≈𝟘 = begin + s · v ≈⟨ *ₗ-congʳ s≈0ᴿ ⟩ + 0ᴿ · v ≈⟨ *ₗ-zeroˡ v ⟩ + 𝟘 ∎ + in s·v≉𝟘 s·v≈𝟘 + } + +non-zeroʳ : {s : R} {v : M} → s · v ≉ᴹ 𝟘 → v ≉ᴹ 𝟘 +non-zeroʳ {s = s} {v = v} s·v≉𝟘 = λ { v≈𝟘 → + let s·v≈𝟘 : s · v ≈ᴹ 𝟘 + s·v≈𝟘 = begin + s · v ≈⟨ *ₗ-congˡ v≈𝟘 ⟩ + s · 𝟘 ≈⟨ *ₗ-zeroʳ s ⟩ + 𝟘 ∎ + in s·v≉𝟘 s·v≈𝟘 + } From 2d7abea16bd457bb2a69a528ec364ea3a962d27a Mon Sep 17 00:00:00 2001 From: David Banas Date: Sun, 8 May 2022 11:49:36 -0700 Subject: [PATCH 03/19] Final edits before initial pull request. --- CHANGELOG.md | 6 ++++++ GenerateEverything.hs | 3 ++- src/Algebra/Module.agda | 1 - 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 200f618201..7c4801dd11 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -950,6 +950,12 @@ New modules Data.Vec.Relation.Unary.Linked.Properties ``` +* Proofs of some axioms of linearity: + ``` + Algebra.Module.Properties + Algebra.Module.Morphism.Linear.Core + Algebra.Module.Morphism.Linear.Properties + ``` Other minor changes ------------------- diff --git a/GenerateEverything.hs b/GenerateEverything.hs index 04da69aa0f..093689d5bb 100644 --- a/GenerateEverything.hs +++ b/GenerateEverything.hs @@ -29,7 +29,8 @@ srcDir = "src" unsafeModules :: [FilePath] unsafeModules = map modToFile - [ "Codata.Musical.Colist" + [ "Algebra.Module.Morphism.Linear.Properties" + , "Codata.Musical.Colist" , "Codata.Musical.Colist.Base" , "Codata.Musical.Colist.Properties" , "Codata.Musical.Colist.Bisimilarity" diff --git a/src/Algebra/Module.agda b/src/Algebra/Module.agda index b7f6e52a21..5cc1379acc 100644 --- a/src/Algebra/Module.agda +++ b/src/Algebra/Module.agda @@ -14,4 +14,3 @@ open import Algebra.Module.Structures public open import Algebra.Module.Structures.Biased public open import Algebra.Module.Bundles public open import Algebra.Module.Definitions public - From b6c7519530f1470396fedf1b8b29727151893be0 Mon Sep 17 00:00:00 2001 From: David Banas Date: Wed, 11 May 2022 05:55:03 -0700 Subject: [PATCH 04/19] Second attempt at PR1767. --- .gitignore | 2 - CHANGELOG.md | 4 +- GenerateEverything.hs | 3 +- src/Algebra/Module/Bundles.agda | 5 + src/Algebra/Module/Morphism/Linear/Core.agda | 132 --------- .../Module/Morphism/Linear/Properties.agda | 267 ++++++++++++------ 6 files changed, 181 insertions(+), 232 deletions(-) delete mode 100644 src/Algebra/Module/Morphism/Linear/Core.agda diff --git a/.gitignore b/.gitignore index 99f960e19f..d3516eb0f2 100644 --- a/.gitignore +++ b/.gitignore @@ -11,8 +11,6 @@ *.vim *~ .*.swp -.#* -\#* ./_build/* .DS_Store .vscode/* diff --git a/CHANGELOG.md b/CHANGELOG.md index 7c4801dd11..bf4a493441 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -952,9 +952,9 @@ New modules * Proofs of some axioms of linearity: ``` - Algebra.Module.Properties - Algebra.Module.Morphism.Linear.Core + Algebra.Module.Bundles Algebra.Module.Morphism.Linear.Properties + Algebra.Module.Properties ``` Other minor changes diff --git a/GenerateEverything.hs b/GenerateEverything.hs index 093689d5bb..04da69aa0f 100644 --- a/GenerateEverything.hs +++ b/GenerateEverything.hs @@ -29,8 +29,7 @@ srcDir = "src" unsafeModules :: [FilePath] unsafeModules = map modToFile - [ "Algebra.Module.Morphism.Linear.Properties" - , "Codata.Musical.Colist" + [ "Codata.Musical.Colist" , "Codata.Musical.Colist.Base" , "Codata.Musical.Colist.Properties" , "Codata.Musical.Colist.Bisimilarity" diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index ffabbbf2de..d99c859165 100644 --- a/src/Algebra/Module/Bundles.agda +++ b/src/Algebra/Module/Bundles.agda @@ -30,6 +30,7 @@ open import Algebra.Core 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 @@ -333,3 +334,7 @@ record Module (commutativeRing : CommutativeRing r ℓr) m ℓm semimodule = record { isSemimodule = isSemimodule } open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm) + + -ᴹ‿involutive : {x : Carrierᴹ} → -ᴹ (-ᴹ x) ≈ᴹ x + -ᴹ‿involutive {x = x} = ⁻¹-involutive +ᴹ-group x + diff --git a/src/Algebra/Module/Morphism/Linear/Core.agda b/src/Algebra/Module/Morphism/Linear/Core.agda deleted file mode 100644 index 04c1c2431e..0000000000 --- a/src/Algebra/Module/Morphism/Linear/Core.agda +++ /dev/null @@ -1,132 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Core definitions for linear maps. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -module Algebra.Module.Morphism.Linear.Core where - -import Algebra.Module.Properties as Properties -import Function.Definitions -import Relation.Binary.Reasoning.Setoid as Reasoning - -open import Algebra using (CommutativeRing) -open import Algebra.Module using (Module) -open import Level using (Level; _⊔_; suc) -open import Relation.Binary using (Rel; Setoid; IsEquivalence) -open import Relation.Binary.PropositionalEquality - using (_≡_; refl; trans; sym) -open import Relation.Nullary using (¬_) - -module _ - {r ℓr m ℓm : Level} - {ring : CommutativeRing r ℓr} - (modA : Module ring m ℓm) - (modB : Module ring m ℓm) - where - - lm = suc (ℓm ⊔ m ⊔ r) - record LinMap : Set lm where - - constructor mkLM - - open Module modA public - using () renaming - ( Carrierᴹ to A - ; _+ᴹ_ to _+ᴬ_ - ; _*ₗ_ to _·ᴬ_ - ; -ᴹ_ to -ᴬ_ - ; _≈ᴹ_ to _≈ᴬ_ - ; 0ᴹ to 0ᴬ - ; +ᴹ-comm to +ᴬ-comm - ; +ᴹ-congˡ to +ᴬ-congˡ - ; +ᴹ-congʳ to +ᴬ-congʳ - ; *ₗ-zeroˡ to ·ᴬ-zeroˡ - ; -ᴹ‿cong to -ᴬ‿cong - ; -ᴹ‿inverseʳ to -ᴬ‿inverseʳ - ; uniqueʳ‿-ᴹ to uniqueʳ‿-ᴬ - ; ≈ᴹ-setoid to ≈ᴬ-setoid - ; ≈ᴹ-sym to symᴬ - ; leftSemimodule to leftSemimoduleᴬ - ) - open Properties leftSemimoduleᴬ public - using () renaming - ( non-zeroʳ to non-zeroʳᴬ - ; non-zeroˡ to non-zeroˡᴬ - ) - - open Module modB public - using () renaming - ( Carrierᴹ to B - ; _+ᴹ_ to _+ᴮ_ - ; _*ₗ_ to _·ᴮ_ - ; -ᴹ_ to -ᴮ_ - ; _≈ᴹ_ to _≈ᴮ_ - ; 0ᴹ to 0ᴮ - ; +ᴹ-comm to +ᴮ-comm - ; +ᴹ-congˡ to +ᴮ-congˡ - ; +ᴹ-congʳ to +ᴮ-congʳ - ; *ₗ-zeroˡ to ·ᴮ-zeroˡ - ; -ᴹ‿cong to -ᴮ‿cong - ; -ᴹ‿inverseʳ to -ᴮ‿inverseʳ - ; uniqueʳ‿-ᴹ to uniqueʳ‿-ᴮ - ; ≈ᴹ-setoid to ≈ᴮ-setoid - ; ≈ᴹ-sym to symᴮ - ; leftSemimodule to leftSemimoduleᴮ - ) - open Properties leftSemimoduleᴮ public - using () renaming - ( non-zeroʳ to non-zeroʳᴮ - ; non-zeroˡ to non-zeroˡᴮ - ) - - open CommutativeRing ring public - using () renaming - ( Carrier to S - ; 0# to 𝟘 - ; 1# to 𝟙 - ) - open module Reasoningᴬ = Reasoning ≈ᴬ-setoid public - using () renaming - ( begin_ to beginᴬ_ - ; _∎ to _∎ᴬ - ) - infixr 2 step-≈ᴬ - step-≈ᴬ = Reasoningᴬ.step-≈ - syntax step-≈ᴬ x y≈z x≈y = x ≈ᴬ⟨ x≈y ⟩ y≈z - open module Reasoningᴮ = Reasoning ≈ᴮ-setoid public - open Function.Definitions _≈ᴬ_ _≈ᴮ_ - - field - f : A → B - adds : ∀ {a₁ a₂ : A} → f (a₁ +ᴬ a₂) ≈ᴮ f a₁ +ᴮ f a₂ - scales : ∀ {s : S} {a : A} → f (s ·ᴬ a) ≈ᴮ s ·ᴮ f a - f-cong : Congruent f - ¬-involutive-≈ᴬ : {a₁ a₂ : A} → ¬ (¬ (a₁ ≈ᴬ a₂)) → a₁ ≈ᴬ a₂ - ¬-involutive-≈ᴮ : {b₁ b₂ : B} → ¬ (¬ (b₁ ≈ᴮ b₂)) → b₁ ≈ᴮ b₂ - -ᴬ‿involutive : {a : A} → -ᴬ (-ᴬ a) ≈ᴬ a - -ᴮ‿involutive : {b : B} → -ᴮ (-ᴮ b) ≈ᴮ b - - _≉ᴬ_ : A → A → Set ℓm - x ≉ᴬ y = ¬ (x ≈ᴬ y) - - _≉ᴮ_ : B → B → Set ℓm - x ≉ᴮ y = ¬ (x ≈ᴮ y) - - _≈ᴸᴹ_ : Rel LinMap m - lm₁ ≈ᴸᴹ lm₂ = f ≡ f - - isEquivalence : IsEquivalence _≈ᴸᴹ_ - isEquivalence = record - { refl = refl - ; sym = sym - ; trans = trans - } - - open IsEquivalence isEquivalence public - - ≈ᴸᴹ-setoid : Setoid lm m - ≈ᴸᴹ-setoid = record { isEquivalence = isEquivalence } - -- open LinMap public diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index cc9897e49a..bcff83cdd8 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -4,124 +4,203 @@ -- Properties of linear maps. ------------------------------------------------------------------------ -{-# OPTIONS --without-K #-} +{-# OPTIONS --without-K --safe #-} -module Algebra.Module.Morphism.Linear.Properties where +open import Algebra using (CommutativeRing) +open import Algebra.Module using (Module) +open import Level using (Level; _⊔_) + +module Algebra.Module.Morphism.Linear.Properties + {r ℓr m ℓm : Level} + {ring : CommutativeRing r ℓr} + (modA modB : Module ring m ℓm) + where + +import Algebra.Module.Properties as Properties +import Function.Definitions +import Relation.Binary.Reasoning.Setoid as Reasoning +import Algebra.Module.Morphism.Structures as MorphismStructures open import Agda.Builtin.Sigma -open import Algebra using (CommutativeRing) --- open import Algebra.Lattice.Properties.BooleanAlgebra using (¬-involutive) -open import Algebra.Module using (Module) -open import Algebra.Module.Morphism.Linear.Core -open import Axiom.Extensionality.Propositional using (Extensionality) +open import Axiom.DoubleNegationElimination open import Data.List -open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax; _×_) -open import Function using (_↔_; mk↔; id; const) -open import Level using (Level; _⊔_) +open import Data.Product + using (Σ; _,_; ∃; Σ-syntax; ∃-syntax; _×_) open import Relation.Nullary using (¬_) open import Relation.Nullary.Negation using (contraposition) -private - variable - ℓ₁ ℓ₂ r ℓr m ℓm : Level - ring : CommutativeRing r ℓr - modA modB : Module ring m ℓm - -postulate - extensionality : Extensionality ℓ₁ ℓ₂ - -- ≡-involutive : ∀ {A : Set ℓ₁} → {x y : A} → ¬ (x ≢ y) → x ≡ y +open MorphismStructures.ModuleMorphisms modA modB +open Module modA + using () renaming + ( Carrierᴹ to A + ; _+ᴹ_ to _+ᴬ_ + ; _*ₗ_ to _·ᴬ_ + ; -ᴹ_ to -ᴬ_ + ; _≈ᴹ_ to _≈ᴬ_ + ; 0ᴹ to 0ᴬ + ; +ᴹ-comm to +ᴬ-comm + ; +ᴹ-congˡ to +ᴬ-congˡ + ; +ᴹ-congʳ to +ᴬ-congʳ + ; *ₗ-zeroˡ to ·ᴬ-zeroˡ + ; -ᴹ‿cong to -ᴬ‿cong + ; -ᴹ‿inverseʳ to -ᴬ‿inverseʳ + ; -ᴹ‿involutive to -ᴬ‿involutive + ; uniqueʳ‿-ᴹ to uniqueʳ‿-ᴬ + ; ≈ᴹ-setoid to ≈ᴬ-setoid + ; ≈ᴹ-sym to symᴬ + ; leftSemimodule to leftSemimoduleᴬ + ) +open Properties leftSemimoduleᴬ public + using () renaming + ( non-zeroʳ to non-zeroʳᴬ + ; non-zeroˡ to non-zeroˡᴬ + ) +open Module modB + using () renaming + ( Carrierᴹ to B + ; _+ᴹ_ to _+ᴮ_ + ; _*ₗ_ to _·ᴮ_ + ; -ᴹ_ to -ᴮ_ + ; _≈ᴹ_ to _≈ᴮ_ + ; 0ᴹ to 0ᴮ + ; +ᴹ-comm to +ᴮ-comm + ; +ᴹ-congˡ to +ᴮ-congˡ + ; +ᴹ-congʳ to +ᴮ-congʳ + ; *ₗ-zeroˡ to ·ᴮ-zeroˡ + ; -ᴹ‿cong to -ᴮ‿cong + ; -ᴹ‿inverseʳ to -ᴮ‿inverseʳ + ; -ᴹ‿involutive to -ᴮ‿involutive + ; uniqueʳ‿-ᴹ to uniqueʳ‿-ᴮ + ; ≈ᴹ-setoid to ≈ᴮ-setoid + ; ≈ᴹ-sym to symᴮ + ; leftSemimodule to leftSemimoduleᴮ + ) +open Properties leftSemimoduleᴮ public + using () renaming + ( non-zeroʳ to non-zeroʳᴮ + ; non-zeroˡ to non-zeroˡᴮ + ) +open CommutativeRing ring public + using () renaming + ( Carrier to S + ; 0# to 𝟘 + ; 1# to 𝟙 + ) +open module Reasoningᴬ = Reasoning ≈ᴬ-setoid public + using () renaming + ( begin_ to beginᴬ_ + ; _∎ to _∎ᴬ + ) +infixr 2 step-≈ᴬ +step-≈ᴬ = Reasoningᴬ.step-≈ +syntax step-≈ᴬ x y≈z x≈y = x ≈ᴬ⟨ x≈y ⟩ y≈z +open module Reasoningᴮ = Reasoning ≈ᴮ-setoid public +open Function.Definitions _≈ᴬ_ _≈ᴮ_ + +_≉ᴬ_ : A → A → Set ℓm +x ≉ᴬ y = ¬ (x ≈ᴬ y) + +_≉ᴮ_ : B → B → Set ℓm +x ≉ᴮ y = ¬ (x ≈ᴮ y) -module _ (lm : LinMap modA modB) where +module _ + {⟦_⟧ : A → B} + (isModuleHomomorphism : IsModuleHomomorphism ⟦_⟧) + where - open LinMap lm + open IsModuleHomomorphism isModuleHomomorphism -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f - f𝟘≈𝟘 : {x : A} → f 0ᴬ ≈ᴮ 0ᴮ + f𝟘≈𝟘 : {x : A} → ⟦ 0ᴬ ⟧ ≈ᴮ 0ᴮ f𝟘≈𝟘 {x = x} = begin - f 0ᴬ ≈⟨ f-cong (symᴬ (·ᴬ-zeroˡ x)) ⟩ - f (𝟘 ·ᴬ x) ≈⟨ scales ⟩ - 𝟘 ·ᴮ f x ≈⟨ ·ᴮ-zeroˡ (f x) ⟩ + ⟦ 0ᴬ ⟧ ≈⟨ ⟦⟧-cong (symᴬ (·ᴬ-zeroˡ x)) ⟩ + ⟦ (𝟘 ·ᴬ x) ⟧ ≈⟨ *ₗ-homo 𝟘 x ⟩ + 𝟘 ·ᴮ ⟦ x ⟧ ≈⟨ ·ᴮ-zeroˡ ⟦ x ⟧ ⟩ 0ᴮ ∎ - x≈𝟘→fx≈𝟘 : {x : A} → x ≈ᴬ 0ᴬ → f x ≈ᴮ 0ᴮ + x≈𝟘→fx≈𝟘 : {x : A} → x ≈ᴬ 0ᴬ → ⟦ x ⟧ ≈ᴮ 0ᴮ x≈𝟘→fx≈𝟘 {x = x} x≈𝟘 = begin - f x ≈⟨ f-cong x≈𝟘 ⟩ - f 0ᴬ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ + ⟦ x ⟧ ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ + ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ 0ᴮ ∎ - fx≉𝟘→x≉𝟘 : {x : A} → f x ≉ᴮ 0ᴮ → x ≉ᴬ 0ᴬ + fx≉𝟘→x≉𝟘 : {x : A} → ⟦ x ⟧ ≉ᴮ 0ᴮ → x ≉ᴬ 0ᴬ fx≉𝟘→x≉𝟘 = contraposition x≈𝟘→fx≈𝟘 -- Zero is a unique output of linear map ≉ `const 𝟘`. zero-unique : {x : A} → - Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (f y ≉ᴮ 0ᴮ)) → - x ≉ᴬ 0ᴬ → f x ≉ᴮ 0ᴮ + Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (⟦ y ⟧ ≉ᴮ 0ᴮ)) → + x ≉ᴬ 0ᴬ → ⟦ x ⟧ ≉ᴮ 0ᴮ zero-unique {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 = - let y≉𝟘 : y ≉ᴬ 0ᴬ - y≉𝟘 = fx≉𝟘→x≉𝟘 fy≉𝟘 - fs·x≈fy : f (s ·ᴬ x) ≈ᴮ f y - fs·x≈fy = f-cong s·x≈y - s·fx≈fy : s ·ᴮ f x ≈ᴮ f y - s·fx≈fy = begin - s ·ᴮ f x ≈⟨ symᴮ scales ⟩ - f (s ·ᴬ x) ≈⟨ fs·x≈fy ⟩ - f y ∎ - s·fx≉𝟘 : (s ·ᴮ f x) ≉ᴮ 0ᴮ - s·fx≉𝟘 = λ s·fx≈𝟘 → - fy≉𝟘 ( begin - f y ≈⟨ f-cong (symᴬ s·x≈y) ⟩ - f (s ·ᴬ x) ≈⟨ scales ⟩ - s ·ᴮ f x ≈⟨ s·fx≈𝟘 ⟩ - 0ᴮ ∎ - ) - in non-zeroʳᴮ s·fx≉𝟘 - - fx≈𝟘⇒x≈𝟘 : {x : A} → - Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (f y ≉ᴮ 0ᴮ)) → - f x ≈ᴮ 0ᴮ → x ≈ᴬ 0ᴬ - fx≈𝟘⇒x≈𝟘 {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) fx≈𝟘 = - let ¬x≉𝟘 : ¬ (x ≉ᴬ 0ᴬ) - ¬x≉𝟘 = λ x≉𝟘 → zero-unique ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 fx≈𝟘 - in ¬-involutive-≈ᴬ ¬x≉𝟘 - + non-zeroʳᴮ s·fx≉𝟘 + where + y≉𝟘 : y ≉ᴬ 0ᴬ + y≉𝟘 = fx≉𝟘→x≉𝟘 fy≉𝟘 + fs·x≈fy : ⟦ (s ·ᴬ x) ⟧ ≈ᴮ ⟦ y ⟧ + fs·x≈fy = ⟦⟧-cong s·x≈y + s·fx≈fy : s ·ᴮ ⟦ x ⟧ ≈ᴮ ⟦ y ⟧ + s·fx≈fy = begin + s ·ᴮ ⟦ x ⟧ ≈⟨ symᴮ (*ₗ-homo s x) ⟩ + ⟦ (s ·ᴬ x) ⟧ ≈⟨ fs·x≈fy ⟩ + ⟦ y ⟧ ∎ + s·fx≉𝟘 : (s ·ᴮ ⟦ x ⟧) ≉ᴮ 0ᴮ + s·fx≉𝟘 = λ s·fx≈𝟘 → + fy≉𝟘 ( begin + ⟦ y ⟧ ≈⟨ ⟦⟧-cong (symᴬ s·x≈y) ⟩ + ⟦ (s ·ᴬ x) ⟧ ≈⟨ *ₗ-homo s x ⟩ + s ·ᴮ ⟦ x ⟧ ≈⟨ s·fx≈𝟘 ⟩ + 0ᴮ ∎ + ) + -- f is odd (i.e. - f (-x) ≈ - (f x)). - fx+f-x≈𝟘 : {x : A} → f x +ᴮ f (-ᴬ x) ≈ᴮ 0ᴮ + fx+f-x≈𝟘 : {x : A} → ⟦ x ⟧ +ᴮ ⟦ (-ᴬ x) ⟧ ≈ᴮ 0ᴮ fx+f-x≈𝟘 {x = x} = begin - f x +ᴮ f (-ᴬ x) ≈⟨ symᴮ adds ⟩ - f (x +ᴬ (-ᴬ x)) ≈⟨ f-cong (-ᴬ‿inverseʳ x) ⟩ - f 0ᴬ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ + ⟦ x ⟧ +ᴮ ⟦ (-ᴬ x) ⟧ ≈⟨ symᴮ (+ᴹ-homo x (-ᴬ x)) ⟩ + ⟦ (x +ᴬ (-ᴬ x)) ⟧ ≈⟨ ⟦⟧-cong (-ᴬ‿inverseʳ x) ⟩ + ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ 0ᴮ ∎ - f-x≈-fx : {x : A} → f (-ᴬ x) ≈ᴮ -ᴮ (f x) - f-x≈-fx {x = x} = uniqueʳ‿-ᴮ (f x) (f (-ᴬ x)) fx+f-x≈𝟘 - - -- A non-trivial linear function is injective. - inj-lm : {x y : A} → - Σ[ (s , z) ∈ S × A ] ((s ·ᴬ (x +ᴬ -ᴬ y) ≈ᴬ z) × (f z ≉ᴮ 0ᴮ)) → - f x ≈ᴮ f y → x ≈ᴬ y - inj-lm {x = x} {y = y} ((s , z) , (s·[x-y]≈z , fz≉𝟘)) fx≈fy = - let fx-fy≈𝟘 : f x +ᴮ (-ᴮ f y) ≈ᴮ 0ᴮ - fx-fy≈𝟘 = begin - f x +ᴮ (-ᴮ f y) ≈⟨ +ᴮ-congˡ (-ᴮ‿cong (symᴮ fx≈fy)) ⟩ - f x +ᴮ (-ᴮ f x) ≈⟨ -ᴮ‿inverseʳ (f x) ⟩ - 0ᴮ ∎ - fx-y≈𝟘 : f (x +ᴬ (-ᴬ y)) ≈ᴮ 0ᴮ - fx-y≈𝟘 = begin - f (x +ᴬ (-ᴬ y)) ≈⟨ adds ⟩ - f x +ᴮ f (-ᴬ y) ≈⟨ +ᴮ-congˡ f-x≈-fx ⟩ - f x +ᴮ (-ᴮ (f y)) ≈⟨ fx-fy≈𝟘 ⟩ - 0ᴮ ∎ - x-y≈𝟘 : x +ᴬ (-ᴬ y) ≈ᴬ 0ᴬ - x-y≈𝟘 = fx≈𝟘⇒x≈𝟘 {x = x +ᴬ (-ᴬ y)} ((s , z) , s·[x-y]≈z , fz≉𝟘) fx-y≈𝟘 - x≈--y : x ≈ᴬ -ᴬ (-ᴬ y) - x≈--y = uniqueʳ‿-ᴬ (-ᴬ y) x - ( beginᴬ - -ᴬ y +ᴬ x ≈ᴬ⟨ +ᴬ-comm (-ᴬ y) x ⟩ - x +ᴬ -ᴬ y ≈ᴬ⟨ x-y≈𝟘 ⟩ - 0ᴬ ∎ᴬ - ) - in beginᴬ - x ≈ᴬ⟨ x≈--y ⟩ - -ᴬ (-ᴬ y) ≈ᴬ⟨ -ᴬ‿involutive ⟩ - y ∎ᴬ + f-x≈-fx : {x : A} → ⟦ (-ᴬ x) ⟧ ≈ᴮ -ᴮ ⟦ x ⟧ + f-x≈-fx {x = x} = uniqueʳ‿-ᴮ ⟦ x ⟧ ⟦ -ᴬ x ⟧ fx+f-x≈𝟘 + module _ {dne : DoubleNegationElimination _} where + + fx≈𝟘⇒x≈𝟘 : {x : A} → + Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (⟦ y ⟧ ≉ᴮ 0ᴮ)) → + ⟦ x ⟧ ≈ᴮ 0ᴮ → x ≈ᴬ 0ᴬ + fx≈𝟘⇒x≈𝟘 {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) fx≈𝟘 = + dne ¬x≉𝟘 + where + ¬x≉𝟘 : ¬ (x ≉ᴬ 0ᴬ) + ¬x≉𝟘 = λ x≉𝟘 → zero-unique ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 fx≈𝟘 + + -- A non-trivial linear function is injective. + inj-lm : {x y : A} → + Σ[ (s , z) ∈ S × A ] ((s ·ᴬ (x +ᴬ -ᴬ y) ≈ᴬ z) × (⟦ z ⟧ ≉ᴮ 0ᴮ)) → + ⟦ x ⟧ ≈ᴮ ⟦ y ⟧ → x ≈ᴬ y + inj-lm {x = x} {y = y} ((s , z) , (s·[x-y]≈z , fz≉𝟘)) fx≈fy = + beginᴬ + x ≈ᴬ⟨ x≈--y ⟩ + -ᴬ (-ᴬ y) ≈ᴬ⟨ -ᴬ‿involutive ⟩ + y ∎ᴬ + where + fx-fy≈𝟘 : ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈ᴮ 0ᴮ + fx-fy≈𝟘 = begin + ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈⟨ +ᴮ-congˡ (-ᴮ‿cong (symᴮ fx≈fy)) ⟩ + ⟦ x ⟧ +ᴮ (-ᴮ ⟦ x ⟧) ≈⟨ -ᴮ‿inverseʳ (⟦ x ⟧) ⟩ + 0ᴮ ∎ + fx-y≈𝟘 : ⟦ (x +ᴬ (-ᴬ y)) ⟧ ≈ᴮ 0ᴮ + fx-y≈𝟘 = begin + ⟦ x +ᴬ (-ᴬ y) ⟧ ≈⟨ +ᴹ-homo x (-ᴬ y) ⟩ + ⟦ x ⟧ +ᴮ ⟦ -ᴬ y ⟧ ≈⟨ +ᴮ-congˡ f-x≈-fx ⟩ + ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈⟨ fx-fy≈𝟘 ⟩ + 0ᴮ ∎ + x-y≈𝟘 : x +ᴬ (-ᴬ y) ≈ᴬ 0ᴬ + x-y≈𝟘 = fx≈𝟘⇒x≈𝟘 {x = x +ᴬ (-ᴬ y)} ((s , z) , s·[x-y]≈z , fz≉𝟘) fx-y≈𝟘 + x≈--y : x ≈ᴬ -ᴬ (-ᴬ y) + x≈--y = uniqueʳ‿-ᴬ (-ᴬ y) x + ( beginᴬ + -ᴬ y +ᴬ x ≈ᴬ⟨ +ᴬ-comm (-ᴬ y) x ⟩ + x +ᴬ -ᴬ y ≈ᴬ⟨ x-y≈𝟘 ⟩ + 0ᴬ ∎ᴬ + ) From 7c205f91924022c42c432b10bc742ae943fdfe8c Mon Sep 17 00:00:00 2001 From: David Banas Date: Fri, 13 May 2022 09:58:39 -0700 Subject: [PATCH 05/19] Removed some unneeded `public`s. --- .../Module/Morphism/Linear/Properties.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index bcff83cdd8..bcda42c266 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -50,7 +50,7 @@ open Module modA ; ≈ᴹ-sym to symᴬ ; leftSemimodule to leftSemimoduleᴬ ) -open Properties leftSemimoduleᴬ public +open Properties leftSemimoduleᴬ using () renaming ( non-zeroʳ to non-zeroʳᴬ ; non-zeroˡ to non-zeroˡᴬ @@ -75,18 +75,18 @@ open Module modB ; ≈ᴹ-sym to symᴮ ; leftSemimodule to leftSemimoduleᴮ ) -open Properties leftSemimoduleᴮ public +open Properties leftSemimoduleᴮ using () renaming ( non-zeroʳ to non-zeroʳᴮ ; non-zeroˡ to non-zeroˡᴮ ) -open CommutativeRing ring public - using () renaming +open CommutativeRing ring + using (_≈_; _*_; _+_) renaming ( Carrier to S ; 0# to 𝟘 ; 1# to 𝟙 ) -open module Reasoningᴬ = Reasoning ≈ᴬ-setoid public +open module Reasoningᴬ = Reasoning ≈ᴬ-setoid using () renaming ( begin_ to beginᴬ_ ; _∎ to _∎ᴬ @@ -94,7 +94,7 @@ open module Reasoningᴬ = Reasoning ≈ᴬ-setoid public infixr 2 step-≈ᴬ step-≈ᴬ = Reasoningᴬ.step-≈ syntax step-≈ᴬ x y≈z x≈y = x ≈ᴬ⟨ x≈y ⟩ y≈z -open module Reasoningᴮ = Reasoning ≈ᴮ-setoid public +open module Reasoningᴮ = Reasoning ≈ᴮ-setoid open Function.Definitions _≈ᴬ_ _≈ᴮ_ _≉ᴬ_ : A → A → Set ℓm @@ -123,7 +123,7 @@ module _ ⟦ x ⟧ ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ 0ᴮ ∎ - + fx≉𝟘→x≉𝟘 : {x : A} → ⟦ x ⟧ ≉ᴮ 0ᴮ → x ≉ᴬ 0ᴬ fx≉𝟘→x≉𝟘 = contraposition x≈𝟘→fx≈𝟘 @@ -173,7 +173,7 @@ module _ where ¬x≉𝟘 : ¬ (x ≉ᴬ 0ᴬ) ¬x≉𝟘 = λ x≉𝟘 → zero-unique ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 fx≈𝟘 - + -- A non-trivial linear function is injective. inj-lm : {x y : A} → Σ[ (s , z) ∈ S × A ] ((s ·ᴬ (x +ᴬ -ᴬ y) ≈ᴬ z) × (⟦ z ⟧ ≉ᴮ 0ᴮ)) → From ea7368322d3e6a76bb1e23b3afca70b412aeb655 Mon Sep 17 00:00:00 2001 From: David Banas Date: Sat, 14 May 2022 10:11:18 -0700 Subject: [PATCH 06/19] Shifted to proof-local reasoning module openning, as per Jacques. --- .../Module/Morphism/Linear/Properties.agda | 79 ++++++++++++------- 1 file changed, 50 insertions(+), 29 deletions(-) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index bcda42c266..f77ac855c0 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -86,15 +86,15 @@ open CommutativeRing ring ; 0# to 𝟘 ; 1# to 𝟙 ) -open module Reasoningᴬ = Reasoning ≈ᴬ-setoid - using () renaming - ( begin_ to beginᴬ_ - ; _∎ to _∎ᴬ - ) -infixr 2 step-≈ᴬ -step-≈ᴬ = Reasoningᴬ.step-≈ -syntax step-≈ᴬ x y≈z x≈y = x ≈ᴬ⟨ x≈y ⟩ y≈z -open module Reasoningᴮ = Reasoning ≈ᴮ-setoid +-- open module Reasoningᴬ = Reasoning ≈ᴬ-setoid +-- using () renaming +-- ( begin_ to beginᴬ_ +-- ; _∎ to _∎ᴬ +-- ) +-- infixr 2 step-≈ᴬ +-- step-≈ᴬ = Reasoningᴬ.step-≈ +-- syntax step-≈ᴬ x y≈z x≈y = x ≈ᴬ⟨ x≈y ⟩ y≈z +-- open module Reasoningᴮ = Reasoning ≈ᴮ-setoid open Function.Definitions _≈ᴬ_ _≈ᴮ_ _≉ᴬ_ : A → A → Set ℓm @@ -109,6 +109,7 @@ module _ where open IsModuleHomomorphism isModuleHomomorphism + -- open Reasoning ≈ᴮ-setoid -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f f𝟘≈𝟘 : {x : A} → ⟦ 0ᴬ ⟧ ≈ᴮ 0ᴮ @@ -117,12 +118,14 @@ module _ ⟦ (𝟘 ·ᴬ x) ⟧ ≈⟨ *ₗ-homo 𝟘 x ⟩ 𝟘 ·ᴮ ⟦ x ⟧ ≈⟨ ·ᴮ-zeroˡ ⟦ x ⟧ ⟩ 0ᴮ ∎ + where open Reasoning ≈ᴮ-setoid x≈𝟘→fx≈𝟘 : {x : A} → x ≈ᴬ 0ᴬ → ⟦ x ⟧ ≈ᴮ 0ᴮ x≈𝟘→fx≈𝟘 {x = x} x≈𝟘 = begin ⟦ x ⟧ ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ 0ᴮ ∎ + where open Reasoning ≈ᴮ-setoid fx≉𝟘→x≉𝟘 : {x : A} → ⟦ x ⟧ ≉ᴮ 0ᴮ → x ≉ᴬ 0ᴬ fx≉𝟘→x≉𝟘 = contraposition x≈𝟘→fx≈𝟘 @@ -133,7 +136,9 @@ module _ x ≉ᴬ 0ᴬ → ⟦ x ⟧ ≉ᴮ 0ᴮ zero-unique {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 = non-zeroʳᴮ s·fx≉𝟘 + -- where where + open Reasoning ≈ᴮ-setoid y≉𝟘 : y ≉ᴬ 0ᴬ y≉𝟘 = fx≉𝟘→x≉𝟘 fy≉𝟘 fs·x≈fy : ⟦ (s ·ᴬ x) ⟧ ≈ᴮ ⟦ y ⟧ @@ -159,6 +164,7 @@ module _ ⟦ (x +ᴬ (-ᴬ x)) ⟧ ≈⟨ ⟦⟧-cong (-ᴬ‿inverseʳ x) ⟩ ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ 0ᴮ ∎ + where open Reasoning ≈ᴮ-setoid f-x≈-fx : {x : A} → ⟦ (-ᴬ x) ⟧ ≈ᴮ -ᴮ ⟦ x ⟧ f-x≈-fx {x = x} = uniqueʳ‿-ᴮ ⟦ x ⟧ ⟦ -ᴬ x ⟧ fx+f-x≈𝟘 @@ -175,32 +181,47 @@ module _ ¬x≉𝟘 = λ x≉𝟘 → zero-unique ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 fx≈𝟘 -- A non-trivial linear function is injective. + fx-fy≈𝟘 : {x y : A} {fx≈fy : ⟦ x ⟧ ≈ᴮ ⟦ y ⟧} → ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈ᴮ 0ᴮ + fx-fy≈𝟘 {x = x} {y = y} {fx≈fy = fx≈fy} = begin + ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈⟨ +ᴮ-congˡ (-ᴮ‿cong (symᴮ fx≈fy)) ⟩ + ⟦ x ⟧ +ᴮ (-ᴮ ⟦ x ⟧) ≈⟨ -ᴮ‿inverseʳ (⟦ x ⟧) ⟩ + 0ᴮ ∎ + where open Reasoning ≈ᴮ-setoid + + fx-y≈𝟘 : {x y : A} {fx≈fy : ⟦ x ⟧ ≈ᴮ ⟦ y ⟧} → ⟦ (x +ᴬ (-ᴬ y)) ⟧ ≈ᴮ 0ᴮ + fx-y≈𝟘 {x = x} {y = y} {fx≈fy = fx≈fy} = begin + ⟦ x +ᴬ (-ᴬ y) ⟧ ≈⟨ +ᴹ-homo x (-ᴬ y) ⟩ + ⟦ x ⟧ +ᴮ ⟦ -ᴬ y ⟧ ≈⟨ +ᴮ-congˡ f-x≈-fx ⟩ + ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈⟨ fx-fy≈𝟘 {fx≈fy = fx≈fy} ⟩ + 0ᴮ ∎ + where open Reasoning ≈ᴮ-setoid + inj-lm : {x y : A} → Σ[ (s , z) ∈ S × A ] ((s ·ᴬ (x +ᴬ -ᴬ y) ≈ᴬ z) × (⟦ z ⟧ ≉ᴮ 0ᴮ)) → ⟦ x ⟧ ≈ᴮ ⟦ y ⟧ → x ≈ᴬ y inj-lm {x = x} {y = y} ((s , z) , (s·[x-y]≈z , fz≉𝟘)) fx≈fy = - beginᴬ - x ≈ᴬ⟨ x≈--y ⟩ - -ᴬ (-ᴬ y) ≈ᴬ⟨ -ᴬ‿involutive ⟩ - y ∎ᴬ + -- beginᴬ + -- x ≈ᴬ⟨ x≈--y ⟩ + -- -ᴬ (-ᴬ y) ≈ᴬ⟨ -ᴬ‿involutive ⟩ + -- y ∎ᴬ + begin + x ≈⟨ x≈--y ⟩ + -ᴬ (-ᴬ y) ≈⟨ -ᴬ‿involutive ⟩ + y ∎ where - fx-fy≈𝟘 : ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈ᴮ 0ᴮ - fx-fy≈𝟘 = begin - ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈⟨ +ᴮ-congˡ (-ᴮ‿cong (symᴮ fx≈fy)) ⟩ - ⟦ x ⟧ +ᴮ (-ᴮ ⟦ x ⟧) ≈⟨ -ᴮ‿inverseʳ (⟦ x ⟧) ⟩ - 0ᴮ ∎ - fx-y≈𝟘 : ⟦ (x +ᴬ (-ᴬ y)) ⟧ ≈ᴮ 0ᴮ - fx-y≈𝟘 = begin - ⟦ x +ᴬ (-ᴬ y) ⟧ ≈⟨ +ᴹ-homo x (-ᴬ y) ⟩ - ⟦ x ⟧ +ᴮ ⟦ -ᴬ y ⟧ ≈⟨ +ᴮ-congˡ f-x≈-fx ⟩ - ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈⟨ fx-fy≈𝟘 ⟩ - 0ᴮ ∎ + open Reasoning ≈ᴬ-setoid x-y≈𝟘 : x +ᴬ (-ᴬ y) ≈ᴬ 0ᴬ - x-y≈𝟘 = fx≈𝟘⇒x≈𝟘 {x = x +ᴬ (-ᴬ y)} ((s , z) , s·[x-y]≈z , fz≉𝟘) fx-y≈𝟘 + x-y≈𝟘 = fx≈𝟘⇒x≈𝟘 {x = x +ᴬ (-ᴬ y)} + ((s , z) , s·[x-y]≈z , fz≉𝟘) + (fx-y≈𝟘 {fx≈fy = fx≈fy}) x≈--y : x ≈ᴬ -ᴬ (-ᴬ y) x≈--y = uniqueʳ‿-ᴬ (-ᴬ y) x - ( beginᴬ - -ᴬ y +ᴬ x ≈ᴬ⟨ +ᴬ-comm (-ᴬ y) x ⟩ - x +ᴬ -ᴬ y ≈ᴬ⟨ x-y≈𝟘 ⟩ - 0ᴬ ∎ᴬ + -- ( beginᴬ + -- -ᴬ y +ᴬ x ≈ᴬ⟨ +ᴬ-comm (-ᴬ y) x ⟩ + -- x +ᴬ -ᴬ y ≈ᴬ⟨ x-y≈𝟘 ⟩ + -- 0ᴬ ∎ᴬ + ( begin + -ᴬ y +ᴬ x ≈⟨ +ᴬ-comm (-ᴬ y) x ⟩ + x +ᴬ -ᴬ y ≈⟨ x-y≈𝟘 ⟩ + 0ᴬ ∎ ) From c9c8798075afef71958fe5e3faa9e3555a0ba410 Mon Sep 17 00:00:00 2001 From: David Banas Date: Sat, 14 May 2022 10:19:31 -0700 Subject: [PATCH 07/19] Eliminated unneccesary `x`, as per Jacques. --- .../Module/Morphism/Linear/Properties.agda | 34 +++++-------------- 1 file changed, 8 insertions(+), 26 deletions(-) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index f77ac855c0..4a7bee97ca 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -38,6 +38,7 @@ open Module modA ; -ᴹ_ to -ᴬ_ ; _≈ᴹ_ to _≈ᴬ_ ; 0ᴹ to 0ᴬ + ; 1ᴹ to 1ᴬ ; +ᴹ-comm to +ᴬ-comm ; +ᴹ-congˡ to +ᴬ-congˡ ; +ᴹ-congʳ to +ᴬ-congʳ @@ -86,15 +87,6 @@ open CommutativeRing ring ; 0# to 𝟘 ; 1# to 𝟙 ) --- open module Reasoningᴬ = Reasoning ≈ᴬ-setoid --- using () renaming --- ( begin_ to beginᴬ_ --- ; _∎ to _∎ᴬ --- ) --- infixr 2 step-≈ᴬ --- step-≈ᴬ = Reasoningᴬ.step-≈ --- syntax step-≈ᴬ x y≈z x≈y = x ≈ᴬ⟨ x≈y ⟩ y≈z --- open module Reasoningᴮ = Reasoning ≈ᴮ-setoid open Function.Definitions _≈ᴬ_ _≈ᴮ_ _≉ᴬ_ : A → A → Set ℓm @@ -109,21 +101,20 @@ module _ where open IsModuleHomomorphism isModuleHomomorphism - -- open Reasoning ≈ᴮ-setoid -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f - f𝟘≈𝟘 : {x : A} → ⟦ 0ᴬ ⟧ ≈ᴮ 0ᴮ - f𝟘≈𝟘 {x = x} = begin - ⟦ 0ᴬ ⟧ ≈⟨ ⟦⟧-cong (symᴬ (·ᴬ-zeroˡ x)) ⟩ - ⟦ (𝟘 ·ᴬ x) ⟧ ≈⟨ *ₗ-homo 𝟘 x ⟩ - 𝟘 ·ᴮ ⟦ x ⟧ ≈⟨ ·ᴮ-zeroˡ ⟦ x ⟧ ⟩ + f𝟘≈𝟘 : ⟦ 0ᴬ ⟧ ≈ᴮ 0ᴮ + f𝟘≈𝟘 = begin + ⟦ 0ᴬ ⟧ ≈⟨ ⟦⟧-cong (symᴬ (·ᴬ-zeroˡ 0ᴬ)) ⟩ + ⟦ (𝟘 ·ᴬ 0ᴬ) ⟧ ≈⟨ *ₗ-homo 𝟘 0ᴬ ⟩ + 𝟘 ·ᴮ ⟦ 0ᴬ ⟧ ≈⟨ ·ᴮ-zeroˡ ⟦ 0ᴬ ⟧ ⟩ 0ᴮ ∎ where open Reasoning ≈ᴮ-setoid x≈𝟘→fx≈𝟘 : {x : A} → x ≈ᴬ 0ᴬ → ⟦ x ⟧ ≈ᴮ 0ᴮ x≈𝟘→fx≈𝟘 {x = x} x≈𝟘 = begin ⟦ x ⟧ ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ - ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ + ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 ⟩ 0ᴮ ∎ where open Reasoning ≈ᴮ-setoid @@ -136,7 +127,6 @@ module _ x ≉ᴬ 0ᴬ → ⟦ x ⟧ ≉ᴮ 0ᴮ zero-unique {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 = non-zeroʳᴮ s·fx≉𝟘 - -- where where open Reasoning ≈ᴮ-setoid y≉𝟘 : y ≉ᴬ 0ᴬ @@ -162,7 +152,7 @@ module _ fx+f-x≈𝟘 {x = x} = begin ⟦ x ⟧ +ᴮ ⟦ (-ᴬ x) ⟧ ≈⟨ symᴮ (+ᴹ-homo x (-ᴬ x)) ⟩ ⟦ (x +ᴬ (-ᴬ x)) ⟧ ≈⟨ ⟦⟧-cong (-ᴬ‿inverseʳ x) ⟩ - ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 {x = x} ⟩ + ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 ⟩ 0ᴮ ∎ where open Reasoning ≈ᴮ-setoid @@ -200,10 +190,6 @@ module _ Σ[ (s , z) ∈ S × A ] ((s ·ᴬ (x +ᴬ -ᴬ y) ≈ᴬ z) × (⟦ z ⟧ ≉ᴮ 0ᴮ)) → ⟦ x ⟧ ≈ᴮ ⟦ y ⟧ → x ≈ᴬ y inj-lm {x = x} {y = y} ((s , z) , (s·[x-y]≈z , fz≉𝟘)) fx≈fy = - -- beginᴬ - -- x ≈ᴬ⟨ x≈--y ⟩ - -- -ᴬ (-ᴬ y) ≈ᴬ⟨ -ᴬ‿involutive ⟩ - -- y ∎ᴬ begin x ≈⟨ x≈--y ⟩ -ᴬ (-ᴬ y) ≈⟨ -ᴬ‿involutive ⟩ @@ -216,10 +202,6 @@ module _ (fx-y≈𝟘 {fx≈fy = fx≈fy}) x≈--y : x ≈ᴬ -ᴬ (-ᴬ y) x≈--y = uniqueʳ‿-ᴬ (-ᴬ y) x - -- ( beginᴬ - -- -ᴬ y +ᴬ x ≈ᴬ⟨ +ᴬ-comm (-ᴬ y) x ⟩ - -- x +ᴬ -ᴬ y ≈ᴬ⟨ x-y≈𝟘 ⟩ - -- 0ᴬ ∎ᴬ ( begin -ᴬ y +ᴬ x ≈⟨ +ᴬ-comm (-ᴬ y) x ⟩ x +ᴬ -ᴬ y ≈⟨ x-y≈𝟘 ⟩ From c18c68a9430858a19326b04004c5d44139b5a6b0 Mon Sep 17 00:00:00 2001 From: David Banas Date: Sat, 14 May 2022 10:33:43 -0700 Subject: [PATCH 08/19] Reverted to `f` from semantic brackets, as per Jacques. --- .../Module/Morphism/Linear/Properties.agda | 77 +++++++++---------- 1 file changed, 38 insertions(+), 39 deletions(-) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index 4a7bee97ca..34f5246c6e 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -38,7 +38,6 @@ open Module modA ; -ᴹ_ to -ᴬ_ ; _≈ᴹ_ to _≈ᴬ_ ; 0ᴹ to 0ᴬ - ; 1ᴹ to 1ᴬ ; +ᴹ-comm to +ᴬ-comm ; +ᴹ-congˡ to +ᴬ-congˡ ; +ᴹ-congʳ to +ᴬ-congʳ @@ -96,74 +95,74 @@ _≉ᴮ_ : B → B → Set ℓm x ≉ᴮ y = ¬ (x ≈ᴮ y) module _ - {⟦_⟧ : A → B} - (isModuleHomomorphism : IsModuleHomomorphism ⟦_⟧) + {f : A → B} + (isModuleHomomorphism : IsModuleHomomorphism f) where open IsModuleHomomorphism isModuleHomomorphism -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f - f𝟘≈𝟘 : ⟦ 0ᴬ ⟧ ≈ᴮ 0ᴮ + f𝟘≈𝟘 : f 0ᴬ ≈ᴮ 0ᴮ f𝟘≈𝟘 = begin - ⟦ 0ᴬ ⟧ ≈⟨ ⟦⟧-cong (symᴬ (·ᴬ-zeroˡ 0ᴬ)) ⟩ - ⟦ (𝟘 ·ᴬ 0ᴬ) ⟧ ≈⟨ *ₗ-homo 𝟘 0ᴬ ⟩ - 𝟘 ·ᴮ ⟦ 0ᴬ ⟧ ≈⟨ ·ᴮ-zeroˡ ⟦ 0ᴬ ⟧ ⟩ + f 0ᴬ ≈⟨ ⟦⟧-cong (symᴬ (·ᴬ-zeroˡ 0ᴬ)) ⟩ + f (𝟘 ·ᴬ 0ᴬ) ≈⟨ *ₗ-homo 𝟘 0ᴬ ⟩ + 𝟘 ·ᴮ f 0ᴬ ≈⟨ ·ᴮ-zeroˡ (f 0ᴬ) ⟩ 0ᴮ ∎ where open Reasoning ≈ᴮ-setoid - x≈𝟘→fx≈𝟘 : {x : A} → x ≈ᴬ 0ᴬ → ⟦ x ⟧ ≈ᴮ 0ᴮ + x≈𝟘→fx≈𝟘 : {x : A} → x ≈ᴬ 0ᴬ → f x ≈ᴮ 0ᴮ x≈𝟘→fx≈𝟘 {x = x} x≈𝟘 = begin - ⟦ x ⟧ ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ - ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 ⟩ + f x ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ + f 0ᴬ ≈⟨ f𝟘≈𝟘 ⟩ 0ᴮ ∎ where open Reasoning ≈ᴮ-setoid - fx≉𝟘→x≉𝟘 : {x : A} → ⟦ x ⟧ ≉ᴮ 0ᴮ → x ≉ᴬ 0ᴬ + fx≉𝟘→x≉𝟘 : {x : A} → f x ≉ᴮ 0ᴮ → x ≉ᴬ 0ᴬ fx≉𝟘→x≉𝟘 = contraposition x≈𝟘→fx≈𝟘 -- Zero is a unique output of linear map ≉ `const 𝟘`. zero-unique : {x : A} → - Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (⟦ y ⟧ ≉ᴮ 0ᴮ)) → - x ≉ᴬ 0ᴬ → ⟦ x ⟧ ≉ᴮ 0ᴮ + Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (f y ≉ᴮ 0ᴮ)) → + x ≉ᴬ 0ᴬ → f x ≉ᴮ 0ᴮ zero-unique {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 = non-zeroʳᴮ s·fx≉𝟘 where open Reasoning ≈ᴮ-setoid y≉𝟘 : y ≉ᴬ 0ᴬ y≉𝟘 = fx≉𝟘→x≉𝟘 fy≉𝟘 - fs·x≈fy : ⟦ (s ·ᴬ x) ⟧ ≈ᴮ ⟦ y ⟧ + fs·x≈fy : f (s ·ᴬ x) ≈ᴮ f y fs·x≈fy = ⟦⟧-cong s·x≈y - s·fx≈fy : s ·ᴮ ⟦ x ⟧ ≈ᴮ ⟦ y ⟧ + s·fx≈fy : s ·ᴮ f x ≈ᴮ f y s·fx≈fy = begin - s ·ᴮ ⟦ x ⟧ ≈⟨ symᴮ (*ₗ-homo s x) ⟩ - ⟦ (s ·ᴬ x) ⟧ ≈⟨ fs·x≈fy ⟩ - ⟦ y ⟧ ∎ - s·fx≉𝟘 : (s ·ᴮ ⟦ x ⟧) ≉ᴮ 0ᴮ + s ·ᴮ f x ≈⟨ symᴮ (*ₗ-homo s x) ⟩ + f (s ·ᴬ x) ≈⟨ fs·x≈fy ⟩ + f y ∎ + s·fx≉𝟘 : (s ·ᴮ f x) ≉ᴮ 0ᴮ s·fx≉𝟘 = λ s·fx≈𝟘 → fy≉𝟘 ( begin - ⟦ y ⟧ ≈⟨ ⟦⟧-cong (symᴬ s·x≈y) ⟩ - ⟦ (s ·ᴬ x) ⟧ ≈⟨ *ₗ-homo s x ⟩ - s ·ᴮ ⟦ x ⟧ ≈⟨ s·fx≈𝟘 ⟩ + f y ≈⟨ ⟦⟧-cong (symᴬ s·x≈y) ⟩ + f (s ·ᴬ x) ≈⟨ *ₗ-homo s x ⟩ + s ·ᴮ f x ≈⟨ s·fx≈𝟘 ⟩ 0ᴮ ∎ ) -- f is odd (i.e. - f (-x) ≈ - (f x)). - fx+f-x≈𝟘 : {x : A} → ⟦ x ⟧ +ᴮ ⟦ (-ᴬ x) ⟧ ≈ᴮ 0ᴮ + fx+f-x≈𝟘 : {x : A} → f x +ᴮ f (-ᴬ x) ≈ᴮ 0ᴮ fx+f-x≈𝟘 {x = x} = begin - ⟦ x ⟧ +ᴮ ⟦ (-ᴬ x) ⟧ ≈⟨ symᴮ (+ᴹ-homo x (-ᴬ x)) ⟩ - ⟦ (x +ᴬ (-ᴬ x)) ⟧ ≈⟨ ⟦⟧-cong (-ᴬ‿inverseʳ x) ⟩ - ⟦ 0ᴬ ⟧ ≈⟨ f𝟘≈𝟘 ⟩ + f x +ᴮ f (-ᴬ x) ≈⟨ symᴮ (+ᴹ-homo x (-ᴬ x)) ⟩ + f (x +ᴬ (-ᴬ x)) ≈⟨ ⟦⟧-cong (-ᴬ‿inverseʳ x) ⟩ + f 0ᴬ ≈⟨ f𝟘≈𝟘 ⟩ 0ᴮ ∎ where open Reasoning ≈ᴮ-setoid - f-x≈-fx : {x : A} → ⟦ (-ᴬ x) ⟧ ≈ᴮ -ᴮ ⟦ x ⟧ - f-x≈-fx {x = x} = uniqueʳ‿-ᴮ ⟦ x ⟧ ⟦ -ᴬ x ⟧ fx+f-x≈𝟘 + f-x≈-fx : {x : A} → f (-ᴬ x) ≈ᴮ -ᴮ f x + f-x≈-fx {x = x} = uniqueʳ‿-ᴮ (f x) (f (-ᴬ x)) fx+f-x≈𝟘 module _ {dne : DoubleNegationElimination _} where fx≈𝟘⇒x≈𝟘 : {x : A} → - Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (⟦ y ⟧ ≉ᴮ 0ᴮ)) → - ⟦ x ⟧ ≈ᴮ 0ᴮ → x ≈ᴬ 0ᴬ + Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (f y ≉ᴮ 0ᴮ)) → + f x ≈ᴮ 0ᴮ → x ≈ᴬ 0ᴬ fx≈𝟘⇒x≈𝟘 {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) fx≈𝟘 = dne ¬x≉𝟘 where @@ -171,24 +170,24 @@ module _ ¬x≉𝟘 = λ x≉𝟘 → zero-unique ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 fx≈𝟘 -- A non-trivial linear function is injective. - fx-fy≈𝟘 : {x y : A} {fx≈fy : ⟦ x ⟧ ≈ᴮ ⟦ y ⟧} → ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈ᴮ 0ᴮ + fx-fy≈𝟘 : {x y : A} {fx≈fy : f x ≈ᴮ f y} → f x +ᴮ (-ᴮ f y) ≈ᴮ 0ᴮ fx-fy≈𝟘 {x = x} {y = y} {fx≈fy = fx≈fy} = begin - ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈⟨ +ᴮ-congˡ (-ᴮ‿cong (symᴮ fx≈fy)) ⟩ - ⟦ x ⟧ +ᴮ (-ᴮ ⟦ x ⟧) ≈⟨ -ᴮ‿inverseʳ (⟦ x ⟧) ⟩ + f x +ᴮ (-ᴮ f y) ≈⟨ +ᴮ-congˡ (-ᴮ‿cong (symᴮ fx≈fy)) ⟩ + f x +ᴮ (-ᴮ f x) ≈⟨ -ᴮ‿inverseʳ (f x) ⟩ 0ᴮ ∎ where open Reasoning ≈ᴮ-setoid - fx-y≈𝟘 : {x y : A} {fx≈fy : ⟦ x ⟧ ≈ᴮ ⟦ y ⟧} → ⟦ (x +ᴬ (-ᴬ y)) ⟧ ≈ᴮ 0ᴮ + fx-y≈𝟘 : {x y : A} {fx≈fy : f x ≈ᴮ f y} → f (x +ᴬ (-ᴬ y)) ≈ᴮ 0ᴮ fx-y≈𝟘 {x = x} {y = y} {fx≈fy = fx≈fy} = begin - ⟦ x +ᴬ (-ᴬ y) ⟧ ≈⟨ +ᴹ-homo x (-ᴬ y) ⟩ - ⟦ x ⟧ +ᴮ ⟦ -ᴬ y ⟧ ≈⟨ +ᴮ-congˡ f-x≈-fx ⟩ - ⟦ x ⟧ +ᴮ (-ᴮ ⟦ y ⟧) ≈⟨ fx-fy≈𝟘 {fx≈fy = fx≈fy} ⟩ + f (x +ᴬ (-ᴬ y)) ≈⟨ +ᴹ-homo x (-ᴬ y) ⟩ + f x +ᴮ f (-ᴬ y) ≈⟨ +ᴮ-congˡ f-x≈-fx ⟩ + f x +ᴮ (-ᴮ f y) ≈⟨ fx-fy≈𝟘 {fx≈fy = fx≈fy} ⟩ 0ᴮ ∎ where open Reasoning ≈ᴮ-setoid inj-lm : {x y : A} → - Σ[ (s , z) ∈ S × A ] ((s ·ᴬ (x +ᴬ -ᴬ y) ≈ᴬ z) × (⟦ z ⟧ ≉ᴮ 0ᴮ)) → - ⟦ x ⟧ ≈ᴮ ⟦ y ⟧ → x ≈ᴬ y + Σ[ (s , z) ∈ S × A ] ((s ·ᴬ (x +ᴬ -ᴬ y) ≈ᴬ z) × (f z ≉ᴮ 0ᴮ)) → + f x ≈ᴮ f y → x ≈ᴬ y inj-lm {x = x} {y = y} ((s , z) , (s·[x-y]≈z , fz≉𝟘)) fx≈fy = begin x ≈⟨ x≈--y ⟩ From caabb3a779b795315559fc6752638d2e56b36ba7 Mon Sep 17 00:00:00 2001 From: David Banas Date: Sat, 14 May 2022 11:15:29 -0700 Subject: [PATCH 09/19] Switched to `A.` notation, as per Jacques. --- .../Module/Morphism/Linear/Properties.agda | 172 +++++++----------- 1 file changed, 68 insertions(+), 104 deletions(-) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index 34f5246c6e..e4eae9a110 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -30,52 +30,16 @@ open import Relation.Nullary using (¬_) open import Relation.Nullary.Negation using (contraposition) open MorphismStructures.ModuleMorphisms modA modB -open Module modA - using () renaming - ( Carrierᴹ to A - ; _+ᴹ_ to _+ᴬ_ - ; _*ₗ_ to _·ᴬ_ - ; -ᴹ_ to -ᴬ_ - ; _≈ᴹ_ to _≈ᴬ_ - ; 0ᴹ to 0ᴬ - ; +ᴹ-comm to +ᴬ-comm - ; +ᴹ-congˡ to +ᴬ-congˡ - ; +ᴹ-congʳ to +ᴬ-congʳ - ; *ₗ-zeroˡ to ·ᴬ-zeroˡ - ; -ᴹ‿cong to -ᴬ‿cong - ; -ᴹ‿inverseʳ to -ᴬ‿inverseʳ - ; -ᴹ‿involutive to -ᴬ‿involutive - ; uniqueʳ‿-ᴹ to uniqueʳ‿-ᴬ - ; ≈ᴹ-setoid to ≈ᴬ-setoid - ; ≈ᴹ-sym to symᴬ - ; leftSemimodule to leftSemimoduleᴬ - ) -open Properties leftSemimoduleᴬ +module A = Module modA +open A using () renaming (Carrierᴹ to A) +open Properties A.leftSemimodule using () renaming ( non-zeroʳ to non-zeroʳᴬ ; non-zeroˡ to non-zeroˡᴬ ) -open Module modB - using () renaming - ( Carrierᴹ to B - ; _+ᴹ_ to _+ᴮ_ - ; _*ₗ_ to _·ᴮ_ - ; -ᴹ_ to -ᴮ_ - ; _≈ᴹ_ to _≈ᴮ_ - ; 0ᴹ to 0ᴮ - ; +ᴹ-comm to +ᴮ-comm - ; +ᴹ-congˡ to +ᴮ-congˡ - ; +ᴹ-congʳ to +ᴮ-congʳ - ; *ₗ-zeroˡ to ·ᴮ-zeroˡ - ; -ᴹ‿cong to -ᴮ‿cong - ; -ᴹ‿inverseʳ to -ᴮ‿inverseʳ - ; -ᴹ‿involutive to -ᴮ‿involutive - ; uniqueʳ‿-ᴹ to uniqueʳ‿-ᴮ - ; ≈ᴹ-setoid to ≈ᴮ-setoid - ; ≈ᴹ-sym to symᴮ - ; leftSemimodule to leftSemimoduleᴮ - ) -open Properties leftSemimoduleᴮ +module B = Module modB +open B using () renaming (Carrierᴹ to B) +open Properties B.leftSemimodule using () renaming ( non-zeroʳ to non-zeroʳᴮ ; non-zeroˡ to non-zeroˡᴮ @@ -86,13 +50,13 @@ open CommutativeRing ring ; 0# to 𝟘 ; 1# to 𝟙 ) -open Function.Definitions _≈ᴬ_ _≈ᴮ_ +open Function.Definitions A._≈ᴹ_ B._≈ᴹ_ _≉ᴬ_ : A → A → Set ℓm -x ≉ᴬ y = ¬ (x ≈ᴬ y) +x ≉ᴬ y = ¬ (x A.≈ᴹ y) _≉ᴮ_ : B → B → Set ℓm -x ≉ᴮ y = ¬ (x ≈ᴮ y) +x ≉ᴮ y = ¬ (x B.≈ᴹ y) module _ {f : A → B} @@ -102,107 +66,107 @@ module _ open IsModuleHomomorphism isModuleHomomorphism -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f - f𝟘≈𝟘 : f 0ᴬ ≈ᴮ 0ᴮ + f𝟘≈𝟘 : f A.0ᴹ B.≈ᴹ B.0ᴹ f𝟘≈𝟘 = begin - f 0ᴬ ≈⟨ ⟦⟧-cong (symᴬ (·ᴬ-zeroˡ 0ᴬ)) ⟩ - f (𝟘 ·ᴬ 0ᴬ) ≈⟨ *ₗ-homo 𝟘 0ᴬ ⟩ - 𝟘 ·ᴮ f 0ᴬ ≈⟨ ·ᴮ-zeroˡ (f 0ᴬ) ⟩ - 0ᴮ ∎ - where open Reasoning ≈ᴮ-setoid + f A.0ᴹ ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym (A.*ₗ-zeroˡ A.0ᴹ)) ⟩ + f (𝟘 A.*ₗ A.0ᴹ) ≈⟨ *ₗ-homo 𝟘 A.0ᴹ ⟩ + 𝟘 B.*ₗ f A.0ᴹ ≈⟨ B.*ₗ-zeroˡ (f A.0ᴹ) ⟩ + B.0ᴹ ∎ + where open Reasoning B.≈ᴹ-setoid - x≈𝟘→fx≈𝟘 : {x : A} → x ≈ᴬ 0ᴬ → f x ≈ᴮ 0ᴮ + x≈𝟘→fx≈𝟘 : {x : A} → x A.≈ᴹ A.0ᴹ → f x B.≈ᴹ B.0ᴹ x≈𝟘→fx≈𝟘 {x = x} x≈𝟘 = begin - f x ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ - f 0ᴬ ≈⟨ f𝟘≈𝟘 ⟩ - 0ᴮ ∎ - where open Reasoning ≈ᴮ-setoid + f x ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ + f A.0ᴹ ≈⟨ f𝟘≈𝟘 ⟩ + B.0ᴹ ∎ + where open Reasoning B.≈ᴹ-setoid - fx≉𝟘→x≉𝟘 : {x : A} → f x ≉ᴮ 0ᴮ → x ≉ᴬ 0ᴬ + fx≉𝟘→x≉𝟘 : {x : A} → f x ≉ᴮ B.0ᴹ → x ≉ᴬ A.0ᴹ fx≉𝟘→x≉𝟘 = contraposition x≈𝟘→fx≈𝟘 -- Zero is a unique output of linear map ≉ `const 𝟘`. zero-unique : {x : A} → - Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (f y ≉ᴮ 0ᴮ)) → - x ≉ᴬ 0ᴬ → f x ≉ᴮ 0ᴮ + Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y ≉ᴮ B.0ᴹ)) → + x ≉ᴬ A.0ᴹ → f x ≉ᴮ B.0ᴹ zero-unique {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 = non-zeroʳᴮ s·fx≉𝟘 where - open Reasoning ≈ᴮ-setoid - y≉𝟘 : y ≉ᴬ 0ᴬ + open Reasoning B.≈ᴹ-setoid + y≉𝟘 : y ≉ᴬ A.0ᴹ y≉𝟘 = fx≉𝟘→x≉𝟘 fy≉𝟘 - fs·x≈fy : f (s ·ᴬ x) ≈ᴮ f y + fs·x≈fy : f (s A.*ₗ x) B.≈ᴹ f y fs·x≈fy = ⟦⟧-cong s·x≈y - s·fx≈fy : s ·ᴮ f x ≈ᴮ f y + s·fx≈fy : s B.*ₗ f x B.≈ᴹ f y s·fx≈fy = begin - s ·ᴮ f x ≈⟨ symᴮ (*ₗ-homo s x) ⟩ - f (s ·ᴬ x) ≈⟨ fs·x≈fy ⟩ + s B.*ₗ f x ≈⟨ B.≈ᴹ-sym (*ₗ-homo s x) ⟩ + f (s A.*ₗ x) ≈⟨ fs·x≈fy ⟩ f y ∎ - s·fx≉𝟘 : (s ·ᴮ f x) ≉ᴮ 0ᴮ + s·fx≉𝟘 : (s B.*ₗ f x) ≉ᴮ B.0ᴹ s·fx≉𝟘 = λ s·fx≈𝟘 → fy≉𝟘 ( begin - f y ≈⟨ ⟦⟧-cong (symᴬ s·x≈y) ⟩ - f (s ·ᴬ x) ≈⟨ *ₗ-homo s x ⟩ - s ·ᴮ f x ≈⟨ s·fx≈𝟘 ⟩ - 0ᴮ ∎ + f y ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym s·x≈y) ⟩ + f (s A.*ₗ x) ≈⟨ *ₗ-homo s x ⟩ + s B.*ₗ f x ≈⟨ s·fx≈𝟘 ⟩ + B.0ᴹ ∎ ) -- f is odd (i.e. - f (-x) ≈ - (f x)). - fx+f-x≈𝟘 : {x : A} → f x +ᴮ f (-ᴬ x) ≈ᴮ 0ᴮ + fx+f-x≈𝟘 : {x : A} → f x B.+ᴹ f (A.-ᴹ x) B.≈ᴹ B.0ᴹ fx+f-x≈𝟘 {x = x} = begin - f x +ᴮ f (-ᴬ x) ≈⟨ symᴮ (+ᴹ-homo x (-ᴬ x)) ⟩ - f (x +ᴬ (-ᴬ x)) ≈⟨ ⟦⟧-cong (-ᴬ‿inverseʳ x) ⟩ - f 0ᴬ ≈⟨ f𝟘≈𝟘 ⟩ - 0ᴮ ∎ - where open Reasoning ≈ᴮ-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ᴹ ≈⟨ f𝟘≈𝟘 ⟩ + B.0ᴹ ∎ + where open Reasoning B.≈ᴹ-setoid - f-x≈-fx : {x : A} → f (-ᴬ x) ≈ᴮ -ᴮ f x - f-x≈-fx {x = x} = uniqueʳ‿-ᴮ (f x) (f (-ᴬ x)) fx+f-x≈𝟘 + f-x≈-fx : {x : A} → f (A.-ᴹ x) B.≈ᴹ B.-ᴹ f x + f-x≈-fx {x = x} = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) fx+f-x≈𝟘 module _ {dne : DoubleNegationElimination _} where fx≈𝟘⇒x≈𝟘 : {x : A} → - Σ[ (s , y) ∈ S × A ] ((s ·ᴬ x ≈ᴬ y) × (f y ≉ᴮ 0ᴮ)) → - f x ≈ᴮ 0ᴮ → x ≈ᴬ 0ᴬ + Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y ≉ᴮ B.0ᴹ)) → + f x B.≈ᴹ B.0ᴹ → x A.≈ᴹ A.0ᴹ fx≈𝟘⇒x≈𝟘 {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) fx≈𝟘 = dne ¬x≉𝟘 where - ¬x≉𝟘 : ¬ (x ≉ᴬ 0ᴬ) + ¬x≉𝟘 : ¬ (x ≉ᴬ A.0ᴹ) ¬x≉𝟘 = λ x≉𝟘 → zero-unique ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 fx≈𝟘 -- A non-trivial linear function is injective. - fx-fy≈𝟘 : {x y : A} {fx≈fy : f x ≈ᴮ f y} → f x +ᴮ (-ᴮ f y) ≈ᴮ 0ᴮ + fx-fy≈𝟘 : {x y : A} {fx≈fy : f x B.≈ᴹ f y} → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ fx-fy≈𝟘 {x = x} {y = y} {fx≈fy = fx≈fy} = begin - f x +ᴮ (-ᴮ f y) ≈⟨ +ᴮ-congˡ (-ᴮ‿cong (symᴮ fx≈fy)) ⟩ - f x +ᴮ (-ᴮ f x) ≈⟨ -ᴮ‿inverseʳ (f x) ⟩ - 0ᴮ ∎ - where open Reasoning ≈ᴮ-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ᴹ ∎ + where open Reasoning B.≈ᴹ-setoid - fx-y≈𝟘 : {x y : A} {fx≈fy : f x ≈ᴮ f y} → f (x +ᴬ (-ᴬ y)) ≈ᴮ 0ᴮ + fx-y≈𝟘 : {x y : A} {fx≈fy : f x B.≈ᴹ f y} → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ fx-y≈𝟘 {x = x} {y = y} {fx≈fy = fx≈fy} = begin - f (x +ᴬ (-ᴬ y)) ≈⟨ +ᴹ-homo x (-ᴬ y) ⟩ - f x +ᴮ f (-ᴬ y) ≈⟨ +ᴮ-congˡ f-x≈-fx ⟩ - f x +ᴮ (-ᴮ f y) ≈⟨ fx-fy≈𝟘 {fx≈fy = fx≈fy} ⟩ - 0ᴮ ∎ - where open Reasoning ≈ᴮ-setoid + f (x A.+ᴹ (A.-ᴹ y)) ≈⟨ +ᴹ-homo x (A.-ᴹ y) ⟩ + f x B.+ᴹ f (A.-ᴹ y) ≈⟨ B.+ᴹ-congˡ f-x≈-fx ⟩ + f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx-fy≈𝟘 {fx≈fy = fx≈fy} ⟩ + B.0ᴹ ∎ + where open Reasoning B.≈ᴹ-setoid inj-lm : {x y : A} → - Σ[ (s , z) ∈ S × A ] ((s ·ᴬ (x +ᴬ -ᴬ y) ≈ᴬ z) × (f z ≉ᴮ 0ᴮ)) → - f x ≈ᴮ f y → x ≈ᴬ y + Σ[ (s , z) ∈ S × A ] ((s A.*ₗ (x A.+ᴹ A.-ᴹ y) A.≈ᴹ z) × (f z ≉ᴮ B.0ᴹ)) → + f x B.≈ᴹ f y → x A.≈ᴹ y inj-lm {x = x} {y = y} ((s , z) , (s·[x-y]≈z , fz≉𝟘)) fx≈fy = begin - x ≈⟨ x≈--y ⟩ - -ᴬ (-ᴬ y) ≈⟨ -ᴬ‿involutive ⟩ + x ≈⟨ x≈--y ⟩ + A.-ᴹ (A.-ᴹ y) ≈⟨ A.-ᴹ‿involutive ⟩ y ∎ where - open Reasoning ≈ᴬ-setoid - x-y≈𝟘 : x +ᴬ (-ᴬ y) ≈ᴬ 0ᴬ - x-y≈𝟘 = fx≈𝟘⇒x≈𝟘 {x = x +ᴬ (-ᴬ y)} + open Reasoning A.≈ᴹ-setoid + x-y≈𝟘 : x A.+ᴹ (A.-ᴹ y) A.≈ᴹ A.0ᴹ + x-y≈𝟘 = fx≈𝟘⇒x≈𝟘 {x = x A.+ᴹ (A.-ᴹ y)} ((s , z) , s·[x-y]≈z , fz≉𝟘) (fx-y≈𝟘 {fx≈fy = fx≈fy}) - x≈--y : x ≈ᴬ -ᴬ (-ᴬ y) - x≈--y = uniqueʳ‿-ᴬ (-ᴬ y) x + x≈--y : x A.≈ᴹ A.-ᴹ (A.-ᴹ y) + x≈--y = A.uniqueʳ‿-ᴹ (A.-ᴹ y) x ( begin - -ᴬ y +ᴬ x ≈⟨ +ᴬ-comm (-ᴬ y) x ⟩ - x +ᴬ -ᴬ y ≈⟨ x-y≈𝟘 ⟩ - 0ᴬ ∎ + A.-ᴹ y A.+ᴹ x ≈⟨ A.+ᴹ-comm (A.-ᴹ y) x ⟩ + x A.+ᴹ A.-ᴹ y ≈⟨ x-y≈𝟘 ⟩ + A.0ᴹ ∎ ) From 3c119562cc92e8a5cee5048c817474dd85df7f46 Mon Sep 17 00:00:00 2001 From: David Banas Date: Sun, 15 May 2022 16:53:57 -0700 Subject: [PATCH 10/19] Changes requested by Matthew Daggitt. --- CHANGELOG.md | 6 +- src/Algebra/Module/Bundles.agda | 39 +++++- .../Module/Morphism/Linear/Properties.agda | 127 ++++++++---------- src/Algebra/Module/Properties.agda | 58 ++++---- 4 files changed, 124 insertions(+), 106 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index bf4a493441..2c731b7ba0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -952,7 +952,6 @@ New modules * Proofs of some axioms of linearity: ``` - Algebra.Module.Bundles Algebra.Module.Morphism.Linear.Properties Algebra.Module.Properties ``` @@ -1046,6 +1045,11 @@ Other minor changes _^ᵗ_ : A → ℕ → A ``` +* Added new proofs to `Algebra.Module.Bundles`: + ``` + -ᴹ-involutive : Involutive _≈ᴹ_ -ᴹ_ + ``` + * Added new proofs to `Algebra.Properties.CommutativeSemigroup`: ``` interchange : Interchangable _∙_ _∙_ diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index d99c859165..0986263993 100644 --- a/src/Algebra/Module/Bundles.agda +++ b/src/Algebra/Module/Bundles.agda @@ -27,6 +27,7 @@ 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 @@ -34,6 +35,7 @@ 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 @@ -60,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 @@ -93,6 +99,10 @@ record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ -ᴹ_ : Op₁ Carrierᴹ isLeftModule : IsLeftModule ring _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ + infix 4 _≉ᴹ_ + _≉ᴹ_ : Rel Carrierᴹ _ + a ≉ᴹ b = ¬ (a ≈ᴹ b) + open IsLeftModule isLeftModule public leftSemimodule : LeftSemimodule semiring m ℓm @@ -128,6 +138,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 @@ -161,6 +175,10 @@ record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ -ᴹ_ : Op₁ Carrierᴹ isRightModule : IsRightModule ring _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ + infix 4 _≉ᴹ_ + _≉ᴹ_ : Rel Carrierᴹ _ + a ≉ᴹ b = ¬ (a ≈ᴹ b) + open IsRightModule isRightModule public rightSemimodule : RightSemimodule semiring m ℓm @@ -199,6 +217,10 @@ record Bisemimodule (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs 0ᴹ : Carrierᴹ isBisemimodule : IsBisemimodule R-semiring S-semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ + infix 4 _≉ᴹ_ + _≉ᴹ_ : Rel Carrierᴹ _ + a ≉ᴹ b = ¬ (a ≈ᴹ b) + open IsBisemimodule isBisemimodule public leftSemimodule : LeftSemimodule R-semiring m ℓm @@ -231,6 +253,10 @@ record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm -ᴹ_ : Op₁ Carrierᴹ isBimodule : IsBimodule R-ring S-ring _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ + infix 4 _≉ᴹ_ + _≉ᴹ_ : Rel Carrierᴹ _ + a ≉ᴹ b = ¬ (a ≈ᴹ b) + open IsBimodule isBimodule public leftModule : LeftModule R-ring m ℓm @@ -271,6 +297,10 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm 0ᴹ : Carrierᴹ isSemimodule : IsSemimodule commutativeSemiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ + infix 4 _≉ᴹ_ + _≉ᴹ_ : Rel Carrierᴹ _ + a ≉ᴹ b = ¬ (a ≈ᴹ b) + open IsSemimodule isSemimodule public private @@ -320,6 +350,10 @@ record Module (commutativeRing : CommutativeRing r ℓr) m ℓm -ᴹ_ : Op₁ Carrierᴹ isModule : IsModule commutativeRing _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ + infix 4 _≉ᴹ_ + _≉ᴹ_ : Rel Carrierᴹ _ + a ≉ᴹ b = ¬ (a ≈ᴹ b) + open IsModule isModule public bimodule : Bimodule ring ring m ℓm @@ -335,6 +369,5 @@ record Module (commutativeRing : CommutativeRing r ℓr) m ℓm open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm) - -ᴹ‿involutive : {x : Carrierᴹ} → -ᴹ (-ᴹ x) ≈ᴹ x - -ᴹ‿involutive {x = x} = ⁻¹-involutive +ᴹ-group x - + -ᴹ-involutive : Involutive _≈ᴹ_ -ᴹ_ + -ᴹ-involutive = ⁻¹-involutive +ᴹ-group diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index e4eae9a110..5fc9509378 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -16,12 +16,11 @@ module Algebra.Module.Morphism.Linear.Properties (modA modB : Module ring m ℓm) where -import Algebra.Module.Properties as Properties +import Algebra.Module.Properties as ModuleProperties import Function.Definitions import Relation.Binary.Reasoning.Setoid as Reasoning import Algebra.Module.Morphism.Structures as MorphismStructures -open import Agda.Builtin.Sigma open import Axiom.DoubleNegationElimination open import Data.List open import Data.Product @@ -32,31 +31,22 @@ open import Relation.Nullary.Negation using (contraposition) open MorphismStructures.ModuleMorphisms modA modB module A = Module modA open A using () renaming (Carrierᴹ to A) -open Properties A.leftSemimodule - using () renaming - ( non-zeroʳ to non-zeroʳᴬ - ; non-zeroˡ to non-zeroˡᴬ - ) +-- module A = ModuleProperties A.leftSemimodule +-- open ModuleProperties A.leftSemimodule +-- using () renaming +-- ( non-zeroʳ to non-zeroʳᴬ +-- ; non-zeroˡ to non-zeroˡᴬ +-- ) module B = Module modB open B using () renaming (Carrierᴹ to B) -open Properties B.leftSemimodule - using () renaming - ( non-zeroʳ to non-zeroʳᴮ - ; non-zeroˡ to non-zeroˡᴮ - ) +module B2 = ModuleProperties B.leftSemimodule +-- open ModuleProperties B.leftSemimodule +-- using () renaming +-- ( non-zeroʳ to non-zeroʳᴮ +-- ; non-zeroˡ to non-zeroˡᴮ +-- ) open CommutativeRing ring - using (_≈_; _*_; _+_) renaming - ( Carrier to S - ; 0# to 𝟘 - ; 1# to 𝟙 - ) -open Function.Definitions A._≈ᴹ_ B._≈ᴹ_ - -_≉ᴬ_ : A → A → Set ℓm -x ≉ᴬ y = ¬ (x A.≈ᴹ y) - -_≉ᴮ_ : B → B → Set ℓm -x ≉ᴮ y = ¬ (x B.≈ᴹ y) + using (_≈_; _*_; _+_; 0#) renaming (Carrier to S) module _ {f : A → B} @@ -68,105 +58,106 @@ module _ -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f f𝟘≈𝟘 : f A.0ᴹ B.≈ᴹ B.0ᴹ f𝟘≈𝟘 = begin - f A.0ᴹ ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym (A.*ₗ-zeroˡ A.0ᴹ)) ⟩ - f (𝟘 A.*ₗ A.0ᴹ) ≈⟨ *ₗ-homo 𝟘 A.0ᴹ ⟩ - 𝟘 B.*ₗ f A.0ᴹ ≈⟨ B.*ₗ-zeroˡ (f A.0ᴹ) ⟩ - B.0ᴹ ∎ + f A.0ᴹ ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym (A.*ₗ-zeroˡ A.0ᴹ)) ⟩ + f (0# A.*ₗ A.0ᴹ) ≈⟨ *ₗ-homo 0# A.0ᴹ ⟩ + 0# B.*ₗ f A.0ᴹ ≈⟨ B.*ₗ-zeroˡ (f A.0ᴹ) ⟩ + B.0ᴹ ∎ where open Reasoning B.≈ᴹ-setoid - x≈𝟘→fx≈𝟘 : {x : A} → x A.≈ᴹ A.0ᴹ → f x B.≈ᴹ B.0ᴹ - x≈𝟘→fx≈𝟘 {x = x} x≈𝟘 = begin + x≈𝟘⇒fx≈𝟘 : ∀ {x} → x A.≈ᴹ A.0ᴹ → f x B.≈ᴹ B.0ᴹ + x≈𝟘⇒fx≈𝟘 {x} x≈𝟘 = begin f x ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ f A.0ᴹ ≈⟨ f𝟘≈𝟘 ⟩ - B.0ᴹ ∎ + B.0ᴹ ∎ where open Reasoning B.≈ᴹ-setoid - fx≉𝟘→x≉𝟘 : {x : A} → f x ≉ᴮ B.0ᴹ → x ≉ᴬ A.0ᴹ - fx≉𝟘→x≉𝟘 = contraposition x≈𝟘→fx≈𝟘 + fx≉𝟘⇒x≉𝟘 : ∀ {x} → f x B.≉ᴹ B.0ᴹ → x A.≉ᴹ A.0ᴹ + fx≉𝟘⇒x≉𝟘 = contraposition x≈𝟘⇒fx≈𝟘 -- Zero is a unique output of linear map ≉ `const 𝟘`. - zero-unique : {x : A} → - Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y ≉ᴮ B.0ᴹ)) → - x ≉ᴬ A.0ᴹ → f x ≉ᴮ B.0ᴹ - zero-unique {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 = - non-zeroʳᴮ s·fx≉𝟘 + zero-unique : ∀ {x} → + Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)) → + x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ + zero-unique {x} ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 = + B2.non-zeroʳ s·fx≉𝟘 where open Reasoning B.≈ᴹ-setoid - y≉𝟘 : y ≉ᴬ A.0ᴹ - y≉𝟘 = fx≉𝟘→x≉𝟘 fy≉𝟘 + y≉𝟘 : y A.≉ᴹ A.0ᴹ + y≉𝟘 = fx≉𝟘⇒x≉𝟘 fy≉𝟘 fs·x≈fy : f (s A.*ₗ x) B.≈ᴹ f y fs·x≈fy = ⟦⟧-cong s·x≈y s·fx≈fy : s B.*ₗ f x B.≈ᴹ f y s·fx≈fy = begin s B.*ₗ f x ≈⟨ B.≈ᴹ-sym (*ₗ-homo s x) ⟩ f (s A.*ₗ x) ≈⟨ fs·x≈fy ⟩ - f y ∎ - s·fx≉𝟘 : (s B.*ₗ f x) ≉ᴮ B.0ᴹ - s·fx≉𝟘 = λ s·fx≈𝟘 → + f y ∎ + s·fx≉𝟘 : (s B.*ₗ f x) B.≉ᴹ B.0ᴹ + s·fx≉𝟘 s·fx≈𝟘 = fy≉𝟘 ( begin f y ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym s·x≈y) ⟩ f (s A.*ₗ x) ≈⟨ *ₗ-homo s x ⟩ s B.*ₗ f x ≈⟨ s·fx≈𝟘 ⟩ - B.0ᴹ ∎ + B.0ᴹ ∎ ) -- f is odd (i.e. - f (-x) ≈ - (f x)). - fx+f-x≈𝟘 : {x : A} → f x B.+ᴹ f (A.-ᴹ x) B.≈ᴹ B.0ᴹ - fx+f-x≈𝟘 {x = x} = begin + fx+f[-x]≈𝟘 : ∀ {x} → f x B.+ᴹ f (A.-ᴹ x) B.≈ᴹ B.0ᴹ + fx+f[-x]≈𝟘 {x} = begin f x B.+ᴹ f (A.-ᴹ x) ≈⟨ B.≈ᴹ-sym (+ᴹ-homo x (A.-ᴹ x)) ⟩ f (x A.+ᴹ (A.-ᴹ x)) ≈⟨ ⟦⟧-cong (A.-ᴹ‿inverseʳ x) ⟩ f A.0ᴹ ≈⟨ f𝟘≈𝟘 ⟩ - B.0ᴹ ∎ + B.0ᴹ ∎ where open Reasoning B.≈ᴹ-setoid - f-x≈-fx : {x : A} → f (A.-ᴹ x) B.≈ᴹ B.-ᴹ f x - f-x≈-fx {x = x} = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) fx+f-x≈𝟘 + f[-x]≈-fx : ∀ {x} → f (A.-ᴹ x) B.≈ᴹ B.-ᴹ f x + f[-x]≈-fx {x} = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) fx+f[-x]≈𝟘 module _ {dne : DoubleNegationElimination _} where - fx≈𝟘⇒x≈𝟘 : {x : A} → - Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y ≉ᴮ B.0ᴹ)) → + fx≈𝟘⇒x≈𝟘 : ∀ {x} → + Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)) → f x B.≈ᴹ B.0ᴹ → x A.≈ᴹ A.0ᴹ - fx≈𝟘⇒x≈𝟘 {x = x} ((s , y) , (s·x≈y , fy≉𝟘)) fx≈𝟘 = + fx≈𝟘⇒x≈𝟘 {x} ((s , y) , (s·x≈y , fy≉𝟘)) fx≈𝟘 = dne ¬x≉𝟘 where - ¬x≉𝟘 : ¬ (x ≉ᴬ A.0ᴹ) + ¬x≉𝟘 : ¬ (x A.≉ᴹ A.0ᴹ) ¬x≉𝟘 = λ x≉𝟘 → zero-unique ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 fx≈𝟘 -- A non-trivial linear function is injective. - fx-fy≈𝟘 : {x y : A} {fx≈fy : f x B.≈ᴹ f y} → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ - fx-fy≈𝟘 {x = x} {y = y} {fx≈fy = fx≈fy} = begin + fx-fy≈𝟘 : ∀ {x} {y} → (f x B.≈ᴹ f y) → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ + fx-fy≈𝟘 {x} {y} fx≈fy = begin 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ᴹ ∎ + B.0ᴹ ∎ where open Reasoning B.≈ᴹ-setoid - fx-y≈𝟘 : {x y : A} {fx≈fy : f x B.≈ᴹ f y} → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ - fx-y≈𝟘 {x = x} {y = y} {fx≈fy = fx≈fy} = begin + fx-y≈𝟘 : ∀ {x} {y} → (f x B.≈ᴹ f y) → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ + fx-y≈𝟘 {x} {y} fx≈fy = begin f (x A.+ᴹ (A.-ᴹ y)) ≈⟨ +ᴹ-homo x (A.-ᴹ y) ⟩ - f x B.+ᴹ f (A.-ᴹ y) ≈⟨ B.+ᴹ-congˡ f-x≈-fx ⟩ - f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx-fy≈𝟘 {fx≈fy = fx≈fy} ⟩ - B.0ᴹ ∎ + f x B.+ᴹ f (A.-ᴹ y) ≈⟨ B.+ᴹ-congˡ f[-x]≈-fx ⟩ + f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx-fy≈𝟘 fx≈fy ⟩ + B.0ᴹ ∎ where open Reasoning B.≈ᴹ-setoid - inj-lm : {x y : A} → - Σ[ (s , z) ∈ S × A ] ((s A.*ₗ (x A.+ᴹ A.-ᴹ y) A.≈ᴹ z) × (f z ≉ᴮ B.0ᴹ)) → + inj-lm : ∀ {x} {y} → + Σ[ (s , z) ∈ S × A ] ( (s A.*ₗ (x A.+ᴹ A.-ᴹ y) A.≈ᴹ z) + × (f z B.≉ᴹ B.0ᴹ)) → f x B.≈ᴹ f y → x A.≈ᴹ y - inj-lm {x = x} {y = y} ((s , z) , (s·[x-y]≈z , fz≉𝟘)) fx≈fy = + inj-lm {x} {y} ((s , z) , (s·[x-y]≈z , fz≉𝟘)) fx≈fy = begin x ≈⟨ x≈--y ⟩ - A.-ᴹ (A.-ᴹ y) ≈⟨ A.-ᴹ‿involutive ⟩ - y ∎ + A.-ᴹ (A.-ᴹ y) ≈⟨ A.-ᴹ-involutive y ⟩ + y ∎ where open Reasoning A.≈ᴹ-setoid x-y≈𝟘 : x A.+ᴹ (A.-ᴹ y) A.≈ᴹ A.0ᴹ x-y≈𝟘 = fx≈𝟘⇒x≈𝟘 {x = x A.+ᴹ (A.-ᴹ y)} ((s , z) , s·[x-y]≈z , fz≉𝟘) - (fx-y≈𝟘 {fx≈fy = fx≈fy}) + (fx-y≈𝟘 fx≈fy) x≈--y : x A.≈ᴹ A.-ᴹ (A.-ᴹ y) x≈--y = A.uniqueʳ‿-ᴹ (A.-ᴹ y) x ( begin A.-ᴹ y A.+ᴹ x ≈⟨ A.+ᴹ-comm (A.-ᴹ y) x ⟩ x A.+ᴹ A.-ᴹ y ≈⟨ x-y≈𝟘 ⟩ - A.0ᴹ ∎ + A.0ᴹ ∎ ) diff --git a/src/Algebra/Module/Properties.agda b/src/Algebra/Module/Properties.agda index 59a5f4ec59..beb16b9705 100644 --- a/src/Algebra/Module/Properties.agda +++ b/src/Algebra/Module/Properties.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Properties of scaling. +-- Properties of modules. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -15,43 +15,33 @@ module Algebra.Module.Properties (lsmod : LeftSemimodule semiring m ℓm) where -open import Relation.Nullary using (¬_) +open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (contraposition) open LeftSemimodule lsmod - using (*ₗ-zeroˡ; *ₗ-zeroʳ; ≈ᴹ-setoid; _≈ᴹ_; *ₗ-congˡ; *ₗ-congʳ) - renaming - ( Carrierᴹ to M - ; _*ₗ_ to _·_ - ; 0ᴹ to 𝟘 - ) -infix 3 _≉ᴹ_ -_≉ᴹ_ : M → M → Set ℓm -x ≉ᴹ y = ¬ (x ≈ᴹ y) + using ( *ₗ-zeroˡ; *ₗ-zeroʳ; ≈ᴹ-setoid; *ₗ-congˡ; *ₗ-congʳ + ; _*ₗ_; 0ᴹ; _≈ᴹ_; _≉ᴹ_) + renaming (Carrierᴹ to M) open Semiring semiring - using (_≉_) renaming - ( Carrier to R - ; 0# to 0ᴿ - ) + using (_≈_; _≉_; 0#) renaming (Carrier to R) open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid -non-zeroˡ : {s : R} {v : M} → s · v ≉ᴹ 𝟘 → s ≉ 0ᴿ -non-zeroˡ {s = s} {v = v} s·v≉𝟘 = λ { s≈0ᴿ → - let s·v≈𝟘 : s · v ≈ᴹ 𝟘 - s·v≈𝟘 = begin - s · v ≈⟨ *ₗ-congʳ s≈0ᴿ ⟩ - 0ᴿ · v ≈⟨ *ₗ-zeroˡ v ⟩ - 𝟘 ∎ - in s·v≉𝟘 s·v≈𝟘 - } - -non-zeroʳ : {s : R} {v : M} → s · v ≉ᴹ 𝟘 → v ≉ᴹ 𝟘 -non-zeroʳ {s = s} {v = v} s·v≉𝟘 = λ { v≈𝟘 → - let s·v≈𝟘 : s · v ≈ᴹ 𝟘 - s·v≈𝟘 = begin - s · v ≈⟨ *ₗ-congˡ v≈𝟘 ⟩ - s · 𝟘 ≈⟨ *ₗ-zeroʳ s ⟩ - 𝟘 ∎ - in s·v≉𝟘 s·v≈𝟘 - } +s≈𝟘⇒s*v≈𝟘 : ∀ {s} {v} → s ≈ 0# → s *ₗ v ≈ᴹ 0ᴹ +s≈𝟘⇒s*v≈𝟘 {s} {v} s≈𝟘 = begin + s *ₗ v ≈⟨ *ₗ-congʳ s≈𝟘 ⟩ + 0# *ₗ v ≈⟨ *ₗ-zeroˡ v ⟩ + 0ᴹ ∎ + +v≈𝟘⇒s*v≈𝟘 : ∀ {s} {v} → v ≈ᴹ 0ᴹ → s *ₗ v ≈ᴹ 0ᴹ +v≈𝟘⇒s*v≈𝟘 {s} {v} v≈𝟘 = begin + s *ₗ v ≈⟨ *ₗ-congˡ v≈𝟘 ⟩ + s *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ s ⟩ + 0ᴹ ∎ + +non-zeroˡ : ∀ {s} {v} → s *ₗ v ≉ᴹ 0ᴹ → s ≉ 0# +non-zeroˡ = contraposition s≈𝟘⇒s*v≈𝟘 + +non-zeroʳ : ∀ {s} {v} → s *ₗ v ≉ᴹ 0ᴹ → v ≉ᴹ 0ᴹ +non-zeroʳ = contraposition v≈𝟘⇒s*v≈𝟘 From 88e5c2a777e529c0971dc29d8cc81d44047e6704 Mon Sep 17 00:00:00 2001 From: David Banas Date: Sat, 21 May 2022 13:26:29 -0700 Subject: [PATCH 11/19] Temporary check-in only! --- .../Module/Morphism/Linear/Properties.agda | 104 ++++++++---------- 1 file changed, 45 insertions(+), 59 deletions(-) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index 5fc9509378..0bf7cb5446 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -8,7 +8,7 @@ open import Algebra using (CommutativeRing) open import Algebra.Module using (Module) -open import Level using (Level; _⊔_) +open import Level using (Level) module Algebra.Module.Morphism.Linear.Properties {r ℓr m ℓm : Level} @@ -16,37 +16,23 @@ module Algebra.Module.Morphism.Linear.Properties (modA modB : Module ring m ℓm) where -import Algebra.Module.Properties as ModuleProperties -import Function.Definitions -import Relation.Binary.Reasoning.Setoid as Reasoning -import Algebra.Module.Morphism.Structures as MorphismStructures +import Algebra.Module.Properties as ModuleProperties +import Relation.Binary.Reasoning.Setoid as Reasoning +import Algebra.Module.Morphism.Structures as MorphismStructures open import Axiom.DoubleNegationElimination -open import Data.List open import Data.Product - using (Σ; _,_; ∃; Σ-syntax; ∃-syntax; _×_) open import Relation.Nullary using (¬_) open import Relation.Nullary.Negation using (contraposition) open MorphismStructures.ModuleMorphisms modA modB module A = Module modA open A using () renaming (Carrierᴹ to A) --- module A = ModuleProperties A.leftSemimodule --- open ModuleProperties A.leftSemimodule --- using () renaming --- ( non-zeroʳ to non-zeroʳᴬ --- ; non-zeroˡ to non-zeroˡᴬ --- ) module B = Module modB open B using () renaming (Carrierᴹ to B) -module B2 = ModuleProperties B.leftSemimodule --- open ModuleProperties B.leftSemimodule --- using () renaming --- ( non-zeroʳ to non-zeroʳᴮ --- ; non-zeroˡ to non-zeroˡᴮ --- ) -open CommutativeRing ring - using (_≈_; _*_; _+_; 0#) renaming (Carrier to S) +module PA = ModuleProperties modA +module PB = ModuleProperties modB +open CommutativeRing ring renaming (Carrier to S) module _ {f : A → B} @@ -56,34 +42,34 @@ module _ open IsModuleHomomorphism isModuleHomomorphism -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f - f𝟘≈𝟘 : f A.0ᴹ B.≈ᴹ B.0ᴹ - f𝟘≈𝟘 = begin + f0≈0 : f A.0ᴹ B.≈ᴹ B.0ᴹ + f0≈0 = begin f A.0ᴹ ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym (A.*ₗ-zeroˡ A.0ᴹ)) ⟩ f (0# A.*ₗ A.0ᴹ) ≈⟨ *ₗ-homo 0# A.0ᴹ ⟩ 0# B.*ₗ f A.0ᴹ ≈⟨ B.*ₗ-zeroˡ (f A.0ᴹ) ⟩ B.0ᴹ ∎ where open Reasoning B.≈ᴹ-setoid - x≈𝟘⇒fx≈𝟘 : ∀ {x} → x A.≈ᴹ A.0ᴹ → f x B.≈ᴹ B.0ᴹ - x≈𝟘⇒fx≈𝟘 {x} x≈𝟘 = begin - f x ≈⟨ ⟦⟧-cong x≈𝟘 ⟩ - f A.0ᴹ ≈⟨ f𝟘≈𝟘 ⟩ + x≈0⇒fx≈0 : ∀ {x} → x A.≈ᴹ A.0ᴹ → f x B.≈ᴹ B.0ᴹ + x≈0⇒fx≈0 {x} x≈0 = begin + f x ≈⟨ ⟦⟧-cong x≈0 ⟩ + f A.0ᴹ ≈⟨ f0≈0 ⟩ B.0ᴹ ∎ where open Reasoning B.≈ᴹ-setoid - fx≉𝟘⇒x≉𝟘 : ∀ {x} → f x B.≉ᴹ B.0ᴹ → x A.≉ᴹ A.0ᴹ - fx≉𝟘⇒x≉𝟘 = contraposition x≈𝟘⇒fx≈𝟘 + 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 linear map ≉ `const 𝟘`. + -- Zero is a unique output of linear map ≉ `const 0`. zero-unique : ∀ {x} → Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)) → x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ - zero-unique {x} ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 = - B2.non-zeroʳ s·fx≉𝟘 + zero-unique {x} ((s , y) , (s·x≈y , fy≉0)) x≉0 = + PB.non-zeroʳ s·fx≉0 where open Reasoning B.≈ᴹ-setoid - y≉𝟘 : y A.≉ᴹ A.0ᴹ - y≉𝟘 = fx≉𝟘⇒x≉𝟘 fy≉𝟘 + y≉0 : y A.≉ᴹ A.0ᴹ + y≉0 = fx≉0⇒x≉0 fy≉0 fs·x≈fy : f (s A.*ₗ x) B.≈ᴹ f y fs·x≈fy = ⟦⟧-cong s·x≈y s·fx≈fy : s B.*ₗ f x B.≈ᴹ f y @@ -91,51 +77,51 @@ module _ s B.*ₗ f x ≈⟨ B.≈ᴹ-sym (*ₗ-homo s x) ⟩ f (s A.*ₗ x) ≈⟨ fs·x≈fy ⟩ f y ∎ - s·fx≉𝟘 : (s B.*ₗ f x) B.≉ᴹ B.0ᴹ - s·fx≉𝟘 s·fx≈𝟘 = - fy≉𝟘 ( begin + s·fx≉0 : (s B.*ₗ f x) B.≉ᴹ B.0ᴹ + s·fx≉0 s·fx≈0 = + fy≉0 ( begin f y ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym s·x≈y) ⟩ f (s A.*ₗ x) ≈⟨ *ₗ-homo s x ⟩ - s B.*ₗ f x ≈⟨ s·fx≈𝟘 ⟩ + s B.*ₗ f x ≈⟨ s·fx≈0 ⟩ B.0ᴹ ∎ ) -- f is odd (i.e. - f (-x) ≈ - (f x)). - fx+f[-x]≈𝟘 : ∀ {x} → f x B.+ᴹ f (A.-ᴹ x) B.≈ᴹ B.0ᴹ - fx+f[-x]≈𝟘 {x} = begin + fx+f[-x]≈0 : ∀ {x} → f x B.+ᴹ f (A.-ᴹ x) B.≈ᴹ B.0ᴹ + fx+f[-x]≈0 {x} = begin f x B.+ᴹ f (A.-ᴹ x) ≈⟨ B.≈ᴹ-sym (+ᴹ-homo x (A.-ᴹ x)) ⟩ f (x A.+ᴹ (A.-ᴹ x)) ≈⟨ ⟦⟧-cong (A.-ᴹ‿inverseʳ x) ⟩ - f A.0ᴹ ≈⟨ f𝟘≈𝟘 ⟩ + f A.0ᴹ ≈⟨ f0≈0 ⟩ B.0ᴹ ∎ where open Reasoning B.≈ᴹ-setoid f[-x]≈-fx : ∀ {x} → f (A.-ᴹ x) B.≈ᴹ B.-ᴹ f x - f[-x]≈-fx {x} = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) fx+f[-x]≈𝟘 + f[-x]≈-fx {x} = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) fx+f[-x]≈0 module _ {dne : DoubleNegationElimination _} where - fx≈𝟘⇒x≈𝟘 : ∀ {x} → + fx≈0⇒x≈0 : ∀ {x} → Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)) → f x B.≈ᴹ B.0ᴹ → x A.≈ᴹ A.0ᴹ - fx≈𝟘⇒x≈𝟘 {x} ((s , y) , (s·x≈y , fy≉𝟘)) fx≈𝟘 = - dne ¬x≉𝟘 + fx≈0⇒x≈0 {x} ((s , y) , (s·x≈y , fy≉0)) fx≈0 = + dne ¬x≉0 where - ¬x≉𝟘 : ¬ (x A.≉ᴹ A.0ᴹ) - ¬x≉𝟘 = λ x≉𝟘 → zero-unique ((s , y) , (s·x≈y , fy≉𝟘)) x≉𝟘 fx≈𝟘 + ¬x≉0 : ¬ (x A.≉ᴹ A.0ᴹ) + ¬x≉0 = λ x≉0 → zero-unique ((s , y) , (s·x≈y , fy≉0)) x≉0 fx≈0 -- A non-trivial linear function is injective. - fx-fy≈𝟘 : ∀ {x} {y} → (f x B.≈ᴹ f y) → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ - fx-fy≈𝟘 {x} {y} fx≈fy = begin + fx-fy≈0 : ∀ {x} {y} → (f x B.≈ᴹ f y) → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ + fx-fy≈0 {x} {y} fx≈fy = begin 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ᴹ ∎ where open Reasoning B.≈ᴹ-setoid - fx-y≈𝟘 : ∀ {x} {y} → (f x B.≈ᴹ f y) → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ - fx-y≈𝟘 {x} {y} fx≈fy = begin + fx-y≈0 : ∀ {x} {y} → (f x B.≈ᴹ f y) → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ + fx-y≈0 {x} {y} fx≈fy = begin f (x A.+ᴹ (A.-ᴹ y)) ≈⟨ +ᴹ-homo x (A.-ᴹ y) ⟩ f x B.+ᴹ f (A.-ᴹ y) ≈⟨ B.+ᴹ-congˡ f[-x]≈-fx ⟩ - f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx-fy≈𝟘 fx≈fy ⟩ + f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx-fy≈0 fx≈fy ⟩ B.0ᴹ ∎ where open Reasoning B.≈ᴹ-setoid @@ -143,21 +129,21 @@ module _ Σ[ (s , z) ∈ S × A ] ( (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≉𝟘)) fx≈fy = + inj-lm {x} {y} ((s , z) , (s·[x-y]≈z , fz≉0)) fx≈fy = begin x ≈⟨ x≈--y ⟩ - A.-ᴹ (A.-ᴹ y) ≈⟨ A.-ᴹ-involutive y ⟩ + A.-ᴹ (A.-ᴹ y) ≈⟨ PA.-ᴹ-involutive y ⟩ y ∎ where open Reasoning A.≈ᴹ-setoid - x-y≈𝟘 : x A.+ᴹ (A.-ᴹ y) A.≈ᴹ A.0ᴹ - x-y≈𝟘 = fx≈𝟘⇒x≈𝟘 {x = x A.+ᴹ (A.-ᴹ y)} - ((s , z) , s·[x-y]≈z , fz≉𝟘) - (fx-y≈𝟘 fx≈fy) + x-y≈0 : x A.+ᴹ (A.-ᴹ y) A.≈ᴹ A.0ᴹ + x-y≈0 = fx≈0⇒x≈0 {x = x A.+ᴹ (A.-ᴹ y)} + ((s , z) , s·[x-y]≈z , fz≉0) + (fx-y≈0 fx≈fy) x≈--y : x A.≈ᴹ A.-ᴹ (A.-ᴹ y) x≈--y = A.uniqueʳ‿-ᴹ (A.-ᴹ y) x ( begin A.-ᴹ y A.+ᴹ x ≈⟨ A.+ᴹ-comm (A.-ᴹ y) x ⟩ - x A.+ᴹ A.-ᴹ y ≈⟨ x-y≈𝟘 ⟩ + x A.+ᴹ A.-ᴹ y ≈⟨ x-y≈0 ⟩ A.0ᴹ ∎ ) From d2da8f0facde4cc9a01a441b8d86db3973ff3dfb Mon Sep 17 00:00:00 2001 From: David Banas Date: Sat, 21 May 2022 15:30:51 -0700 Subject: [PATCH 12/19] Changes, as per Matthew Daggitt, re: PR #1767 --- src/Algebra/Module/Bundles.agda | 45 +++++-------------- .../Module/Morphism/Linear/Properties.agda | 44 +++++++----------- src/Algebra/Module/Properties.agda | 43 +++++------------- src/Algebra/Module/Properties/Semimodule.agda | 40 +++++++++++++++++ 4 files changed, 75 insertions(+), 97 deletions(-) create mode 100644 src/Algebra/Module/Properties/Semimodule.agda diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index 0986263993..f6224ef201 100644 --- a/src/Algebra/Module/Bundles.agda +++ b/src/Algebra/Module/Bundles.agda @@ -99,10 +99,6 @@ record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ -ᴹ_ : Op₁ Carrierᴹ isLeftModule : IsLeftModule ring _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ - infix 4 _≉ᴹ_ - _≉ᴹ_ : Rel Carrierᴹ _ - a ≉ᴹ b = ¬ (a ≈ᴹ b) - open IsLeftModule isLeftModule public leftSemimodule : LeftSemimodule semiring m ℓm @@ -110,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 } @@ -175,10 +171,6 @@ record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ -ᴹ_ : Op₁ Carrierᴹ isRightModule : IsRightModule ring _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ - infix 4 _≉ᴹ_ - _≉ᴹ_ : Rel Carrierᴹ _ - a ≉ᴹ b = ¬ (a ≈ᴹ b) - open IsRightModule isRightModule public rightSemimodule : RightSemimodule semiring m ℓm @@ -186,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 } @@ -217,10 +209,6 @@ record Bisemimodule (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs 0ᴹ : Carrierᴹ isBisemimodule : IsBisemimodule R-semiring S-semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ - infix 4 _≉ᴹ_ - _≉ᴹ_ : Rel Carrierᴹ _ - a ≉ᴹ b = ¬ (a ≈ᴹ b) - open IsBisemimodule isBisemimodule public leftSemimodule : LeftSemimodule R-semiring m ℓm @@ -231,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 @@ -253,10 +241,6 @@ record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm -ᴹ_ : Op₁ Carrierᴹ isBimodule : IsBimodule R-ring S-ring _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ - infix 4 _≉ᴹ_ - _≉ᴹ_ : Rel Carrierᴹ _ - a ≉ᴹ b = ¬ (a ≈ᴹ b) - open IsBimodule isBimodule public leftModule : LeftModule R-ring m ℓm @@ -267,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 } @@ -297,10 +282,6 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm 0ᴹ : Carrierᴹ isSemimodule : IsSemimodule commutativeSemiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_ - infix 4 _≉ᴹ_ - _≉ᴹ_ : Rel Carrierᴹ _ - a ≉ᴹ b = ¬ (a ≈ᴹ b) - open IsSemimodule isSemimodule public private @@ -313,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 @@ -346,14 +327,10 @@ 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ᴹ -ᴹ_ _*ₗ_ _*ᵣ_ - infix 4 _≉ᴹ_ - _≉ᴹ_ : Rel Carrierᴹ _ - a ≉ᴹ b = ¬ (a ≈ᴹ b) - open IsModule isModule public bimodule : Bimodule ring ring m ℓm @@ -362,12 +339,10 @@ 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 } open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm) - - -ᴹ-involutive : Involutive _≈ᴹ_ -ᴹ_ - -ᴹ-involutive = ⁻¹-involutive +ᴹ-group diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index 0bf7cb5446..48263cbc71 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -17,11 +17,11 @@ module Algebra.Module.Morphism.Linear.Properties where import Algebra.Module.Properties as ModuleProperties -import Relation.Binary.Reasoning.Setoid as Reasoning import Algebra.Module.Morphism.Structures as MorphismStructures 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) @@ -43,43 +43,33 @@ module _ -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f f0≈0 : f A.0ᴹ B.≈ᴹ B.0ᴹ - f0≈0 = begin + f0≈0 = begin⟨ B.≈ᴹ-setoid ⟩ f A.0ᴹ ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym (A.*ₗ-zeroˡ A.0ᴹ)) ⟩ f (0# A.*ₗ A.0ᴹ) ≈⟨ *ₗ-homo 0# A.0ᴹ ⟩ 0# B.*ₗ f A.0ᴹ ≈⟨ B.*ₗ-zeroˡ (f A.0ᴹ) ⟩ B.0ᴹ ∎ - where open Reasoning B.≈ᴹ-setoid x≈0⇒fx≈0 : ∀ {x} → x A.≈ᴹ A.0ᴹ → f x B.≈ᴹ B.0ᴹ - x≈0⇒fx≈0 {x} x≈0 = begin + x≈0⇒fx≈0 {x} x≈0 = begin⟨ B.≈ᴹ-setoid ⟩ f x ≈⟨ ⟦⟧-cong x≈0 ⟩ f A.0ᴹ ≈⟨ f0≈0 ⟩ B.0ᴹ ∎ - where open Reasoning B.≈ᴹ-setoid 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 linear map ≉ `const 0`. zero-unique : ∀ {x} → - Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)) → - x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ + Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)) → + x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ zero-unique {x} ((s , y) , (s·x≈y , fy≉0)) x≉0 = - PB.non-zeroʳ s·fx≉0 + PB.s*v≉0⇒v≉0 s·fx≉0 where - open Reasoning B.≈ᴹ-setoid y≉0 : y A.≉ᴹ A.0ᴹ y≉0 = fx≉0⇒x≉0 fy≉0 - fs·x≈fy : f (s A.*ₗ x) B.≈ᴹ f y - fs·x≈fy = ⟦⟧-cong s·x≈y - s·fx≈fy : s B.*ₗ f x B.≈ᴹ f y - s·fx≈fy = begin - s B.*ₗ f x ≈⟨ B.≈ᴹ-sym (*ₗ-homo s x) ⟩ - f (s A.*ₗ x) ≈⟨ fs·x≈fy ⟩ - f y ∎ s·fx≉0 : (s B.*ₗ f x) B.≉ᴹ B.0ᴹ s·fx≉0 s·fx≈0 = - fy≉0 ( begin + 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 ⟩ @@ -88,12 +78,11 @@ module _ -- f is odd (i.e. - f (-x) ≈ - (f x)). fx+f[-x]≈0 : ∀ {x} → f x B.+ᴹ f (A.-ᴹ x) B.≈ᴹ B.0ᴹ - fx+f[-x]≈0 {x} = begin + 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ᴹ ≈⟨ f0≈0 ⟩ B.0ᴹ ∎ - where open Reasoning B.≈ᴹ-setoid f[-x]≈-fx : ∀ {x} → f (A.-ᴹ x) B.≈ᴹ B.-ᴹ f x f[-x]≈-fx {x} = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) fx+f[-x]≈0 @@ -110,39 +99,36 @@ module _ ¬x≉0 = λ x≉0 → zero-unique ((s , y) , (s·x≈y , fy≉0)) x≉0 fx≈0 -- A non-trivial linear function is injective. - fx-fy≈0 : ∀ {x} {y} → (f x B.≈ᴹ f y) → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ - fx-fy≈0 {x} {y} fx≈fy = begin + fx-fy≈0 : ∀ {x y} → f x B.≈ᴹ f y → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ + 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ᴹ ∎ - where open Reasoning B.≈ᴹ-setoid - fx-y≈0 : ∀ {x} {y} → (f x B.≈ᴹ f y) → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ - fx-y≈0 {x} {y} fx≈fy = begin + fx-y≈0 : ∀ {x y} → f x B.≈ᴹ f y → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ + fx-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 ⟩ f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx-fy≈0 fx≈fy ⟩ B.0ᴹ ∎ - where open Reasoning B.≈ᴹ-setoid - inj-lm : ∀ {x} {y} → + inj-lm : ∀ {x y} → Σ[ (s , z) ∈ S × A ] ( (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 + begin⟨ A.≈ᴹ-setoid ⟩ x ≈⟨ x≈--y ⟩ A.-ᴹ (A.-ᴹ y) ≈⟨ PA.-ᴹ-involutive y ⟩ y ∎ where - open Reasoning A.≈ᴹ-setoid x-y≈0 : x A.+ᴹ (A.-ᴹ y) A.≈ᴹ A.0ᴹ x-y≈0 = fx≈0⇒x≈0 {x = x A.+ᴹ (A.-ᴹ y)} ((s , z) , s·[x-y]≈z , fz≉0) (fx-y≈0 fx≈fy) x≈--y : x A.≈ᴹ A.-ᴹ (A.-ᴹ y) x≈--y = A.uniqueʳ‿-ᴹ (A.-ᴹ y) x - ( begin + ( begin⟨ A.≈ᴹ-setoid ⟩ A.-ᴹ y A.+ᴹ x ≈⟨ A.+ᴹ-comm (A.-ᴹ y) x ⟩ x A.+ᴹ A.-ᴹ y ≈⟨ x-y≈0 ⟩ A.0ᴹ ∎ diff --git a/src/Algebra/Module/Properties.agda b/src/Algebra/Module/Properties.agda index beb16b9705..980d92a6bd 100644 --- a/src/Algebra/Module/Properties.agda +++ b/src/Algebra/Module/Properties.agda @@ -6,42 +6,19 @@ {-# OPTIONS --without-K --safe #-} -open import Algebra using (Semiring) -open import Algebra.Module.Bundles using (LeftSemimodule) +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} {semiring : Semiring r ℓr} - (lsmod : LeftSemimodule semiring m ℓm) + {r ℓr m ℓm : Level} + {ring : CommutativeRing r ℓr} + (mod : Module ring m ℓm) where -open import Relation.Nullary using (¬_) -open import Relation.Nullary.Negation using (contraposition) +open Module mod +open import Algebra.Module.Properties.Semimodule semimodule public +open import Algebra.Properties.Group using (⁻¹-involutive) -open LeftSemimodule lsmod - using ( *ₗ-zeroˡ; *ₗ-zeroʳ; ≈ᴹ-setoid; *ₗ-congˡ; *ₗ-congʳ - ; _*ₗ_; 0ᴹ; _≈ᴹ_; _≉ᴹ_) - renaming (Carrierᴹ to M) - -open Semiring semiring - using (_≈_; _≉_; 0#) renaming (Carrier to R) - -open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid - -s≈𝟘⇒s*v≈𝟘 : ∀ {s} {v} → s ≈ 0# → s *ₗ v ≈ᴹ 0ᴹ -s≈𝟘⇒s*v≈𝟘 {s} {v} s≈𝟘 = begin - s *ₗ v ≈⟨ *ₗ-congʳ s≈𝟘 ⟩ - 0# *ₗ v ≈⟨ *ₗ-zeroˡ v ⟩ - 0ᴹ ∎ - -v≈𝟘⇒s*v≈𝟘 : ∀ {s} {v} → v ≈ᴹ 0ᴹ → s *ₗ v ≈ᴹ 0ᴹ -v≈𝟘⇒s*v≈𝟘 {s} {v} v≈𝟘 = begin - s *ₗ v ≈⟨ *ₗ-congˡ v≈𝟘 ⟩ - s *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ s ⟩ - 0ᴹ ∎ - -non-zeroˡ : ∀ {s} {v} → s *ₗ v ≉ᴹ 0ᴹ → s ≉ 0# -non-zeroˡ = contraposition s≈𝟘⇒s*v≈𝟘 - -non-zeroʳ : ∀ {s} {v} → s *ₗ v ≉ᴹ 0ᴹ → v ≉ᴹ 0ᴹ -non-zeroʳ = contraposition v≈𝟘⇒s*v≈𝟘 +-ᴹ-involutive : Involutive _≈ᴹ_ -ᴹ_ +-ᴹ-involutive = ⁻¹-involutive +ᴹ-group diff --git a/src/Algebra/Module/Properties/Semimodule.agda b/src/Algebra/Module/Properties/Semimodule.agda new file mode 100644 index 0000000000..0f150edf4b --- /dev/null +++ b/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 + +s≈0⇒s*v≈0 : ∀ {s} {v} → s ≈ 0# → s *ₗ v ≈ᴹ 0ᴹ +s≈0⇒s*v≈0 {s} {v} s≈0 = begin + s *ₗ v ≈⟨ *ₗ-congʳ s≈0 ⟩ + 0# *ₗ v ≈⟨ *ₗ-zeroˡ v ⟩ + 0ᴹ ∎ + +v≈0⇒s*v≈0 : ∀ {s} {v} → v ≈ᴹ 0ᴹ → s *ₗ v ≈ᴹ 0ᴹ +v≈0⇒s*v≈0 {s} {v} v≈0 = begin + s *ₗ v ≈⟨ *ₗ-congˡ v≈0 ⟩ + s *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ s ⟩ + 0ᴹ ∎ + +s*v≉0⇒s≉0 : ∀ {s} {v} → s *ₗ v ≉ᴹ 0ᴹ → s ≉ 0# +s*v≉0⇒s≉0 = contraposition s≈0⇒s*v≈0 + +s*v≉0⇒v≉0 : ∀ {s} {v} → s *ₗ v ≉ᴹ 0ᴹ → v ≉ᴹ 0ᴹ +s*v≉0⇒v≉0 = contraposition v≈0⇒s*v≈0 From c5de4d1637fdd7514b78a0b4108b1519ae264b7c Mon Sep 17 00:00:00 2001 From: David Banas Date: Sun, 29 May 2022 09:48:13 -0700 Subject: [PATCH 13/19] Responding to Jacques feedback. --- .../Module/Morphism/Linear/Properties.agda | 44 ++++++++----------- 1 file changed, 18 insertions(+), 26 deletions(-) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index 48263cbc71..4ee6f94daf 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -41,24 +41,16 @@ module _ open IsModuleHomomorphism isModuleHomomorphism - -- f(x) ≈ 0 iff x ≈ 0, for linear non-trivial f - f0≈0 : f A.0ᴹ B.≈ᴹ B.0ᴹ - f0≈0 = begin⟨ B.≈ᴹ-setoid ⟩ - f A.0ᴹ ≈⟨ ⟦⟧-cong (A.≈ᴹ-sym (A.*ₗ-zeroˡ A.0ᴹ)) ⟩ - f (0# A.*ₗ A.0ᴹ) ≈⟨ *ₗ-homo 0# A.0ᴹ ⟩ - 0# B.*ₗ f A.0ᴹ ≈⟨ B.*ₗ-zeroˡ (f A.0ᴹ) ⟩ - 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ᴹ ≈⟨ f0≈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 linear map ≉ `const 0`. + -- Zero is a unique output of non-trivial (i.e. - ≉ `const 0`) linear map. zero-unique : ∀ {x} → Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)) → x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ @@ -81,12 +73,26 @@ module _ 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ᴹ ≈⟨ f0≈0 ⟩ + f A.0ᴹ ≈⟨ 0ᴹ-homo ⟩ B.0ᴹ ∎ f[-x]≈-fx : ∀ {x} → f (A.-ᴹ x) B.≈ᴹ B.-ᴹ f x f[-x]≈-fx {x} = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) fx+f[-x]≈0 + -- A non-trivial linear function is injective. + fx-fy≈0 : ∀ {x y} → f x B.≈ᴹ f y → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ + 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-y≈0 : ∀ {x y} → f x B.≈ᴹ f y → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ + fx-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 ⟩ + f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx-fy≈0 fx≈fy ⟩ + B.0ᴹ ∎ + module _ {dne : DoubleNegationElimination _} where fx≈0⇒x≈0 : ∀ {x} → @@ -97,21 +103,7 @@ module _ where ¬x≉0 : ¬ (x A.≉ᴹ A.0ᴹ) ¬x≉0 = λ x≉0 → zero-unique ((s , y) , (s·x≈y , fy≉0)) x≉0 fx≈0 - - -- A non-trivial linear function is injective. - fx-fy≈0 : ∀ {x y} → f x B.≈ᴹ f y → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ - 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-y≈0 : ∀ {x y} → f x B.≈ᴹ f y → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ - fx-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 ⟩ - f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx-fy≈0 fx≈fy ⟩ - B.0ᴹ ∎ - + inj-lm : ∀ {x y} → Σ[ (s , z) ∈ S × A ] ( (s A.*ₗ (x A.+ᴹ A.-ᴹ y) A.≈ᴹ z) × (f z B.≉ᴹ B.0ᴹ)) → From b790ffbd0ae65449681c463c378307102d8747b3 Mon Sep 17 00:00:00 2001 From: David Banas Date: Wed, 13 Jul 2022 07:31:42 -0700 Subject: [PATCH 14/19] Clean-up after merging in upstream master. --- src/Algebra/Module/Morphism/Linear/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index 4ee6f94daf..b45b377496 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -103,7 +103,7 @@ module _ where ¬x≉0 : ¬ (x A.≉ᴹ A.0ᴹ) ¬x≉0 = λ x≉0 → zero-unique ((s , y) , (s·x≈y , fy≉0)) x≉0 fx≈0 - + inj-lm : ∀ {x y} → Σ[ (s , z) ∈ S × A ] ( (s A.*ₗ (x A.+ᴹ A.-ᴹ y) A.≈ᴹ z) × (f z B.≉ᴹ B.0ᴹ)) → From 48ad48c0bf7a238b2847d41d33c766d4530fdc3f Mon Sep 17 00:00:00 2001 From: David Banas Date: Wed, 13 Jul 2022 07:34:14 -0700 Subject: [PATCH 15/19] Some additions to `.gitignore`. --- .gitignore | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.gitignore b/.gitignore index d3516eb0f2..99f960e19f 100644 --- a/.gitignore +++ b/.gitignore @@ -11,6 +11,8 @@ *.vim *~ .*.swp +.#* +\#* ./_build/* .DS_Store .vscode/* From 8b0a487ba44a8867f1b641617eeccb5be69b3796 Mon Sep 17 00:00:00 2001 From: David Banas Date: Fri, 15 Jul 2022 06:43:01 -0700 Subject: [PATCH 16/19] Responding to Matthew`s requests. --- .../Module/Morphism/Linear/Properties.agda | 43 +++++++++---------- src/Algebra/Module/Properties/Semimodule.agda | 8 ++-- 2 files changed, 24 insertions(+), 27 deletions(-) diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/Linear/Properties.agda index b45b377496..f017c77be2 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/Linear/Properties.agda @@ -41,6 +41,12 @@ module _ open IsModuleHomomorphism isModuleHomomorphism + NonTrivial : A → Set (r Level.⊔ m Level.⊔ ℓm) + NonTrivial x = (∃₂ λ s y → ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ))) + -- NonTrivial x = Σ[ (s , y) ∈ S × A ] ( (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 ⟩ @@ -51,14 +57,10 @@ module _ fx≉0⇒x≉0 = contraposition x≈0⇒fx≈0 -- Zero is a unique output of non-trivial (i.e. - ≉ `const 0`) linear map. - zero-unique : ∀ {x} → - Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)) → - x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ - zero-unique {x} ((s , y) , (s·x≈y , fy≉0)) x≉0 = + zero-unique : ∀ {x} → NonTrivial x → x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ + zero-unique {x} (s , y , s·x≈y , fy≉0) x≉0 = PB.s*v≉0⇒v≉0 s·fx≉0 where - y≉0 : y A.≉ᴹ A.0ᴹ - y≉0 = fx≉0⇒x≉0 fy≉0 s·fx≉0 : (s B.*ₗ f x) B.≉ᴹ B.0ᴹ s·fx≉0 s·fx≈0 = fy≉0 ( begin⟨ B.≈ᴹ-setoid ⟩ @@ -80,44 +82,39 @@ module _ f[-x]≈-fx {x} = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) fx+f[-x]≈0 -- A non-trivial linear function is injective. - fx-fy≈0 : ∀ {x y} → f x B.≈ᴹ f y → f x B.+ᴹ (B.-ᴹ f y) B.≈ᴹ B.0ᴹ - fx-fy≈0 {x} {y} fx≈fy = begin⟨ B.≈ᴹ-setoid ⟩ + 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-y≈0 : ∀ {x y} → f x B.≈ᴹ f y → f (x A.+ᴹ (A.-ᴹ y)) B.≈ᴹ B.0ᴹ - fx-y≈0 {x} {y} fx≈fy = begin⟨ B.≈ᴹ-setoid ⟩ + 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 ⟩ - f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx-fy≈0 fx≈fy ⟩ + f x B.+ᴹ (B.-ᴹ f y) ≈⟨ fx≈fy⇒fx-fy≈0 fx≈fy ⟩ B.0ᴹ ∎ module _ {dne : DoubleNegationElimination _} where - fx≈0⇒x≈0 : ∀ {x} → - Σ[ (s , y) ∈ S × A ] ((s A.*ₗ x A.≈ᴹ y) × (f y B.≉ᴹ B.0ᴹ)) → - f x B.≈ᴹ B.0ᴹ → x A.≈ᴹ A.0ᴹ - fx≈0⇒x≈0 {x} ((s , y) , (s·x≈y , fy≉0)) fx≈0 = + 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 → zero-unique ((s , y) , (s·x≈y , fy≉0)) x≉0 fx≈0 + ¬x≉0 = λ x≉0 → zero-unique (s , y , s·x≈y , fy≉0) x≉0 fx≈0 inj-lm : ∀ {x y} → - Σ[ (s , z) ∈ S × A ] ( (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 = + (∃₂ λ 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 {x = x A.+ᴹ (A.-ᴹ y)} - ((s , z) , s·[x-y]≈z , fz≉0) - (fx-y≈0 fx≈fy) + 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 ⟩ diff --git a/src/Algebra/Module/Properties/Semimodule.agda b/src/Algebra/Module/Properties/Semimodule.agda index 0f150edf4b..366711786a 100644 --- a/src/Algebra/Module/Properties/Semimodule.agda +++ b/src/Algebra/Module/Properties/Semimodule.agda @@ -21,20 +21,20 @@ open Semimodule semimod open import Relation.Nullary.Negation using (contraposition) open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid -s≈0⇒s*v≈0 : ∀ {s} {v} → s ≈ 0# → s *ₗ v ≈ᴹ 0ᴹ +s≈0⇒s*v≈0 : ∀ {s v} → s ≈ 0# → s *ₗ v ≈ᴹ 0ᴹ s≈0⇒s*v≈0 {s} {v} s≈0 = begin s *ₗ v ≈⟨ *ₗ-congʳ s≈0 ⟩ 0# *ₗ v ≈⟨ *ₗ-zeroˡ v ⟩ 0ᴹ ∎ -v≈0⇒s*v≈0 : ∀ {s} {v} → v ≈ᴹ 0ᴹ → s *ₗ v ≈ᴹ 0ᴹ +v≈0⇒s*v≈0 : ∀ {s v} → v ≈ᴹ 0ᴹ → s *ₗ v ≈ᴹ 0ᴹ v≈0⇒s*v≈0 {s} {v} v≈0 = begin s *ₗ v ≈⟨ *ₗ-congˡ v≈0 ⟩ s *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ s ⟩ 0ᴹ ∎ -s*v≉0⇒s≉0 : ∀ {s} {v} → s *ₗ v ≉ᴹ 0ᴹ → s ≉ 0# +s*v≉0⇒s≉0 : ∀ {s v} → s *ₗ v ≉ᴹ 0ᴹ → s ≉ 0# s*v≉0⇒s≉0 = contraposition s≈0⇒s*v≈0 -s*v≉0⇒v≉0 : ∀ {s} {v} → s *ₗ v ≉ᴹ 0ᴹ → v ≉ᴹ 0ᴹ +s*v≉0⇒v≉0 : ∀ {s v} → s *ₗ v ≉ᴹ 0ᴹ → v ≉ᴹ 0ᴹ s*v≉0⇒v≉0 = contraposition v≈0⇒s*v≈0 From aec22036485c38a211bf7db9035d127577057aaa Mon Sep 17 00:00:00 2001 From: David Banas Date: Sat, 16 Jul 2022 09:00:15 -0700 Subject: [PATCH 17/19] Responding to additional requests from Matthew. --- CHANGELOG.md | 2 +- ...roperties.agda => ModuleHomomorphism.agda} | 48 +++++++++---------- 2 files changed, 23 insertions(+), 27 deletions(-) rename src/Algebra/Module/Morphism/{Linear/Properties.agda => ModuleHomomorphism.agda} (76%) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3c9a61499b..b4f6810080 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -989,7 +989,7 @@ New modules * Proofs of some axioms of linearity: ``` - Algebra.Module.Morphism.Linear.Properties + Algebra.Module.Morphism.ModuleHomomorphism Algebra.Module.Properties ``` diff --git a/src/Algebra/Module/Morphism/Linear/Properties.agda b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda similarity index 76% rename from src/Algebra/Module/Morphism/Linear/Properties.agda rename to src/Algebra/Module/Morphism/ModuleHomomorphism.agda index f017c77be2..909fe73315 100644 --- a/src/Algebra/Module/Morphism/Linear/Properties.agda +++ b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda @@ -6,19 +6,19 @@ {-# 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.Linear.Properties +module Algebra.Module.Morphism.ModuleHomomorphism {r ℓr m ℓm : Level} {ring : CommutativeRing r ℓr} (modA modB : Module ring m ℓm) where -import Algebra.Module.Properties as ModuleProperties -import Algebra.Module.Morphism.Structures as MorphismStructures - open import Axiom.DoubleNegationElimination open import Data.Product open import Relation.Binary.Reasoning.MultiSetoid @@ -41,11 +41,11 @@ module _ 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ᴹ))) - -- NonTrivial x = Σ[ (s , y) ∈ S × A ] ( (s A.*ₗ x A.≈ᴹ y) - -- × (f y B.≉ᴹ B.0ᴹ) - -- ) + 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 ⟩ @@ -57,29 +57,25 @@ module _ fx≉0⇒x≉0 = contraposition x≈0⇒fx≈0 -- Zero is a unique output of non-trivial (i.e. - ≉ `const 0`) linear map. - zero-unique : ∀ {x} → NonTrivial x → x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ - zero-unique {x} (s , y , s·x≈y , fy≉0) x≉0 = - PB.s*v≉0⇒v≉0 s·fx≉0 - where - s·fx≉0 : (s B.*ₗ f x) B.≉ᴹ B.0ᴹ - s·fx≉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ᴹ ∎ - ) + 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.s*v≉0⇒v≉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} → f x B.+ᴹ f (A.-ᴹ x) B.≈ᴹ B.0ᴹ - fx+f[-x]≈0 {x} = begin⟨ B.≈ᴹ-setoid ⟩ + 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} → f (A.-ᴹ x) B.≈ᴹ B.-ᴹ f x - f[-x]≈-fx {x} = B.uniqueʳ‿-ᴹ (f x) (f (A.-ᴹ x)) fx+f[-x]≈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ᴹ @@ -91,7 +87,7 @@ module _ 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 ⟩ + 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ᴹ ∎ @@ -102,7 +98,7 @@ module _ dne ¬x≉0 where ¬x≉0 : ¬ (x A.≉ᴹ A.0ᴹ) - ¬x≉0 = λ x≉0 → zero-unique (s , y , s·x≈y , fy≉0) x≉0 fx≈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ᴹ))) → From b6da4e9395d31188c09ab4e688068fc0483bcfe5 Mon Sep 17 00:00:00 2001 From: David Banas Date: Mon, 18 Jul 2022 19:00:27 -0700 Subject: [PATCH 18/19] Responding to Matthew`s final requests. --- .../Module/Morphism/ModuleHomomorphism.agda | 171 +++++++++--------- src/Algebra/Module/Properties/Semimodule.agda | 24 +-- 2 files changed, 96 insertions(+), 99 deletions(-) diff --git a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda index 909fe73315..62485f454c 100644 --- a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda +++ b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda @@ -17,6 +17,11 @@ 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 @@ -25,96 +30,88 @@ open import Relation.Binary.Reasoning.MultiSetoid open import Relation.Nullary using (¬_) open import Relation.Nullary.Negation using (contraposition) -open MorphismStructures.ModuleMorphisms modA modB module A = Module modA -open A using () renaming (Carrierᴹ to A) module B = Module modB -open B using () renaming (Carrierᴹ to B) module PA = ModuleProperties modA module PB = ModuleProperties modB open CommutativeRing ring renaming (Carrier to S) -module _ - {f : A → B} - (isModuleHomomorphism : IsModuleHomomorphism f) - where - - 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.s*v≉0⇒v≉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ᴹ ∎ - ) +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ᴹ ∎ + ) diff --git a/src/Algebra/Module/Properties/Semimodule.agda b/src/Algebra/Module/Properties/Semimodule.agda index 366711786a..f7c5e51c17 100644 --- a/src/Algebra/Module/Properties/Semimodule.agda +++ b/src/Algebra/Module/Properties/Semimodule.agda @@ -21,20 +21,20 @@ open Semimodule semimod open import Relation.Nullary.Negation using (contraposition) open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid -s≈0⇒s*v≈0 : ∀ {s v} → s ≈ 0# → s *ₗ v ≈ᴹ 0ᴹ -s≈0⇒s*v≈0 {s} {v} s≈0 = begin - s *ₗ v ≈⟨ *ₗ-congʳ s≈0 ⟩ - 0# *ₗ v ≈⟨ *ₗ-zeroˡ v ⟩ +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ᴹ ∎ -v≈0⇒s*v≈0 : ∀ {s v} → v ≈ᴹ 0ᴹ → s *ₗ v ≈ᴹ 0ᴹ -v≈0⇒s*v≈0 {s} {v} v≈0 = begin - s *ₗ v ≈⟨ *ₗ-congˡ v≈0 ⟩ - s *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ s ⟩ +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ᴹ ∎ -s*v≉0⇒s≉0 : ∀ {s v} → s *ₗ v ≉ᴹ 0ᴹ → s ≉ 0# -s*v≉0⇒s≉0 = contraposition s≈0⇒s*v≈0 +x*y≉0⇒x≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → x ≉ 0# +x*y≉0⇒x≉0 = contraposition x≈0⇒x*y≈0 -s*v≉0⇒v≉0 : ∀ {s v} → s *ₗ v ≉ᴹ 0ᴹ → v ≉ᴹ 0ᴹ -s*v≉0⇒v≉0 = contraposition v≈0⇒s*v≈0 +x*y≉0⇒y≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → y ≉ᴹ 0ᴹ +x*y≉0⇒y≉0 = contraposition y≈0⇒x*y≈0 From be44f3272a6950af851ee0ad5d8865473fb1728b Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Wed, 20 Jul 2022 03:56:58 +0800 Subject: [PATCH 19/19] Tweak to CHANGELOG --- CHANGELOG.md | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b4f6810080..0254d5da92 100644 --- a/CHANGELOG.md +++ b/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: @@ -1082,11 +1083,6 @@ Other minor changes _^ᵗ_ : A → ℕ → A ``` -* Added new proofs to `Algebra.Module.Bundles`: - ``` - -ᴹ-involutive : Involutive _≈ᴹ_ -ᴹ_ - ``` - * Added new proofs to `Algebra.Properties.CommutativeSemigroup`: ``` interchange : Interchangable _∙_ _∙_