compContinuousLinearMapₗ — Mathlib

English

Given a linear map f: M → L, precomposition with f induces a linear map on the space of continuous alternating maps: g ↦ g ∘ f. This is linear in g.

Русский

Дано линейное отображение f: M → M', предсоставление (precomposition) с f задаёт линейное отображение на пространстве непрерывных чередующих отображений: g ↦ g ∘ f, и линейно по g.

LaTeX

$$$$ \\text{Let } T(g) = g \\circ f. \\quad T(a g_1 + b g_2) = a T(g_1) + b T(g_2). $$$$

Lean4

/-- `ContinuousAlternatingMap.compContinuousLinearMap` as a bundled `LinearMap`. -/
@[simps]
def compContinuousLinearMapₗ (f : M →L[R] M') : (M' [⋀^ι]→L[R] N) →ₗ[R] (M [⋀^ι]→L[R] N)
    where
  toFun g := g.compContinuousLinearMap f
  map_add' g g' := by ext; simp
  map_smul' c g := by ext; simp

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