map — Mathlib

English

The morphism map f n: M.exteriorPower n ⟶ N.exteriorPower n is induced by f: M ⟶ N.

Русский

Отображение map f n: ∧^n M → ∧^n N индуцировано из f: M ⟶ N.

LaTeX

$$map {M,N} {f} {n} : M.exteriorPower n ⟶ N.exteriorPower n$$

Lean4

/-- The morphism `M.exteriorPower n ⟶ N.exteriorPower n` induced by a morphism `M ⟶ N`
in `ModuleCat R`. -/
noncomputable def map {M N : ModuleCat.{v} R} (f : M ⟶ N) (n : ℕ) : M.exteriorPower n ⟶ N.exteriorPower n :=
  ofHom (_root_.exteriorPower.map n f.hom)

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