From 9a9fd05cf56ed31ddb6f1377dc794299a8facb18 Mon Sep 17 00:00:00 2001 From: David Silverstone Date: Wed, 5 Aug 2026 09:16:45 -0700 Subject: [PATCH 1/2] [ add ] negatives for commutative monoids and semirings --- CHANGELOG.md | 6 + .../Add/Negatives/CommutativeMonoid.agda | 383 +++++++++++++++++ .../Construct/Add/Negatives/Semiring.agda | 398 ++++++++++++++++++ 3 files changed, 787 insertions(+) create mode 100644 src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda create mode 100644 src/Algebra/Construct/Add/Negatives/Semiring.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index eb838bcbe1..b22e6948ab 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -281,6 +281,12 @@ Deprecated names New modules ----------- +* `Algebra.Construct.Add.Negatives.CommutativeMonoid` and + `Algebra.Construct.Add.Negatives.Semiring` for the group completion of a + commutative monoid and the ring completion of a semiring, + respectively, including isomorphisms when the input is already an + abelian group or ring. + * `Algebra.Properties.KleeneAlgebra` has been completely rewritten. * `Codata.Guarded.Stream.Relation.Unary.Linked` for a proof that each pair diff --git a/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda b/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda new file mode 100644 index 0000000000..b6d80c189b --- /dev/null +++ b/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda @@ -0,0 +1,383 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Group completion of a commutative monoid, i.e. the Grothendieck group +-- of the monoid. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Algebra.Construct.Add.Negatives.CommutativeMonoid where + +open import Algebra.Bundles using (AbelianGroup; CommutativeMonoid) +import Algebra.Construct.DirectProduct as DirectProduct +import Algebra.Definitions as Definitions +open import Algebra.Morphism.Bundles using (MonoidHomomorphism) +open import Algebra.Morphism.Structures using + (IsGroupHomomorphism; IsGroupIsomorphism; IsMonoidHomomorphism) +import Algebra.Properties.AbelianGroup as AbelianGroupProperties +import Algebra.Properties.CommutativeSemigroup + as CommSemigroupProperties +open import Algebra.Structures using (IsAbelianGroup) +open import Data.Product.Base as Product + using (∃-syntax; _,_; -,_; <_,_>; proj₁; proj₂; uncurry) +open import Function.Base using (const; id; _∘_; _∘₂_) +import Function.Consequences.Setoid as Consequences +open import Function.Definitions using (Bijective; Congruent) +open import Level using (Level; _⊔_) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions + using (Reflexive; Symmetric; Transitive) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Relation.Binary.Structures using (IsEquivalence) + +module _ {m ℓ : Level} (monoid : CommutativeMonoid m ℓ) where + + private + module M = CommutativeMonoid monoid + open M using (commutativeSemigroup; rawMonoid; setoid) + renaming + ( Carrier to Base ; _≈_ to _≈ₘ_ + ; _∙_ to _+ₘ_ ; ε to 0ₘ + ; refl to ≈ₘ-refl ; sym to ≈ₘ-sym + ; ∙-cong to +ₘ-cong + ; ∙-congˡ to +ₘ-congˡ ; ∙-congʳ to +ₘ-congʳ + ; assoc to +ₘ-assoc ; comm to +ₘ-comm + ; identityˡ to +ₘ-identityˡ ; identityʳ to +ₘ-identityʳ + ) + + directProduct : CommutativeMonoid m ℓ + directProduct = DirectProduct.commutativeMonoid monoid monoid + + module M² = CommutativeMonoid directProduct + open CommSemigroupProperties commutativeSemigroup using (medial) + + open ≈-Reasoning setoid + + + ------------------------------------------------------------------------ + -- Formal differences + + open M² public using (Carrier) renaming (_∙_ to _+_; ε to 0#) + + pos : Carrier → Base + pos = proj₁ + + neg : Carrier → Base + neg = proj₂ + + ------------------------------------------------------------------------ + -- Equality + + infix 4 _≈_ + + _≈_ : Rel Carrier (m ⊔ ℓ) + x ≈ y = ∃[ slack ] + (pos x +ₘ neg y) +ₘ slack ≈ₘ (pos y +ₘ neg x) +ₘ slack + + open Definitions _≈_ using (Congruent₁; Congruent₂; LeftInverse) + + private + rearrange : ∀ a b c d u v → + ((a +ₘ c) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) ≈ₘ + ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v) + rearrange a b c d u v = begin + ((a +ₘ c) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) + ≈⟨ +ₘ-congʳ (medial a c b d) ⟩ + ((a +ₘ b) +ₘ (c +ₘ d)) +ₘ (u +ₘ v) + ≈⟨ medial (a +ₘ b) (c +ₘ d) u v ⟩ + ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v) ∎ + + composeˡ : ∀ a b c d u v → + (a +ₘ b) +ₘ ((c +ₘ d) +ₘ (u +ₘ v)) ≈ₘ + ((a +ₘ d) +ₘ u) +ₘ ((c +ₘ b) +ₘ v) + composeˡ a b c d u v = begin + (a +ₘ b) +ₘ ((c +ₘ d) +ₘ (u +ₘ v)) + ≈⟨ +ₘ-assoc (a +ₘ b) (c +ₘ d) (u +ₘ v) ⟨ + ((a +ₘ b) +ₘ (c +ₘ d)) +ₘ (u +ₘ v) + ≈⟨ +ₘ-congʳ (medial a b c d) ⟩ + ((a +ₘ c) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) + ≈⟨ +ₘ-congʳ (+ₘ-congˡ (+ₘ-comm b d)) ⟩ + ((a +ₘ c) +ₘ (d +ₘ b)) +ₘ (u +ₘ v) + ≈⟨ rearrange a d c b u v ⟩ + ((a +ₘ d) +ₘ u) +ₘ ((c +ₘ b) +ₘ v) ∎ + + composeʳ : ∀ a b c d u v → + ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v) ≈ₘ + (c +ₘ b) +ₘ ((a +ₘ d) +ₘ (u +ₘ v)) + composeʳ a b c d u v = begin + ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v) + ≈⟨ rearrange a b c d u v ⟨ + ((a +ₘ c) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) + ≈⟨ +ₘ-congʳ (+ₘ-congˡ (+ₘ-comm b d)) ⟩ + ((a +ₘ c) +ₘ (d +ₘ b)) +ₘ (u +ₘ v) + ≈⟨ +ₘ-congʳ (medial a c d b) ⟩ + ((a +ₘ d) +ₘ (c +ₘ b)) +ₘ (u +ₘ v) + ≈⟨ +ₘ-congʳ (+ₘ-comm (a +ₘ d) (c +ₘ b)) ⟩ + ((c +ₘ b) +ₘ (a +ₘ d)) +ₘ (u +ₘ v) + ≈⟨ +ₘ-assoc (c +ₘ b) (a +ₘ d) (u +ₘ v) ⟩ + (c +ₘ b) +ₘ ((a +ₘ d) +ₘ (u +ₘ v)) ∎ + + ≈-from-parts : ∀ {x y} → + pos x ≈ₘ pos y → neg x ≈ₘ neg y → x ≈ y + ≈-from-parts x⁺≈y⁺ x⁻≈y⁻ = + 0ₘ , +ₘ-congʳ (+ₘ-cong x⁺≈y⁺ (≈ₘ-sym x⁻≈y⁻)) + + private + pointwise⇒≈ : ∀ {x y} → M²._≈_ x y → x ≈ y + pointwise⇒≈ = uncurry ≈-from-parts + + ≈-refl : Reflexive _≈_ + ≈-refl = pointwise⇒≈ M².refl + + ≈-trans : Transitive _≈_ + ≈-trans {a , b} {c , d} {e , f} = + Product.zip (λ u v → (c +ₘ d) +ₘ (u +ₘ v)) + λ {u} {v} eq₁ eq₂ → begin + (a +ₘ f) +ₘ ((c +ₘ d) +ₘ (u +ₘ v)) + ≈⟨ composeˡ a f c d u v ⟩ + ((a +ₘ d) +ₘ u) +ₘ ((c +ₘ f) +ₘ v) + ≈⟨ +ₘ-cong eq₁ eq₂ ⟩ + ((c +ₘ b) +ₘ u) +ₘ ((e +ₘ d) +ₘ v) + ≈⟨ composeʳ c b e d u v ⟩ + (e +ₘ b) +ₘ ((c +ₘ d) +ₘ (u +ₘ v)) ∎ + + ≈-isEquivalence : IsEquivalence _≈_ + ≈-isEquivalence = record + { refl = ≈-refl + ; sym = Product.map₂ ≈ₘ-sym + ; trans = ≈-trans + } + + ------------------------------------------------------------------------ + -- Operations + + infix 8 -_ + + -_ : Carrier → Carrier + -_ = Product.swap + + +-cong : Congruent₂ _+_ + +-cong {a , b} {a′ , b′} {c , d} {c′ , d′} = + Product.zip _+ₘ_ λ {u} {v} eq₁ eq₂ → begin + ((a +ₘ c) +ₘ (b′ +ₘ d′)) +ₘ (u +ₘ v) + ≈⟨ rearrange a b′ c d′ u v ⟩ + ((a +ₘ b′) +ₘ u) +ₘ ((c +ₘ d′) +ₘ v) + ≈⟨ +ₘ-cong eq₁ eq₂ ⟩ + ((a′ +ₘ b) +ₘ u) +ₘ ((c′ +ₘ d) +ₘ v) + ≈⟨ rearrange a′ b c′ d u v ⟨ + ((a′ +ₘ c′) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) ∎ + + -‿cong : Congruent₁ -_ + -‿cong {a , b} {c , d} = Product.map₂ λ {u} eq → begin + (b +ₘ c) +ₘ u ≈⟨ +ₘ-congʳ (+ₘ-comm b c) ⟩ + (c +ₘ b) +ₘ u ≈⟨ eq ⟨ + (a +ₘ d) +ₘ u ≈⟨ +ₘ-congʳ (+ₘ-comm a d) ⟩ + (d +ₘ a) +ₘ u ∎ + + +-inverseˡ : LeftInverse 0# -_ _+_ + +-inverseˡ (a , b) = -, (begin + ((b +ₘ a) +ₘ 0ₘ) +ₘ 0ₘ ≈⟨ +ₘ-identityʳ _ ⟩ + (b +ₘ a) +ₘ 0ₘ ≈⟨ +ₘ-congʳ (+ₘ-comm b a) ⟩ + (a +ₘ b) +ₘ 0ₘ ≈⟨ +ₘ-congʳ (+ₘ-identityˡ _) ⟨ + (0ₘ +ₘ (a +ₘ b)) +ₘ 0ₘ ∎) + + ------------------------------------------------------------------------ + -- Bundle + + completion-is-abelian-group : IsAbelianGroup _≈_ _+_ 0# -_ + completion-is-abelian-group = record + { isGroup = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = ≈-isEquivalence + ; ∙-cong = +-cong + } + ; assoc = λ x → pointwise⇒≈ ∘₂ M².assoc x + } + ; identity = Product.map + (pointwise⇒≈ ∘_) (pointwise⇒≈ ∘_) M².identity + } + ; inverse = +-inverseˡ , λ x → + ≈-trans (pointwise⇒≈ (M².comm x (- x))) (+-inverseˡ x) + ; ⁻¹-cong = -‿cong + } + ; comm = pointwise⇒≈ ∘₂ M².comm + } + + abelianGroup : AbelianGroup m (m ⊔ ℓ) + abelianGroup = record + { Carrier = Carrier + ; _≈_ = _≈_ + ; _∙_ = _+_ + ; ε = 0# + ; _⁻¹ = -_ + ; isAbelianGroup = completion-is-abelian-group + } + + open AbelianGroup abelianGroup + using () renaming (rawMonoid to rawMonoid#) + + ------------------------------------------------------------------------ + -- Canonical embedding + + embed : Base → Carrier + embed = < id , const 0ₘ > + + embed-cong : Congruent _≈ₘ_ _≈_ embed + embed-cong x≈y = ≈-from-parts x≈y ≈ₘ-refl + + embed-∙ : ∀ x y → embed (x +ₘ y) ≈ embed x + embed y + embed-∙ x y = + ≈-from-parts ≈ₘ-refl (≈ₘ-sym (+ₘ-identityˡ 0ₘ)) + + embed-isMonoidHomomorphism : + IsMonoidHomomorphism rawMonoid rawMonoid# embed + embed-isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = embed-cong } + ; ∙-homo = embed-∙ + } + ; ε-homo = ≈-refl + } + + embed-monoidHomomorphism : + MonoidHomomorphism rawMonoid rawMonoid# + embed-monoidHomomorphism = record + { ⟦_⟧ = embed + ; isMonoidHomomorphism = embed-isMonoidHomomorphism + } + + decompose : ∀ x → x ≈ embed (pos x) + - embed (neg x) + decompose (a , b) = + ≈-from-parts (≈ₘ-sym (+ₘ-identityʳ a)) + (≈ₘ-sym (+ₘ-identityˡ b)) + + + ------------------------------------------------------------------------ + -- Trivial completions + + open Definitions _≈ₘ_ using (RightZero) + + absorbing⇒trivial : (∞ : Base) → RightZero ∞ _+ₘ_ → + ∀ x → x ≈ 0# + absorbing⇒trivial ∞ zeroʳ (a , b) = -, (begin + (a +ₘ 0ₘ) +ₘ ∞ ≈⟨ zeroʳ (a +ₘ 0ₘ) ⟩ + ∞ ≈⟨ zeroʳ (0ₘ +ₘ b) ⟨ + (0ₘ +ₘ b) +ₘ ∞ ∎) + + +------------------------------------------------------------------------ +-- Completion of an abelian group + +module AlreadyGroup {m ℓ : Level} (G : AbelianGroup m ℓ) where + + private + module G = AbelianGroup G + module Gₚ = AbelianGroupProperties G + open CommSemigroupProperties G.commutativeSemigroup using (medial) + open Gₚ using + (//-rightDividesˡ; ∙-cancelʳ; ε⁻¹≈ε + ; ⁻¹-anti-homo‿-; ⁻¹-∙-comm) + + completion : AbelianGroup m (m ⊔ ℓ) + completion = abelianGroup G.commutativeMonoid + + module C = AbelianGroup completion + open Consequences C.setoid G.setoid using + (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ + ; strictlyInverseʳ⇒inverseʳ) + + open G using () renaming + ( _≈_ to _≈g_ ; _∙_ to _+g_ + ; ε to 0g ; _⁻¹ to -g_ + ; sym to ≈g-sym + ; ∙-congˡ to +g-congˡ ; ∙-congʳ to +g-congʳ + ; assoc to +g-assoc ; comm to +g-comm + ; identityʳ to +g-identityʳ + ) + + open ≈-Reasoning G.setoid + + reduce-difference : ∀ a b c → + (a G.- b) +g (b +g c) ≈g a +g c + reduce-difference a b c = begin + (a G.- b) +g (b +g c) ≈⟨ +g-assoc _ _ _ ⟨ + ((a G.- b) +g b) +g c ≈⟨ +g-congʳ (//-rightDividesˡ _ _) ⟩ + a +g c ∎ + + self-completion-to-self : C.Carrier → G.Carrier + self-completion-to-self = Product.uncurry G._-_ + + to-self-cong : Congruent C._≈_ G._≈_ self-completion-to-self + to-self-cong {a , b} {c , d} = Product.uncurry λ slack eq → + ∙-cancelʳ (b +g d) _ _ (begin + (a G.- b) +g (b +g d) ≈⟨ reduce-difference a b d ⟩ + a +g d ≈⟨ ∙-cancelʳ slack _ _ eq ⟩ + c +g b ≈⟨ reduce-difference c d b ⟨ + (c G.- d) +g (d +g b) ≈⟨ +g-congˡ (+g-comm b d) ⟨ + (c G.- d) +g (b +g d) ∎) + + to-self-∙ : ∀ x y → + self-completion-to-self (C._∙_ x y) ≈g + self-completion-to-self x +g self-completion-to-self y + to-self-∙ (a , b) (c , d) = begin + (a +g c) G.- (b +g d) ≡⟨⟩ + (a +g c) +g -g (b +g d) ≈⟨ +g-congˡ (⁻¹-∙-comm _ _) ⟨ + (a +g c) +g (-g b +g -g d) ≈⟨ medial a c (-g b) (-g d) ⟩ + (a +g -g b) +g (c +g -g d) ≡⟨⟩ + (a G.- b) +g (c G.- d) ∎ + + to-self-embed : ∀ x → + self-completion-to-self (embed G.commutativeMonoid x) ≈g x + to-self-embed x = begin + x G.- 0g ≡⟨⟩ + x +g -g 0g ≈⟨ +g-congˡ ε⁻¹≈ε ⟩ + x +g 0g ≈⟨ +g-identityʳ x ⟩ + x ∎ + + to-self-⁻¹ : ∀ x → + self-completion-to-self (C._⁻¹ x) ≈g + -g self-completion-to-self x + to-self-⁻¹ (a , b) = ≈g-sym (⁻¹-anti-homo‿- a b) + + to-self-isGroupHomomorphism : + IsGroupHomomorphism C.rawGroup G.rawGroup self-completion-to-self + to-self-isGroupHomomorphism = record + { isMonoidHomomorphism = record + { isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = to-self-cong } + ; ∙-homo = to-self-∙ + } + ; ε-homo = to-self-embed 0g + } + ; ⁻¹-homo = to-self-⁻¹ + } + + embed-to-self : ∀ x → + embed G.commutativeMonoid (self-completion-to-self x) C.≈ x + embed-to-self (a , b) = -, (begin + ((a G.- b) +g b) +g 0g ≈⟨ +g-identityʳ _ ⟩ + (a G.- b) +g b ≈⟨ //-rightDividesˡ b a ⟩ + a ≈⟨ +g-identityʳ a ⟨ + a +g 0g ≈⟨ +g-identityʳ _ ⟨ + (a +g 0g) +g 0g ∎) + + to-self-bijective : + Bijective C._≈_ G._≈_ self-completion-to-self + to-self-bijective = inverseᵇ⇒bijective + ( strictlyInverseˡ⇒inverseˡ to-self-cong to-self-embed + , strictlyInverseʳ⇒inverseʳ (embed-cong G.commutativeMonoid) + embed-to-self + ) + + self-completion-≅ : + IsGroupIsomorphism C.rawGroup G.rawGroup self-completion-to-self + self-completion-≅ = record + { isGroupMonomorphism = record + { isGroupHomomorphism = to-self-isGroupHomomorphism + ; injective = proj₁ to-self-bijective + } + ; surjective = proj₂ to-self-bijective + } diff --git a/src/Algebra/Construct/Add/Negatives/Semiring.agda b/src/Algebra/Construct/Add/Negatives/Semiring.agda new file mode 100644 index 0000000000..3c64be412a --- /dev/null +++ b/src/Algebra/Construct/Add/Negatives/Semiring.agda @@ -0,0 +1,398 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Ring completion of a semiring, freely adjoining negatives +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Algebra.Construct.Add.Negatives.Semiring where + +open import Algebra.Bundles + using (AbelianGroup; CommutativeRing; Ring; Semiring) +import Algebra.Construct.Add.Negatives.CommutativeMonoid as Negatives +import Algebra.Definitions as Definitions +open import Algebra.Morphism.Bundles using (SemiringHomomorphism) +open import Algebra.Morphism.Structures using + (IsGroupIsomorphism; IsRingHomomorphism; IsRingIsomorphism + ; IsSemiringHomomorphism) +import Algebra.Properties.CommutativeSemigroup as CSProperties +import Algebra.Properties.Ring as RingProperties +open import Algebra.Structures using (IsRing) +open import Data.Product.Base as Product + using (_,_; <_,_>) +open import Function.Base using (_∘_; _∘₂_) +open import Function.Definitions using (Congruent) +open import Level using (Level; _⊔_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Relation.Binary.Structures using (IsEquivalence) + +module _ {m ℓ : Level} (semiring : Semiring m ℓ) where + + private + module S = Semiring semiring + open CSProperties S.+-commutativeSemigroup using (medial) + + open S using () renaming + ( Carrier to Base + ; _+_ to _+ₛ_ ; _*_ to _*ₛ_ ; _≈_ to _≈ₛ_ + ; 0# to 0ₛ ; 1# to 1ₛ + ) + + ---------------------------------------------------------------------- + -- Additive completion + + private + +Group : AbelianGroup m (m ⊔ ℓ) + +Group = Negatives.abelianGroup S.+-commutativeMonoid + + module Additive = AbelianGroup +Group + + open Additive public using (Carrier) + renaming (_≈_ to _≈_; _∙_ to _+_; ε to 0#; _⁻¹ to -_) + open Additive using () renaming + (∙-cong to +-cong; ⁻¹-cong to -‿cong) + + pos neg : Carrier → Base + pos = Negatives.pos S.+-commutativeMonoid + neg = Negatives.neg S.+-commutativeMonoid + + private + ≈-from-parts : ∀ {x y} → + pos x S.≈ pos y → neg x S.≈ neg y → x ≈ y + ≈-from-parts = Negatives.≈-from-parts S.+-commutativeMonoid + + module ≈ = IsEquivalence Additive.isEquivalence + + variable + x y z : Carrier + a b c d : Base + + infix 4 _≈[_]_ + _≈[_]_ : Carrier → Base → Carrier → Set ℓ + x ≈[ slack ] y = + (pos x +ₛ neg y) +ₛ slack ≈ₛ (pos y +ₛ neg x) +ₛ slack + + open Definitions _≈_ using + (Associative; Congruent₂; LeftCongruent; LeftIdentity + ; RightCongruent; RightIdentity + ; _DistributesOverˡ_; _DistributesOverʳ_) + open Definitions (_≈ₛ_) using (Commutative; RightZero) + + ---------------------------------------------------------------------- + -- Addition permutations + + private + swap-middle : ∀ p q r s → + (p +ₛ q) +ₛ (r +ₛ s) ≈ₛ + (p +ₛ r) +ₛ (s +ₛ q) + swap-middle p q r s = S.trans + (medial p q r s) + (S.+-congˡ (S.+-comm q s)) + + ---------------------------------------------------------------------- + -- Multiplication + + infixl 7 _*_ + + private + prod⁺ : Carrier → Carrier → Base + prod⁺ = Product.uncurry′ S._+_ ∘₂ Product.zip′ S._*_ S._*_ + + _*_ : Carrier → Carrier → Carrier + _*_ x = < prod⁺ x , prod⁺ x ∘ -_ > + + 1# : Carrier + 1# = 1ₛ , 0ₛ + + private + scaleˡ : Base → Carrier → Carrier + scaleˡ a = Product.map (a *ₛ_) (a *ₛ_) + + scaleʳ : Carrier → Base → Carrier + scaleʳ x a = Product.map (_*ₛ a) (_*ₛ a) x + + map-cong : ∀ f → Congruent _≈ₛ_ _≈ₛ_ f → + (∀ a b c → f ((a +ₛ b) +ₛ c) ≈ₛ + (f a +ₛ f b) +ₛ f c) → + Congruent _≈_ _≈_ (Product.map f f) + map-cong f cong distrib = Product.map f λ {slack} eq → begin + (f _ +ₛ f _) +ₛ f slack ≈⟨ distrib _ _ slack ⟨ + f ((_ +ₛ _) +ₛ slack) ≈⟨ cong eq ⟩ + f ((_ +ₛ _) +ₛ slack) ≈⟨ distrib _ _ slack ⟩ + (f _ +ₛ f _) +ₛ f slack ∎ + where open ≈-Reasoning S.setoid + + scale-congˡ : Congruent _≈_ _≈_ (scaleˡ a) + scale-congˡ {a} = map-cong (a *ₛ_) S.*-congˡ λ x y z → + S.trans (S.distribˡ _ _ _) (S.+-congʳ (S.distribˡ _ _ _)) + + scale-congʳ : Congruent _≈_ _≈_ (λ x → scaleʳ x a) + scale-congʳ {a} = map-cong (_*ₛ a) S.*-congʳ λ x y z → + S.trans (S.distribʳ _ _ _) (S.+-congʳ (S.distribʳ _ _ _)) + + *-as-scalesʳ : x * y ≈ scaleʳ x (pos y) + - scaleʳ x (neg y) + *-as-scalesʳ {(a , b)} {(c , d)} = + ≈-from-parts S.refl (S.+-comm (a *ₛ d) (b *ₛ c)) + + *-congʳ : RightCongruent _*_ + *-congʳ {y} {x} {x′} x≈x′ = begin + x * y + ≈⟨ *-as-scalesʳ ⟩ + scaleʳ x (pos y) + - scaleʳ x (neg y) + ≈⟨ +-cong (scale-congʳ x≈x′) + (-‿cong (scale-congʳ x≈x′)) ⟩ + scaleʳ x′ (pos y) + - scaleʳ x′ (neg y) + ≈⟨ *-as-scalesʳ ⟨ + x′ * y ∎ + where open ≈-Reasoning Additive.setoid + + *-congˡ : LeftCongruent _*_ + *-congˡ {x} y≈y′ = + +-cong (scale-congˡ y≈y′) (-‿cong (scale-congˡ y≈y′)) + + *-cong : Congruent₂ _*_ + *-cong x≈ y≈ = ≈.trans (*-congʳ x≈) (*-congˡ y≈) + + open ≈-Reasoning S.setoid + + ---------------------------------------------------------------------- + -- Ring laws + + private + distrib⁺ˡ : ∀ x y z → + prod⁺ x (y + z) ≈ₛ prod⁺ x y +ₛ prod⁺ x z + distrib⁺ˡ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = + S.trans + (S.+-cong (S.distribˡ _ _ _) (S.distribˡ _ _ _)) + (medial (x⁺ *ₛ y⁺) (x⁺ *ₛ z⁺) + (x⁻ *ₛ y⁻) (x⁻ *ₛ z⁻)) + + distrib⁺ʳ : ∀ x y z → + prod⁺ (x + y) z ≈ₛ prod⁺ x z +ₛ prod⁺ y z + distrib⁺ʳ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = + S.trans + (S.+-cong (S.distribʳ _ _ _) (S.distribʳ _ _ _)) + (medial (x⁺ *ₛ z⁺) (y⁺ *ₛ z⁺) + (x⁻ *ₛ z⁻) (y⁻ *ₛ z⁻)) + + assoc⁺ : ∀ x y z → prod⁺ (x * y) z ≈ₛ prod⁺ x (y * z) + assoc⁺ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = begin + (((x⁺ *ₛ y⁺) +ₛ (x⁻ *ₛ y⁻)) *ₛ z⁺) +ₛ + (((x⁺ *ₛ y⁻) +ₛ (x⁻ *ₛ y⁺)) *ₛ z⁻) + ≈⟨ S.+-cong (S.distribʳ _ _ _) (S.distribʳ _ _ _) ⟩ + (((x⁺ *ₛ y⁺) *ₛ z⁺) +ₛ ((x⁻ *ₛ y⁻) *ₛ z⁺)) + +ₛ (((x⁺ *ₛ y⁻) *ₛ z⁻) + +ₛ ((x⁻ *ₛ y⁺) *ₛ z⁻)) + ≈⟨ S.+-cong (S.+-cong (S.*-assoc _ _ _) (S.*-assoc _ _ _)) + (S.+-cong (S.*-assoc _ _ _) (S.*-assoc _ _ _)) ⟩ + (x⁺ *ₛ (y⁺ *ₛ z⁺)) +ₛ (x⁻ *ₛ (y⁻ *ₛ z⁺)) + +ₛ ((x⁺ *ₛ (y⁻ *ₛ z⁻)) + +ₛ (x⁻ *ₛ (y⁺ *ₛ z⁻))) + ≈⟨ swap-middle _ _ _ _ ⟩ + (x⁺ *ₛ (y⁺ *ₛ z⁺)) +ₛ (x⁺ *ₛ (y⁻ *ₛ z⁻)) + +ₛ ((x⁻ *ₛ (y⁺ *ₛ z⁻)) + +ₛ (x⁻ *ₛ (y⁻ *ₛ z⁺))) + ≈⟨ S.+-cong (S.distribˡ _ _ _) (S.distribˡ _ _ _) ⟨ + (x⁺ *ₛ ((y⁺ *ₛ z⁺) +ₛ (y⁻ *ₛ z⁻))) +ₛ + (x⁻ *ₛ ((y⁺ *ₛ z⁻) +ₛ (y⁻ *ₛ z⁺))) ∎ + + *-assoc : Associative _*_ + *-assoc x y z = ≈-from-parts + (assoc⁺ x y z) (assoc⁺ x y (- z)) + + *-identityˡ : LeftIdentity 1# _*_ + *-identityˡ (x⁺ , x⁻) = ≈-from-parts + (S.trans (S.+-cong (S.*-identityˡ _) (S.zeroˡ _)) + (S.+-identityʳ x⁺)) + (S.trans (S.+-cong (S.*-identityˡ _) (S.zeroˡ _)) + (S.+-identityʳ x⁻)) + + *-identityʳ : RightIdentity 1# _*_ + *-identityʳ (x⁺ , x⁻) = ≈-from-parts + (S.trans (S.+-cong (S.*-identityʳ _) (S.zeroʳ _)) + (S.+-identityʳ x⁺)) + (S.trans (S.+-comm (x⁺ *ₛ 0ₛ) (x⁻ *ₛ 1ₛ)) + (S.trans (S.+-cong (S.*-identityʳ _) (S.zeroʳ _)) + (S.+-identityʳ x⁻))) + + distribˡ : _*_ DistributesOverˡ _+_ + distribˡ x y z = ≈-from-parts + (distrib⁺ˡ x y z) (distrib⁺ˡ x (- y) (- z)) + + distribʳ : _*_ DistributesOverʳ _+_ + distribʳ x y z = ≈-from-parts + (distrib⁺ʳ y z x) (distrib⁺ʳ y z (- x)) + + ---------------------------------------------------------------------- + -- Bundle + + completion-is-ring : IsRing _≈_ _+_ _*_ -_ 0# 1# + completion-is-ring = record + { +-isAbelianGroup = AbelianGroup.isAbelianGroup +Group + ; *-cong = *-cong + ; *-assoc = *-assoc + ; *-identity = *-identityˡ , *-identityʳ + ; distrib = distribˡ , distribʳ + } + + ring : Ring m (m ⊔ ℓ) + ring = record + { Carrier = Carrier + ; _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + ; isRing = completion-is-ring + } + + private module R = Semiring (Ring.semiring ring) + + ------------------------------------------------------------------------ + -- Commutative specialization + + private + *-comm : Commutative S._*_ → ∀ x y → x * y ≈ y * x + *-comm comm (a , b) (c , d) = ≈-from-parts + (S.+-cong (comm a c) (comm b d)) + (begin + (a *ₛ d) +ₛ (b *ₛ c) + ≈⟨ S.+-cong (comm a d) (comm b c) ⟩ + (d *ₛ a) +ₛ (c *ₛ b) + ≈⟨ S.+-comm (d *ₛ a) (c *ₛ b) ⟩ + (c *ₛ b) +ₛ (d *ₛ a) ∎) + + commutativeRing : Commutative S._*_ → CommutativeRing m (m ⊔ ℓ) + commutativeRing comm = record + { isCommutativeRing = record + { isRing = completion-is-ring + ; *-comm = *-comm comm + } + } + + + ---------------------------------------------------------------------- + -- Canonical embedding + + embed : Base → Carrier + embed = Negatives.embed S.+-commutativeMonoid + + decompose : ∀ x → x ≈ embed (pos x) + - embed (neg x) + decompose = Negatives.decompose S.+-commutativeMonoid + + embed-* : ∀ x y → embed (x *ₛ y) ≈ embed x * embed y + embed-* x y = ≈-from-parts + (begin + x *ₛ y ≈⟨ S.+-identityʳ _ ⟨ + (x *ₛ y) +ₛ 0ₛ ≈⟨ S.+-congˡ (S.zeroˡ _) ⟨ + (x *ₛ y) +ₛ (0ₛ *ₛ 0ₛ) ∎) + (begin + 0ₛ ≈⟨ S.+-identityˡ _ ⟨ + 0ₛ +ₛ 0ₛ ≈⟨ S.+-cong (S.zeroʳ _) (S.zeroˡ _) ⟨ + (x *ₛ 0ₛ) +ₛ (0ₛ *ₛ y) ∎) + + embed-isSemiringHomomorphism : + IsSemiringHomomorphism S.rawSemiring R.rawSemiring embed + embed-isSemiringHomomorphism = record + { isNearSemiringHomomorphism = record + { +-isMonoidHomomorphism = + Negatives.embed-isMonoidHomomorphism + S.+-commutativeMonoid + ; *-homo = embed-* + } + ; 1#-homo = ≈.refl + } + + embed-semiringHomomorphism : + SemiringHomomorphism S.rawSemiring R.rawSemiring + embed-semiringHomomorphism = record + { ⟦_⟧ = embed + ; isSemiringHomomorphism = embed-isSemiringHomomorphism + } + + + ---------------------------------------------------------------------- + -- Trivial completions + + +-absorbing⇒trivial : (∞ : Base) → RightZero ∞ S._+_ → + ∀ x → x ≈ 0# + +-absorbing⇒trivial = + Negatives.absorbing⇒trivial S.+-commutativeMonoid + + +-absorbing⇒1#≈0# : (∞ : Base) → + RightZero ∞ S._+_ → 1# ≈ 0# + +-absorbing⇒1#≈0# ∞ zeroʳ = +-absorbing⇒trivial ∞ zeroʳ 1# + + +------------------------------------------------------------------------ +-- Completion of a ring + +module AlreadyRing {m ℓ : Level} (R : Ring m ℓ) where + + private + module R = Ring R + module Rₚ = RingProperties R + open CSProperties R.+-commutativeSemigroup using (medial) + module Additive = Negatives.AlreadyGroup R.+-abelianGroup + module Additive≅ = IsGroupIsomorphism Additive.self-completion-≅ + + completion : Ring m (m ⊔ ℓ) + completion = ring R.semiring + + module C = Ring completion + + open R using () renaming + ( _≈_ to _≈r_ ; _+_ to _+r_ + ; _*_ to _*r_ ; -_ to -r_ + ; 0# to 0r ; 1# to 1r + ; +-cong to +r-cong ; +-congˡ to +r-congˡ + ) + + open ≈-Reasoning R.setoid + + self-completion-to-self : C.Carrier → R.Carrier + self-completion-to-self = Product.uncurry R._-_ + + to-self-* : ∀ x y → + self-completion-to-self (C._*_ x y) ≈r + self-completion-to-self x *r self-completion-to-self y + to-self-* (a , b) (c , d) = begin + (a *r c +r b *r d) R.- (a *r d +r b *r c) ≡⟨⟩ + (a *r c +r b *r d) +r -r (a *r d +r b *r c) + ≈⟨ +r-congˡ (Rₚ.-‿+-comm (a *r d) (b *r c)) ⟨ + (a *r c +r b *r d) +r (-r (a *r d) +r -r (b *r c)) + ≈⟨ medial (a *r c) (b *r d) + (-r (a *r d)) (-r (b *r c)) ⟩ + (a *r c R.- a *r d) +r (b *r d R.- b *r c) + ≈⟨ +r-congˡ (Rₚ.⁻¹-anti-homo‿- (b *r c) (b *r d)) ⟨ + (a *r c R.- a *r d) R.- (b *r c R.- b *r d) + ≈⟨ +r-cong (Rₚ.x[y-z]≈xy-xz a c d) + (R.-‿cong (Rₚ.x[y-z]≈xy-xz b c d)) ⟨ + a *r (c R.- d) R.- b *r (c R.- d) + ≈⟨ Rₚ.[y-z]x≈yx-zx (c R.- d) a b ⟨ + (a R.- b) *r (c R.- d) ∎ + + to-self-isRingHomomorphism : + IsRingHomomorphism C.rawRing R.rawRing self-completion-to-self + to-self-isRingHomomorphism = record + { isSemiringHomomorphism = record + { isNearSemiringHomomorphism = record + { +-isMonoidHomomorphism = Additive≅.isMonoidHomomorphism + ; *-homo = to-self-* + } + ; 1#-homo = Additive.to-self-embed 1r + } + ; -‿homo = Additive≅.⁻¹-homo + } + + self-completion-≅ : + IsRingIsomorphism C.rawRing R.rawRing self-completion-to-self + self-completion-≅ = record + { isRingMonomorphism = record + { isRingHomomorphism = to-self-isRingHomomorphism + ; injective = Additive≅.injective + } + ; surjective = Additive≅.surjective + } From dd7e33b08f000a574b6e1f06945656851fb3bb94 Mon Sep 17 00:00:00 2001 From: David Silverstone Date: Thu, 6 Aug 2026 08:37:18 -0700 Subject: [PATCH 2/2] [ refactor ] Simplify group and ring completions Reuse algebra properties and remove single-use proof scaffolding. Address review feedback by hiding projections, exposing zero-slack balance, qualifying bundle operations, and aligning absorption with left slack. --- .../Add/Negatives/CommutativeMonoid.agda | 266 ++++++-------- .../Construct/Add/Negatives/Semiring.agda | 334 ++++++++---------- 2 files changed, 252 insertions(+), 348 deletions(-) diff --git a/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda b/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda index b6d80c189b..9abf94144f 100644 --- a/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda +++ b/src/Algebra/Construct/Add/Negatives/CommutativeMonoid.agda @@ -18,6 +18,7 @@ open import Algebra.Morphism.Structures using import Algebra.Properties.AbelianGroup as AbelianGroupProperties import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties +import Algebra.Properties.Monoid as MonoidProperties open import Algebra.Structures using (IsAbelianGroup) open import Data.Product.Base as Product using (∃-syntax; _,_; -,_; <_,_>; proj₁; proj₂; uncurry) @@ -26,8 +27,6 @@ import Function.Consequences.Setoid as Consequences open import Function.Definitions using (Bijective; Congruent) open import Level using (Level; _⊔_) open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Definitions - using (Reflexive; Symmetric; Transitive) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Relation.Binary.Structures using (IsEquivalence) @@ -35,21 +34,19 @@ module _ {m ℓ : Level} (monoid : CommutativeMonoid m ℓ) where private module M = CommutativeMonoid monoid + module Mₚ = MonoidProperties M.monoid open M using (commutativeSemigroup; rawMonoid; setoid) renaming ( Carrier to Base ; _≈_ to _≈ₘ_ ; _∙_ to _+ₘ_ ; ε to 0ₘ ; refl to ≈ₘ-refl ; sym to ≈ₘ-sym - ; ∙-cong to +ₘ-cong + ; comm to +ₘ-comm ; ∙-cong to +ₘ-cong ; ∙-congˡ to +ₘ-congˡ ; ∙-congʳ to +ₘ-congʳ - ; assoc to +ₘ-assoc ; comm to +ₘ-comm ; identityˡ to +ₘ-identityˡ ; identityʳ to +ₘ-identityʳ ) - directProduct : CommutativeMonoid m ℓ - directProduct = DirectProduct.commutativeMonoid monoid monoid - - module M² = CommutativeMonoid directProduct + module M² = CommutativeMonoid + (DirectProduct.commutativeMonoid monoid monoid) open CommSemigroupProperties commutativeSemigroup using (medial) open ≈-Reasoning setoid @@ -60,95 +57,84 @@ module _ {m ℓ : Level} (monoid : CommutativeMonoid m ℓ) where open M² public using (Carrier) renaming (_∙_ to _+_; ε to 0#) - pos : Carrier → Base - pos = proj₁ - - neg : Carrier → Base - neg = proj₂ - ------------------------------------------------------------------------ -- Equality - infix 4 _≈_ + infix 4 _≈₀_ _≈_ + -- The zero-slack balance relation. It need not be transitive unless + -- the original monoid is cancellative. + _≈₀_ : Rel Carrier ℓ + (a , b) ≈₀ (c , d) = a +ₘ d ≈ₘ c +ₘ b + + -- The completion relation stabilizes _≈₀_ by a common left summand. _≈_ : Rel Carrier (m ⊔ ℓ) - x ≈ y = ∃[ slack ] - (pos x +ₘ neg y) +ₘ slack ≈ₘ (pos y +ₘ neg x) +ₘ slack + (a , b) ≈ (c , d) = ∃[ slack ] + slack +ₘ (a +ₘ d) ≈ₘ slack +ₘ (c +ₘ b) open Definitions _≈_ using (Congruent₁; Congruent₂; LeftInverse) private rearrange : ∀ a b c d u v → - ((a +ₘ c) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) ≈ₘ - ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v) + (u +ₘ v) +ₘ ((a +ₘ c) +ₘ (b +ₘ d)) ≈ₘ + (u +ₘ (a +ₘ b)) +ₘ (v +ₘ (c +ₘ d)) rearrange a b c d u v = begin + (u +ₘ v) +ₘ ((a +ₘ c) +ₘ (b +ₘ d)) + ≈⟨ +ₘ-comm _ _ ⟩ ((a +ₘ c) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) ≈⟨ +ₘ-congʳ (medial a c b d) ⟩ ((a +ₘ b) +ₘ (c +ₘ d)) +ₘ (u +ₘ v) ≈⟨ medial (a +ₘ b) (c +ₘ d) u v ⟩ - ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v) ∎ + ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v) + ≈⟨ +ₘ-cong (+ₘ-comm _ _) (+ₘ-comm _ _) ⟩ + (u +ₘ (a +ₘ b)) +ₘ (v +ₘ (c +ₘ d)) ∎ composeˡ : ∀ a b c d u v → - (a +ₘ b) +ₘ ((c +ₘ d) +ₘ (u +ₘ v)) ≈ₘ - ((a +ₘ d) +ₘ u) +ₘ ((c +ₘ b) +ₘ v) + ((u +ₘ v) +ₘ (c +ₘ d)) +ₘ (a +ₘ b) ≈ₘ + (u +ₘ (a +ₘ d)) +ₘ (v +ₘ (c +ₘ b)) composeˡ a b c d u v = begin - (a +ₘ b) +ₘ ((c +ₘ d) +ₘ (u +ₘ v)) - ≈⟨ +ₘ-assoc (a +ₘ b) (c +ₘ d) (u +ₘ v) ⟨ - ((a +ₘ b) +ₘ (c +ₘ d)) +ₘ (u +ₘ v) - ≈⟨ +ₘ-congʳ (medial a b c d) ⟩ - ((a +ₘ c) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) - ≈⟨ +ₘ-congʳ (+ₘ-congˡ (+ₘ-comm b d)) ⟩ - ((a +ₘ c) +ₘ (d +ₘ b)) +ₘ (u +ₘ v) + ((u +ₘ v) +ₘ (c +ₘ d)) +ₘ (a +ₘ b) + ≈⟨ M.assoc (u +ₘ v) (c +ₘ d) (a +ₘ b) ⟩ + (u +ₘ v) +ₘ ((c +ₘ d) +ₘ (a +ₘ b)) + ≈⟨ +ₘ-congˡ (medial c d a b) ⟩ + (u +ₘ v) +ₘ ((c +ₘ a) +ₘ (d +ₘ b)) + ≈⟨ +ₘ-congˡ (+ₘ-congʳ (+ₘ-comm c a)) ⟩ + (u +ₘ v) +ₘ ((a +ₘ c) +ₘ (d +ₘ b)) ≈⟨ rearrange a d c b u v ⟩ - ((a +ₘ d) +ₘ u) +ₘ ((c +ₘ b) +ₘ v) ∎ + (u +ₘ (a +ₘ d)) +ₘ (v +ₘ (c +ₘ b)) ∎ - composeʳ : ∀ a b c d u v → - ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v) ≈ₘ - (c +ₘ b) +ₘ ((a +ₘ d) +ₘ (u +ₘ v)) - composeʳ a b c d u v = begin - ((a +ₘ b) +ₘ u) +ₘ ((c +ₘ d) +ₘ v) - ≈⟨ rearrange a b c d u v ⟨ - ((a +ₘ c) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) - ≈⟨ +ₘ-congʳ (+ₘ-congˡ (+ₘ-comm b d)) ⟩ - ((a +ₘ c) +ₘ (d +ₘ b)) +ₘ (u +ₘ v) - ≈⟨ +ₘ-congʳ (medial a c d b) ⟩ - ((a +ₘ d) +ₘ (c +ₘ b)) +ₘ (u +ₘ v) - ≈⟨ +ₘ-congʳ (+ₘ-comm (a +ₘ d) (c +ₘ b)) ⟩ - ((c +ₘ b) +ₘ (a +ₘ d)) +ₘ (u +ₘ v) - ≈⟨ +ₘ-assoc (c +ₘ b) (a +ₘ d) (u +ₘ v) ⟩ - (c +ₘ b) +ₘ ((a +ₘ d) +ₘ (u +ₘ v)) ∎ - - ≈-from-parts : ∀ {x y} → - pos x ≈ₘ pos y → neg x ≈ₘ neg y → x ≈ y - ≈-from-parts x⁺≈y⁺ x⁻≈y⁻ = - 0ₘ , +ₘ-congʳ (+ₘ-cong x⁺≈y⁺ (≈ₘ-sym x⁻≈y⁻)) + ≈₀⇒≈ : ∀ {x y} → x ≈₀ y → x ≈ y + ≈₀⇒≈ eq = 0ₘ , +ₘ-congˡ eq + + ≈-from-parts : ∀ {a b c d} → a ≈ₘ c → b ≈ₘ d → (a , b) ≈ (c , d) + ≈-from-parts x⁺≈y⁺ x⁻≈y⁻ = ≈₀⇒≈ (+ₘ-cong x⁺≈y⁺ (≈ₘ-sym x⁻≈y⁻)) private pointwise⇒≈ : ∀ {x y} → M²._≈_ x y → x ≈ y pointwise⇒≈ = uncurry ≈-from-parts - ≈-refl : Reflexive _≈_ - ≈-refl = pointwise⇒≈ M².refl - - ≈-trans : Transitive _≈_ - ≈-trans {a , b} {c , d} {e , f} = - Product.zip (λ u v → (c +ₘ d) +ₘ (u +ₘ v)) - λ {u} {v} eq₁ eq₂ → begin - (a +ₘ f) +ₘ ((c +ₘ d) +ₘ (u +ₘ v)) - ≈⟨ composeˡ a f c d u v ⟩ - ((a +ₘ d) +ₘ u) +ₘ ((c +ₘ f) +ₘ v) - ≈⟨ +ₘ-cong eq₁ eq₂ ⟩ - ((c +ₘ b) +ₘ u) +ₘ ((e +ₘ d) +ₘ v) - ≈⟨ composeʳ c b e d u v ⟩ - (e +ₘ b) +ₘ ((c +ₘ d) +ₘ (u +ₘ v)) ∎ - ≈-isEquivalence : IsEquivalence _≈_ ≈-isEquivalence = record - { refl = ≈-refl + { refl = pointwise⇒≈ M².refl ; sym = Product.map₂ ≈ₘ-sym - ; trans = ≈-trans + ; trans = λ { {a , b} {c , d} {e , f} → + Product.zip (λ u v → (u +ₘ v) +ₘ (c +ₘ d)) + λ {u} {v} eq₁ eq₂ → begin + ((u +ₘ v) +ₘ (c +ₘ d)) +ₘ (a +ₘ f) + ≈⟨ composeˡ a f c d u v ⟩ + (u +ₘ (a +ₘ d)) +ₘ (v +ₘ (c +ₘ f)) + ≈⟨ +ₘ-cong eq₁ eq₂ ⟩ + (u +ₘ (c +ₘ b)) +ₘ (v +ₘ (e +ₘ d)) + ≈⟨ +ₘ-comm _ _ ⟩ + (v +ₘ (e +ₘ d)) +ₘ (u +ₘ (c +ₘ b)) + ≈⟨ composeˡ e b c d v u ⟨ + ((v +ₘ u) +ₘ (c +ₘ d)) +ₘ (e +ₘ b) + ≈⟨ +ₘ-congʳ (+ₘ-congʳ (+ₘ-comm v u)) ⟩ + ((u +ₘ v) +ₘ (c +ₘ d)) +ₘ (e +ₘ b) ∎ } } + private module ≈ = IsEquivalence ≈-isEquivalence + ------------------------------------------------------------------------ -- Operations @@ -160,27 +146,26 @@ module _ {m ℓ : Level} (monoid : CommutativeMonoid m ℓ) where +-cong : Congruent₂ _+_ +-cong {a , b} {a′ , b′} {c , d} {c′ , d′} = Product.zip _+ₘ_ λ {u} {v} eq₁ eq₂ → begin - ((a +ₘ c) +ₘ (b′ +ₘ d′)) +ₘ (u +ₘ v) - ≈⟨ rearrange a b′ c d′ u v ⟩ - ((a +ₘ b′) +ₘ u) +ₘ ((c +ₘ d′) +ₘ v) - ≈⟨ +ₘ-cong eq₁ eq₂ ⟩ - ((a′ +ₘ b) +ₘ u) +ₘ ((c′ +ₘ d) +ₘ v) - ≈⟨ rearrange a′ b c′ d u v ⟨ - ((a′ +ₘ c′) +ₘ (b +ₘ d)) +ₘ (u +ₘ v) ∎ + (u +ₘ v) +ₘ ((a +ₘ c) +ₘ (b′ +ₘ d′)) ≈⟨ rearrange a b′ c d′ u v ⟩ + (u +ₘ (a +ₘ b′)) +ₘ (v +ₘ (c +ₘ d′)) ≈⟨ +ₘ-cong eq₁ eq₂ ⟩ + (u +ₘ (a′ +ₘ b)) +ₘ (v +ₘ (c′ +ₘ d)) ≈⟨ rearrange a′ b c′ d u v ⟨ + (u +ₘ v) +ₘ ((a′ +ₘ c′) +ₘ (b +ₘ d)) ∎ -‿cong : Congruent₁ -_ -‿cong {a , b} {c , d} = Product.map₂ λ {u} eq → begin - (b +ₘ c) +ₘ u ≈⟨ +ₘ-congʳ (+ₘ-comm b c) ⟩ - (c +ₘ b) +ₘ u ≈⟨ eq ⟨ - (a +ₘ d) +ₘ u ≈⟨ +ₘ-congʳ (+ₘ-comm a d) ⟩ - (d +ₘ a) +ₘ u ∎ + u +ₘ (b +ₘ c) ≈⟨ +ₘ-congˡ (+ₘ-comm b c) ⟩ + u +ₘ (c +ₘ b) ≈⟨ eq ⟨ + u +ₘ (a +ₘ d) ≈⟨ +ₘ-congˡ (+ₘ-comm a d) ⟩ + u +ₘ (d +ₘ a) ∎ +-inverseˡ : LeftInverse 0# -_ _+_ +-inverseˡ (a , b) = -, (begin - ((b +ₘ a) +ₘ 0ₘ) +ₘ 0ₘ ≈⟨ +ₘ-identityʳ _ ⟩ - (b +ₘ a) +ₘ 0ₘ ≈⟨ +ₘ-congʳ (+ₘ-comm b a) ⟩ - (a +ₘ b) +ₘ 0ₘ ≈⟨ +ₘ-congʳ (+ₘ-identityˡ _) ⟨ - (0ₘ +ₘ (a +ₘ b)) +ₘ 0ₘ ∎) + 0ₘ +ₘ ((b +ₘ a) +ₘ 0ₘ) ≈⟨ +ₘ-identityˡ _ ⟩ + (b +ₘ a) +ₘ 0ₘ ≈⟨ +ₘ-identityʳ _ ⟩ + b +ₘ a ≈⟨ +ₘ-comm b a ⟩ + a +ₘ b ≈⟨ +ₘ-identityˡ _ ⟨ + 0ₘ +ₘ (a +ₘ b) ≈⟨ +ₘ-congˡ (+ₘ-identityˡ _) ⟨ + 0ₘ +ₘ (0ₘ +ₘ (a +ₘ b)) ∎) ------------------------------------------------------------------------ -- Bundle @@ -199,22 +184,14 @@ module _ {m ℓ : Level} (monoid : CommutativeMonoid m ℓ) where ; identity = Product.map (pointwise⇒≈ ∘_) (pointwise⇒≈ ∘_) M².identity } - ; inverse = +-inverseˡ , λ x → - ≈-trans (pointwise⇒≈ (M².comm x (- x))) (+-inverseˡ x) + ; inverse = +-inverseˡ , +-inverseˡ ∘ -_ ; ⁻¹-cong = -‿cong } ; comm = pointwise⇒≈ ∘₂ M².comm } abelianGroup : AbelianGroup m (m ⊔ ℓ) - abelianGroup = record - { Carrier = Carrier - ; _≈_ = _≈_ - ; _∙_ = _+_ - ; ε = 0# - ; _⁻¹ = -_ - ; isAbelianGroup = completion-is-abelian-group - } + abelianGroup = record { isAbelianGroup = completion-is-abelian-group } open AbelianGroup abelianGroup using () renaming (rawMonoid to rawMonoid#) @@ -229,8 +206,7 @@ module _ {m ℓ : Level} (monoid : CommutativeMonoid m ℓ) where embed-cong x≈y = ≈-from-parts x≈y ≈ₘ-refl embed-∙ : ∀ x y → embed (x +ₘ y) ≈ embed x + embed y - embed-∙ x y = - ≈-from-parts ≈ₘ-refl (≈ₘ-sym (+ₘ-identityˡ 0ₘ)) + embed-∙ x y = ≈-from-parts ≈ₘ-refl (Mₚ.introˡ ≈ₘ-refl 0ₘ) embed-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid rawMonoid# embed @@ -239,33 +215,31 @@ module _ {m ℓ : Level} (monoid : CommutativeMonoid m ℓ) where { isRelHomomorphism = record { cong = embed-cong } ; ∙-homo = embed-∙ } - ; ε-homo = ≈-refl + ; ε-homo = ≈.refl } embed-monoidHomomorphism : MonoidHomomorphism rawMonoid rawMonoid# embed-monoidHomomorphism = record - { ⟦_⟧ = embed - ; isMonoidHomomorphism = embed-isMonoidHomomorphism - } + { isMonoidHomomorphism = embed-isMonoidHomomorphism } - decompose : ∀ x → x ≈ embed (pos x) + - embed (neg x) + decompose : ∀ x → x ≈ embed (proj₁ x) + - embed (proj₂ x) decompose (a , b) = - ≈-from-parts (≈ₘ-sym (+ₘ-identityʳ a)) - (≈ₘ-sym (+ₘ-identityˡ b)) + ≈-from-parts (Mₚ.introʳ ≈ₘ-refl a) + (Mₚ.introˡ ≈ₘ-refl b) ------------------------------------------------------------------------ -- Trivial completions - open Definitions _≈ₘ_ using (RightZero) + open Definitions _≈ₘ_ using () renaming (LeftZero to LeftAbsorbing) - absorbing⇒trivial : (∞ : Base) → RightZero ∞ _+ₘ_ → + absorbing⇒trivial : (∞ : Base) → LeftAbsorbing ∞ _+ₘ_ → ∀ x → x ≈ 0# - absorbing⇒trivial ∞ zeroʳ (a , b) = -, (begin - (a +ₘ 0ₘ) +ₘ ∞ ≈⟨ zeroʳ (a +ₘ 0ₘ) ⟩ - ∞ ≈⟨ zeroʳ (0ₘ +ₘ b) ⟨ - (0ₘ +ₘ b) +ₘ ∞ ∎) + absorbing⇒trivial ∞ absorbˡ (a , b) = -, (begin + ∞ +ₘ (a +ₘ 0ₘ) ≈⟨ absorbˡ (a +ₘ 0ₘ) ⟩ + ∞ ≈⟨ absorbˡ (0ₘ +ₘ b) ⟨ + ∞ +ₘ (0ₘ +ₘ b) ∎) ------------------------------------------------------------------------ @@ -276,71 +250,49 @@ module AlreadyGroup {m ℓ : Level} (G : AbelianGroup m ℓ) where private module G = AbelianGroup G module Gₚ = AbelianGroupProperties G + module Gₘ = MonoidProperties G.monoid open CommSemigroupProperties G.commutativeSemigroup using (medial) + open Gₘ using (cancelᶜ; elimʳ; introʳ) open Gₚ using - (//-rightDividesˡ; ∙-cancelʳ; ε⁻¹≈ε - ; ⁻¹-anti-homo‿-; ⁻¹-∙-comm) + (∙-cancelˡ; ∙-cancelʳ; ε⁻¹≈ε; ⁻¹-anti-homo‿-; ⁻¹-∙-comm) - completion : AbelianGroup m (m ⊔ ℓ) - completion = abelianGroup G.commutativeMonoid - - module C = AbelianGroup completion + module C = AbelianGroup (abelianGroup G.commutativeMonoid) open Consequences C.setoid G.setoid using (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ ; strictlyInverseʳ⇒inverseʳ) - open G using () renaming - ( _≈_ to _≈g_ ; _∙_ to _+g_ - ; ε to 0g ; _⁻¹ to -g_ - ; sym to ≈g-sym - ; ∙-congˡ to +g-congˡ ; ∙-congʳ to +g-congʳ - ; assoc to +g-assoc ; comm to +g-comm - ; identityʳ to +g-identityʳ - ) - open ≈-Reasoning G.setoid - reduce-difference : ∀ a b c → - (a G.- b) +g (b +g c) ≈g a +g c - reduce-difference a b c = begin - (a G.- b) +g (b +g c) ≈⟨ +g-assoc _ _ _ ⟨ - ((a G.- b) +g b) +g c ≈⟨ +g-congʳ (//-rightDividesˡ _ _) ⟩ - a +g c ∎ - self-completion-to-self : C.Carrier → G.Carrier self-completion-to-self = Product.uncurry G._-_ to-self-cong : Congruent C._≈_ G._≈_ self-completion-to-self to-self-cong {a , b} {c , d} = Product.uncurry λ slack eq → - ∙-cancelʳ (b +g d) _ _ (begin - (a G.- b) +g (b +g d) ≈⟨ reduce-difference a b d ⟩ - a +g d ≈⟨ ∙-cancelʳ slack _ _ eq ⟩ - c +g b ≈⟨ reduce-difference c d b ⟨ - (c G.- d) +g (d +g b) ≈⟨ +g-congˡ (+g-comm b d) ⟨ - (c G.- d) +g (b +g d) ∎) + ∙-cancelʳ (b G.∙ d) _ _ (begin + (a G.- b) G.∙ (b G.∙ d) ≈⟨ cancelᶜ (G.inverseˡ b) a d ⟩ + a G.∙ d ≈⟨ ∙-cancelˡ slack _ _ eq ⟩ + c G.∙ b ≈⟨ cancelᶜ (G.inverseˡ d) c b ⟨ + (c G.- d) G.∙ (d G.∙ b) ≈⟨ G.∙-congˡ (G.comm b d) ⟨ + (c G.- d) G.∙ (b G.∙ d) ∎) to-self-∙ : ∀ x y → - self-completion-to-self (C._∙_ x y) ≈g - self-completion-to-self x +g self-completion-to-self y + self-completion-to-self (C._∙_ x y) G.≈ + self-completion-to-self x G.∙ self-completion-to-self y to-self-∙ (a , b) (c , d) = begin - (a +g c) G.- (b +g d) ≡⟨⟩ - (a +g c) +g -g (b +g d) ≈⟨ +g-congˡ (⁻¹-∙-comm _ _) ⟨ - (a +g c) +g (-g b +g -g d) ≈⟨ medial a c (-g b) (-g d) ⟩ - (a +g -g b) +g (c +g -g d) ≡⟨⟩ - (a G.- b) +g (c G.- d) ∎ + (a G.∙ c) G.- (b G.∙ d) ≡⟨⟩ + (a G.∙ c) G.∙ (b G.∙ d) G.⁻¹ ≈⟨ G.∙-congˡ (⁻¹-∙-comm _ _) ⟨ + (a G.∙ c) G.∙ (b G.⁻¹ G.∙ d G.⁻¹) ≈⟨ medial a c (b G.⁻¹) (d G.⁻¹) ⟩ + (a G.∙ b G.⁻¹) G.∙ (c G.∙ d G.⁻¹) ≡⟨⟩ + (a G.- b) G.∙ (c G.- d) ∎ to-self-embed : ∀ x → - self-completion-to-self (embed G.commutativeMonoid x) ≈g x - to-self-embed x = begin - x G.- 0g ≡⟨⟩ - x +g -g 0g ≈⟨ +g-congˡ ε⁻¹≈ε ⟩ - x +g 0g ≈⟨ +g-identityʳ x ⟩ - x ∎ + self-completion-to-self (embed G.commutativeMonoid x) G.≈ x + to-self-embed x = elimʳ ε⁻¹≈ε x to-self-⁻¹ : ∀ x → - self-completion-to-self (C._⁻¹ x) ≈g - -g self-completion-to-self x - to-self-⁻¹ (a , b) = ≈g-sym (⁻¹-anti-homo‿- a b) + self-completion-to-self (C._⁻¹ x) G.≈ + self-completion-to-self x G.⁻¹ + to-self-⁻¹ (a , b) = G.sym (⁻¹-anti-homo‿- a b) to-self-isGroupHomomorphism : IsGroupHomomorphism C.rawGroup G.rawGroup self-completion-to-self @@ -350,7 +302,7 @@ module AlreadyGroup {m ℓ : Level} (G : AbelianGroup m ℓ) where { isRelHomomorphism = record { cong = to-self-cong } ; ∙-homo = to-self-∙ } - ; ε-homo = to-self-embed 0g + ; ε-homo = to-self-embed G.ε } ; ⁻¹-homo = to-self-⁻¹ } @@ -358,11 +310,11 @@ module AlreadyGroup {m ℓ : Level} (G : AbelianGroup m ℓ) where embed-to-self : ∀ x → embed G.commutativeMonoid (self-completion-to-self x) C.≈ x embed-to-self (a , b) = -, (begin - ((a G.- b) +g b) +g 0g ≈⟨ +g-identityʳ _ ⟩ - (a G.- b) +g b ≈⟨ //-rightDividesˡ b a ⟩ - a ≈⟨ +g-identityʳ a ⟨ - a +g 0g ≈⟨ +g-identityʳ _ ⟨ - (a +g 0g) +g 0g ∎) + G.ε G.∙ ((a G.- b) G.∙ b) ≈⟨ G.identityˡ _ ⟩ + (a G.- b) G.∙ b ≈⟨ Gₘ.cancelʳ (G.inverseˡ b) a ⟩ + a ≈⟨ introʳ G.refl _ ⟩ + a G.∙ G.ε ≈⟨ G.identityˡ _ ⟨ + G.ε G.∙ (a G.∙ G.ε) ∎) to-self-bijective : Bijective C._≈_ G._≈_ self-completion-to-self diff --git a/src/Algebra/Construct/Add/Negatives/Semiring.agda b/src/Algebra/Construct/Add/Negatives/Semiring.agda index 3c64be412a..cfb3e512b9 100644 --- a/src/Algebra/Construct/Add/Negatives/Semiring.agda +++ b/src/Algebra/Construct/Add/Negatives/Semiring.agda @@ -17,20 +17,19 @@ open import Algebra.Morphism.Structures using (IsGroupIsomorphism; IsRingHomomorphism; IsRingIsomorphism ; IsSemiringHomomorphism) import Algebra.Properties.CommutativeSemigroup as CSProperties +import Algebra.Properties.Monoid as MonoidProperties import Algebra.Properties.Ring as RingProperties open import Algebra.Structures using (IsRing) -open import Data.Product.Base as Product - using (_,_; <_,_>) -open import Function.Base using (_∘_; _∘₂_) +open import Data.Product.Base as Product using (_,_; proj₁; proj₂) open import Function.Definitions using (Congruent) open import Level using (Level; _⊔_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Relation.Binary.Structures using (IsEquivalence) module _ {m ℓ : Level} (semiring : Semiring m ℓ) where private module S = Semiring semiring + module Sₘ = MonoidProperties S.+-monoid open CSProperties S.+-commutativeSemigroup using (medial) open S using () renaming @@ -43,52 +42,30 @@ module _ {m ℓ : Level} (semiring : Semiring m ℓ) where -- Additive completion private - +Group : AbelianGroup m (m ⊔ ℓ) - +Group = Negatives.abelianGroup S.+-commutativeMonoid - - module Additive = AbelianGroup +Group + -- Ring completion reuses the commutative-monoid completion verbatim + -- for its additive structure and only extends multiplication below. + module Additive = AbelianGroup + (Negatives.abelianGroup S.+-commutativeMonoid) open Additive public using (Carrier) renaming (_≈_ to _≈_; _∙_ to _+_; ε to 0#; _⁻¹ to -_) open Additive using () renaming (∙-cong to +-cong; ⁻¹-cong to -‿cong) - pos neg : Carrier → Base - pos = Negatives.pos S.+-commutativeMonoid - neg = Negatives.neg S.+-commutativeMonoid - private + pos neg : Carrier → Base + pos = proj₁ + neg = proj₂ + ≈-from-parts : ∀ {x y} → pos x S.≈ pos y → neg x S.≈ neg y → x ≈ y ≈-from-parts = Negatives.≈-from-parts S.+-commutativeMonoid - module ≈ = IsEquivalence Additive.isEquivalence - variable x y z : Carrier - a b c d : Base - - infix 4 _≈[_]_ - _≈[_]_ : Carrier → Base → Carrier → Set ℓ - x ≈[ slack ] y = - (pos x +ₛ neg y) +ₛ slack ≈ₛ (pos y +ₛ neg x) +ₛ slack + a : Base - open Definitions _≈_ using - (Associative; Congruent₂; LeftCongruent; LeftIdentity - ; RightCongruent; RightIdentity - ; _DistributesOverˡ_; _DistributesOverʳ_) - open Definitions (_≈ₛ_) using (Commutative; RightZero) - - ---------------------------------------------------------------------- - -- Addition permutations - - private - swap-middle : ∀ p q r s → - (p +ₛ q) +ₛ (r +ₛ s) ≈ₛ - (p +ₛ r) +ₛ (s +ₛ q) - swap-middle p q r s = S.trans - (medial p q r s) - (S.+-congˡ (S.+-comm q s)) + open Definitions _≈_ using (Congruent₂) ---------------------------------------------------------------------- -- Multiplication @@ -97,10 +74,10 @@ module _ {m ℓ : Level} (semiring : Semiring m ℓ) where private prod⁺ : Carrier → Carrier → Base - prod⁺ = Product.uncurry′ S._+_ ∘₂ Product.zip′ S._*_ S._*_ + prod⁺ (a , b) (c , d) = a *ₛ c +ₛ b *ₛ d _*_ : Carrier → Carrier → Carrier - _*_ x = < prod⁺ x , prod⁺ x ∘ -_ > + x * y = prod⁺ x y , prod⁺ x (- y) 1# : Carrier 1# = 1ₛ , 0ₛ @@ -112,47 +89,42 @@ module _ {m ℓ : Level} (semiring : Semiring m ℓ) where scaleʳ : Carrier → Base → Carrier scaleʳ x a = Product.map (_*ₛ a) (_*ₛ a) x + -- Mapping a completion equality changes its witness from `slack` to + -- `f slack`, so the witness must be exposed here. map-cong : ∀ f → Congruent _≈ₛ_ _≈ₛ_ f → - (∀ a b c → f ((a +ₛ b) +ₛ c) ≈ₛ - (f a +ₛ f b) +ₛ f c) → + (∀ a b → f (a +ₛ b) ≈ₛ f a +ₛ f b) → Congruent _≈_ _≈_ (Product.map f f) - map-cong f cong distrib = Product.map f λ {slack} eq → begin - (f _ +ₛ f _) +ₛ f slack ≈⟨ distrib _ _ slack ⟨ - f ((_ +ₛ _) +ₛ slack) ≈⟨ cong eq ⟩ - f ((_ +ₛ _) +ₛ slack) ≈⟨ distrib _ _ slack ⟩ - (f _ +ₛ f _) +ₛ f slack ∎ + map-cong f cong homo = Product.map f λ {slack} eq → begin + f slack +ₛ (f _ +ₛ f _) ≈⟨ S.+-congˡ (homo _ _) ⟨ + f slack +ₛ f (_ +ₛ _) ≈⟨ homo slack (_ +ₛ _) ⟨ + f (slack +ₛ (_ +ₛ _)) ≈⟨ cong eq ⟩ + f (slack +ₛ (_ +ₛ _)) ≈⟨ homo slack (_ +ₛ _) ⟩ + f slack +ₛ f (_ +ₛ _) ≈⟨ S.+-congˡ (homo _ _) ⟩ + f slack +ₛ (f _ +ₛ f _) ∎ where open ≈-Reasoning S.setoid scale-congˡ : Congruent _≈_ _≈_ (scaleˡ a) - scale-congˡ {a} = map-cong (a *ₛ_) S.*-congˡ λ x y z → - S.trans (S.distribˡ _ _ _) (S.+-congʳ (S.distribˡ _ _ _)) + scale-congˡ {a} = map-cong (a *ₛ_) S.*-congˡ (S.distribˡ a) scale-congʳ : Congruent _≈_ _≈_ (λ x → scaleʳ x a) - scale-congʳ {a} = map-cong (_*ₛ a) S.*-congʳ λ x y z → - S.trans (S.distribʳ _ _ _) (S.+-congʳ (S.distribʳ _ _ _)) + scale-congʳ {a} = map-cong (_*ₛ a) S.*-congʳ (S.distribʳ a) *-as-scalesʳ : x * y ≈ scaleʳ x (pos y) + - scaleʳ x (neg y) *-as-scalesʳ {(a , b)} {(c , d)} = ≈-from-parts S.refl (S.+-comm (a *ₛ d) (b *ₛ c)) - *-congʳ : RightCongruent _*_ - *-congʳ {y} {x} {x′} x≈x′ = begin - x * y - ≈⟨ *-as-scalesʳ ⟩ - scaleʳ x (pos y) + - scaleʳ x (neg y) - ≈⟨ +-cong (scale-congʳ x≈x′) - (-‿cong (scale-congʳ x≈x′)) ⟩ - scaleʳ x′ (pos y) + - scaleʳ x′ (neg y) - ≈⟨ *-as-scalesʳ ⟨ - x′ * y ∎ - where open ≈-Reasoning Additive.setoid - - *-congˡ : LeftCongruent _*_ - *-congˡ {x} y≈y′ = - +-cong (scale-congˡ y≈y′) (-‿cong (scale-congˡ y≈y′)) - - *-cong : Congruent₂ _*_ - *-cong x≈ y≈ = ≈.trans (*-congʳ x≈) (*-congˡ y≈) + *-cong : Congruent₂ _*_ + *-cong {a , b} {a′ , b′} {y} {y′} x≈x′ y≈y′ = begin + (a , b) * y + ≈⟨ *-as-scalesʳ ⟩ + scaleʳ (a , b) (pos y) + - scaleʳ (a , b) (neg y) + ≈⟨ +-cong (scale-congʳ x≈x′) (-‿cong (scale-congʳ x≈x′)) ⟩ + scaleʳ (a′ , b′) (pos y) + - scaleʳ (a′ , b′) (neg y) + ≈⟨ *-as-scalesʳ ⟨ + (a′ , b′) * y + ≈⟨ +-cong (scale-congˡ y≈y′) (-‿cong (scale-congˡ y≈y′)) ⟩ + (a′ , b′) * y′ ∎ + where open ≈-Reasoning Additive.setoid open ≈-Reasoning S.setoid @@ -162,113 +134,107 @@ module _ {m ℓ : Level} (semiring : Semiring m ℓ) where private distrib⁺ˡ : ∀ x y z → prod⁺ x (y + z) ≈ₛ prod⁺ x y +ₛ prod⁺ x z - distrib⁺ˡ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = - S.trans - (S.+-cong (S.distribˡ _ _ _) (S.distribˡ _ _ _)) - (medial (x⁺ *ₛ y⁺) (x⁺ *ₛ z⁺) - (x⁻ *ₛ y⁻) (x⁻ *ₛ z⁻)) + distrib⁺ˡ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = begin + x⁺ *ₛ (y⁺ +ₛ z⁺) +ₛ x⁻ *ₛ (y⁻ +ₛ z⁻) + ≈⟨ S.+-cong (S.distribˡ _ _ _) (S.distribˡ _ _ _) ⟩ + (x⁺ *ₛ y⁺ +ₛ x⁺ *ₛ z⁺) +ₛ (x⁻ *ₛ y⁻ +ₛ x⁻ *ₛ z⁻) + ≈⟨ medial _ _ _ _ ⟩ + (x⁺ *ₛ y⁺ +ₛ x⁻ *ₛ y⁻) +ₛ (x⁺ *ₛ z⁺ +ₛ x⁻ *ₛ z⁻) ∎ distrib⁺ʳ : ∀ x y z → prod⁺ (x + y) z ≈ₛ prod⁺ x z +ₛ prod⁺ y z - distrib⁺ʳ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = - S.trans - (S.+-cong (S.distribʳ _ _ _) (S.distribʳ _ _ _)) - (medial (x⁺ *ₛ z⁺) (y⁺ *ₛ z⁺) - (x⁻ *ₛ z⁻) (y⁻ *ₛ z⁻)) + distrib⁺ʳ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = begin + (x⁺ +ₛ y⁺) *ₛ z⁺ +ₛ (x⁻ +ₛ y⁻) *ₛ z⁻ + ≈⟨ S.+-cong (S.distribʳ _ _ _) (S.distribʳ _ _ _) ⟩ + (x⁺ *ₛ z⁺ +ₛ y⁺ *ₛ z⁺) +ₛ (x⁻ *ₛ z⁻ +ₛ y⁻ *ₛ z⁻) + ≈⟨ medial _ _ _ _ ⟩ + (x⁺ *ₛ z⁺ +ₛ x⁻ *ₛ z⁻) +ₛ (y⁺ *ₛ z⁺ +ₛ y⁻ *ₛ z⁻) ∎ + + scale-prod : ∀ a x y → + prod⁺ (scaleˡ a x) y ≈ₛ a *ₛ prod⁺ x y + scale-prod a (b , c) (d , e) = begin + (a *ₛ b) *ₛ d +ₛ (a *ₛ c) *ₛ e + ≈⟨ S.+-cong (S.*-assoc _ _ _) (S.*-assoc _ _ _) ⟩ + a *ₛ (b *ₛ d) +ₛ a *ₛ (c *ₛ e) + ≈⟨ S.distribˡ _ _ _ ⟨ + a *ₛ (b *ₛ d +ₛ c *ₛ e) ∎ + + neg-scale-prod : ∀ a x y → + prod⁺ (- scaleˡ a x) y ≈ₛ a *ₛ prod⁺ x (- y) + neg-scale-prod a (b , c) (d , e) = begin + (a *ₛ c) *ₛ d +ₛ (a *ₛ b) *ₛ e ≈⟨ scale-prod a (c , b) (d , e) ⟩ + a *ₛ (c *ₛ d +ₛ b *ₛ e) ≈⟨ S.*-congˡ (S.+-comm _ _) ⟩ + a *ₛ (b *ₛ e +ₛ c *ₛ d) ∎ assoc⁺ : ∀ x y z → prod⁺ (x * y) z ≈ₛ prod⁺ x (y * z) - assoc⁺ (x⁺ , x⁻) (y⁺ , y⁻) (z⁺ , z⁻) = begin - (((x⁺ *ₛ y⁺) +ₛ (x⁻ *ₛ y⁻)) *ₛ z⁺) +ₛ - (((x⁺ *ₛ y⁻) +ₛ (x⁻ *ₛ y⁺)) *ₛ z⁻) - ≈⟨ S.+-cong (S.distribʳ _ _ _) (S.distribʳ _ _ _) ⟩ - (((x⁺ *ₛ y⁺) *ₛ z⁺) +ₛ ((x⁻ *ₛ y⁻) *ₛ z⁺)) - +ₛ (((x⁺ *ₛ y⁻) *ₛ z⁻) - +ₛ ((x⁻ *ₛ y⁺) *ₛ z⁻)) - ≈⟨ S.+-cong (S.+-cong (S.*-assoc _ _ _) (S.*-assoc _ _ _)) - (S.+-cong (S.*-assoc _ _ _) (S.*-assoc _ _ _)) ⟩ - (x⁺ *ₛ (y⁺ *ₛ z⁺)) +ₛ (x⁻ *ₛ (y⁻ *ₛ z⁺)) - +ₛ ((x⁺ *ₛ (y⁻ *ₛ z⁻)) - +ₛ (x⁻ *ₛ (y⁺ *ₛ z⁻))) - ≈⟨ swap-middle _ _ _ _ ⟩ - (x⁺ *ₛ (y⁺ *ₛ z⁺)) +ₛ (x⁺ *ₛ (y⁻ *ₛ z⁻)) - +ₛ ((x⁻ *ₛ (y⁺ *ₛ z⁻)) - +ₛ (x⁻ *ₛ (y⁻ *ₛ z⁺))) - ≈⟨ S.+-cong (S.distribˡ _ _ _) (S.distribˡ _ _ _) ⟨ - (x⁺ *ₛ ((y⁺ *ₛ z⁺) +ₛ (y⁻ *ₛ z⁻))) +ₛ - (x⁻ *ₛ ((y⁺ *ₛ z⁻) +ₛ (y⁻ *ₛ z⁺))) ∎ - - *-assoc : Associative _*_ - *-assoc x y z = ≈-from-parts - (assoc⁺ x y z) (assoc⁺ x y (- z)) - - *-identityˡ : LeftIdentity 1# _*_ - *-identityˡ (x⁺ , x⁻) = ≈-from-parts - (S.trans (S.+-cong (S.*-identityˡ _) (S.zeroˡ _)) - (S.+-identityʳ x⁺)) - (S.trans (S.+-cong (S.*-identityˡ _) (S.zeroˡ _)) - (S.+-identityʳ x⁻)) - - *-identityʳ : RightIdentity 1# _*_ - *-identityʳ (x⁺ , x⁻) = ≈-from-parts - (S.trans (S.+-cong (S.*-identityʳ _) (S.zeroʳ _)) - (S.+-identityʳ x⁺)) - (S.trans (S.+-comm (x⁺ *ₛ 0ₛ) (x⁻ *ₛ 1ₛ)) - (S.trans (S.+-cong (S.*-identityʳ _) (S.zeroʳ _)) - (S.+-identityʳ x⁻))) - - distribˡ : _*_ DistributesOverˡ _+_ - distribˡ x y z = ≈-from-parts - (distrib⁺ˡ x y z) (distrib⁺ˡ x (- y) (- z)) - - distribʳ : _*_ DistributesOverʳ _+_ - distribʳ x y z = ≈-from-parts - (distrib⁺ʳ y z x) (distrib⁺ʳ y z (- x)) + assoc⁺ (a , b) y z = begin + prod⁺ ((a , b) * y) z + ≡⟨⟩ + prod⁺ (scaleˡ a y + - scaleˡ b y) z + ≈⟨ distrib⁺ʳ (scaleˡ a y) (- scaleˡ b y) z ⟩ + prod⁺ (scaleˡ a y) z +ₛ prod⁺ (- scaleˡ b y) z + ≈⟨ S.+-cong (scale-prod a y z) (neg-scale-prod b y z) ⟩ + a *ₛ prod⁺ y z +ₛ b *ₛ prod⁺ y (- z) + ≡⟨⟩ + prod⁺ (a , b) (y * z) ∎ ---------------------------------------------------------------------- -- Bundle completion-is-ring : IsRing _≈_ _+_ _*_ -_ 0# 1# completion-is-ring = record - { +-isAbelianGroup = AbelianGroup.isAbelianGroup +Group + { +-isAbelianGroup = Additive.isAbelianGroup ; *-cong = *-cong - ; *-assoc = *-assoc - ; *-identity = *-identityˡ , *-identityʳ - ; distrib = distribˡ , distribʳ + ; *-assoc = λ x y z → ≈-from-parts + (assoc⁺ x y z) (assoc⁺ x y (- z)) + ; *-identity = + ( (λ { (x⁺ , x⁻) → ≈-from-parts + (begin + 1ₛ *ₛ x⁺ +ₛ 0ₛ *ₛ x⁻ ≈⟨ S.+-congʳ (S.*-identityˡ _) ⟩ + x⁺ +ₛ 0ₛ *ₛ x⁻ ≈⟨ Sₘ.elimʳ (S.zeroˡ _) x⁺ ⟩ + x⁺ ∎) + (begin + 1ₛ *ₛ x⁻ +ₛ 0ₛ *ₛ x⁺ ≈⟨ S.+-congʳ (S.*-identityˡ _) ⟩ + x⁻ +ₛ 0ₛ *ₛ x⁺ ≈⟨ Sₘ.elimʳ (S.zeroˡ _) x⁻ ⟩ + x⁻ ∎) }) + , (λ { (x⁺ , x⁻) → ≈-from-parts + (begin + x⁺ *ₛ 1ₛ +ₛ x⁻ *ₛ 0ₛ ≈⟨ S.+-congʳ (S.*-identityʳ _) ⟩ + x⁺ +ₛ x⁻ *ₛ 0ₛ ≈⟨ Sₘ.elimʳ (S.zeroʳ _) x⁺ ⟩ + x⁺ ∎) + (begin + x⁺ *ₛ 0ₛ +ₛ x⁻ *ₛ 1ₛ ≈⟨ S.+-congˡ (S.*-identityʳ _) ⟩ + x⁺ *ₛ 0ₛ +ₛ x⁻ ≈⟨ Sₘ.elimˡ (S.zeroʳ _) x⁻ ⟩ + x⁻ ∎) }) + ) + ; distrib = + ( (λ x y z → ≈-from-parts + (distrib⁺ˡ x y z) (distrib⁺ˡ x (- y) (- z))) + , (λ x y z → ≈-from-parts + (distrib⁺ʳ y z x) (distrib⁺ʳ y z (- x))) + ) } ring : Ring m (m ⊔ ℓ) - ring = record - { Carrier = Carrier - ; _≈_ = _≈_ - ; _+_ = _+_ - ; _*_ = _*_ - ; -_ = -_ - ; 0# = 0# - ; 1# = 1# - ; isRing = completion-is-ring - } + ring = record { isRing = completion-is-ring } private module R = Semiring (Ring.semiring ring) + open Definitions (_≈ₛ_) + using (Commutative) renaming (LeftZero to LeftAbsorbing) ------------------------------------------------------------------------ -- Commutative specialization - private - *-comm : Commutative S._*_ → ∀ x y → x * y ≈ y * x - *-comm comm (a , b) (c , d) = ≈-from-parts - (S.+-cong (comm a c) (comm b d)) - (begin - (a *ₛ d) +ₛ (b *ₛ c) - ≈⟨ S.+-cong (comm a d) (comm b c) ⟩ - (d *ₛ a) +ₛ (c *ₛ b) - ≈⟨ S.+-comm (d *ₛ a) (c *ₛ b) ⟩ - (c *ₛ b) +ₛ (d *ₛ a) ∎) - commutativeRing : Commutative S._*_ → CommutativeRing m (m ⊔ ℓ) commutativeRing comm = record { isCommutativeRing = record { isRing = completion-is-ring - ; *-comm = *-comm comm + ; *-comm = λ { (a , b) (c , d) → ≈-from-parts + (S.+-cong (comm a c) (comm b d)) + (begin + a *ₛ d +ₛ b *ₛ c ≈⟨ S.+-cong (comm a d) (comm b c) ⟩ + d *ₛ a +ₛ c *ₛ b ≈⟨ S.+-comm _ _ ⟩ + c *ₛ b +ₛ d *ₛ a ∎) } } } @@ -279,18 +245,15 @@ module _ {m ℓ : Level} (semiring : Semiring m ℓ) where embed : Base → Carrier embed = Negatives.embed S.+-commutativeMonoid - decompose : ∀ x → x ≈ embed (pos x) + - embed (neg x) + decompose : ∀ x → x ≈ embed (proj₁ x) + - embed (proj₂ x) decompose = Negatives.decompose S.+-commutativeMonoid embed-* : ∀ x y → embed (x *ₛ y) ≈ embed x * embed y embed-* x y = ≈-from-parts + (Sₘ.introʳ (S.zeroˡ 0ₛ) (x *ₛ y)) (begin - x *ₛ y ≈⟨ S.+-identityʳ _ ⟨ - (x *ₛ y) +ₛ 0ₛ ≈⟨ S.+-congˡ (S.zeroˡ _) ⟨ - (x *ₛ y) +ₛ (0ₛ *ₛ 0ₛ) ∎) - (begin - 0ₛ ≈⟨ S.+-identityˡ _ ⟨ - 0ₛ +ₛ 0ₛ ≈⟨ S.+-cong (S.zeroʳ _) (S.zeroˡ _) ⟨ + 0ₛ ≈⟨ S.zeroˡ y ⟨ + 0ₛ *ₛ y ≈⟨ Sₘ.introˡ (S.zeroʳ x) _ ⟩ (x *ₛ 0ₛ) +ₛ (0ₛ *ₛ y) ∎) embed-isSemiringHomomorphism : @@ -302,28 +265,26 @@ module _ {m ℓ : Level} (semiring : Semiring m ℓ) where S.+-commutativeMonoid ; *-homo = embed-* } - ; 1#-homo = ≈.refl + ; 1#-homo = Additive.refl } embed-semiringHomomorphism : SemiringHomomorphism S.rawSemiring R.rawSemiring embed-semiringHomomorphism = record - { ⟦_⟧ = embed - ; isSemiringHomomorphism = embed-isSemiringHomomorphism - } + { isSemiringHomomorphism = embed-isSemiringHomomorphism } ---------------------------------------------------------------------- -- Trivial completions - +-absorbing⇒trivial : (∞ : Base) → RightZero ∞ S._+_ → + +-absorbing⇒trivial : (∞ : Base) → LeftAbsorbing ∞ S._+_ → ∀ x → x ≈ 0# +-absorbing⇒trivial = Negatives.absorbing⇒trivial S.+-commutativeMonoid - +-absorbing⇒1#≈0# : (∞ : Base) → - RightZero ∞ S._+_ → 1# ≈ 0# - +-absorbing⇒1#≈0# ∞ zeroʳ = +-absorbing⇒trivial ∞ zeroʳ 1# + +-absorbing⇒1#≈0# : (∞ : Base) → LeftAbsorbing ∞ S._+_ → + 1# ≈ 0# + +-absorbing⇒1#≈0# ∞ absorbˡ = +-absorbing⇒trivial ∞ absorbˡ 1# ------------------------------------------------------------------------ @@ -338,17 +299,7 @@ module AlreadyRing {m ℓ : Level} (R : Ring m ℓ) where module Additive = Negatives.AlreadyGroup R.+-abelianGroup module Additive≅ = IsGroupIsomorphism Additive.self-completion-≅ - completion : Ring m (m ⊔ ℓ) - completion = ring R.semiring - - module C = Ring completion - - open R using () renaming - ( _≈_ to _≈r_ ; _+_ to _+r_ - ; _*_ to _*r_ ; -_ to -r_ - ; 0# to 0r ; 1# to 1r - ; +-cong to +r-cong ; +-congˡ to +r-congˡ - ) + module C = Ring (ring R.semiring) open ≈-Reasoning R.setoid @@ -356,23 +307,24 @@ module AlreadyRing {m ℓ : Level} (R : Ring m ℓ) where self-completion-to-self = Product.uncurry R._-_ to-self-* : ∀ x y → - self-completion-to-self (C._*_ x y) ≈r - self-completion-to-self x *r self-completion-to-self y + self-completion-to-self (C._*_ x y) R.≈ + self-completion-to-self x R.* self-completion-to-self y to-self-* (a , b) (c , d) = begin - (a *r c +r b *r d) R.- (a *r d +r b *r c) ≡⟨⟩ - (a *r c +r b *r d) +r -r (a *r d +r b *r c) - ≈⟨ +r-congˡ (Rₚ.-‿+-comm (a *r d) (b *r c)) ⟨ - (a *r c +r b *r d) +r (-r (a *r d) +r -r (b *r c)) - ≈⟨ medial (a *r c) (b *r d) - (-r (a *r d)) (-r (b *r c)) ⟩ - (a *r c R.- a *r d) +r (b *r d R.- b *r c) - ≈⟨ +r-congˡ (Rₚ.⁻¹-anti-homo‿- (b *r c) (b *r d)) ⟨ - (a *r c R.- a *r d) R.- (b *r c R.- b *r d) - ≈⟨ +r-cong (Rₚ.x[y-z]≈xy-xz a c d) - (R.-‿cong (Rₚ.x[y-z]≈xy-xz b c d)) ⟨ - a *r (c R.- d) R.- b *r (c R.- d) + (a R.* c R.+ b R.* d) R.- (a R.* d R.+ b R.* c) ≡⟨⟩ + (a R.* c R.+ b R.* d) R.+ R.-_ (a R.* d R.+ b R.* c) + ≈⟨ R.+-congˡ (Rₚ.-‿+-comm (a R.* d) (b R.* c)) ⟨ + (a R.* c R.+ b R.* d) R.+ + (R.-_ (a R.* d) R.+ R.-_ (b R.* c)) + ≈⟨ medial (a R.* c) (b R.* d) + (R.-_ (a R.* d)) (R.-_ (b R.* c)) ⟩ + (a R.* c R.- a R.* d) R.+ (b R.* d R.- b R.* c) + ≈⟨ R.+-congˡ (Rₚ.⁻¹-anti-homo‿- (b R.* c) (b R.* d)) ⟨ + (a R.* c R.- a R.* d) R.- (b R.* c R.- b R.* d) + ≈⟨ R.+-cong (Rₚ.x[y-z]≈xy-xz a c d) + (R.-‿cong (Rₚ.x[y-z]≈xy-xz b c d)) ⟨ + a R.* (c R.- d) R.- b R.* (c R.- d) ≈⟨ Rₚ.[y-z]x≈yx-zx (c R.- d) a b ⟨ - (a R.- b) *r (c R.- d) ∎ + (a R.- b) R.* (c R.- d) ∎ to-self-isRingHomomorphism : IsRingHomomorphism C.rawRing R.rawRing self-completion-to-self @@ -382,7 +334,7 @@ module AlreadyRing {m ℓ : Level} (R : Ring m ℓ) where { +-isMonoidHomomorphism = Additive≅.isMonoidHomomorphism ; *-homo = to-self-* } - ; 1#-homo = Additive.to-self-embed 1r + ; 1#-homo = Additive.to-self-embed R.1# } ; -‿homo = Additive≅.⁻¹-homo }