ofModule_asModule_act — Mathlib

English

The action of the representation on an element x, transported through the module equivalence, equals the specified action via RestrictScalars.

Русский

Действие представления на элемент x, перенесённое через модульную эквив, равно заданному действию через RestrictScalars.

LaTeX

$$ofModule_asModule_act : ...$$

Lean4

@[simp]
theorem ofModule_asModule_act (g : G) (x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule) :
    ofModule ρ.asModule g x =
      (RestrictScalars.addEquiv _ _ _).symm
        (ρ.asModuleEquiv.symm (ρ g (ρ.asModuleEquiv (RestrictScalars.addEquiv _ _ _ x)))) :=
  by
  apply_fun RestrictScalars.addEquiv _ _ ρ.asModule using (RestrictScalars.addEquiv _ _ ρ.asModule).injective
  dsimp [ofModule, RestrictScalars.lsmul_apply_apply]
  simp

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