In this section we show that special product rules induce associative commutative algebras of series. In fact, over the rationals the converse is true (and easy to see), however we do not prove this in Agda.

{-# OPTIONS --guardedness --sized-types #-}

open import Preliminaries.Base
open import General.ProductRules
open import Special.Polynomials using (Special)

module Special.Products
    (R : CommutativeRing)
    (Σ : Set)
    (P : ProductRule R)
    (special : Special R P)
    where

open import Preliminaries.Algebra R

open import General.Series R Σ
open import General.Terms R
    renaming (_+_ to _[+]_; _*_ to _[*]_; _·_ to _[·]_; -_ to [-]_; _-_ to _[-]_)
open import General.Products R Σ
open Product P

open import Special.Polynomials R as P using ()
open P.Special

private variable
    X Y : Set
    i : Size
    m n : ℕ

In the following, fix a product rule P that is special. The main result of this section is that the resulting P-product endows the set of series with the structure of an associative commutative algebra.

isSeriesAlgebra : IsAlgebra _≈_ _+_ _*_ -_ 𝟘 _·_

Axioms

We begin by showing that the P-product is associative, commutative, and distributive over addition, and compatible with scalar multiplication. The additional size parameter allows Agda to verify that the definitions are productive.

*-assoc : ∀ (f g h : A ⟪ Σ ⟫) → (f * g) * h ≈[ i ] f * (g * h)
*-comm : ∀ (f g : A ⟪ Σ ⟫) → f * g ≈[ i ] g * f
*-distribʳ : ∀ (f g h : A ⟪ Σ ⟫) → (g + h) * f ≈[ i ] (g * f) + (h * f)
*-distribˡ : ∀ (f g h : A ⟪ Σ ⟫) → f * (g + h) ≈[ i ] (f * g) + (f * h)
·-*-distrib : ∀ (c : A) (f g : A ⟪ Σ ⟫) → (c · f) * g ≈[ i ] c · (f * g)

The proof of the properties above is by coinduction, relying on the fact that the semantics of terms is invariant under term equivalence.

sem-inv :
    ∀ {p q : Term X} {ϱ : SEnv X} →
    p P.≈ q →
    -------------------------------
    ⟦ p ⟧ ϱ ≈[ i ] ⟦ q ⟧ ϱ

Semantic invariance is in turn coinductively proved using the series properties above. This circularity is well-founded because the size parameter decreases.

Associativity

ν-≈ (*-assoc f g h) = *R-assoc (ν f) (ν g) (ν h)
δ-≈ (*-assoc f g h) a =
    let ϱ = f ∷ δ f a ∷ g ∷ δ g a ∷ h ∷ δ h a ∷ [] in
    begin
        δ ((f * g) * h) a
            ≈⟨⟩
        ⟦ P ⟧⟨ f * g , ⟦ P ⟧⟨ f , δ f a , g , δ g a ⟩ , h , δ h a ⟩
            ≈⟨ ⟦ P ⟧≈ᵥ  [ ≈-refl , eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []} , ≈-refl , ≈-refl ] ⟨
        ⟦ P ⟧⟨ ⟦ x [*] y ⟧ᵥ ϱ , ⟦ [ P ]⟨ x , x′ , y , y′ ⟩ ⟧ᵥ ϱ , ⟦ z ⟧ᵥ ϱ , ⟦ z′ ⟧ᵥ ϱ ⟩
            ≈⟨ eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []} ⟨
        ⟦ [ P ]⟨ x [*] y , [ P ]⟨ x , x′ , y , y′ ⟩ , z , z′ ⟩ ⟧ᵥ ϱ
            ≈⟨ sem-inv (P-assoc special) ⟩
        ⟦ [ P ]⟨ x , x′ , y [*] z , [ P ]⟨ y , y′ , z , z′ ⟩ ⟩ ⟧ᵥ ϱ
            ≈⟨ eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []} ⟩
        ⟦ P ⟧⟨ f , δ f a , g * h , ⟦ [ P ]⟨ y , y′ , z , z′ ⟩ ⟧ᵥ ϱ ⟩
            ≈⟨ ⟦ P ⟧≈ᵥ [ ≈-refl , ≈-refl , ≈-refl , eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []} ] ⟩
        ⟦ P ⟧⟨ f , δ f a , g * h , ⟦ P ⟧⟨ g , δ g a , h , δ h a ⟩ ⟩
            ≈⟨⟩
        δ (f * (g * h)) a
        ∎ where open EqS

Commutativity

ν-≈ (*-comm f g) = *R-comm (ν f) (ν g)
δ-≈ (*-comm f g) a =
    let ϱ = f ∷ δ f a ∷ g ∷ δ g a ∷ [] in
    begin
        ⟦ P ⟧ᵥ ϱ
            ≈⟨ eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []} ⟨
        ⟦ [ P ]⟨ x , x′ , y , y′ ⟩ ⟧ᵥ ϱ
            ≈⟨ sem-inv (P-comm special) ⟩
        ⟦ [ P ]⟨ y , y′ , x , x′ ⟩ ⟧ᵥ ϱ
            ≈⟨ eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []} ⟩
        ⟦ P ⟧⟨ g , δ g a , f , δ f a ⟩
        ∎ where open EqS

Distributivity

ν-≈ (*-distribʳ f g h) = R-distribʳ (ν f) (ν g) (ν h)
δ-≈ (*-distribʳ h f g) a =
    let ϱ = f ∷ δ f a ∷ g ∷ δ g a ∷ h ∷ δ h a ∷ [] in
    begin
        ⟦ P ⟧⟨ f + g , δ f a + δ g a , h , δ h a ⟩
            ≈⟨⟩
        ⟦ P ⟧⟨ ⟦ x [+] y ⟧ᵥ ϱ , ⟦ x′ [+] y′ ⟧ᵥ ϱ , ⟦ z ⟧ᵥ ϱ , ⟦ z′ ⟧ᵥ ϱ ⟩
            ≈⟨ eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []} ⟨
        ⟦ [ P ]⟨ x [+] y , x′ [+] y′ , z , z′ ⟩ ⟧ᵥ ϱ
            ≈⟨ sem-inv (P-add special) ⟩
        ⟦ [ P ]⟨ x , x′ , z , z′ ⟩ [+] [ P ]⟨ y , y′ , z , z′ ⟩ ⟧ᵥ ϱ
            ≈⟨  (eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []}
                    ⟨ +-cong ⟩
                eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []}) ⟩
        ⟦ P ⟧⟨ f , δ f a , h , δ h a ⟩ + ⟦ P ⟧⟨ g , δ g a , h , δ h a ⟩
    ∎ where open EqS

*-distribˡ f g h =
    begin
        f * (g + h)
            ≈⟨ *-comm _ _ ⟩
        (g + h) * f
            ≈⟨ *-distribʳ _ _ _ ⟩
        g * f + h * f
            ≈⟨ +-cong (*-comm _ _) (*-comm _ _) ⟩
        f * g + f * h
    ∎ where open EqS

Compatibility with scalar multiplication

ν-≈ (·-*-distrib c f g) = *R-assoc _ _ _
δ-≈ (·-*-distrib c f g) a =
    let ϱ = f ∷ δ f a ∷ g ∷ δ g a ∷ [] in
    begin
        δ ((c · f) * g) a
            ≈⟨⟩
        ⟦ P ⟧⟨ c · f , c · δ f a , g , δ g a ⟩
            ≈⟨⟩
        ⟦ P ⟧⟨ c · ⟦ x ⟧ᵥ ϱ , c · ⟦ x′ ⟧ᵥ ϱ , ⟦ y ⟧ᵥ ϱ , ⟦ y′ ⟧ᵥ ϱ ⟩
            ≈⟨⟩
        ⟦ P ⟧⟨ ⟦ c [·] x ⟧ᵥ ϱ , ⟦ c [·] x′ ⟧ᵥ ϱ , ⟦ y ⟧ᵥ ϱ , ⟦ y′ ⟧ᵥ ϱ ⟩
            ≈⟨ eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ _} ⟨
        ⟦ [ P ]⟨ c [·] x , c [·] x′ , y , y′ ⟩ ⟧ᵥ ϱ
            ≈⟨ sem-inv (P-compat special c) ⟩
        ⟦ c [·] [ P ]⟨ x , x′ , y , y′ ⟩ ⟧ᵥ ϱ
            ≈⟨⟩
        c · ⟦ [ P ]⟨ x , x′ , y , y′ ⟩ ⟧ᵥ ϱ
            ≈⟨ ·-cong R-refl (eval-substᵥ P {_ ∷ _ ∷ _ ∷ _ ∷ []}) ⟩
        c · ⟦ P ⟧⟨ ⟦ x ⟧ᵥ ϱ , ⟦ x′ ⟧ᵥ ϱ , ⟦ y ⟧ᵥ ϱ , ⟦ y′ ⟧ᵥ ϱ ⟩
            ≈⟨⟩
        c · ⟦ P ⟧⟨ f , δ f a , g , δ g a ⟩
            ≈⟨⟩
        δ (c · (f * g)) a
    ∎ where open EqS

Semantic invariance

Finally, we prove semantic invariance, relying on the properties above.

sem-inv P.≈-refl = ≈-refl
sem-inv (P.≈-sym w) = ≈-sym (sem-inv w)
sem-inv (P.≈-trans u v)= ≈-trans (sem-inv u) (sem-inv v)
sem-inv (P.·-cong c≈d p≈q) = ·-cong c≈d (sem-inv p≈q)
sem-inv (P.·-one _) = ·-one _
sem-inv (P.·-+-distrib c p q)  = ·-+-distrib _ _ _ where open DistributivityProperties
sem-inv (P.+-·-distrib p c d)  = +-·-distrib _ _ _ where open DistributivityProperties
sem-inv (P.·-*-distrib c p q)  = ·-*-distrib _ _ _
sem-inv (P.*-·-distrib c d p)  = *-·-distrib _ _ _ where open DistributivityProperties
sem-inv (P.+-cong P0≈P1 Q0≈Q1) = +-cong (sem-inv P0≈P1) (sem-inv Q0≈Q1)
sem-inv (P.+-zeroʳ p) = +-identityʳ _
sem-inv (P.+-assoc p q r) = +-assoc _ _ _
sem-inv (P.+-comm p q) = +-comm _ _
sem-inv (P.+-invʳ p) = -‿inverseʳ _
sem-inv (P.*-cong P0≈P1 Q0≈Q1) = *-cong (sem-inv P0≈P1) (sem-inv Q0≈Q1)
sem-inv (P.*-assoc _ _ _) = *-assoc _ _ _
sem-inv (P.*-comm _ _) = *-comm _ _
sem-inv (P.*-distribʳ _ _ _) = *-distribʳ _ _ _

Algebra structure

We now put together all the properties above. First of all, multiplication endows the set of series with a semigroup structure.

*-isSemigroup : IsSemigroup _≈_ _*_
*-isSemigroup = record {
    isMagma = record {
        isEquivalence = isEquivalence-≈;
        ∙-cong = *-cong
        };
    assoc = *-assoc
    }

In turn, this provides a (commutative) ring structure, perhaps without an identity.

isRingWithoutOne : IsRingWithoutOne _≈_ _+_ _*_ -_ 𝟘
isRingWithoutOne = record
    { +-isAbelianGroup = +-isAbelianGroup
    ; *-cong = *-cong
    ; *-assoc = *-assoc
    ; distrib = record { fst = *-distribˡ ; snd = *-distribʳ }
    }

isCommutativeRingWithoutOne : IsCommutativeRingWithoutOne _≈_ _+_ _*_ -_ 𝟘
isCommutativeRingWithoutOne = record {
        isRingWithoutOne = isRingWithoutOne ;
        *-comm = *-comm 
    }

Finally, we obtain an associative commutative algebra structure.

isSeriesAlgebra = record {
        isCommutativeRingWithoutOne = isCommutativeRingWithoutOne
    ; isLeftModule = isLeftModule
    ; compatible = ·-*-distrib }

Special products