I — Mathlib · SciLib

English

I is additive: it preserves sums on morphisms between representations.

Русский

I сохранит суммы морфизмов между представлениями.

LaTeX

$$$\\text{I R G}.Additive$$$

Lean4

/-- The functor taking a representation `rep` to the representation `C(G, rep)`. -/
@[simps]
def I : Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G
    where
  obj := Iobj
  map {M N}
    φ :=
    { hom := TopModuleCat.ofHom (ContinuousLinearMap.compLeftContinuous _ _ φ.hom.hom)
      comm
        g := by
        ext f g'
        change (M.ρ g ≫ φ.hom).hom (f (g⁻¹ * g')) = (φ.hom ≫ N.ρ g).hom (f (g⁻¹ * g'))
        rw [φ.comm] }
  map_id _ := rfl
  map_comp _ _ := rfl

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