Contents

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

In this section we define the class of P-finite series, which are series that belong to a finitely generated algebra of series that is closed under left derivatives.

To this end, we fix the coefficient ring R, the alphabet Σ, and a product rule P.

open import Preliminaries.Base renaming (_,,_ to _,_)
open import General.ProductRules

module General.FinitelyGenerated
    (R : CommutativeRing)
    (Σ : Set)
    (P : ProductRule R)
    where
open import Size

open import Preliminaries.Vector
open import Preliminaries.Algebra R

open import General.Terms R
    renaming (_+_ to _[+]_; _*_ to _[*]_; _·_ to _[·]_)

open import General.Series R Σ
open import General.Products R Σ
open Product P

private variable
    X : Set
    m n : ℕ
    c : A
    f g h : A ⟪ Σ ⟫
    gs : Vec (A ⟪ Σ ⟫) n

Finitely genereated algebras of series

For a series f and a vector of generators gs, we write f ∈[ gs ] to denote that f can be obtained from the generators gs by a finite sequence of algebra operations.

infix 4 _∈[_] [_]∋_
infixr 8 _·∈_
infixr 6 _+∈_
infixr 7 _*∈_
infixr 8 _≈∈_

data [_]∋_ (gs : Vec (A ⟪ Σ ⟫) n) : A ⟪ Σ ⟫ → Set where
    𝟘∈ : [ gs ]∋ 𝟘
    gen∈ : g ∈ gs → [ gs ]∋ g
    _·∈_ : ∀ c → [ gs ]∋ f → [ gs ]∋ c · f
    _+∈_ : [ gs ]∋ f → [ gs ]∋ g → [ gs ]∋ f + g
    _*∈_ : [ gs ]∋ f → [ gs ]∋ g → [ gs ]∋ f * g
    -- closure under equivalence of series
    -- we need to assume this since the base ring is parametrised by an equivalence relation
    _≈∈_ : f ≈ g → [ gs ]∋ g → [ gs ]∋ f

_∈[_] : (f : A ⟪ Σ ⟫) (gs : Vec (A ⟪ Σ ⟫) n) → Set
f ∈[ gs ] = [ gs ]∋ f

If ϱ is an environment mapping variables to series in the algebra generated by gs, then also ⟦ p ⟧ ϱ belongs to this algebra.

In other words, the algebra generated by gs is closed under the algebra operations.

subalgebra :
    ∀ {ϱ} (p : Term X) →
    (∀ x → ϱ x ∈[ gs ]) →
    ---------------------
    ⟦ p ⟧ ϱ ∈[ gs ]

subalgebra 0T _ = 𝟘∈
subalgebra (var x) ass = ass x
subalgebra (c [·] p) ass = _ ·∈ subalgebra p ass
subalgebra (p [+] q) ass = subalgebra p ass +∈ subalgebra q ass
subalgebra (p [*] q) ass = subalgebra p ass *∈ subalgebra q ass

We obtain a special case.

subalgebraᵥ : ∀ p → ⟦ p ⟧ᵥ gs ∈[ gs ]
subalgebraᵥ p = subalgebra p λ x → gen∈ (∈-lookup x _)

Viceversa, for every element in the algebra generated by gs we can compute a term witnessing membership.

extract :
    ∀ f (gs : Vec (A ⟪ Σ ⟫) n) →
    f ∈[ gs ] →
    ----------------------------
    ∃[ α ] f ≈ ⟦ α ⟧ᵥ gs
extract {n} f gs f∈[gs] = go f f∈[gs] where

    -- there are n variables
    Y : Set
    Y = Fin n

    -- if f belongs to a finitely generated algebra,
    -- then it can be expressed as a polynomial in the generators
    go : ∀ f → f ∈[ gs ] → ∃[ α ] f ≈ ⟦ α ⟧ (lookup gs)
    go f 𝟘∈ = 0T , ≈-refl
    go f (gen∈ f∈gs) = var i , f≈⟦i⟧ϱ where

        -- index of f in gs
        i : Y
        i with lookup-∈ f∈gs
        ... | i , _ = i

        -- proof that f indeed is element i of gs′
        f≡ϱi : f ≡ lookup gs i
        f≡ϱi with lookup-∈ f∈gs
        ... | _ , eq = eq

        f≈⟦i⟧ϱ : f ≈ ⟦ var i ⟧ (lookup gs)
        f≈⟦i⟧ϱ = ≡→≈ f≡ϱi

    go f (c ·∈ f∈[gs])
        with go _ f∈[gs]
    ... | α , f≈⟦α⟧ = c [·] α , ·-cong R-refl f≈⟦α⟧

    go f (f∈[gs] +∈ g∈[gs])
        with go _ f∈[gs] | go _ g∈[gs]
    ... | α , f≈⟦α⟧ | β , g≈⟦β⟧ = α [+] β , +-cong f≈⟦α⟧ g≈⟦β⟧
    
    go f (f∈[gs] *∈ g∈[gs])
        with go _ f∈[gs] | go _ g∈[gs]
    ... | α , f≈⟦α⟧ | β , g≈⟦β⟧ = α [*] β , *-cong f≈⟦α⟧ g≈⟦β⟧

    go f (f≈g ≈∈ f∈[gs])
        with go _ f∈[gs]
    ... | α , g≈⟦α⟧ = α , ≈-trans f≈g g≈⟦α⟧

P-finite series

We present two, equivalent, definitions for P-finite series. One is more intuitive, while the other is more convenient to work with.

Official definition

We start with the intuitive definition. We say that a series is P-finite if it belongs to a finitely generated algebra of series that is closed under left derivatives. This is formalised as follows.

module OfficialDefinition where

    infix 3 P-fin[_,_,_]
    record P-fin (f : A ⟪ Σ ⟫) (n : ℕ) : Set where
        constructor P-fin[_,_,_]
        field
            gen : Vec (A ⟪ Σ ⟫) n
            memb : f ∈[ gen ]
            closed : ∀ a {g} → g ∈[ gen ] → δ g a ∈[ gen ]

        elem : A ⟪ Σ ⟫
        elem = f

    open P-fin

Working definition

We now present a more convenient definition of P-finite series, which will be our working definition for the rest of the document.

The working definition is more restrictive since it requires closure under left derivatives only for the generators (instead for all elements of the algebra).

module SimplifiedDefinition where

    infix 3 P-fin[_,_,_]
    record P-fin (f : A ⟪ Σ ⟫) (n : ℕ) : Set where
        constructor P-fin[_,_,_]
        field
            gen : Vec (A ⟪ Σ ⟫) n
            memb : f ∈[ gen ]
            closed : ∀ a {g} → g ∈ gen → δ g a ∈[ gen ]

        elem : A ⟪ Σ ⟫
        elem = f

Equivalence of the two definitions

Before proceeding, we show that the two definitions are in fact equivalent.

module EquivalenceOfDefinitions where

    open SimplifiedDefinition
    open OfficialDefinition renaming (P-fin to P-fin′; P-fin[_,_,_] to P-fin′[_,_,_])
    open P-fin public

The simplified definition is a special case of the official one, so one direction is easy to prove.

    official→simplified :
        P-fin′ f n → P-fin f n

    official→simplified P-fin′[ gen , f∈[gen] , cl′ ] =
        P-fin[ gen , f∈[gen] , cl ] where
            cl :  ∀ a {g} → g ∈ gen → δ g a ∈[ gen ]
            cl a g∈gen = cl′ a (gen∈ g∈gen)

For the other direction, we will use the following auxiliary lemma

    δ-closed :
        ∀ (F : P-fin f n) a {g} →
        g ∈[ gen F ] →
        -------------------------
        δ g a ∈[ gen F ]

It says that the algebra generated by the generators of a P-finite series (in the simplified sense) is closed under left derivatives.

With this lemma in hand, it is easy to show that the simplified definition implies the official one.

    simplified→official :
        P-fin f n → P-fin′ f n

    simplified→official F = P-fin′[ gen F , memb F , δ-closed F ]

We conclude by proving the auxiliary lemma.

    δ-closed F a = go where
        go : ∀ {g} → g ∈[ gen F ] → δ g a ∈[ gen F ]
        go 𝟘∈ = 𝟘∈
        go (gen∈ g∈gen) = closed F a g∈gen
        go (c ·∈ g∈[F]) = c ·∈ go g∈[F]
        go (g∈[F] +∈ h∈[F]) = go g∈[F] +∈ go h∈[F]
        go (_*∈_ {g} {h} g∈[gen] h∈[gen]) = subalgebra P ass where

            ass : ∀ x → lookup (g ∷ δ g a ∷ h ∷ δ h a ∷ []) x ∈[ gen F ]
            ass zero = g∈[gen]
            ass (suc zero) = go g∈[gen]
            ass (suc (suc zero)) = h∈[gen]
            ass (suc (suc (suc zero))) = go h∈[gen]
            
        go (f≈g ≈∈ f∈[F]) = (δ-≈ f≈g a) ≈∈ go f∈[F]

Therefore, from now on we work with the simplified definition.

open SimplifiedDefinition public
open EquivalenceOfDefinitions using (δ-closed) public
open P-fin public

Closure properties of P-finite series

We show some natural closure properties for the class of P-finite series. The use of the simplified definition makes the proofs easier.

In the proofs we will use the following auxiliary properties, which will be proved at the end.

_++-gen_ : P-fin f m → P-fin g n → Vec (A ⟪ Σ ⟫) (m +ℕ n)
F ++-gen G = gen F ++ gen G

_++-memb-+_ : (F : P-fin f m) (G : P-fin g n) → elem F + elem G ∈[ F ++-gen G ]
_++-memb-*_ : (F : P-fin f m) (G : P-fin g n) → elem F * elem G ∈[ F ++-gen G ]
_++-closed_ : ∀ (F : P-fin f m) (G : P-fin g n) a {h} → h ∈ (F ++-gen G) →
    δ h a ∈[ F ++-gen G ]

Zero

The zero series 𝟘 is P-finite for the empty tuple of generators.

P-fin-𝟘 : P-fin 𝟘 0
P-fin-𝟘 = P-fin[ [] , 𝟘∈ , (λ a {g} ()) ]

Scalar multiplication

P-finite series are closed under scalar multiplication. We use the same set of generators.

P-fin-· : 
    P-fin f n →
    ----------------
    P-fin (c · f) n

P-fin-· F = P-fin[ gen F , _ ·∈ memb F , closed F ]

Addition

P-finite series are closed under addition. The set of generators is the concatenation of generators.

P-fin-+ :
    P-fin f m →
    P-fin g n →
    ----------------------
    P-fin (f + g) (m +ℕ n)

P-fin-+ F G = P-fin[ F ++-gen G , F ++-memb-+ G , F ++-closed G ]

Multiplication

P-finite series are closed under multiplication. The set of generators is the concatenation of generators.

P-fin-* :
    P-fin f m →
    P-fin g n →
    ----------------------
    P-fin (f * g) (m +ℕ n)

P-fin-* F G = P-fin[ F ++-gen G , F ++-memb-* G , F ++-closed G ]

The previous closure properties can be aggregated by saying that, for every term, if each variable evaluates to a P-finite series, then the whole term evaluates to a P-finite series too.

Left derivatives

P-finite series are closed under left derivatives. The set of generators does not change.

P-fin-δ :
    P-fin f m →
    ∀ a →
    ---------------
    P-fin (δ f a) m

P-fin-δ F a = P-fin[ gen F , δ-closed F a (memb F) , closed F ]

Left anti-derivatives

When the alphabet Σ is finite, we can also show that P-finite series are closed under left anti-derivatives. This is elaborated in a separate section.

Appendix

We prove here the auxiliary lemmas used in the closure properties.

++-∈ˡ : ∀ {fs : Vec (A ⟪ Σ ⟫) m} {gs : Vec (A ⟪ Σ ⟫) n} → f ∈[ fs ] → f ∈[ fs ++ gs ]
++-∈ˡ 𝟘∈ = 𝟘∈
++-∈ˡ (gen∈ f∈fs) = gen∈ (∈-++⁺ˡ f∈fs)
++-∈ˡ (c ·∈ f∈[fs]) = c ·∈ ++-∈ˡ f∈[fs]
++-∈ˡ (f∈[fs] +∈ g∈[fs]) = ++-∈ˡ f∈[fs] +∈ ++-∈ˡ g∈[fs]
++-∈ˡ (f∈[fs] *∈ g∈[fs]) = ++-∈ˡ f∈[fs] *∈ ++-∈ˡ g∈[fs]
++-∈ˡ (f≈g ≈∈ g∈[fs]) = f≈g ≈∈ ++-∈ˡ g∈[fs]

++-∈ʳ : ∀ {fs : Vec (A ⟪ Σ ⟫) m} {gs : Vec (A ⟪ Σ ⟫) n} → f ∈[ gs ] → f ∈[ fs ++ gs ]
++-∈ʳ 𝟘∈ = 𝟘∈
++-∈ʳ (gen∈ f∈fs) = gen∈ (∈-++⁺ʳ _ f∈fs)
++-∈ʳ (c ·∈ f∈[fs]) = c ·∈ ++-∈ʳ f∈[fs]
++-∈ʳ (f∈[fs] +∈ g∈[fs]) = ++-∈ʳ f∈[fs] +∈ ++-∈ʳ g∈[fs]
++-∈ʳ (f∈[fs] *∈ g∈[fs]) = ++-∈ʳ f∈[fs] *∈ ++-∈ʳ g∈[fs]
++-∈ʳ (f≈g ≈∈ g∈[fs]) = f≈g ≈∈ ++-∈ʳ g∈[fs]

F ++-memb-+ G = ++-∈ˡ (memb F) +∈ ++-∈ʳ ((memb G))
F ++-memb-* G = ++-∈ˡ (memb F) *∈ ++-∈ʳ (memb G)
   
_++-closed_ F G a h∈fs++gs with ∈ᵥ-++ h∈fs++gs
... | inj₁ h∈fs = ++-∈ˡ (closed F a h∈fs)
... | inj₂ h∈gs = ++-∈ʳ (closed G a h∈gs)

References