From c05e2029a18743fddcf00971988157e244d82e97 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 3 Jan 2024 12:40:41 +0000 Subject: [PATCH 01/23] Nagata's construction --- CHANGELOG.md | 5 + src/Algebra/Module/Construct/Nagata.agda | 171 +++++++++++++++++++++++ 2 files changed, 176 insertions(+) create mode 100644 src/Algebra/Module/Construct/Nagata.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 8be73afc66..f2784fcff7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,6 +29,11 @@ Deprecated names New modules ----------- +* Nagata's construction of the "idealization of a module": + ```agda + Algebra.Module.Construct.Nagata + ``` + Additions to existing modules ----------------------------- diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda new file mode 100644 index 0000000000..c655cefd65 --- /dev/null +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -0,0 +1,171 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The non-commutative analogue of Nagata's construction +-- of the "idealization of a module", defined here +-- on R-R-*bi*modules M over a ring R. +-- +-- Elements of R ⋉ M are pairs |R| × |M| +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Algebra.Module.Construct.Nagata where + +open import Algebra.Bundles +open import Algebra.Core +import Algebra.Consequences.Setoid as Consequences +import Algebra.Definitions as Definitions +open import Algebra.Module.Bundles +open import Algebra.Module.Core +open import Algebra.Module.Definitions +import Algebra.Module.Construct.DirectProduct as DirectProduct +import Algebra.Module.Construct.TensorUnit as TensorUnit +open import Algebra.Structures +open import Data.Product using (_×_; _,_; proj₁; proj₂) +open import Data.Product.Relation.Binary.Pointwise.NonDependent +open import Level using (Level; _⊔_) +open import Relation.Binary using (Rel; Setoid; IsEquivalence) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +private + variable + m ℓm r ℓr : Level + +------------------------------------------------------------------------ +-- Definitions + +module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where + + open Ring ring + renaming (Carrier to R + ; 0# to 0ᴿ + ; 1# to 1ᴿ + ; _+_ to _+ᴿ_ + ; _*_ to _*ᴿ_ + ; *-cong to *ᴿ-cong + ; *-assoc to *ᴿ-assoc + ; *-identityʳ to *ᴿ-identityʳ + ; *-identityˡ to *ᴿ-identityˡ + ; distribˡ to *ᴿ-distribˡ-+ᴿ + ; distribʳ to *ᴿ-distribʳ-+ᴿ + ) + + open Bimodule bimodule + renaming (Carrierᴹ to M + ) + + open AbelianGroup +ᴹ-abelianGroup + renaming (setoid to setoidᴹ + ; isEquivalence to isEquivalenceᴹ + ) + + open IsEquivalence isEquivalenceᴹ + renaming (sym to symᴹ) + + +ᴺ-bimodule = DirectProduct.bimodule TensorUnit.bimodule bimodule + + open Bimodule +ᴺ-bimodule public using () + renaming (Carrierᴹ to N + ; _≈ᴹ_ to _≈ᴺ_ + ; _+ᴹ_ to _+ᴺ_ + ; 0ᴹ to 0ᴺ + ; -ᴹ_ to -ᴺ_ + ; +ᴹ-abelianGroup to +ᴺ-abelianGroup + ) + + ιᴿ : R → N + ιᴿ r = r , 0ᴹ + + ιᴹ : M → N + ιᴹ m = 0ᴿ , m + + 1ᴺ : N + 1ᴺ = ιᴿ 1ᴿ + + open AbelianGroup +ᴺ-abelianGroup + renaming (isAbelianGroup to +ᴺ-isAbelianGroup) + + open Definitions _≈ᴺ_ + + infixl 7 _*ᴺ_ + + _*ᴺ_ : Op₂ N + (r₁ , m₁) *ᴺ (r₂ , m₂) = r₁ *ᴿ r₂ , r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂ + + *ᴺ-identity : Identity 1ᴺ _*ᴺ_ + *ᴺ-identity = lᴺ , rᴺ + where + open ≈-Reasoning setoidᴹ + lᴺ : LeftIdentity 1ᴺ _*ᴺ_ + lᴺ (r , m) = (*ᴿ-identityˡ r) , (begin + (1ᴿ *ₗ m +ᴹ 0ᴹ *ᵣ r) ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ + (m +ᴹ 0ᴹ) ≈⟨ +ᴹ-identityʳ m ⟩ + m ∎) + rᴺ : RightIdentity 1ᴺ _*ᴺ_ + rᴺ (r , m) = (*ᴿ-identityʳ r) , (begin + r *ₗ 0ᴹ +ᴹ m *ᵣ 1ᴿ ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ + 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ + m ∎) + + *ᴺ-cong : Congruent₂ _*ᴺ_ + *ᴺ-cong (r₁ , m₁) (r₂ , m₂) = *ᴿ-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) + + *ᴺ-assoc : Associative _*ᴺ_ + *ᴺ-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-assoc r₁ r₂ r₃ , (begin + (r₁ *ᴿ r₂) *ₗ m₃ +ᴹ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) *ᵣ r₃ + ≈⟨ +ᴹ-cong (*ₗ-assoc r₁ r₂ m₃) (*ᵣ-distribʳ r₃ (r₁ *ₗ m₂) (m₁ *ᵣ r₂)) ⟩ + r₁ *ₗ (r₂ *ₗ m₃) +ᴹ ((r₁ *ₗ m₂) *ᵣ r₃ +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) + ≈⟨ +ᴹ-congˡ (+ᴹ-congʳ (*ₗ-*ᵣ-assoc r₁ m₂ r₃)) ⟩ + r₁ *ₗ (r₂ *ₗ m₃) +ᴹ (r₁ *ₗ (m₂ *ᵣ r₃) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) + ≈⟨ symᴹ (+ᴹ-assoc (r₁ *ₗ (r₂ *ₗ m₃)) (r₁ *ₗ (m₂ *ᵣ r₃)) ((m₁ *ᵣ r₂) *ᵣ r₃)) ⟩ + (r₁ *ₗ (r₂ *ₗ m₃) +ᴹ r₁ *ₗ (m₂ *ᵣ r₃)) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃ + ≈⟨ +ᴹ-cong (symᴹ (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ + r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ *ᴿ r₃) ∎) + where + open ≈-Reasoning setoidᴹ + + *ᴺ-distrib-+ᴺ : _*ᴺ_ DistributesOver _+ᴺ_ + *ᴺ-distrib-+ᴺ = lᴺ , rᴺ + where + open ≈-Reasoning setoidᴹ + open Consequences setoidᴹ + +ᴹ-middleFour = comm∧assoc⇒middleFour +ᴹ-cong +ᴹ-comm +ᴹ-assoc + lᴺ : _*ᴺ_ DistributesOverˡ _+ᴺ_ + lᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-distribˡ-+ᴿ r₁ r₂ r₃ , (begin + r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ +ᴿ r₃) + ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ + (r₁ *ₗ m₂ +ᴹ r₁ *ₗ m₃) +ᴹ (m₁ *ᵣ r₂ +ᴹ m₁ *ᵣ r₃) + ≈⟨ +ᴹ-middleFour (r₁ *ₗ m₂) (r₁ *ₗ m₃) (m₁ *ᵣ r₂) (m₁ *ᵣ r₃) ⟩ + (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) + rᴺ : _*ᴺ_ DistributesOverʳ _+ᴺ_ + rᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-distribʳ-+ᴿ r₁ r₂ r₃ , (begin + (r₂ +ᴿ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ + ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ + (r₂ *ₗ m₁ +ᴹ r₃ *ₗ m₁) +ᴹ (m₂ *ᵣ r₁ +ᴹ m₃ *ᵣ r₁) + ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ + (r₂ *ₗ m₁ +ᴹ m₂ *ᵣ r₁) +ᴹ (r₃ *ₗ m₁ +ᴹ m₃ *ᵣ r₁) ∎) + + +------------------------------------------------------------------------ +-- The Fundamental Lemma, due to Nagata + + isRingᴺ : IsRing _≈ᴺ_ _+ᴺ_ _*ᴺ_ -ᴺ_ 0ᴺ 1ᴺ + isRingᴺ = record + { +-isAbelianGroup = +ᴺ-isAbelianGroup + ; *-cong = *ᴺ-cong + ; *-assoc = *ᴺ-assoc + ; *-identity = *ᴺ-identity + ; distrib = *ᴺ-distrib-+ᴺ + --; zero = zeroᴺ + } + +------------------------------------------------------------------------ +-- Bundle + +infixl 4 _⋉_ + +_⋉_ : (R : Ring r ℓr) (M : Bimodule R R m ℓm) → Ring (r ⊔ m) (ℓr ⊔ ℓm) + +R ⋉ M = record { isRing = isRingᴺ } where open Nagata R M + From f4ebde84409efba0bc4baf849b02fdb46d172e84 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 3 Jan 2024 14:06:56 +0000 Subject: [PATCH 02/23] removed redundant `zero` --- src/Algebra/Module/Construct/Nagata.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda index c655cefd65..680210f685 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -157,7 +157,6 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ; *-assoc = *ᴺ-assoc ; *-identity = *ᴺ-identity ; distrib = *ᴺ-distrib-+ᴺ - --; zero = zeroᴺ } ------------------------------------------------------------------------ From 96184844538b270c7d213c1775382313aebf38ef Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 07:45:30 +0000 Subject: [PATCH 03/23] first round of Jacques' review comments --- src/Algebra/Module/Construct/Nagata.agda | 79 +++++++++++++++--------- 1 file changed, 51 insertions(+), 28 deletions(-) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda index 680210f685..cdfe68dc61 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -1,29 +1,43 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- The non-commutative analogue of Nagata's construction --- of the "idealization of a module", defined here --- on R-R-*bi*modules M over a ring R. +-- The non-commutative analogue of Nagata's construction of +-- the "idealization of a module", (Local Rings, 1962; Wiley) +-- defined here on R-R-*bi*modules M over a ring R, as used in +-- "Forward- or reverse-mode automatic differentiation: What's the difference?" +-- (Van den Berg, Schrijvers, McKinna, Vandenbroucke; +-- Science of Computer Programming, Vol. 234, January 2024 +-- https://doi.org/10.1016/j.scico.2023.103010) +-- +-- The construction N =def R ⋉ M , for which there is unfortunately +-- no consistent notation in the literature, consists of: +-- * carrier: pairs |R| × |M| +-- * with additive structure that of the direct sum R ⊕ M _of modules_ +-- * but with multiplication _*ᴺ_ such that M forms an _ideal_ of N +-- * moreover satisfying 'm *ᴺ m ≈ 0' for every m ∈ M ⊆ N +-- +-- The fundamental lemma (proved here) is that N, in fact, defines a Ring. +-- +-- Nagata's more fundamental insight (not yet shown here) is that +-- the lattice of R-submodules of M is in order-isomorphism with +-- the lattice of _ideals_ of R ⋉ M , and hence that the study of +-- modules can be reduced to that of ideals of a ring, and vice versa. -- --- Elements of R ⋉ M are pairs |R| × |M| ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Algebra.Module.Construct.Nagata where -open import Algebra.Bundles +open import Algebra.Bundles using (AbelianGroup; Ring) open import Algebra.Core import Algebra.Consequences.Setoid as Consequences import Algebra.Definitions as Definitions -open import Algebra.Module.Bundles -open import Algebra.Module.Core -open import Algebra.Module.Definitions +open import Algebra.Module.Bundles using (Bimodule) import Algebra.Module.Construct.DirectProduct as DirectProduct import Algebra.Module.Construct.TensorUnit as TensorUnit -open import Algebra.Structures -open import Data.Product using (_×_; _,_; proj₁; proj₂) -open import Data.Product.Relation.Binary.Pointwise.NonDependent +open import Algebra.Structures using (IsAbelianGroup; IsRing) +open import Data.Product using (_,_; ∃-syntax) open import Level using (Level; _⊔_) open import Relation.Binary using (Rel; Setoid; IsEquivalence) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning @@ -74,39 +88,53 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ; +ᴹ-abelianGroup to +ᴺ-abelianGroup ) + open AbelianGroup +ᴺ-abelianGroup + renaming (isAbelianGroup to +ᴺ-isAbelianGroup) + + open Definitions _≈ᴺ_ + +-- injections ι from the components of the direct sum +-- ιᴹ in fact exhibits M as an _ideal_ of R ⋉ M (not yet shown) ιᴿ : R → N ιᴿ r = r , 0ᴹ ιᴹ : M → N ιᴹ m = 0ᴿ , m +-- multiplicative unit + 1ᴺ : N 1ᴺ = ιᴿ 1ᴿ - open AbelianGroup +ᴺ-abelianGroup - renaming (isAbelianGroup to +ᴺ-isAbelianGroup) - - open Definitions _≈ᴺ_ +-- multiplication infixl 7 _*ᴺ_ _*ᴺ_ : Op₂ N (r₁ , m₁) *ᴺ (r₂ , m₂) = r₁ *ᴿ r₂ , r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂ +-- properties: because we work in the direct sum, every proof +-- has an 'R'-component, which inherits directly from R, +-- and an 'M'-component, where the work happens + + open ≈-Reasoning setoidᴹ + + private + +ᴹ-middleFour = Consequences.comm∧assoc⇒middleFour setoidᴹ +ᴹ-cong +ᴹ-comm +ᴹ-assoc + *ᴺ-identity : Identity 1ᴺ _*ᴺ_ *ᴺ-identity = lᴺ , rᴺ where - open ≈-Reasoning setoidᴹ lᴺ : LeftIdentity 1ᴺ _*ᴺ_ - lᴺ (r , m) = (*ᴿ-identityˡ r) , (begin - (1ᴿ *ₗ m +ᴹ 0ᴹ *ᵣ r) ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ - (m +ᴹ 0ᴹ) ≈⟨ +ᴹ-identityʳ m ⟩ - m ∎) + lᴺ (r , m) = *ᴿ-identityˡ r , (begin + 1ᴿ *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ + m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ + m ∎) rᴺ : RightIdentity 1ᴺ _*ᴺ_ rᴺ (r , m) = (*ᴿ-identityʳ r) , (begin r *ₗ 0ᴹ +ᴹ m *ᵣ 1ᴿ ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ - 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ - m ∎) + 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ + m ∎) *ᴺ-cong : Congruent₂ _*ᴺ_ *ᴺ-cong (r₁ , m₁) (r₂ , m₂) = *ᴿ-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) @@ -122,15 +150,10 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where (r₁ *ₗ (r₂ *ₗ m₃) +ᴹ r₁ *ₗ (m₂ *ᵣ r₃)) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃ ≈⟨ +ᴹ-cong (symᴹ (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ *ᴿ r₃) ∎) - where - open ≈-Reasoning setoidᴹ *ᴺ-distrib-+ᴺ : _*ᴺ_ DistributesOver _+ᴺ_ *ᴺ-distrib-+ᴺ = lᴺ , rᴺ where - open ≈-Reasoning setoidᴹ - open Consequences setoidᴹ - +ᴹ-middleFour = comm∧assoc⇒middleFour +ᴹ-cong +ᴹ-comm +ᴹ-assoc lᴺ : _*ᴺ_ DistributesOverˡ _+ᴺ_ lᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-distribˡ-+ᴿ r₁ r₂ r₃ , (begin r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ +ᴿ r₃) @@ -148,7 +171,7 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ------------------------------------------------------------------------ --- The Fundamental Lemma, due to Nagata +-- The Fundamental Lemma isRingᴺ : IsRing _≈ᴺ_ _+ᴺ_ _*ᴺ_ -ᴺ_ 0ᴺ 1ᴺ isRingᴺ = record From 934b275166234ab969df463ca97964ccd628b5a8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 08:22:56 +0000 Subject: [PATCH 04/23] proved the additional properties --- src/Algebra/Module/Construct/Nagata.agda | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda index cdfe68dc61..7243571ec4 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -64,6 +64,7 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ; distribˡ to *ᴿ-distribˡ-+ᴿ ; distribʳ to *ᴿ-distribʳ-+ᴿ ) + --hiding (zero; zeroˡ; zeroʳ) open Bimodule bimodule renaming (Carrierᴹ to M @@ -182,6 +183,21 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ; distrib = *ᴺ-distrib-+ᴺ } +------------------------------------------------------------------------ +-- M is an ideal of R ⋉ M satisying m * m ≈ 0 + + idealˡ-M : (n : N) (m : M) → ∃[ n*m ] n *ᴺ ιᴹ m ≈ᴺ ιᴹ n*m + idealˡ-M (r₀ , m₀) m = _ , zeroʳ r₀ , ≈ᴹ-refl + + idealʳ-M : (n : N) (m : M) → ∃[ m*n ] ιᴹ m *ᴺ n ≈ᴺ ιᴹ m*n + idealʳ-M (r₀ , m₀) m = _ , zeroˡ r₀ , ≈ᴹ-refl + + m*m≈0 : (m : M) → ιᴹ m *ᴺ ιᴹ m ≈ᴺ 0ᴺ + m*m≈0 m = zeroˡ 0ᴿ , (begin + 0ᴿ *ₗ m +ᴹ m *ᵣ 0ᴿ ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m) (*ᵣ-zeroʳ m) ⟩ + 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ + 0ᴹ ∎) + ------------------------------------------------------------------------ -- Bundle From 7db0e4d828c4dc75ef18403916b2798e21290fb1 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 09:12:38 +0000 Subject: [PATCH 05/23] some of Matthew's suggestions, plus more vertical whitespace, less horizontal; more comments --- src/Algebra/Module/Construct/Nagata.agda | 92 ++++++++++++++---------- 1 file changed, 55 insertions(+), 37 deletions(-) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda index 7243571ec4..c5f96ad160 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -16,7 +16,11 @@ -- * but with multiplication _*ᴺ_ such that M forms an _ideal_ of N -- * moreover satisfying 'm *ᴺ m ≈ 0' for every m ∈ M ⊆ N -- --- The fundamental lemma (proved here) is that N, in fact, defines a Ring. +-- The fundamental lemma (proved here) is that N, in fact, defines a Ring: +-- this ring is essentially the 'ring of dual numbers' construction R[M] +-- (Clifford, 1874; generalised!) for an ideal M, and thus the synthetic/algebraic +-- analogue of the tangent space of M (considered as a 'vector space' over R) +-- in differential geometry, hence its application to Automatic Differentiation. -- -- Nagata's more fundamental insight (not yet shown here) is that -- the lattice of R-submodules of M is in order-isomorphism with @@ -64,7 +68,6 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ; distribˡ to *ᴿ-distribˡ-+ᴿ ; distribʳ to *ᴿ-distribʳ-+ᴿ ) - --hiding (zero; zeroˡ; zeroʳ) open Bimodule bimodule renaming (Carrierᴹ to M @@ -94,7 +97,7 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where open Definitions _≈ᴺ_ --- injections ι from the components of the direct sum +-- Injections ι from the components of the direct sum -- ιᴹ in fact exhibits M as an _ideal_ of R ⋉ M (not yet shown) ιᴿ : R → N ιᴿ r = r , 0ᴹ @@ -102,21 +105,21 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ιᴹ : M → N ιᴹ m = 0ᴿ , m --- multiplicative unit +-- Multiplicative unit 1ᴺ : N 1ᴺ = ιᴿ 1ᴿ --- multiplication +-- Multiplication infixl 7 _*ᴺ_ _*ᴺ_ : Op₂ N (r₁ , m₁) *ᴺ (r₂ , m₂) = r₁ *ᴿ r₂ , r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂ --- properties: because we work in the direct sum, every proof --- has an 'R'-component, which inherits directly from R, --- and an 'M'-component, where the work happens +-- Properties: because we work in the direct sum, every proof has +-- * an 'R'-component, which inherits directly from R, and +-- * an 'M'-component, where the work happens open ≈-Reasoning setoidᴹ @@ -126,28 +129,32 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where *ᴺ-identity : Identity 1ᴺ _*ᴺ_ *ᴺ-identity = lᴺ , rᴺ where - lᴺ : LeftIdentity 1ᴺ _*ᴺ_ - lᴺ (r , m) = *ᴿ-identityˡ r , (begin - 1ᴿ *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ - m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ - m ∎) - rᴺ : RightIdentity 1ᴺ _*ᴺ_ - rᴺ (r , m) = (*ᴿ-identityʳ r) , (begin - r *ₗ 0ᴹ +ᴹ m *ᵣ 1ᴿ ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ - 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ - m ∎) + lᴺ : LeftIdentity 1ᴺ _*ᴺ_ + lᴺ (r , m) = *ᴿ-identityˡ r , (begin + + 1ᴿ *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ + m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ + m ∎) + + rᴺ : RightIdentity 1ᴺ _*ᴺ_ + rᴺ (r , m) = *ᴿ-identityʳ r , (begin + + r *ₗ 0ᴹ +ᴹ m *ᵣ 1ᴿ ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ + 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ + m ∎) *ᴺ-cong : Congruent₂ _*ᴺ_ *ᴺ-cong (r₁ , m₁) (r₂ , m₂) = *ᴿ-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) *ᴺ-assoc : Associative _*ᴺ_ *ᴺ-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-assoc r₁ r₂ r₃ , (begin + (r₁ *ᴿ r₂) *ₗ m₃ +ᴹ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) *ᵣ r₃ ≈⟨ +ᴹ-cong (*ₗ-assoc r₁ r₂ m₃) (*ᵣ-distribʳ r₃ (r₁ *ₗ m₂) (m₁ *ᵣ r₂)) ⟩ r₁ *ₗ (r₂ *ₗ m₃) +ᴹ ((r₁ *ₗ m₂) *ᵣ r₃ +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) ≈⟨ +ᴹ-congˡ (+ᴹ-congʳ (*ₗ-*ᵣ-assoc r₁ m₂ r₃)) ⟩ r₁ *ₗ (r₂ *ₗ m₃) +ᴹ (r₁ *ₗ (m₂ *ᵣ r₃) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) - ≈⟨ symᴹ (+ᴹ-assoc (r₁ *ₗ (r₂ *ₗ m₃)) (r₁ *ₗ (m₂ *ᵣ r₃)) ((m₁ *ᵣ r₂) *ᵣ r₃)) ⟩ + ≈⟨ +ᴹ-assoc (r₁ *ₗ (r₂ *ₗ m₃)) (r₁ *ₗ (m₂ *ᵣ r₃)) ((m₁ *ᵣ r₂) *ᵣ r₃) ⟨ (r₁ *ₗ (r₂ *ₗ m₃) +ᴹ r₁ *ₗ (m₂ *ᵣ r₃)) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃ ≈⟨ +ᴹ-cong (symᴹ (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ *ᴿ r₃) ∎) @@ -155,25 +162,30 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where *ᴺ-distrib-+ᴺ : _*ᴺ_ DistributesOver _+ᴺ_ *ᴺ-distrib-+ᴺ = lᴺ , rᴺ where - lᴺ : _*ᴺ_ DistributesOverˡ _+ᴺ_ - lᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-distribˡ-+ᴿ r₁ r₂ r₃ , (begin - r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ +ᴿ r₃) - ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ - (r₁ *ₗ m₂ +ᴹ r₁ *ₗ m₃) +ᴹ (m₁ *ᵣ r₂ +ᴹ m₁ *ᵣ r₃) - ≈⟨ +ᴹ-middleFour (r₁ *ₗ m₂) (r₁ *ₗ m₃) (m₁ *ᵣ r₂) (m₁ *ᵣ r₃) ⟩ - (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) - rᴺ : _*ᴺ_ DistributesOverʳ _+ᴺ_ - rᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-distribʳ-+ᴿ r₁ r₂ r₃ , (begin - (r₂ +ᴿ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ - ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ - (r₂ *ₗ m₁ +ᴹ r₃ *ₗ m₁) +ᴹ (m₂ *ᵣ r₁ +ᴹ m₃ *ᵣ r₁) - ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ - (r₂ *ₗ m₁ +ᴹ m₂ *ᵣ r₁) +ᴹ (r₃ *ₗ m₁ +ᴹ m₃ *ᵣ r₁) ∎) + lᴺ : _*ᴺ_ DistributesOverˡ _+ᴺ_ + lᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-distribˡ-+ᴿ r₁ r₂ r₃ , (begin + + r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ +ᴿ r₃) + ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ + (r₁ *ₗ m₂ +ᴹ r₁ *ₗ m₃) +ᴹ (m₁ *ᵣ r₂ +ᴹ m₁ *ᵣ r₃) + ≈⟨ +ᴹ-middleFour (r₁ *ₗ m₂) (r₁ *ₗ m₃) (m₁ *ᵣ r₂) (m₁ *ᵣ r₃) ⟩ + (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) + + rᴺ : _*ᴺ_ DistributesOverʳ _+ᴺ_ + rᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-distribʳ-+ᴿ r₁ r₂ r₃ , (begin + + (r₂ +ᴿ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ + ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ + (r₂ *ₗ m₁ +ᴹ r₃ *ₗ m₁) +ᴹ (m₂ *ᵣ r₁ +ᴹ m₃ *ᵣ r₁) + ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ + (r₂ *ₗ m₁ +ᴹ m₂ *ᵣ r₁) +ᴹ (r₃ *ₗ m₁ +ᴹ m₃ *ᵣ r₁) ∎) ------------------------------------------------------------------------ -- The Fundamental Lemma +-- Structure + isRingᴺ : IsRing _≈ᴺ_ _+ᴺ_ _*ᴺ_ -ᴺ_ 0ᴺ 1ᴺ isRingᴺ = record { +-isAbelianGroup = +ᴺ-isAbelianGroup @@ -183,27 +195,33 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ; distrib = *ᴺ-distrib-+ᴺ } +-- Bundle + + ringᴺ : Ring (r ⊔ m) (ℓr ⊔ ℓm) + ringᴺ = record { isRing = isRingᴺ } + ------------------------------------------------------------------------ -- M is an ideal of R ⋉ M satisying m * m ≈ 0 idealˡ-M : (n : N) (m : M) → ∃[ n*m ] n *ᴺ ιᴹ m ≈ᴺ ιᴹ n*m idealˡ-M (r₀ , m₀) m = _ , zeroʳ r₀ , ≈ᴹ-refl - idealʳ-M : (n : N) (m : M) → ∃[ m*n ] ιᴹ m *ᴺ n ≈ᴺ ιᴹ m*n - idealʳ-M (r₀ , m₀) m = _ , zeroˡ r₀ , ≈ᴹ-refl + idealʳ-M : (m : M) (n : N) → ∃[ m*n ] ιᴹ m *ᴺ n ≈ᴺ ιᴹ m*n + idealʳ-M m (r₀ , m₀) = _ , zeroˡ r₀ , ≈ᴹ-refl m*m≈0 : (m : M) → ιᴹ m *ᴺ ιᴹ m ≈ᴺ 0ᴺ m*m≈0 m = zeroˡ 0ᴿ , (begin + 0ᴿ *ₗ m +ᴹ m *ᵣ 0ᴿ ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m) (*ᵣ-zeroʳ m) ⟩ 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ 0ᴹ ∎) ------------------------------------------------------------------------ --- Bundle +-- Export infixl 4 _⋉_ _⋉_ : (R : Ring r ℓr) (M : Bimodule R R m ℓm) → Ring (r ⊔ m) (ℓr ⊔ ℓm) -R ⋉ M = record { isRing = isRingᴺ } where open Nagata R M +R ⋉ M = ringᴺ where open Nagata R M From fdb7ab191cd6a3ad54ff1ea4f2f552e919045e0f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 11:04:12 +0000 Subject: [PATCH 06/23] Matthew's suggestion: using `private` modules --- src/Algebra/Module/Construct/Nagata.agda | 125 ++++++++++------------- 1 file changed, 52 insertions(+), 73 deletions(-) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda index c5f96ad160..07b84799f9 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -55,101 +55,80 @@ private module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where - open Ring ring - renaming (Carrier to R - ; 0# to 0ᴿ - ; 1# to 1ᴿ - ; _+_ to _+ᴿ_ - ; _*_ to _*ᴿ_ - ; *-cong to *ᴿ-cong - ; *-assoc to *ᴿ-assoc - ; *-identityʳ to *ᴿ-identityʳ - ; *-identityˡ to *ᴿ-identityˡ - ; distribˡ to *ᴿ-distribˡ-+ᴿ - ; distribʳ to *ᴿ-distribʳ-+ᴿ - ) - - open Bimodule bimodule - renaming (Carrierᴹ to M - ) - - open AbelianGroup +ᴹ-abelianGroup - renaming (setoid to setoidᴹ - ; isEquivalence to isEquivalenceᴹ - ) - - open IsEquivalence isEquivalenceᴹ - renaming (sym to symᴹ) - - +ᴺ-bimodule = DirectProduct.bimodule TensorUnit.bimodule bimodule - - open Bimodule +ᴺ-bimodule public using () - renaming (Carrierᴹ to N - ; _≈ᴹ_ to _≈ᴺ_ - ; _+ᴹ_ to _+ᴺ_ - ; 0ᴹ to 0ᴺ - ; -ᴹ_ to -ᴺ_ - ; +ᴹ-abelianGroup to +ᴺ-abelianGroup - ) - - open AbelianGroup +ᴺ-abelianGroup - renaming (isAbelianGroup to +ᴺ-isAbelianGroup) - - open Definitions _≈ᴺ_ + private + open module R = Ring ring + renaming (Carrier to R) + + open module M = Bimodule bimodule + renaming (Carrierᴹ to M) + + open AbelianGroup M.+ᴹ-abelianGroup + renaming (setoid to setoidᴹ; sym to symᴹ) + + +ᴹ-middleFour = Consequences.comm∧assoc⇒middleFour setoidᴹ +ᴹ-cong +ᴹ-comm +ᴹ-assoc + + open ≈-Reasoning setoidᴹ + + open module N = Bimodule (DirectProduct.bimodule TensorUnit.bimodule bimodule) + using () + renaming (Carrierᴹ to N + ; _≈ᴹ_ to _≈ᴺ_ + ; _+ᴹ_ to _+ᴺ_ + ; 0ᴹ to 0ᴺ + ; -ᴹ_ to -ᴺ_ + ; +ᴹ-isAbelianGroup to +ᴺ-isAbelianGroup + ) + + open Definitions _≈ᴺ_ -- Injections ι from the components of the direct sum --- ιᴹ in fact exhibits M as an _ideal_ of R ⋉ M (not yet shown) +-- ιᴹ in fact exhibits M as an _ideal_ of R ⋉ M (see below) ιᴿ : R → N ιᴿ r = r , 0ᴹ ιᴹ : M → N - ιᴹ m = 0ᴿ , m + ιᴹ m = R.0# , m -- Multiplicative unit 1ᴺ : N - 1ᴺ = ιᴿ 1ᴿ + 1ᴺ = ιᴿ R.1# -- Multiplication infixl 7 _*ᴺ_ _*ᴺ_ : Op₂ N - (r₁ , m₁) *ᴺ (r₂ , m₂) = r₁ *ᴿ r₂ , r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂ + (r₁ , m₁) *ᴺ (r₂ , m₂) = r₁ R.* r₂ , r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂ -- Properties: because we work in the direct sum, every proof has -- * an 'R'-component, which inherits directly from R, and -- * an 'M'-component, where the work happens - open ≈-Reasoning setoidᴹ - - private - +ᴹ-middleFour = Consequences.comm∧assoc⇒middleFour setoidᴹ +ᴹ-cong +ᴹ-comm +ᴹ-assoc - *ᴺ-identity : Identity 1ᴺ _*ᴺ_ *ᴺ-identity = lᴺ , rᴺ where lᴺ : LeftIdentity 1ᴺ _*ᴺ_ - lᴺ (r , m) = *ᴿ-identityˡ r , (begin + lᴺ (r , m) = R.*-identityˡ r , (begin - 1ᴿ *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ - m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ - m ∎) + R.1# *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ + m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ + m ∎) rᴺ : RightIdentity 1ᴺ _*ᴺ_ - rᴺ (r , m) = *ᴿ-identityʳ r , (begin + rᴺ (r , m) = R.*-identityʳ r , (begin - r *ₗ 0ᴹ +ᴹ m *ᵣ 1ᴿ ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ - 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ - m ∎) + r *ₗ 0ᴹ +ᴹ m *ᵣ R.1# ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ + 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ + m ∎) *ᴺ-cong : Congruent₂ _*ᴺ_ - *ᴺ-cong (r₁ , m₁) (r₂ , m₂) = *ᴿ-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) + *ᴺ-cong (r₁ , m₁) (r₂ , m₂) = R.*-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) *ᴺ-assoc : Associative _*ᴺ_ - *ᴺ-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-assoc r₁ r₂ r₃ , (begin + *ᴺ-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.*-assoc r₁ r₂ r₃ , (begin - (r₁ *ᴿ r₂) *ₗ m₃ +ᴹ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) *ᵣ r₃ + (r₁ R.* r₂) *ₗ m₃ +ᴹ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) *ᵣ r₃ ≈⟨ +ᴹ-cong (*ₗ-assoc r₁ r₂ m₃) (*ᵣ-distribʳ r₃ (r₁ *ₗ m₂) (m₁ *ᵣ r₂)) ⟩ r₁ *ₗ (r₂ *ₗ m₃) +ᴹ ((r₁ *ₗ m₂) *ᵣ r₃ +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) ≈⟨ +ᴹ-congˡ (+ᴹ-congʳ (*ₗ-*ᵣ-assoc r₁ m₂ r₃)) ⟩ @@ -157,24 +136,24 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ≈⟨ +ᴹ-assoc (r₁ *ₗ (r₂ *ₗ m₃)) (r₁ *ₗ (m₂ *ᵣ r₃)) ((m₁ *ᵣ r₂) *ᵣ r₃) ⟨ (r₁ *ₗ (r₂ *ₗ m₃) +ᴹ r₁ *ₗ (m₂ *ᵣ r₃)) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃ ≈⟨ +ᴹ-cong (symᴹ (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ - r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ *ᴿ r₃) ∎) + r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ R.* r₃) ∎) *ᴺ-distrib-+ᴺ : _*ᴺ_ DistributesOver _+ᴺ_ *ᴺ-distrib-+ᴺ = lᴺ , rᴺ where lᴺ : _*ᴺ_ DistributesOverˡ _+ᴺ_ - lᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-distribˡ-+ᴿ r₁ r₂ r₃ , (begin + lᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ , (begin - r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ +ᴿ r₃) + r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ R.+ r₃) ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ (r₁ *ₗ m₂ +ᴹ r₁ *ₗ m₃) +ᴹ (m₁ *ᵣ r₂ +ᴹ m₁ *ᵣ r₃) ≈⟨ +ᴹ-middleFour (r₁ *ₗ m₂) (r₁ *ₗ m₃) (m₁ *ᵣ r₂) (m₁ *ᵣ r₃) ⟩ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) rᴺ : _*ᴺ_ DistributesOverʳ _+ᴺ_ - rᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = *ᴿ-distribʳ-+ᴿ r₁ r₂ r₃ , (begin + rᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribʳ r₁ r₂ r₃ , (begin - (r₂ +ᴿ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ + (r₂ R.+ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ (r₂ *ₗ m₁ +ᴹ r₃ *ₗ m₁) +ᴹ (m₂ *ᵣ r₁ +ᴹ m₃ *ᵣ r₁) ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ @@ -201,20 +180,20 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ringᴺ = record { isRing = isRingᴺ } ------------------------------------------------------------------------ --- M is an ideal of R ⋉ M satisying m * m ≈ 0 +-- M is an ideal of R ⋉ M satisying m * m ≈ 0# idealˡ-M : (n : N) (m : M) → ∃[ n*m ] n *ᴺ ιᴹ m ≈ᴺ ιᴹ n*m - idealˡ-M (r₀ , m₀) m = _ , zeroʳ r₀ , ≈ᴹ-refl + idealˡ-M n@(r , _) m = _ , zeroʳ r , ≈ᴹ-refl idealʳ-M : (m : M) (n : N) → ∃[ m*n ] ιᴹ m *ᴺ n ≈ᴺ ιᴹ m*n - idealʳ-M m (r₀ , m₀) = _ , zeroˡ r₀ , ≈ᴹ-refl + idealʳ-M m n@(r , _) = _ , zeroˡ r , ≈ᴹ-refl m*m≈0 : (m : M) → ιᴹ m *ᴺ ιᴹ m ≈ᴺ 0ᴺ - m*m≈0 m = zeroˡ 0ᴿ , (begin + m*m≈0 m = zeroˡ R.0# , (begin - 0ᴿ *ₗ m +ᴹ m *ᵣ 0ᴿ ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m) (*ᵣ-zeroʳ m) ⟩ - 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ - 0ᴹ ∎) + R.0# *ₗ m +ᴹ m *ᵣ R.0# ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m) (*ᵣ-zeroʳ m) ⟩ + 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ + 0ᴹ ∎) ------------------------------------------------------------------------ -- Export From 2fd0ef7f6cd5086615b01ed1517b5517dff8b472 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 11:20:55 +0000 Subject: [PATCH 07/23] Matthew's suggestion: lifting out left-/right- sublemmas --- src/Algebra/Module/Construct/Nagata.agda | 34 +++++++++++++----------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda index 07b84799f9..9756921972 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -105,25 +105,26 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where -- * an 'R'-component, which inherits directly from R, and -- * an 'M'-component, where the work happens - *ᴺ-identity : Identity 1ᴺ _*ᴺ_ - *ᴺ-identity = lᴺ , rᴺ - where - lᴺ : LeftIdentity 1ᴺ _*ᴺ_ - lᴺ (r , m) = R.*-identityˡ r , (begin + *ᴺ-cong : Congruent₂ _*ᴺ_ + *ᴺ-cong (r₁ , m₁) (r₂ , m₂) = R.*-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) + + *ᴺ-identityˡ : LeftIdentity 1ᴺ _*ᴺ_ + *ᴺ-identityˡ (r , m) = R.*-identityˡ r , (begin R.1# *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ m ∎) - rᴺ : RightIdentity 1ᴺ _*ᴺ_ - rᴺ (r , m) = R.*-identityʳ r , (begin + *ᴺ-identityʳ : RightIdentity 1ᴺ _*ᴺ_ + *ᴺ-identityʳ (r , m) = R.*-identityʳ r , (begin r *ₗ 0ᴹ +ᴹ m *ᵣ R.1# ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ m ∎) - *ᴺ-cong : Congruent₂ _*ᴺ_ - *ᴺ-cong (r₁ , m₁) (r₂ , m₂) = R.*-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) + + *ᴺ-identity : Identity 1ᴺ _*ᴺ_ + *ᴺ-identity = *ᴺ-identityˡ , *ᴺ-identityʳ *ᴺ-assoc : Associative _*ᴺ_ *ᴺ-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.*-assoc r₁ r₂ r₃ , (begin @@ -138,11 +139,8 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ≈⟨ +ᴹ-cong (symᴹ (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ R.* r₃) ∎) - *ᴺ-distrib-+ᴺ : _*ᴺ_ DistributesOver _+ᴺ_ - *ᴺ-distrib-+ᴺ = lᴺ , rᴺ - where - lᴺ : _*ᴺ_ DistributesOverˡ _+ᴺ_ - lᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ , (begin + *ᴺ-distribˡ-+ᴺ : _*ᴺ_ DistributesOverˡ _+ᴺ_ + *ᴺ-distribˡ-+ᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ , (begin r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ R.+ r₃) ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ @@ -150,8 +148,9 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ≈⟨ +ᴹ-middleFour (r₁ *ₗ m₂) (r₁ *ₗ m₃) (m₁ *ᵣ r₂) (m₁ *ᵣ r₃) ⟩ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) - rᴺ : _*ᴺ_ DistributesOverʳ _+ᴺ_ - rᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribʳ r₁ r₂ r₃ , (begin + + *ᴺ-distribʳ-+ᴺ : _*ᴺ_ DistributesOverʳ _+ᴺ_ + *ᴺ-distribʳ-+ᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribʳ r₁ r₂ r₃ , (begin (r₂ R.+ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ @@ -159,6 +158,9 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ (r₂ *ₗ m₁ +ᴹ m₂ *ᵣ r₁) +ᴹ (r₃ *ₗ m₁ +ᴹ m₃ *ᵣ r₁) ∎) + *ᴺ-distrib-+ᴺ : _*ᴺ_ DistributesOver _+ᴺ_ + *ᴺ-distrib-+ᴺ = *ᴺ-distribˡ-+ᴺ , *ᴺ-distribʳ-+ᴺ + ------------------------------------------------------------------------ -- The Fundamental Lemma From 283d9c6263939455668ae9179884a008e25423fc Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 11:49:00 +0000 Subject: [PATCH 08/23] standardised names, as far as possible --- src/Algebra/Module/Construct/Nagata.agda | 79 ++++++++++++------------ 1 file changed, 40 insertions(+), 39 deletions(-) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda index 9756921972..500647f914 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -13,8 +13,8 @@ -- no consistent notation in the literature, consists of: -- * carrier: pairs |R| × |M| -- * with additive structure that of the direct sum R ⊕ M _of modules_ --- * but with multiplication _*ᴺ_ such that M forms an _ideal_ of N --- * moreover satisfying 'm *ᴺ m ≈ 0' for every m ∈ M ⊆ N +-- * but with multiplication _*_ such that M forms an _ideal_ of N +-- * moreover satisfying 'm * m ≈ 0' for every m ∈ M ⊆ N -- -- The fundamental lemma (proved here) is that N, in fact, defines a Ring: -- this ring is essentially the 'ring of dual numbers' construction R[M] @@ -57,6 +57,7 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where private open module R = Ring ring + using () renaming (Carrier to R) open module M = Bimodule bimodule @@ -73,10 +74,10 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where using () renaming (Carrierᴹ to N ; _≈ᴹ_ to _≈ᴺ_ - ; _+ᴹ_ to _+ᴺ_ - ; 0ᴹ to 0ᴺ - ; -ᴹ_ to -ᴺ_ - ; +ᴹ-isAbelianGroup to +ᴺ-isAbelianGroup + ; _+ᴹ_ to _+_ + ; 0ᴹ to 0# + ; -ᴹ_ to -_ + ; +ᴹ-isAbelianGroup to +-isAbelianGroup ) open Definitions _≈ᴺ_ @@ -91,43 +92,43 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where -- Multiplicative unit - 1ᴺ : N - 1ᴺ = ιᴿ R.1# + 1# : N + 1# = ιᴿ R.1# -- Multiplication - infixl 7 _*ᴺ_ + infixl 7 _*_ - _*ᴺ_ : Op₂ N - (r₁ , m₁) *ᴺ (r₂ , m₂) = r₁ R.* r₂ , r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂ + _*_ : Op₂ N + (r₁ , m₁) * (r₂ , m₂) = r₁ R.* r₂ , r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂ -- Properties: because we work in the direct sum, every proof has -- * an 'R'-component, which inherits directly from R, and -- * an 'M'-component, where the work happens - *ᴺ-cong : Congruent₂ _*ᴺ_ - *ᴺ-cong (r₁ , m₁) (r₂ , m₂) = R.*-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) + *-cong : Congruent₂ _*_ + *-cong (r₁ , m₁) (r₂ , m₂) = R.*-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) - *ᴺ-identityˡ : LeftIdentity 1ᴺ _*ᴺ_ - *ᴺ-identityˡ (r , m) = R.*-identityˡ r , (begin + *-identityˡ : LeftIdentity 1# _*_ + *-identityˡ (r , m) = R.*-identityˡ r , (begin R.1# *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ m ∎) - *ᴺ-identityʳ : RightIdentity 1ᴺ _*ᴺ_ - *ᴺ-identityʳ (r , m) = R.*-identityʳ r , (begin + *-identityʳ : RightIdentity 1# _*_ + *-identityʳ (r , m) = R.*-identityʳ r , (begin r *ₗ 0ᴹ +ᴹ m *ᵣ R.1# ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ m ∎) - *ᴺ-identity : Identity 1ᴺ _*ᴺ_ - *ᴺ-identity = *ᴺ-identityˡ , *ᴺ-identityʳ + *-identity : Identity 1# _*_ + *-identity = *-identityˡ , *-identityʳ - *ᴺ-assoc : Associative _*ᴺ_ - *ᴺ-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.*-assoc r₁ r₂ r₃ , (begin + *-assoc : Associative _*_ + *-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.*-assoc r₁ r₂ r₃ , (begin (r₁ R.* r₂) *ₗ m₃ +ᴹ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) *ᵣ r₃ ≈⟨ +ᴹ-cong (*ₗ-assoc r₁ r₂ m₃) (*ᵣ-distribʳ r₃ (r₁ *ₗ m₂) (m₁ *ᵣ r₂)) ⟩ @@ -139,8 +140,8 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ≈⟨ +ᴹ-cong (symᴹ (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ R.* r₃) ∎) - *ᴺ-distribˡ-+ᴺ : _*ᴺ_ DistributesOverˡ _+ᴺ_ - *ᴺ-distribˡ-+ᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ , (begin + distribˡ : _*_ DistributesOverˡ _+_ + distribˡ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ , (begin r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ R.+ r₃) ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ @@ -149,8 +150,8 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) - *ᴺ-distribʳ-+ᴺ : _*ᴺ_ DistributesOverʳ _+ᴺ_ - *ᴺ-distribʳ-+ᴺ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribʳ r₁ r₂ r₃ , (begin + distribʳ : _*_ DistributesOverʳ _+_ + distribʳ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribʳ r₁ r₂ r₃ , (begin (r₂ R.+ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ @@ -158,8 +159,8 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ (r₂ *ₗ m₁ +ᴹ m₂ *ᵣ r₁) +ᴹ (r₃ *ₗ m₁ +ᴹ m₃ *ᵣ r₁) ∎) - *ᴺ-distrib-+ᴺ : _*ᴺ_ DistributesOver _+ᴺ_ - *ᴺ-distrib-+ᴺ = *ᴺ-distribˡ-+ᴺ , *ᴺ-distribʳ-+ᴺ + distrib : _*_ DistributesOver _+_ + distrib = distribˡ , distribʳ ------------------------------------------------------------------------ @@ -167,13 +168,13 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where -- Structure - isRingᴺ : IsRing _≈ᴺ_ _+ᴺ_ _*ᴺ_ -ᴺ_ 0ᴺ 1ᴺ + isRingᴺ : IsRing _≈ᴺ_ _+_ _*_ -_ 0# 1# isRingᴺ = record - { +-isAbelianGroup = +ᴺ-isAbelianGroup - ; *-cong = *ᴺ-cong - ; *-assoc = *ᴺ-assoc - ; *-identity = *ᴺ-identity - ; distrib = *ᴺ-distrib-+ᴺ + { +-isAbelianGroup = +-isAbelianGroup + ; *-cong = *-cong + ; *-assoc = *-assoc + ; *-identity = *-identity + ; distrib = distrib } -- Bundle @@ -184,14 +185,14 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ------------------------------------------------------------------------ -- M is an ideal of R ⋉ M satisying m * m ≈ 0# - idealˡ-M : (n : N) (m : M) → ∃[ n*m ] n *ᴺ ιᴹ m ≈ᴺ ιᴹ n*m - idealˡ-M n@(r , _) m = _ , zeroʳ r , ≈ᴹ-refl + idealˡ-M : (n : N) (m : M) → ∃[ n*m ] n * ιᴹ m ≈ᴺ ιᴹ n*m + idealˡ-M n@(r , _) m = _ , R.zeroʳ r , ≈ᴹ-refl - idealʳ-M : (m : M) (n : N) → ∃[ m*n ] ιᴹ m *ᴺ n ≈ᴺ ιᴹ m*n - idealʳ-M m n@(r , _) = _ , zeroˡ r , ≈ᴹ-refl + idealʳ-M : (m : M) (n : N) → ∃[ m*n ] ιᴹ m * n ≈ᴺ ιᴹ m*n + idealʳ-M m n@(r , _) = _ , R.zeroˡ r , ≈ᴹ-refl - m*m≈0 : (m : M) → ιᴹ m *ᴺ ιᴹ m ≈ᴺ 0ᴺ - m*m≈0 m = zeroˡ R.0# , (begin + m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ᴺ 0# + m*m≈0 m = R.zeroˡ R.0# , (begin R.0# *ₗ m +ᴹ m *ᵣ R.0# ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m) (*ᵣ-zeroʳ m) ⟩ 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ From 42f9da2a27ab4487b7cc03de9ac182e75abfacad Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 13:47:52 +0000 Subject: [PATCH 09/23] Matthew's suggestion: lifting out left-/right- sublemmas --- src/Algebra/Module/Construct/Nagata.agda | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda index 500647f914..a7d21d4596 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -65,6 +65,7 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where open AbelianGroup M.+ᴹ-abelianGroup renaming (setoid to setoidᴹ; sym to symᴹ) + hiding (_≈_) +ᴹ-middleFour = Consequences.comm∧assoc⇒middleFour setoidᴹ +ᴹ-cong +ᴹ-comm +ᴹ-assoc @@ -73,14 +74,14 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where open module N = Bimodule (DirectProduct.bimodule TensorUnit.bimodule bimodule) using () renaming (Carrierᴹ to N - ; _≈ᴹ_ to _≈ᴺ_ + ; _≈ᴹ_ to _≈_ ; _+ᴹ_ to _+_ ; 0ᴹ to 0# ; -ᴹ_ to -_ ; +ᴹ-isAbelianGroup to +-isAbelianGroup ) - open Definitions _≈ᴺ_ + open Definitions _≈_ -- Injections ι from the components of the direct sum -- ιᴹ in fact exhibits M as an _ideal_ of R ⋉ M (see below) @@ -168,7 +169,7 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where -- Structure - isRingᴺ : IsRing _≈ᴺ_ _+_ _*_ -_ 0# 1# + isRingᴺ : IsRing _≈_ _+_ _*_ -_ 0# 1# isRingᴺ = record { +-isAbelianGroup = +-isAbelianGroup ; *-cong = *-cong @@ -185,13 +186,13 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ------------------------------------------------------------------------ -- M is an ideal of R ⋉ M satisying m * m ≈ 0# - idealˡ-M : (n : N) (m : M) → ∃[ n*m ] n * ιᴹ m ≈ᴺ ιᴹ n*m + idealˡ-M : (n : N) (m : M) → ∃[ n*m ] n * ιᴹ m ≈ ιᴹ n*m idealˡ-M n@(r , _) m = _ , R.zeroʳ r , ≈ᴹ-refl - idealʳ-M : (m : M) (n : N) → ∃[ m*n ] ιᴹ m * n ≈ᴺ ιᴹ m*n + idealʳ-M : (m : M) (n : N) → ∃[ m*n ] ιᴹ m * n ≈ ιᴹ m*n idealʳ-M m n@(r , _) = _ , R.zeroˡ r , ≈ᴹ-refl - m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ᴺ 0# + m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ 0# m*m≈0 m = R.zeroˡ R.0# , (begin R.0# *ₗ m +ᴹ m *ᵣ R.0# ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m) (*ᵣ-zeroʳ m) ⟩ From fdb8bfb33117fb8aff589b426fc6ead5e2fd4882 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 13:56:38 +0000 Subject: [PATCH 10/23] fixed constraint problem with ambiguous symbol; renamed ideal lemmas --- src/Algebra/Module/Construct/Nagata.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Nagata.agda index a7d21d4596..64190c91ef 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Nagata.agda @@ -186,11 +186,11 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ------------------------------------------------------------------------ -- M is an ideal of R ⋉ M satisying m * m ≈ 0# - idealˡ-M : (n : N) (m : M) → ∃[ n*m ] n * ιᴹ m ≈ ιᴹ n*m - idealˡ-M n@(r , _) m = _ , R.zeroʳ r , ≈ᴹ-refl + ιᴹ-idealˡ : (n : N) (m : M) → ∃[ n*m ] n * ιᴹ m ≈ ιᴹ n*m + ιᴹ-idealˡ n@(r , _) m = _ , R.zeroʳ r , ≈ᴹ-refl - idealʳ-M : (m : M) (n : N) → ∃[ m*n ] ιᴹ m * n ≈ ιᴹ m*n - idealʳ-M m n@(r , _) = _ , R.zeroˡ r , ≈ᴹ-refl + ιᴹ-idealʳ : (m : M) (n : N) → ∃[ m*n ] ιᴹ m * n ≈ ιᴹ m*n + ιᴹ-idealʳ m n@(r , _) = _ , R.zeroˡ r , ≈ᴹ-refl m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ 0# m*m≈0 m = R.zeroˡ R.0# , (begin From e11bbc8d614af4a2f0c16917109a57bd8e649d52 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 13:59:35 +0000 Subject: [PATCH 11/23] renamed module --- src/Algebra/Module/Construct/{Nagata.agda => Idealization.agda} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename src/Algebra/Module/Construct/{Nagata.agda => Idealization.agda} (99%) diff --git a/src/Algebra/Module/Construct/Nagata.agda b/src/Algebra/Module/Construct/Idealization.agda similarity index 99% rename from src/Algebra/Module/Construct/Nagata.agda rename to src/Algebra/Module/Construct/Idealization.agda index 64190c91ef..a58d595862 100644 --- a/src/Algebra/Module/Construct/Nagata.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -31,7 +31,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Algebra.Module.Construct.Nagata where +module Algebra.Module.Construct.Idealization where open import Algebra.Bundles using (AbelianGroup; Ring) open import Algebra.Core From 6935d8a177c6dd476b432835c8964edd4d123608 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 14:00:32 +0000 Subject: [PATCH 12/23] renamed module in `CHANGELOG` --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f2784fcff7..6f94a5c7bd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,7 +31,7 @@ New modules * Nagata's construction of the "idealization of a module": ```agda - Algebra.Module.Construct.Nagata + Algebra.Module.Construct.Idealization ``` Additions to existing modules From ae2d7f1b594632338b9f10b25421023358b2e38f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 14:35:10 +0000 Subject: [PATCH 13/23] added generalised annihilation lemma --- src/Algebra/Module/Construct/Idealization.agda | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index a58d595862..0eceeefcfb 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -192,12 +192,15 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ιᴹ-idealʳ : (m : M) (n : N) → ∃[ m*n ] ιᴹ m * n ≈ ιᴹ m*n ιᴹ-idealʳ m n@(r , _) = _ , R.zeroˡ r , ≈ᴹ-refl - m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ 0# - m*m≈0 m = R.zeroˡ R.0# , (begin + *-annihilates-ιᴹ : (m₁ m₂ : M) → ιᴹ m₁ * ιᴹ m₂ ≈ 0# + *-annihilates-ιᴹ m₁ m₂ = R.zeroˡ R.0# , (begin - R.0# *ₗ m +ᴹ m *ᵣ R.0# ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m) (*ᵣ-zeroʳ m) ⟩ - 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ - 0ᴹ ∎) + R.0# *ₗ m₂ +ᴹ m₁ *ᵣ R.0# ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m₂) (*ᵣ-zeroʳ m₁) ⟩ + 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ + 0ᴹ ∎) + + m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ 0# + m*m≈0 m = *-annihilates-ιᴹ m m ------------------------------------------------------------------------ -- Export From d4621a4b8bc47a9d4e43335e1c75746ae34e9b7b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 14:36:17 +0000 Subject: [PATCH 14/23] typos --- src/Algebra/Module/Construct/Idealization.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index 0eceeefcfb..bef4f8317a 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -184,7 +184,7 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where ringᴺ = record { isRing = isRingᴺ } ------------------------------------------------------------------------ --- M is an ideal of R ⋉ M satisying m * m ≈ 0# +-- M is an ideal of R ⋉ M satisfying m₁ * m₂ ≈ 0# ιᴹ-idealˡ : (n : N) (m : M) → ∃[ n*m ] n * ιᴹ m ≈ ιᴹ n*m ιᴹ-idealˡ n@(r , _) m = _ , R.zeroʳ r , ≈ᴹ-refl From afd70a41af999f7f1c71000b709da59d74af404b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 4 Jan 2024 14:49:23 +0000 Subject: [PATCH 15/23] use correct rexported names --- src/Algebra/Module/Construct/Idealization.agda | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index bef4f8317a..8ddebb3a3d 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -64,16 +64,15 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where renaming (Carrierᴹ to M) open AbelianGroup M.+ᴹ-abelianGroup - renaming (setoid to setoidᴹ; sym to symᴹ) hiding (_≈_) - +ᴹ-middleFour = Consequences.comm∧assoc⇒middleFour setoidᴹ +ᴹ-cong +ᴹ-comm +ᴹ-assoc + +ᴹ-middleFour = Consequences.comm∧assoc⇒middleFour ≈ᴹ-setoid +ᴹ-cong +ᴹ-comm +ᴹ-assoc - open ≈-Reasoning setoidᴹ + open ≈-Reasoning ≈ᴹ-setoid open module N = Bimodule (DirectProduct.bimodule TensorUnit.bimodule bimodule) using () - renaming (Carrierᴹ to N + renaming ( Carrierᴹ to N ; _≈ᴹ_ to _≈_ ; _+ᴹ_ to _+_ ; 0ᴹ to 0# @@ -138,7 +137,7 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where r₁ *ₗ (r₂ *ₗ m₃) +ᴹ (r₁ *ₗ (m₂ *ᵣ r₃) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) ≈⟨ +ᴹ-assoc (r₁ *ₗ (r₂ *ₗ m₃)) (r₁ *ₗ (m₂ *ᵣ r₃)) ((m₁ *ᵣ r₂) *ᵣ r₃) ⟨ (r₁ *ₗ (r₂ *ₗ m₃) +ᴹ r₁ *ₗ (m₂ *ᵣ r₃)) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃ - ≈⟨ +ᴹ-cong (symᴹ (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ + ≈⟨ +ᴹ-cong (≈ᴹ-sym (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ R.* r₃) ∎) distribˡ : _*_ DistributesOverˡ _+_ From 03ce1799cf17bb51349839e59ae63f97d79fa440 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 5 Jan 2024 09:01:42 +0000 Subject: [PATCH 16/23] now as a paramterised module instead --- .../Module/Construct/Idealization.agda | 203 +++++++++--------- 1 file changed, 99 insertions(+), 104 deletions(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index 8ddebb3a3d..142113c61d 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -31,13 +31,15 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Algebra.Module.Construct.Idealization where - open import Algebra.Bundles using (AbelianGroup; Ring) +open import Algebra.Module.Bundles using (Bimodule) + +module Algebra.Module.Construct.Idealization + {r ℓr m ℓm} (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where + open import Algebra.Core import Algebra.Consequences.Setoid as Consequences import Algebra.Definitions as Definitions -open import Algebra.Module.Bundles using (Bimodule) import Algebra.Module.Construct.DirectProduct as DirectProduct import Algebra.Module.Construct.TensorUnit as TensorUnit open import Algebra.Structures using (IsAbelianGroup; IsRing) @@ -46,121 +48,114 @@ open import Level using (Level; _⊔_) open import Relation.Binary using (Rel; Setoid; IsEquivalence) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -private - variable - m ℓm r ℓr : Level - ------------------------------------------------------------------------ -- Definitions -module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where - - private - open module R = Ring ring - using () - renaming (Carrier to R) +private + open module R = Ring ring + using () + renaming (Carrier to R) - open module M = Bimodule bimodule - renaming (Carrierᴹ to M) + open module M = Bimodule bimodule + renaming (Carrierᴹ to M) - open AbelianGroup M.+ᴹ-abelianGroup - hiding (_≈_) + open AbelianGroup M.+ᴹ-abelianGroup + hiding (_≈_) - +ᴹ-middleFour = Consequences.comm∧assoc⇒middleFour ≈ᴹ-setoid +ᴹ-cong +ᴹ-comm +ᴹ-assoc + +ᴹ-middleFour = Consequences.comm∧assoc⇒middleFour ≈ᴹ-setoid +ᴹ-cong +ᴹ-comm +ᴹ-assoc - open ≈-Reasoning ≈ᴹ-setoid + open ≈-Reasoning ≈ᴹ-setoid - open module N = Bimodule (DirectProduct.bimodule TensorUnit.bimodule bimodule) - using () - renaming ( Carrierᴹ to N - ; _≈ᴹ_ to _≈_ - ; _+ᴹ_ to _+_ - ; 0ᴹ to 0# - ; -ᴹ_ to -_ - ; +ᴹ-isAbelianGroup to +-isAbelianGroup - ) + open module N = Bimodule (DirectProduct.bimodule TensorUnit.bimodule bimodule) + using () + renaming ( Carrierᴹ to N + ; _≈ᴹ_ to _≈_ + ; _+ᴹ_ to _+_ + ; 0ᴹ to 0# + ; -ᴹ_ to -_ + ; +ᴹ-isAbelianGroup to +-isAbelianGroup + ) - open Definitions _≈_ + open Definitions _≈_ -- Injections ι from the components of the direct sum -- ιᴹ in fact exhibits M as an _ideal_ of R ⋉ M (see below) - ιᴿ : R → N - ιᴿ r = r , 0ᴹ +ιᴿ : R → N +ιᴿ r = r , 0ᴹ - ιᴹ : M → N - ιᴹ m = R.0# , m +ιᴹ : M → N +ιᴹ m = R.0# , m -- Multiplicative unit - 1# : N - 1# = ιᴿ R.1# +1# : N +1# = ιᴿ R.1# -- Multiplication - infixl 7 _*_ +infixl 7 _*_ - _*_ : Op₂ N - (r₁ , m₁) * (r₂ , m₂) = r₁ R.* r₂ , r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂ +_*_ : Op₂ N +(r₁ , m₁) * (r₂ , m₂) = r₁ R.* r₂ , r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂ -- Properties: because we work in the direct sum, every proof has -- * an 'R'-component, which inherits directly from R, and -- * an 'M'-component, where the work happens - *-cong : Congruent₂ _*_ - *-cong (r₁ , m₁) (r₂ , m₂) = R.*-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) - - *-identityˡ : LeftIdentity 1# _*_ - *-identityˡ (r , m) = R.*-identityˡ r , (begin +*-cong : Congruent₂ _*_ +*-cong (r₁ , m₁) (r₂ , m₂) = R.*-cong r₁ r₂ , +ᴹ-cong (*ₗ-cong r₁ m₂) (*ᵣ-cong m₁ r₂) - R.1# *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ - m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ - m ∎) +*-identityˡ : LeftIdentity 1# _*_ +*-identityˡ (r , m) = R.*-identityˡ r , (begin - *-identityʳ : RightIdentity 1# _*_ - *-identityʳ (r , m) = R.*-identityʳ r , (begin + R.1# *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ + m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ + m ∎) - r *ₗ 0ᴹ +ᴹ m *ᵣ R.1# ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ - 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ - m ∎) +*-identityʳ : RightIdentity 1# _*_ +*-identityʳ (r , m) = R.*-identityʳ r , (begin + r *ₗ 0ᴹ +ᴹ m *ᵣ R.1# ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ + 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ + m ∎) - *-identity : Identity 1# _*_ - *-identity = *-identityˡ , *-identityʳ +*-identity : Identity 1# _*_ +*-identity = *-identityˡ , *-identityʳ - *-assoc : Associative _*_ - *-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.*-assoc r₁ r₂ r₃ , (begin +*-assoc : Associative _*_ +*-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.*-assoc r₁ r₂ r₃ , (begin - (r₁ R.* r₂) *ₗ m₃ +ᴹ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) *ᵣ r₃ - ≈⟨ +ᴹ-cong (*ₗ-assoc r₁ r₂ m₃) (*ᵣ-distribʳ r₃ (r₁ *ₗ m₂) (m₁ *ᵣ r₂)) ⟩ - r₁ *ₗ (r₂ *ₗ m₃) +ᴹ ((r₁ *ₗ m₂) *ᵣ r₃ +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) - ≈⟨ +ᴹ-congˡ (+ᴹ-congʳ (*ₗ-*ᵣ-assoc r₁ m₂ r₃)) ⟩ - r₁ *ₗ (r₂ *ₗ m₃) +ᴹ (r₁ *ₗ (m₂ *ᵣ r₃) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) - ≈⟨ +ᴹ-assoc (r₁ *ₗ (r₂ *ₗ m₃)) (r₁ *ₗ (m₂ *ᵣ r₃)) ((m₁ *ᵣ r₂) *ᵣ r₃) ⟨ - (r₁ *ₗ (r₂ *ₗ m₃) +ᴹ r₁ *ₗ (m₂ *ᵣ r₃)) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃ - ≈⟨ +ᴹ-cong (≈ᴹ-sym (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ - r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ R.* r₃) ∎) + (r₁ R.* r₂) *ₗ m₃ +ᴹ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) *ᵣ r₃ + ≈⟨ +ᴹ-cong (*ₗ-assoc r₁ r₂ m₃) (*ᵣ-distribʳ r₃ (r₁ *ₗ m₂) (m₁ *ᵣ r₂)) ⟩ + r₁ *ₗ (r₂ *ₗ m₃) +ᴹ ((r₁ *ₗ m₂) *ᵣ r₃ +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) + ≈⟨ +ᴹ-congˡ (+ᴹ-congʳ (*ₗ-*ᵣ-assoc r₁ m₂ r₃)) ⟩ + r₁ *ₗ (r₂ *ₗ m₃) +ᴹ (r₁ *ₗ (m₂ *ᵣ r₃) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) + ≈⟨ +ᴹ-assoc (r₁ *ₗ (r₂ *ₗ m₃)) (r₁ *ₗ (m₂ *ᵣ r₃)) ((m₁ *ᵣ r₂) *ᵣ r₃) ⟨ + (r₁ *ₗ (r₂ *ₗ m₃) +ᴹ r₁ *ₗ (m₂ *ᵣ r₃)) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃ + ≈⟨ +ᴹ-cong (≈ᴹ-sym (*ₗ-distribˡ r₁ (r₂ *ₗ m₃) (m₂ *ᵣ r₃))) (*ᵣ-assoc m₁ r₂ r₃) ⟩ + r₁ *ₗ (r₂ *ₗ m₃ +ᴹ m₂ *ᵣ r₃) +ᴹ m₁ *ᵣ (r₂ R.* r₃) ∎) - distribˡ : _*_ DistributesOverˡ _+_ - distribˡ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ , (begin +distribˡ : _*_ DistributesOverˡ _+_ +distribˡ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ , (begin - r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ R.+ r₃) - ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ - (r₁ *ₗ m₂ +ᴹ r₁ *ₗ m₃) +ᴹ (m₁ *ᵣ r₂ +ᴹ m₁ *ᵣ r₃) - ≈⟨ +ᴹ-middleFour (r₁ *ₗ m₂) (r₁ *ₗ m₃) (m₁ *ᵣ r₂) (m₁ *ᵣ r₃) ⟩ - (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) + r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ R.+ r₃) + ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ + (r₁ *ₗ m₂ +ᴹ r₁ *ₗ m₃) +ᴹ (m₁ *ᵣ r₂ +ᴹ m₁ *ᵣ r₃) + ≈⟨ +ᴹ-middleFour (r₁ *ₗ m₂) (r₁ *ₗ m₃) (m₁ *ᵣ r₂) (m₁ *ᵣ r₃) ⟩ + (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) - distribʳ : _*_ DistributesOverʳ _+_ - distribʳ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribʳ r₁ r₂ r₃ , (begin +distribʳ : _*_ DistributesOverʳ _+_ +distribʳ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribʳ r₁ r₂ r₃ , (begin - (r₂ R.+ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ - ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ - (r₂ *ₗ m₁ +ᴹ r₃ *ₗ m₁) +ᴹ (m₂ *ᵣ r₁ +ᴹ m₃ *ᵣ r₁) - ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ - (r₂ *ₗ m₁ +ᴹ m₂ *ᵣ r₁) +ᴹ (r₃ *ₗ m₁ +ᴹ m₃ *ᵣ r₁) ∎) + (r₂ R.+ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ + ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ + (r₂ *ₗ m₁ +ᴹ r₃ *ₗ m₁) +ᴹ (m₂ *ᵣ r₁ +ᴹ m₃ *ᵣ r₁) + ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ + (r₂ *ₗ m₁ +ᴹ m₂ *ᵣ r₁) +ᴹ (r₃ *ₗ m₁ +ᴹ m₃ *ᵣ r₁) ∎) - distrib : _*_ DistributesOver _+_ - distrib = distribˡ , distribʳ +distrib : _*_ DistributesOver _+_ +distrib = distribˡ , distribʳ ------------------------------------------------------------------------ @@ -168,45 +163,45 @@ module Nagata (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where -- Structure - isRingᴺ : IsRing _≈_ _+_ _*_ -_ 0# 1# - isRingᴺ = record - { +-isAbelianGroup = +-isAbelianGroup - ; *-cong = *-cong - ; *-assoc = *-assoc - ; *-identity = *-identity - ; distrib = distrib - } +isRingᴺ : IsRing _≈_ _+_ _*_ -_ 0# 1# +isRingᴺ = record + { +-isAbelianGroup = +-isAbelianGroup + ; *-cong = *-cong + ; *-assoc = *-assoc + ; *-identity = *-identity + ; distrib = distrib + } -- Bundle - ringᴺ : Ring (r ⊔ m) (ℓr ⊔ ℓm) - ringᴺ = record { isRing = isRingᴺ } +ringᴺ : Ring (r ⊔ m) (ℓr ⊔ ℓm) +ringᴺ = record { isRing = isRingᴺ } ------------------------------------------------------------------------ -- M is an ideal of R ⋉ M satisfying m₁ * m₂ ≈ 0# - ιᴹ-idealˡ : (n : N) (m : M) → ∃[ n*m ] n * ιᴹ m ≈ ιᴹ n*m - ιᴹ-idealˡ n@(r , _) m = _ , R.zeroʳ r , ≈ᴹ-refl +ιᴹ-idealˡ : (n : N) (m : M) → ∃[ n*m ] n * ιᴹ m ≈ ιᴹ n*m +ιᴹ-idealˡ n@(r , _) m = _ , R.zeroʳ r , ≈ᴹ-refl - ιᴹ-idealʳ : (m : M) (n : N) → ∃[ m*n ] ιᴹ m * n ≈ ιᴹ m*n - ιᴹ-idealʳ m n@(r , _) = _ , R.zeroˡ r , ≈ᴹ-refl +ιᴹ-idealʳ : (m : M) (n : N) → ∃[ m*n ] ιᴹ m * n ≈ ιᴹ m*n +ιᴹ-idealʳ m n@(r , _) = _ , R.zeroˡ r , ≈ᴹ-refl - *-annihilates-ιᴹ : (m₁ m₂ : M) → ιᴹ m₁ * ιᴹ m₂ ≈ 0# - *-annihilates-ιᴹ m₁ m₂ = R.zeroˡ R.0# , (begin +*-annihilates-ιᴹ : (m₁ m₂ : M) → ιᴹ m₁ * ιᴹ m₂ ≈ 0# +*-annihilates-ιᴹ m₁ m₂ = R.zeroˡ R.0# , (begin - R.0# *ₗ m₂ +ᴹ m₁ *ᵣ R.0# ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m₂) (*ᵣ-zeroʳ m₁) ⟩ - 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ - 0ᴹ ∎) + R.0# *ₗ m₂ +ᴹ m₁ *ᵣ R.0# ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m₂) (*ᵣ-zeroʳ m₁) ⟩ + 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ + 0ᴹ ∎) - m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ 0# - m*m≈0 m = *-annihilates-ιᴹ m m +m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ 0# +m*m≈0 m = *-annihilates-ιᴹ m m ------------------------------------------------------------------------ --- Export +-- Export notation infixl 4 _⋉_ -_⋉_ : (R : Ring r ℓr) (M : Bimodule R R m ℓm) → Ring (r ⊔ m) (ℓr ⊔ ℓm) +_⋉_ : (R : Ring r ℓr) → Bimodule R R m ℓm → Ring (r ⊔ m) (ℓr ⊔ ℓm) -R ⋉ M = ringᴺ where open Nagata R M +R ⋉ M = ringᴺ From 583a712ec115090fc9fb39fecb0bb9fc55369531 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 5 Jan 2024 11:43:55 +0000 Subject: [PATCH 17/23] or did you intend this? --- src/Algebra/Module/Construct/Idealization.agda | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index 142113c61d..96e69ebb94 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -201,7 +201,5 @@ m*m≈0 m = *-annihilates-ιᴹ m m infixl 4 _⋉_ -_⋉_ : (R : Ring r ℓr) → Bimodule R R m ℓm → Ring (r ⊔ m) (ℓr ⊔ ℓm) - -R ⋉ M = ringᴺ +_⋉_ = ringᴺ From c859f58037c4fc3ad31c3d870756df90f7102a01 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 5 Jan 2024 11:47:47 +0000 Subject: [PATCH 18/23] fix whitespace --- src/Algebra/Module/Construct/Idealization.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index 96e69ebb94..79bf5aba39 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -192,10 +192,10 @@ ringᴺ = record { isRing = isRingᴺ } R.0# *ₗ m₂ +ᴹ m₁ *ᵣ R.0# ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m₂) (*ᵣ-zeroʳ m₁) ⟩ 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ 0ᴹ ∎) - + m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ 0# m*m≈0 m = *-annihilates-ιᴹ m m - + ------------------------------------------------------------------------ -- Export notation From ab91b5537d778a322b6bf4869be77103110f6216 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 18 Jan 2024 19:40:59 +0000 Subject: [PATCH 19/23] aligned one step of reasoning --- src/Algebra/Module/Construct/Idealization.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index 79bf5aba39..3f76b6d42d 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -128,7 +128,7 @@ _*_ : Op₂ N (r₁ R.* r₂) *ₗ m₃ +ᴹ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) *ᵣ r₃ ≈⟨ +ᴹ-cong (*ₗ-assoc r₁ r₂ m₃) (*ᵣ-distribʳ r₃ (r₁ *ₗ m₂) (m₁ *ᵣ r₂)) ⟩ r₁ *ₗ (r₂ *ₗ m₃) +ᴹ ((r₁ *ₗ m₂) *ᵣ r₃ +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) - ≈⟨ +ᴹ-congˡ (+ᴹ-congʳ (*ₗ-*ᵣ-assoc r₁ m₂ r₃)) ⟩ + ≈⟨ +ᴹ-congˡ (+ᴹ-congʳ (*ₗ-*ᵣ-assoc r₁ m₂ r₃)) ⟩ r₁ *ₗ (r₂ *ₗ m₃) +ᴹ (r₁ *ₗ (m₂ *ᵣ r₃) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) ≈⟨ +ᴹ-assoc (r₁ *ₗ (r₂ *ₗ m₃)) (r₁ *ₗ (m₂ *ᵣ r₃)) ((m₁ *ᵣ r₂) *ᵣ r₃) ⟨ (r₁ *ₗ (r₂ *ₗ m₃) +ᴹ r₁ *ₗ (m₂ *ᵣ r₃)) +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃ From 31ff3c1d346361850d3cdcb75e28687850cbc978 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 18 Jan 2024 19:43:12 +0000 Subject: [PATCH 20/23] more re-alignment of reasoning steps --- .../Module/Construct/Idealization.agda | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index 3f76b6d42d..cde7641c8e 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -138,21 +138,21 @@ _*_ : Op₂ N distribˡ : _*_ DistributesOverˡ _+_ distribˡ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ , (begin - r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ R.+ r₃) - ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ - (r₁ *ₗ m₂ +ᴹ r₁ *ₗ m₃) +ᴹ (m₁ *ᵣ r₂ +ᴹ m₁ *ᵣ r₃) - ≈⟨ +ᴹ-middleFour (r₁ *ₗ m₂) (r₁ *ₗ m₃) (m₁ *ᵣ r₂) (m₁ *ᵣ r₃) ⟩ - (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) + r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ R.+ r₃) + ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ + (r₁ *ₗ m₂ +ᴹ r₁ *ₗ m₃) +ᴹ (m₁ *ᵣ r₂ +ᴹ m₁ *ᵣ r₃) + ≈⟨ +ᴹ-middleFour (r₁ *ₗ m₂) (r₁ *ₗ m₃) (m₁ *ᵣ r₂) (m₁ *ᵣ r₃) ⟩ + (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) +ᴹ (r₁ *ₗ m₃ +ᴹ m₁ *ᵣ r₃) ∎) distribʳ : _*_ DistributesOverʳ _+_ distribʳ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribʳ r₁ r₂ r₃ , (begin - (r₂ R.+ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ - ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ - (r₂ *ₗ m₁ +ᴹ r₃ *ₗ m₁) +ᴹ (m₂ *ᵣ r₁ +ᴹ m₃ *ᵣ r₁) - ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ - (r₂ *ₗ m₁ +ᴹ m₂ *ᵣ r₁) +ᴹ (r₃ *ₗ m₁ +ᴹ m₃ *ᵣ r₁) ∎) + (r₂ R.+ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ + ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ + (r₂ *ₗ m₁ +ᴹ r₃ *ₗ m₁) +ᴹ (m₂ *ᵣ r₁ +ᴹ m₃ *ᵣ r₁) + ≈⟨ +ᴹ-middleFour (r₂ *ₗ m₁) (r₃ *ₗ m₁) (m₂ *ᵣ r₁) (m₃ *ᵣ r₁) ⟩ + (r₂ *ₗ m₁ +ᴹ m₂ *ᵣ r₁) +ᴹ (r₃ *ₗ m₁ +ᴹ m₃ *ᵣ r₁) ∎) distrib : _*_ DistributesOver _+_ distrib = distribˡ , distribʳ From a19c7842da3d0ae280f3f7d56eeae86b5e1fe404 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 18 Jan 2024 19:45:53 +0000 Subject: [PATCH 21/23] more re-alignment of reasoning steps --- src/Algebra/Module/Construct/Idealization.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index cde7641c8e..693629e1de 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -108,16 +108,16 @@ _*_ : Op₂ N *-identityˡ : LeftIdentity 1# _*_ *-identityˡ (r , m) = R.*-identityˡ r , (begin - R.1# *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ - m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ - m ∎) + R.1# *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ + m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ + m ∎) *-identityʳ : RightIdentity 1# _*_ *-identityʳ (r , m) = R.*-identityʳ r , (begin - r *ₗ 0ᴹ +ᴹ m *ᵣ R.1# ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ - 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ - m ∎) + r *ₗ 0ᴹ +ᴹ m *ᵣ R.1# ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ + 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ + m ∎) *-identity : Identity 1# _*_ *-identity = *-identityˡ , *-identityʳ From fe8d2a3235facac5e8c1b0e11e36083b4c592b11 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 30 Jan 2024 15:44:28 +0000 Subject: [PATCH 22/23] Matthew's review comments --- src/Algebra/Module/Construct/Idealization.agda | 17 ++++------------- 1 file changed, 4 insertions(+), 13 deletions(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index 693629e1de..21ebc6f488 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -59,13 +59,8 @@ private open module M = Bimodule bimodule renaming (Carrierᴹ to M) - open AbelianGroup M.+ᴹ-abelianGroup - hiding (_≈_) - +ᴹ-middleFour = Consequences.comm∧assoc⇒middleFour ≈ᴹ-setoid +ᴹ-cong +ᴹ-comm +ᴹ-assoc - open ≈-Reasoning ≈ᴹ-setoid - open module N = Bimodule (DirectProduct.bimodule TensorUnit.bimodule bimodule) using () renaming ( Carrierᴹ to N @@ -76,7 +71,9 @@ private ; +ᴹ-isAbelianGroup to +-isAbelianGroup ) - open Definitions _≈_ +open AbelianGroup M.+ᴹ-abelianGroup hiding (_≈_) +open ≈-Reasoning ≈ᴹ-setoid +open Definitions _≈_ -- Injections ι from the components of the direct sum -- ιᴹ in fact exhibits M as an _ideal_ of R ⋉ M (see below) @@ -107,14 +104,12 @@ _*_ : Op₂ N *-identityˡ : LeftIdentity 1# _*_ *-identityˡ (r , m) = R.*-identityˡ r , (begin - R.1# *ₗ m +ᴹ 0ᴹ *ᵣ r ≈⟨ +ᴹ-cong (*ₗ-identityˡ m) (*ᵣ-zeroˡ r) ⟩ m +ᴹ 0ᴹ ≈⟨ +ᴹ-identityʳ m ⟩ m ∎) *-identityʳ : RightIdentity 1# _*_ *-identityʳ (r , m) = R.*-identityʳ r , (begin - r *ₗ 0ᴹ +ᴹ m *ᵣ R.1# ≈⟨ +ᴹ-cong (*ₗ-zeroʳ r) (*ᵣ-identityʳ m) ⟩ 0ᴹ +ᴹ m ≈⟨ +ᴹ-identityˡ m ⟩ m ∎) @@ -124,7 +119,6 @@ _*_ : Op₂ N *-assoc : Associative _*_ *-assoc (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.*-assoc r₁ r₂ r₃ , (begin - (r₁ R.* r₂) *ₗ m₃ +ᴹ (r₁ *ₗ m₂ +ᴹ m₁ *ᵣ r₂) *ᵣ r₃ ≈⟨ +ᴹ-cong (*ₗ-assoc r₁ r₂ m₃) (*ᵣ-distribʳ r₃ (r₁ *ₗ m₂) (m₁ *ᵣ r₂)) ⟩ r₁ *ₗ (r₂ *ₗ m₃) +ᴹ ((r₁ *ₗ m₂) *ᵣ r₃ +ᴹ (m₁ *ᵣ r₂) *ᵣ r₃) @@ -137,7 +131,6 @@ _*_ : Op₂ N distribˡ : _*_ DistributesOverˡ _+_ distribˡ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ , (begin - r₁ *ₗ (m₂ +ᴹ m₃) +ᴹ m₁ *ᵣ (r₂ R.+ r₃) ≈⟨ +ᴹ-cong (*ₗ-distribˡ r₁ m₂ m₃) (*ᵣ-distribˡ m₁ r₂ r₃) ⟩ (r₁ *ₗ m₂ +ᴹ r₁ *ₗ m₃) +ᴹ (m₁ *ᵣ r₂ +ᴹ m₁ *ᵣ r₃) @@ -147,7 +140,6 @@ distribˡ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribˡ r₁ r₂ r₃ distribʳ : _*_ DistributesOverʳ _+_ distribʳ (r₁ , m₁) (r₂ , m₂) (r₃ , m₃) = R.distribʳ r₁ r₂ r₃ , (begin - (r₂ R.+ r₃) *ₗ m₁ +ᴹ (m₂ +ᴹ m₃) *ᵣ r₁ ≈⟨ +ᴹ-cong (*ₗ-distribʳ m₁ r₂ r₃) (*ᵣ-distribʳ r₁ m₂ m₃) ⟩ (r₂ *ₗ m₁ +ᴹ r₃ *ₗ m₁) +ᴹ (m₂ *ᵣ r₁ +ᴹ m₃ *ᵣ r₁) @@ -197,9 +189,8 @@ m*m≈0 : (m : M) → ιᴹ m * ιᴹ m ≈ 0# m*m≈0 m = *-annihilates-ιᴹ m m ------------------------------------------------------------------------ --- Export notation +-- Infix notation for when opening the module unparameterised infixl 4 _⋉_ _⋉_ = ringᴺ - From 80f30c9e6a7c58553fe299af4926f08e3e5a0302 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 30 Jan 2024 18:14:50 +0000 Subject: [PATCH 23/23] blanklines --- src/Algebra/Module/Construct/Idealization.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda index 21ebc6f488..0526f059fd 100644 --- a/src/Algebra/Module/Construct/Idealization.agda +++ b/src/Algebra/Module/Construct/Idealization.agda @@ -180,7 +180,6 @@ ringᴺ = record { isRing = isRingᴺ } *-annihilates-ιᴹ : (m₁ m₂ : M) → ιᴹ m₁ * ιᴹ m₂ ≈ 0# *-annihilates-ιᴹ m₁ m₂ = R.zeroˡ R.0# , (begin - R.0# *ₗ m₂ +ᴹ m₁ *ᵣ R.0# ≈⟨ +ᴹ-cong (*ₗ-zeroˡ m₂) (*ᵣ-zeroʳ m₁) ⟩ 0ᴹ +ᴹ 0ᴹ ≈⟨ +ᴹ-identityˡ 0ᴹ ⟩ 0ᴹ ∎) @@ -192,5 +191,4 @@ m*m≈0 m = *-annihilates-ιᴹ m m -- Infix notation for when opening the module unparameterised infixl 4 _⋉_ - _⋉_ = ringᴺ