English
Let R be a semiring and let α be a family of R-modules indexed by i in a type ι and κ i a type. Then the space of all functions f from the dependent sum Σ i κ i to α i.1 i.2 is canonically isomorphic (as an R-module) to the space of functions g assigning to each i and each k ∈ κ i an element of α i k. This is the standard currying/uncurrying correspondence for dependent families, realized as a linear equivalence.
Русский
Пусть R — полупрямой кольцо и пусть α — семейство R-модулей, индексируемое по i из типа ι, а κ i — типы. Тогда множество всех функций f: Σ i κ i → α i.1 i.2 имеет естественное структурное изоморфное представление как пространство функций g, сопоставляющих каждому i и каждому k ∈ κ i элемент α i k; это каноническое линейное эквивалентное соответствие карриирования/ракарриирования для зависимых семейств.
LaTeX
$$$$(\\Pi_{(i,k) \\in \\Sigma \\kappa} \\alpha_{i,k}) \\simeq_{\\!R} \\Pi_{i:\\iota} \\Pi_{k:\\kappa(i)} \\alpha_{i,k}$$$$
Lean4
/-- `Equiv.piCurry` as a `LinearEquiv`. -/
def piCurry {ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*) [∀ i k, AddCommMonoid (α i k)]
[∀ i k, Module R (α i k)] : (Π i : Sigma κ, α i.1 i.2) ≃ₗ[R] Π i j, α i j
where
__ := Equiv.piCurry α
map_add' _ _ := rfl
map_smul' _ _ := rfl
