toAlternatingMapLinear — Mathlib

English

The map that sends a continuous alternating map f to its associated alternating map is linear over R. In particular, toAlternatingMapLinear is an R-linear map.

Русский

Отображение, переходящее непрерывное чередующее отображение к соответствующему чередующему отображению, является линейным по отношению к R.

LaTeX

$$$$ toAlternatingMapLinear : (M [⋀^ι]→L[A] N) \\to_R (M [⋀^ι]→ₗ[A] N) $$ и для любых f,h и a: $$ (toAlternatingMapLinear (a f + b h)) = a\\,(toAlternatingMapLinear f) + b\\,(toAlternatingMapLinear h). $$$$

Lean4

/-- Linear map version of the map `toAlternatingMap`
associating to a continuous alternating map the corresponding alternating map. -/
@[simps -fullyApplied apply]
def toAlternatingMapLinear : (M [⋀^ι]→L[A] N) →ₗ[R] (M [⋀^ι]→ₗ[A] N)
    where
  toFun := toAlternatingMap
  map_add' := by simp
  map_smul' := by simp

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