coinvariantsAdjunction_homEquiv_apply_hom

English

In the coinvariants adjunction, applying the forward hom‑equivalence to a morphism f yields the composite coinvariantsMk_X ≫ f; i.e., the forward map is realized by precomposing with coinvariants Mk.

Русский

При применении перехода между гомоморфизмами в adjunction coinvariants применяет композицию coinvariantsMk_X с f.

LaTeX

$$$((\mathrm{coinvariantsAdjunction}_{k,G}).homEquiv X Y f).hom = (\mathrm{coinvariantsMk}_{k,G}).app X \;≫\; f$$$

Lean4

@[simp]
theorem coinvariantsAdjunction_homEquiv_apply_hom {X : Rep k G} {Y : ModuleCat k}
    (f : (coinvariantsFunctor k G).obj X ⟶ Y) :
    ((coinvariantsAdjunction k G).homEquiv X Y f).hom = (coinvariantsMk k G).app X ≫ f := by rfl

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