compAlternatingMapₗ — Mathlib

English

The construction compAlternatingMap is itself linear over S.

Русский

Конструкция compAlternatingMap есть линейное отображение над S.

LaTeX

$$$ \text{compAlternatingMap}_\ell : (N \to_{R} N_2) \to_{S} (M [⋀^ι]→_{R} N) \to_{S} (M [⋀^ι]→_{R} N_2) $$$

Lean4

/-- `LinearMap.compAlternatingMap` as an `S`-linear map. -/
@[simps]
def compAlternatingMapₗ [Semiring S] [Module S N] [Module S N₂] [SMulCommClass R S N] [SMulCommClass R S N₂]
    [LinearMap.CompatibleSMul N N₂ S R] (g : N →ₗ[R] N₂) : (M [⋀^ι]→ₗ[R] N) →ₗ[S] (M [⋀^ι]→ₗ[R] N₂)
    where
  toFun := g.compAlternatingMap
  map_add' := g.compAlternatingMap_add
  map_smul' := g.compAlternatingMap_smul

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