English
There exists a canonical linear equivalence between the family of continuous alternating maps indexed by ι' with values in M' i and a single continuous alternating map into the product ∀ i, M' i. This is the pi-linear equivalence.
Русский
Существует каноническое линейное эквивалентное отображение между семейством непрерывных чередующих отображений, индексируемых ι', с значениями в M' i, и одним непрерывным чередующим отображением в произведение ∀ i, M' i.
LaTeX
$$$$ \\pi\\text{-linearEquiv} : \\Big( \\forall i, M [⋀^ι]→L[A] M' i \\Big) \\simeq_{R} M [⋀^ι]→L[A] (\\forall i, M' i). $$$$
Lean4
/-- `ContinuousAlternatingMap.pi` as a `LinearEquiv`. -/
@[simps +simpRhs]
def piLinearEquiv {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, TopologicalSpace (M' i)]
[∀ i, ContinuousAdd (M' i)] [∀ i, Module R (M' i)] [∀ i, Module A (M' i)] [∀ i, SMulCommClass A R (M' i)]
[∀ i, ContinuousConstSMul R (M' i)] : (∀ i, M [⋀^ι]→L[A] M' i) ≃ₗ[R] M [⋀^ι]→L[A] ∀ i, M' i :=
{ piEquiv with
map_add' := fun _ _ => rfl
map_smul' := fun _ _ => rfl }
