English
The hom-equivalence applied to f in the coind-res setting coincides with the ind-res image after applying the coind iso to f.
Русский
Применение гом-эквивалентности к f в конфигурации коинд-рес совпадает с изображением через ind-res после применения коинд-изоморфизма к f.
LaTeX
$$$ (\mathrm{coindResAdjunction}_{k,S}).\mathrm{homEquiv}_{A,B} \; f = \mathrm{indResHomEquiv}_{S.subtype,A,B} \bigl((\mathrm{indCoindIso}_{A}).hom \circ f\bigr) $$$
Lean4
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the short complex in `ModuleCat k` given by `A --N--> A --(ρ(g) - 𝟙)--> A`
where `N` is the norm map. Its homology is `Hⁱ(G, A)` for even `i` and `Hᵢ(G, A)` for odd `i`. -/
noncomputable abbrev subCompNormHom : ShortComplex (ModuleCat k) :=
ShortComplex.mk (applyAsHom A g - 𝟙 A).hom A.norm.hom (by ext; simp)
