Documentation

Mathlib.RingTheory.MvPolynomial.FreeCommRing

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 #

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
Instances For
    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.
    Instances For
      @[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)