English
If B carries the trivial G‑action, then any morphism f: A ⟶ B factors uniquely through the coinvariants A_G; i.e., there exists a unique linear map Desc f : (A_G) ⟶ B.V such that f = (Desc f) ∘ (coinvariantsMk A).
Русский
Если B имеет тривиальное действие G, то любой морфизм f: A ⟶ B допускает единственную факторизацию через coinvariants: существует единственная линейная карта Desc f: A_G ⟶ B.V такая, что f = Desc f ∘ coinvariantsMk A.
LaTeX
$$$\forall A,B:\mathrm{Rep}(k,G),\\ B.\rho.isTrivial \Rightarrow ∃!\; desc\: (A ⟶ B),\; (\mathrm{coinvariantsMk}\ k\ G).\mathrm{app} A \; ;\; \ desc = f.hom.hom$$
Lean4
/-- The linear map underlying a `G`-representation morphism `A ⟶ B`, where `B` has the trivial
representation, factors through `A_G`. -/
noncomputable abbrev desc [B.ρ.IsTrivial] (f : A ⟶ B) : (coinvariantsFunctor k G).obj A ⟶ B.V :=
ModuleCat.ofHom <|
Representation.Coinvariants.lift _ f.hom.hom fun _ => by
ext
have := hom_comm_apply f
simp_all
