English
The image of an element x ∈ ⨂[R] i, s_i in the FreeAddMonoid lifts x is the set of representations p ∈ FreeAddMonoid (R × Π i, s_i) that map to x under the quotient AddCon.
Русский
Образы элемента x ∈ ⨂[R] i, s_i в FreeAddMonoid образуют множество lift(x) всех представлений p ∈ FreeAddMonoid (R × Π i, s_i), которые отображаются в x через квотацию AddCon.
LaTeX
$$$$ \text{lifts}(x) = \{ p \mid \mathrm{AddCon}.toQuotient(p) = x \} $$$$
Lean4
/-- The image of an element `p` of `FreeAddMonoid (R × Π i, s i)` in the `PiTensorProduct` is
equal to the sum of `a • ⨂ₜ[R] i, m i` over all the entries `(a, m)` of `p`.
-/
theorem _root_.FreeAddMonoid.toPiTensorProduct (p : FreeAddMonoid (R × Π i, s i)) :
AddCon.toQuotient (c := addConGen (PiTensorProduct.Eqv R s)) p =
List.sum (List.map (fun x ↦ x.1 • ⨂ₜ[R] i, x.2 i) p.toList) :=
by
-- TODO: this is defeq abuse: `p` is not a `List`.
match p with
| [] => rw [FreeAddMonoid.toList_nil, List.map_nil, List.sum_nil]; rfl
|
x ::
ps =>
rw [FreeAddMonoid.toList_cons, List.map_cons, List.sum_cons, ← List.singleton_append, ← toPiTensorProduct ps, ←
tprodCoeff_eq_smul_tprod]
rfl
