Documentation

TauCeti.ModelTheory.Algebra.Ring.MvPolynomial

Terms of relational expansions of the ring language as polynomials #

Let L be a relational language, such as the language Language.order with the single relation symbol ≤. The terms of Language.ring.sum L use only the ring operations +, *, -, 0, 1, so a term with variables in α is an integer polynomial in α. For L = Language.order, Language.ring.sum L is the first-order language of ordered rings.

This file defines that polynomial, FirstOrder.Language.Term.toMvPolynomial, with its equations for variables and the ring operations, and proves:

For ordered rings, these are the term-level translation laws between formulas and polynomial sign conditions, used to identify semialgebraic sets with quantifier-free definable sets.

Implementation notes #

The construction of a term realizing a given polynomial follows the corresponding construction for FreeCommRing in Mathlib's Mathlib/ModelTheory/Algebra/Ring/FreeCommRing.lean, by Chris Hughes.

source
noncomputable def FirstOrder.Language.Term.toMvPolynomial {L : Language} [L.IsRelational] {α : Type u_1} :
(ring.sum L).Term α → MvPolynomial α ℤ

The integer polynomial computed by a term of the ring language expanded by the relation symbols of L.

Instances For
    source
    @[simp]
    theorem FirstOrder.Language.Term.toMvPolynomial_var {L : Language} [L.IsRelational] {α : Type u_1} (a : α) :
    (var a).toMvPolynomial = MvPolynomial.X a

    The polynomial of a variable is that variable.

    source
    @[simp]
    theorem FirstOrder.Language.Term.toMvPolynomial_func_add {L : Language} [L.IsRelational] {α : Type u_1} (ts : Fin 2 → (ring.sum L).Term α) :
    (func (Sum.inl Ring.addFunc) ts).toMvPolynomial = (ts 0).toMvPolynomial + (ts 1).toMvPolynomial

    The polynomial of a sum of terms is the sum of their polynomials.

    source
    @[simp]
    theorem FirstOrder.Language.Term.toMvPolynomial_func_mul {L : Language} [L.IsRelational] {α : Type u_1} (ts : Fin 2 → (ring.sum L).Term α) :
    (func (Sum.inl Ring.mulFunc) ts).toMvPolynomial = (ts 0).toMvPolynomial * (ts 1).toMvPolynomial

    The polynomial of a product of terms is the product of their polynomials.

    source
    @[simp]
    theorem FirstOrder.Language.Term.toMvPolynomial_func_neg {L : Language} [L.IsRelational] {α : Type u_1} (ts : Fin 1 → (ring.sum L).Term α) :
    (func (Sum.inl Ring.negFunc) ts).toMvPolynomial = -(ts 0).toMvPolynomial

    The polynomial of the negation of a term is the negation of its polynomial.

    source
    @[simp]
    theorem FirstOrder.Language.Term.toMvPolynomial_func_zero {L : Language} [L.IsRelational] {α : Type u_1} (ts : Fin 0 → (ring.sum L).Term α) :
    (func (Sum.inl Ring.zeroFunc) ts).toMvPolynomial = 0

    The polynomial of the constant 0 is 0.

    source
    @[simp]
    theorem FirstOrder.Language.Term.toMvPolynomial_func_one {L : Language} [L.IsRelational] {α : Type u_1} (ts : Fin 0 → (ring.sum L).Term α) :
    (func (Sum.inl Ring.oneFunc) ts).toMvPolynomial = 1

    The polynomial of the constant 1 is 1.

    source
    theorem FirstOrder.Language.Term.toMvPolynomial_relabel {L : Language} [L.IsRelational] {α : Type u_1} {β : Type u_2} (t : (ring.sum L).Term α) (g : α → β) :
    (relabel g t).toMvPolynomial = (MvPolynomial.rename g) t.toMvPolynomial

    Renaming the variables of a term renames the variables of its polynomial.

    source
    theorem FirstOrder.Language.Term.toMvPolynomial_surjective {L : Language} [L.IsRelational] {α : Type u_1} :
    Function.Surjective toMvPolynomial

    Every integer polynomial is the polynomial of a term of Language.ring.sum L.

    source
    theorem FirstOrder.Language.Term.realize_eq_aeval_toMvPolynomial {L : Language} [L.IsRelational] {α : Type u_1} {R : Type u_3} [CommRing R] [Ring.CompatibleRing R] [L.Structure R] (t : (ring.sum L).Term α) (v : α → R) :
    realize v t = (MvPolynomial.aeval v) t.toMvPolynomial

    In a commutative ring whose ring symbols have their usual meaning, realizing a term of Language.ring.sum L is evaluating its integer polynomial.

    source
    theorem FirstOrder.Language.Term.realize_eq_eval_map_toMvPolynomial {L : Language} [L.IsRelational] {α : Type u_1} {R : Type u_3} [CommRing R] [Ring.CompatibleRing R] [L.Structure R] (t : (ring.sum L).Term α) (v : α → R) :
    realize v t = (MvPolynomial.eval v) ((MvPolynomial.map (Int.castRingHom R)) t.toMvPolynomial)

    In a commutative ring whose ring symbols have their usual meaning, realizing a term of Language.ring.sum L is evaluating its integer polynomial mapped to R.

    source
    theorem MvPolynomial.exists_term_realize_eq_eval {L : FirstOrder.Language} [L.IsRelational] {σ : Type u_1} {R : Type u_2} [CommRing R] [FirstOrder.Ring.CompatibleRing R] [L.Structure R] (p : MvPolynomial σ R) :
    ∃ (t : (FirstOrder.Language.ring.sum L).Term (R ⊕ σ)), ∀ (v : σ → R), FirstOrder.Language.Term.realize (Sum.elim id v) t = (eval v) p

    Every polynomial over R is realized by a term of Language.ring.sum L with parameters from R: the variables Sum.inl r of the term are assigned the values r.