endRingEquiv_symm_comp_ρ — Mathlib

English

In FDRep, the composition of the end ring isomorphism's inverse with the action ρ equals the action ρ itself.

Русский

В FDRep композиция обратного изоморфизма кольцевого конца и действия ρ совпадает с самим действием ρ.

LaTeX

$$(MonoidHomClass.toMonoidHom (ModuleCat.endRingEquiv V.V.obj).symm).comp (ρ V) = (Action.ρ V)$$

Lean4

@[simp]
theorem endRingEquiv_symm_comp_ρ (V : FDRep R G) :
    (MonoidHomClass.toMonoidHom (ModuleCat.endRingEquiv V.V.obj).symm).comp (ρ V) = (Action.ρ V) :=
  rfl

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