English
Let ι and ι' be index sets and σ an bijection between them. The space of alternating multilinear maps with ι inputs is naturally isomorphic to the space with ι' inputs, via permuting the inputs by σ. This is implemented by a linear equivalence domDomCongr_ℓ(σ) whose action on an alternating map f is f ↦ domDomCongr(σ) f; this equivalence is compatible with addition and scalar multiplication and has inverse given by domDomCongr(σ⁻¹).
Русский
Пусть данные индексы ι и ι' связаны биекцияσ. Пространство чередующихся многочленов с ι входами естественным образом эквивалентно пространству с ι' входами путём перестановки аргументов по σ. Это выражается линейным эквалентом domDomCongr_ℓ(σ), действующим на f как f ↦ domDomCongr(σ) f; эта эквалентность совместима с сложением и умножением на скаляры и имеет обратное отображение domDomCongr(σ⁻¹).
LaTeX
$$$\\operatorname{domDomCongr}_{\\ell}(\\sigma) : (M [\\⋀^ι] \\to_{\\ell[R]} N) \\simeq_{S} (M [\\⋀^{ι'}] \\to_{\\ell[R]} N),$\\ with $\\operatorname{toFun}(f) = \\operatorname{domDomCongr}(\\sigma)(f)$$$
Lean4
/-- `AlternatingMap.domDomCongr` as a linear equivalence. -/
@[simps apply symm_apply]
def domDomCongrₗ (σ : ι ≃ ι') : M [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι']→ₗ[R] N
where
toFun := domDomCongr σ
invFun := domDomCongr σ.symm
left_inv f := by ext; simp [Function.comp_def]
right_inv m := by ext; simp [Function.comp_def]
map_add' := domDomCongr_add σ
map_smul' := domDomCongr_smul σ
