ihom_obj_ρ_def — Mathlib

English

The ihom functor is defined as a functor sending B to Rep.of (Representation.linHom A.ρ B.ρ) with the action map given by pre- and post-composition with ρ.

Русский

IHom задаётся как функтор, отправляющий B в Rep.of (Representation.linHom A.ρ B.ρ) с операциями действия через композицию с ρ.

LaTeX

$$$$ \\text{IHom}(A):\\; B \\mapsto \\Rep.of (\\mathrm{Representation.linHom} \\; A.\\rho \\; B.\\rho). $$$$

Lean4

@[simp]
theorem ihom_obj_ρ_def (A B : Rep k G) : ((ihom A).obj B).ρ = ((Rep.ihom A).obj B).ρ :=
  rfl

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