mulRepHom — Mathlib

English

The right regular representation on G → k is defined by (s) • f(t) = f(t s).

Русский

Правая регулярная структура на пространстве функций G → k задается как (s) • f(t) = f(t s).

LaTeX

$$$\\text{rightRegular}(s)\\, f(t) = f(t \\cdot s)$$$

Lean4

/-- The `FDRep k G` morphism induced by multiplication on `G → k`. -/
def mulRepHom : rightFDRep (k := k) (G := G) ⊗ rightFDRep ⟶ rightFDRep
    where
  hom := ofHom (LinearMap.mul' k (G → k))
  comm := by
    intro
    ext u
    refine TensorProduct.induction_on u rfl (fun _ _ ↦ rfl) (fun _ _ hx hy ↦ ?_)
    simp only [map_add, hx, hy]

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