compMultilinearMap_alternatization

English

Composing with a linear map before and after alternatization preserves the structure: alternatization(g ∘ f) = g ∘ AlternatingMap(alternatization f).

Русский

Сжатие линейного отображения до и после чередования сохраняет строение:AlternatingMap(alternatization f).

LaTeX

$$$\\operatorname{alternatization}(g \\circ_{MultilinearMap} f) = g \\circ_{AlternatingMap} \\operatorname{alternatization}(f)$$$

Lean4

/-- Composition with a linear map before and after alternatization are equivalent. -/
theorem compMultilinearMap_alternatization (g : N' →ₗ[R] N'₂) (f : MultilinearMap R (fun _ : ι => M) N') :
    MultilinearMap.alternatization (g.compMultilinearMap f) = g.compAlternatingMap (MultilinearMap.alternatization f) :=
  by
  ext
  simp [MultilinearMap.alternatization_def]

Похожие утверждения