Finite-support semantics

FiniteSupport M is the idempotent support carrier used by monotone arithmetic interpretations. Addition unions supports, while multiplication takes all pairwise products. No algebraic laws on M are imposed here: the arithmetic circuit syntax only needs total binary operations, and concrete applications can add monoid or exponent-vector structure as needed.

structure Algebraic.FiniteSupport (M : Type u) : Type u

A semantic value represented only by its finite set of monomials.

• monomials : Finset M

  Monomials present with nonzero coefficient.

@[instance_reducible]

instance Algebraic.instDecidableEqFiniteSupport {M✝ : Type u_1} [DecidableEq M✝] : DecidableEq (FiniteSupport M✝)

Equations

• Algebraic.instDecidableEqFiniteSupport = Algebraic.instDecidableEqFiniteSupport.decEq

def Algebraic.instDecidableEqFiniteSupport.decEq {M✝ : Type u_1} [DecidableEq M✝] (x✝ x✝¹ : FiniteSupport M✝) : Decidable (x✝ = x✝¹)

Equations

• Algebraic.instDecidableEqFiniteSupport.decEq { monomials := a } { monomials := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Algebraic.FiniteSupport.singleton {M : Type u_1} (monomial : M) : FiniteSupport M

The support consisting of one monomial.

Equations

• Algebraic.FiniteSupport.singleton monomial = { monomials := {monomial} }

def Algebraic.FiniteSupport.empty (M : Type u) : FiniteSupport M

The empty support.

Equations

• Algebraic.FiniteSupport.empty M = { monomials := ∅ }

@[instance_reducible]

instance Algebraic.FiniteSupport.instAddOfDecidableEq {M : Type u_1} [DecidableEq M] : Add (FiniteSupport M)

Equations

• Algebraic.FiniteSupport.instAddOfDecidableEq = { add := fun (left right : Algebraic.FiniteSupport M) => { monomials := left.monomials ∪ right.monomials } }

@[instance_reducible]

instance Algebraic.FiniteSupport.instMulOfDecidableEq {M : Type u_1} [DecidableEq M] [Mul M] : Mul (FiniteSupport M)

Equations

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

@[simp]

theorem Algebraic.FiniteSupport.monomials_singleton {M : Type u_1} (monomial : M) : (singleton monomial).monomials = {monomial}

@[simp]

theorem Algebraic.FiniteSupport.monomials_empty {M : Type u_1} : (empty M).monomials = ∅

@[simp]

theorem Algebraic.FiniteSupport.monomials_add {M : Type u_1} [DecidableEq M] (left right : FiniteSupport M) : (left + right).monomials = left.monomials ∪ right.monomials

theorem Algebraic.FiniteSupport.mem_add {M : Type u_1} [DecidableEq M] (monomial : M) (left right : FiniteSupport M) : monomial ∈ (left + right).monomials ↔ monomial ∈ left.monomials ∨ monomial ∈ right.monomials

@[simp]

theorem Algebraic.FiniteSupport.monomials_mul {M : Type u_1} [DecidableEq M] [Mul M] (left right : FiniteSupport M) : (left * right).monomials = Finset.image₂ (fun (x1 x2 : M) => x1 * x2) left.monomials right.monomials

theorem Algebraic.FiniteSupport.mem_mul {M : Type u_1} [DecidableEq M] [Mul M] (monomial : M) (left right : FiniteSupport M) : monomial ∈ (left * right).monomials ↔ ∃ leftMonomial ∈ left.monomials, ∃ rightMonomial ∈ right.monomials, leftMonomial * rightMonomial = monomial

theorem Algebraic.FiniteSupport.card_mul_le {M : Type u_1} [DecidableEq M] [Mul M] (left right : FiniteSupport M) : (left * right).monomials.card ≤ left.monomials.card * right.monomials.card

Pairwise multiplication produces at most the Cartesian-product number of monomials.