Action_ρ_eq_ρ — Mathlib

English

The G-action ρ on a representation A coincides with the action transported along the endomorphism ring of A; precisely, Action.ρ A equals the endomorphism-ring transported action via ModuleCat.endRingEquiv.

Русский

Действие G на представлении A совпадает с действием, перенесённым вдоль кольца концевых отображений A; то есть Action.ρ A равняется действию, полученному через эквивалентность ModuleCat.endRingEquiv.

LaTeX

$$$\text{Action.ρ } A = (\text{ModuleCat.endRingEquiv }_).symm.toMonoidHom \circ A.ρ$$$

Lean4

theorem Action_ρ_eq_ρ {A : Rep k G} : Action.ρ A = (ModuleCat.endRingEquiv _).symm.toMonoidHom.comp A.ρ :=
  rfl

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