ρ_one

Mathlib.CategoryTheory.Action.Basic

URI: https://scilib.ai/kg/mathlib#Action.ρ_one

English

For any action A, the action of the identity element is the identity on A.V.

Русский

Для любой дествия A действие единицы G даёт тождественный морфизм на A.V.

LaTeX

$$$A.\rho(1) = \mathrm{id}_{A.V}$$$

Lean4

theorem ρ_one {G : Type*} [Monoid G] (A : Action V G) : A.ρ 1 = 𝟙 A.V := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru