colimitSMulAux — Mathlib

English

The auxiliary map for scalar multiplication in the colimit is defined by acting on a representative and re-packaging the result as a colimit element.

Русский

Вспомогательное отображение для скалярного умножения в пределе задаётся действием на представителе и возвратом в элемент колимита.

LaTeX

$$$$ \\text{colimitSMulAux}(r, (j,x)) = M.{\\text{mk}} F \\langle j, r\\cdot x\\rangle $$$$

Lean4

/-- The "unlifted" version of scalar multiplication in the colimit. -/
def colimitSMulAux (r : R) (x : Σ j, F.obj j) : M F :=
  M.mk F ⟨x.1, r • x.2⟩

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