id — Mathlib · SciLib

English

The identity morphism on an action M is the morphism with underlying map equal to the identity on M.V.

Русский

Идентичный морфизм на действии M имеет подлежащую карте равную тождественному отображению на M.V.

LaTeX

$$$\mathrm{id}_{M} : M \to M$ with $\mathrm{Hom} = \mathrm{id}_{M.V}$$$

Lean4

/-- The identity morphism on an `Action V G`. -/
@[simps]
def id (M : Action V G) : Action.Hom M M where hom := 𝟙 M.V

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