Constructing Ring terms from MvPolynomial

This file provides tools for constructing ring terms that can be evaluated to particular MvPolynomials. The main motivation is in model theory. It can be used to construct first order formulas whose realization is a property of an MvPolynomial

Main definitions

• FirstOrder.Ring.genericPolyMap is a function that given a finite set of monomials monoms : ι → Finset (κ →₀ ℕ) returns a function ι → FreeCommRing ((Σ i : ι, monoms i) ⊕ κ) such that genericPolyMap monoms i is a ring term that can be evaluated to a polynomial p : MvPolynomial κ R such that p.support ⊆ monoms i.

def FirstOrder.Ring.genericPolyMap {ι : Type u_1} {κ : Type u_2} (monoms : ι → Finset (κ →₀ ℕ)) : ι → FreeCommRing ((i : ι) × { x : κ →₀ ℕ // x ∈ monoms i } ⊕ κ)

Given a finite set of monomials monoms : ι → Finset (κ →₀ ℕ), the genericPolyMap monoms is an indexed collection of elements of the FreeCommRing, that can be evaluated to any collection p : ι → MvPolynomial κ R of polynomials such that ∀ i, (p i).support ⊆ monoms i.

Equations

• FirstOrder.Ring.genericPolyMap monoms i = ∑ m ∈ (monoms i).attach, FreeCommRing.of (Sum.inl ⟨i, m⟩) * (↑m).prod fun (j : κ) (n : ℕ) => FreeCommRing.of (Sum.inr j) ^ n

noncomputable def FirstOrder.Ring.mvPolynomialSupportLEEquiv {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [DecidableEq κ] [CommRing R] [DecidableEq R] (monoms : ι → Finset (κ →₀ ℕ)) : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i } ≃ ((i : ι) × { x : κ →₀ ℕ // x ∈ monoms i } → R)

Collections of MvPolynomials, p : ι → MvPolynomial κ R such that ∀ i, (p i).support ⊆ monoms i can be identified with functions (Σ i, monoms i) → R by using the coefficient function

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [DecidableEq κ] [CommRing R] [DecidableEq R] (p : ι → MvPolynomial κ R) : ((FirstOrder.Ring.mvPolynomialSupportLEEquiv fun (i : ι) => (p i).support).symm fun (i : (i : ι) × { x : κ →₀ ℕ // x ∈ (p i).support }) => MvPolynomial.coeff (↑i.snd) (p i.fst)) = ⟨p, ⋯⟩

@[simp]

theorem FirstOrder.Ring.lift_genericPolyMap {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [DecidableEq κ] [CommRing R] [DecidableEq R] (monoms : ι → Finset (κ →₀ ℕ)) (f : (i : ι) × { x : κ →₀ ℕ // x ∈ monoms i } ⊕ κ → R) (i : ι) : (FreeCommRing.lift f) (FirstOrder.Ring.genericPolyMap monoms i) = (MvPolynomial.eval (f ∘ Sum.inr)) (↑((FirstOrder.Ring.mvPolynomialSupportLEEquiv monoms).symm (f ∘ Sum.inl)) i)