inclusion — Mathlib

English

The inclusion map i: p →[M] α is an M-equivariant map, i.e., for all m ∈ M and x ∈ p, i(m • x) = m • i(x).

Русский

Включение i: p →[M] α является M-эквивариантным отображением: i(m • x) = m • i(x).

LaTeX

$$$ \\forall m \\in M, \\forall x \\in p:\\ i(m \\cdot x) = m \\cdot i(x) $$$

Lean4

/-- The inclusion of a SubMulAction into the ambient set, as an equivariant map -/
@[to_additive /-- The inclusion of a SubAddAction into the ambient set, as an equivariant map. -/
    ]
def inclusion (s : SubMulAction M α) : s →[M] α where
  -- The inclusion map of the inclusion of a SubMulAction

  toFun := Subtype.val
  map_smul' _ _ := rfl

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