K-semimodules and the free K-tensor

This file develops the algebraic infrastructure required to interpret the aggregation operator on K-annotated relations, following the framework of Amsterdamer, Deutch & Tannen, Provenance for aggregate queries (Section IV-B, Definition 7 of Sen, Maniu & Senellart, ProvSQL).

Main definitions

• KSemiModule K M – a left action of a CommSemiringWithMonus K on an AddCommMonoid M satisfying the six standard semimodule axioms (zero_smul, one_smul, add_smul, smul_add, smul_zero, mul_smul). The same axioms as Mathlib's Module, exposed under our own name so that downstream provenance proofs depend on CommSemiringWithMonus directly (not on the more abstract Semiring).

• KTensor K M – a representation of the free formal sums ∑ αᵢ ⊗ mᵢ, realised as a Multiset (K × M) of monomials. Has Zero, Add and AddCommMonoid, plus a scalar action KTensor.smul, an embed map (K × M) → KTensor K M, and a contraction bind operator.

  Note: KTensor K M is not claimed to be a KSemiModule K. The underlying Multiset (K × M) is the free formal sum modulo permutation only; bilinearity relations such as (α + β) ⊗ m = α ⊗ m + β ⊗ m, 0 ⊗ m = 0, and α ⊗ (m₁ + m₂) = α ⊗ m₁ + α ⊗ m₂ are not enforced. Quotienting by those relations gives Mathlib-style TensorProduct, which is the right target for correctness theorems but adds substantial setoid-quotient machinery; the un-quotiented representation is enough for evaluating aggregations end-to-end.

Main results

• instance : KSemiModule K K – the canonical action of a CommSemiringWithMonus K on itself via multiplication.

References

• Amsterdamer, Deutch & Tannen
• Sen, Maniu & Senellart (Section IV-B, Def. 7)

The KSemiModule typeclass

class KSemiModule (K M : Type) [CommSemiringWithMonus K] [AddCommMonoid M] : Type

A K-semimodule structure on an additive commutative monoid M, relative to a CommSemiringWithMonus K. The six axioms are the bilinearity of the action (α, m) ↦ α • m, matching Mathlib's Module over a semiring.

• smul : K → M → M

  Left action of K on M.

• zero_smul (m : M) : smul 0 m = 0

  0 • m = 0: the zero of K annihilates m.

• one_smul (m : M) : smul 1 m = m

  1 • m = m: the multiplicative unit of K acts trivially.

• add_smul (α β : K) (m : M) : smul (α + β) m = smul α m + smul β m

  (α + β) • m = α • m + β • m: distributivity over K's addition.

• smul_add (α : K) (m n : M) : smul α (m + n) = smul α m + smul α n

  α • (m + n) = α • m + α • n: distributivity over M's addition.

• smul_zero (α : K) : smul α 0 = 0

  α • 0 = 0: the action sends 0 : M to 0.

• mul_smul (α β : K) (m : M) : smul (α * β) m = smul α (smul β m)

  (α * β) • m = α • (β • m): the action is multiplicative in K.

def KSemiModule.«term_⋆ₖ_» : Lean.TrailingParserDescr

Infix notation for the KSemiModule action. We deliberately do not use Mathlib's • to avoid forcing instance resolution on every SemiringWithMonus-flavoured proof.

Equations

• KSemiModule.«term_⋆ₖ_» = Lean.ParserDescr.trailingNode `KSemiModule.«term_⋆ₖ_» 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ₖ ") (Lean.ParserDescr.cat `term 73))

Canonical instance: every CommSemiringWithMonus acts on itself.

@[implicit_reducible]

instance CommSemiringWithMonus.instKSemiModuleSelf {K : Type} [CommSemiringWithMonus K] : KSemiModule K K

The canonical K-semimodule structure on K itself: the action is the semiring's multiplication.

Equations

• CommSemiringWithMonus.instKSemiModuleSelf = { smul := fun (x1 x2 : K) => x1 * x2, zero_smul := ⋯, one_smul := ⋯, add_smul := ⋯, smul_add := ⋯, smul_zero := ⋯, mul_smul := ⋯ }

The free K-tensor KTensor K M

A formal-sum representation of the free K-module generated by M. Each element is a multiset of monomials (α, m) : K × M. Addition is multiset union; the scalar action (β, t) ↦ β • t multiplies the K-coefficient of each monomial by β on the left.

The representation is the free formal sum modulo permutation only: bilinearity relations like (α₁ + α₂) ⊗ m = α₁ ⊗ m + α₂ ⊗ m are not enforced. Equality in the un-quotiented KTensor K M is stricter than in the proper tensor product K ⊗ M. We expose this data structure because it is enough to evaluate aggregations; the proper quotient will appear once we state and prove correctness theorems for the aggregation semantics.

def KTensor (K M : Type) : Type

The free K-tensor on a type M: a formal sum of K-weighted elements of M.

Equations

• KTensor K M = Multiset (K × M)

@[implicit_reducible]

instance KTensor.instZero {K M : Type} : Zero (KTensor K M)

Equations

• KTensor.instZero = { zero := KTensor.instZero._aux_1 }

@[implicit_reducible]

instance KTensor.instAdd {K M : Type} : Add (KTensor K M)

Equations

• KTensor.instAdd = { add := KTensor.instAdd._aux_1 }

@[implicit_reducible]

instance KTensor.instAddCommMonoid {K M : Type} : AddCommMonoid (KTensor K M)

Equations

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

@[implicit_reducible]

unsafe instance KTensor.instRepr {K M : Type} [Repr K] [Repr M] : Repr (KTensor K M)

Equations

• KTensor.instRepr = { reprPrec := KTensor.instRepr._aux_1 }

def KTensor.embed {K M : Type} (α : K) (m : M) : KTensor K M

Embed a single monomial (α, m) as the formal sum α ⊗ m.

Equations

• KTensor.embed α m = {(α, m)}

def KTensor.mapHom {K M K' : Type} (f : K → K') (t : KTensor K M) : KTensor K' M

Push a KTensor K M forward along a function f : K → K', mapping each monomial's K-coefficient through f. Used in particular to push forward along a SemiringWithMonusHom.

Equations

• KTensor.mapHom f t = Multiset.map (fun (p : K × M) => (f p.1, p.2)) t

@[simp]

theorem KTensor.mapHom_zero {K M K' : Type} (f : K → K') : mapHom f 0 = 0

@[simp]

theorem KTensor.mapHom_add {K M K' : Type} (f : K → K') (t u : KTensor K M) : mapHom f (t + u) = mapHom f t + mapHom f u

@[simp]

theorem KTensor.mapHom_embed {K M K' : Type} (f : K → K') (α : K) (m : M) : mapHom f (embed α m) = embed (f α) m

def KTensor.smul {K M : Type} [CommSemiringWithMonus K] (β : K) (t : KTensor K M) : KTensor K M

Scalar action of K on KTensor K M: multiply the K-coefficient of each monomial by β on the left. This is not the action of a KSemiModule instance, because the un-quotiented representation does not satisfy add_smul or zero_smul; we expose it as a plain function for use in the aggregation evaluator.

Equations

• KTensor.smul β t = Multiset.map (fun (p : K × M) => (β * p.1, p.2)) t

@[simp]

theorem KTensor.smul_zero {K M : Type} [CommSemiringWithMonus K] (β : K) : smul β 0 = 0

@[simp]

theorem KTensor.smul_add {K M : Type} [CommSemiringWithMonus K] (β : K) (t u : KTensor K M) : smul β (t + u) = smul β t + smul β u

@[simp]

theorem KTensor.one_smul {K M : Type} [CommSemiringWithMonus K] (t : KTensor K M) : smul 1 t = t

Home · Documentation · Publications · Contributors · Source · Cite