coinvariantsFunctor — Mathlib

English

There is a functor that sends a G-representation to its coinvariants and acts on morphisms by the induced map on coinvariants.

Русский

Существуют функтор, переводящий G-представление в когонварианты и действующий на морфизмах через индуцированное отображение на когонвариантах.

LaTeX

$$coinvariantsFunctor : Rep k G ⥤ ModuleCat k$$

Lean4

/-- The functor sending a representation to its coinvariants. -/
@[simps! obj_carrier map_hom]
noncomputable def coinvariantsFunctor : Rep k G ⥤ ModuleCat k
    where
  obj A := ModuleCat.of k A.ρ.Coinvariants
  map f := ModuleCat.ofHom (Representation.Coinvariants.map _ _ f.hom.hom fun g => ModuleCat.hom_ext_iff.1 <| f.comm g)
  map_id _ := by simp
  map_comp _ _ := by ext; simp

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