coinvariantsAdjunction_homEquiv_symm_apply_hom

English

For X: Rep k G and Y: ModuleCat k, and f: X ⟶ (trivialFunctor k G).obj Y, the symm map of the hom-equivalence equals desc f.

Русский

Для X: Rep k G и Y: ModuleCat k и f: X ⟶ (trivialFunctor k G).obj Y, симметрическая карта гом-эквивалентности равна descent f.

LaTeX

$$$((\\text{coinvariantsAdjunction } k G).homEquiv X Y).symm f = \\text{desc } f$$$

Lean4

@[simp]
theorem coinvariantsAdjunction_homEquiv_symm_apply_hom {X : Rep k G} {Y : ModuleCat k}
    (f : X ⟶ (trivialFunctor k G).obj Y) : ((coinvariantsAdjunction k G).homEquiv X Y).symm f = desc f :=
  by
  ext
  simp [coinvariantsAdjunction, Adjunction.homEquiv_symm_apply]

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