alternatingMapLinearEquiv_comp_ιMulti

English

The alternatingMapLinearEquiv composed with ιMulti R n gives a canonical linear map that identifies the alternating maps with maps out of the wedge power.

Русский

Чередующееся линейное равносоотношение, составленное с ιMulti R n, задаёт каноническое линейное отображение, переводя чередующиеся отображения в отображения из внешнего произведения.

LaTeX

$$$\\text{alternatingMapLinearEquiv} \\circ (\\iotaMulti R n) = \\text{canonical linear map to wedge}$$$

Lean4

@[simp]
theorem alternatingMapLinearEquiv_comp_ιMulti (f : M [⋀^Fin n]→ₗ[R] N) :
    (alternatingMapLinearEquiv f).compAlternatingMap (ιMulti R n) = f :=
  by
  obtain ⟨φ, rfl⟩ := alternatingMapLinearEquiv.symm.surjective f
  dsimp [alternatingMapLinearEquiv]
  simp only [LinearEquiv.symm_apply_apply]
  rfl

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