instPreservesProjectiveObjectsActionModuleCatSubtypeMemSubgroupResSubtype

English

Restriction along a subgroup preserves projective objects in the category of modules, via the adjunction with coinduction along the subgroup; in particular for Subgroup S of G.

Русский

Ограничение вдоль подгруппы сохраняет проективные объекты в категории модулей благодаря adjunction с коиндукцией по подгруппе; в частности для S ≤ G.

LaTeX

$$$\text{Res}_{S} : \mathrm{Mod}(k G) \to \mathrm{Mod}(k S) \text{ preserves projectives}$$$

Lean4

instance {G : Type u} [Group G] (S : Subgroup G) :
    (Action.res (ModuleCat.{u} k) S.subtype).PreservesProjectiveObjects :=
  (Action.res _ S.subtype).preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms
    (resCoindAdjunction k S.subtype)

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