English
Let k be a commutative ring, G a group, X a module over k and Y a representation of G over k. For every morphism f: X → invariantsFunctor k G (Y), the adjunction isomorphism sends f to a morphism whose underlying linear map is the composition of the inclusion of the invariant submodule with f.hom; equivalently, the reciprocal image under the hom-equivalence has as underlying map Submodule.subtype ∘ f.hom.
Русский
Пусть k—слово кольцо, G—группа, X—модуль над k, Y—репрезентация G над k. Для каждого гомоморфизма f: X → invariantsFunctor k G (Y) соответствие по сопряжению переводит f в морфизм, чье базовое линейное отображение является композицией включения инвариантного подмодуля с f.hom; иначе говоря, обратное по отношению к гом-эквивалентности отображение имеет вид Submodule.subtype ∘ f.hom.
LaTeX
$$$(((\mathrm{invariantsAdjunction}\ k\ G).homEquiv X Y).\text{symm } f).hom.hom = \mathrm{Submodule.subtype} \ _ \circ f.hom$$$
Lean4
@[simp]
theorem invariantsAdjunction_homEquiv_symm_apply_hom {X : ModuleCat k} {Y : Rep k G}
(f : X ⟶ (invariantsFunctor k G).obj Y) :
(((invariantsAdjunction k G).homEquiv _ _).symm f).hom.hom = Submodule.subtype _ ∘ₗ f.hom :=
rfl
