instance instLEMvPolynomialNat_provenance {X : Type} : LE (MvPolynomial X ℕ)

Equations

• instLEMvPolynomialNat_provenance = { le := fun (a b : MvPolynomial X ℕ) => ∀ (m : X →₀ ℕ), MvPolynomial.coeff m a ≤ MvPolynomial.coeff m b }

instance instSubMvPolynomialNat_provenance {X : Type} [DecidableEq X] : Sub (MvPolynomial X ℕ)

Equations

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

theorem coeff_sub {X : Type} [DecidableEq X] (p q : MvPolynomial X ℕ) (n : X →₀ ℕ) : MvPolynomial.coeff n (p - q) = MvPolynomial.coeff n p - MvPolynomial.coeff n q

instance instPartialOrderMvPolynomialNat_provenance {X : Type} : PartialOrder (MvPolynomial X ℕ)

Equations

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

instance instIsOrderedAddMonoidMvPolynomialNat_provenance {X : Type} : IsOrderedAddMonoid (MvPolynomial X ℕ)

instance instCanonicallyOrderedAddMvPolynomialNat_provenance {X : Type} : CanonicallyOrderedAdd (MvPolynomial X ℕ)

noncomputable instance instSemiringWithMonusMvPolynomialNat {X : Type} [DecidableEq X] : SemiringWithMonus (MvPolynomial X ℕ)

Marked as noncomputable only because the proof that MvPolynomial is a CommutativeSemiring is done in a non-computable way in Mathlib. We could redefine MvPolynomial to provide computable proofs.

Equations

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

theorem How.not_idempotent {X : Type} [DecidableEq X] : ¬idempotent (MvPolynomial X ℕ)

theorem How.not_absorptive {X : Type} [DecidableEq X] : ¬absorptive (MvPolynomial X ℕ)

theorem How.universal {X : Type} [DecidableEq X] (K : Type) [CommSemiring K] (ν : X → K) : ∃ (h : MvPolynomial X ℕ →+* K), ∀ (i : X), h (MvPolynomial.X i) = ν i

The How[X] semiring is universal among commutative semirings. This was observed in Green, Karnouvarakis, Tannen, Provenance Semirings, Proposition 4.2.

theorem How.not_universal_m {X : Type} [DecidableEq X] [Inhabited X] : ∃ (ν : X → ℕ), ¬∃ (h : SemiringWithMonusHom (MvPolynomial X ℕ) ℕ), ∀ (i : X), (fun (x : MvPolynomial X ℕ) => h.toRingHom x) (MvPolynomial.X i) = ν i

The How[X] semiring is not universal among commutative m-semirings, as long as there is at least one variable in X (if there is none, the notion of universality is trivial). This was shown in Geerts & Poggi, On database query languages for K-relations, Example 10.

theorem How.not_mul_sub_left_distributive {X : Type} [DecidableEq X] [Inhabited X] : ¬mul_sub_left_distributive (MvPolynomial X ℕ)

In How[X], as long as X is non-empty, times is not distributive over monus. Note that this contradicts Amsterdamer, Deutch & Tannen, On the limitations of provenance for queries with differences, table page 4, which claims this semiring satisfies axiom A13.