Constructing Ring terms from MvPolynomial #
This file provides tools for constructing ring terms that can be evaluated to particular
MvPolynomial
s. 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 monomialsmonoms : ι → Finset (κ →₀ ℕ)
returns a functionι → FreeCommRing ((Σ i : ι, monoms i) ⊕ κ)
such thatgenericPolyMap monoms i
is a ring term that can be evaluated to a polynomialp : MvPolynomial κ R
such thatp.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
Instances For
noncomputable def
FirstOrder.Ring.mvPolynomialSupportLEEquiv
{ι : Type u_1}
{κ : Type u_2}
{R : Type u_3}
[DecidableEq κ]
[CommRing R]
[DecidableEq R]
(monoms : ι → Finset (κ →₀ ℕ))
:
Collections of MvPolynomial
s, 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)