English
The unit component of the coindResAdjunction at A equals the unit from Ind-Res composed with the map induced by indCoindIso.
Русский
Компонента единицы у сопряжения coindResAdjunction на A равна единице из Ind-Res, композиционной с отображением, индуцированным indCoindIso.
LaTeX
$$$ (\mathrm{coindResAdjunction}_{k,S}).\mathrm{unit}.app A = (\mathrm{indResAdjunction}_{k,S.subtype}).\mathrm{unit}.app A \circ (\mathrm{Action.res}_{k,S.subtype}).map (\mathrm{indCoindIso}_{A}).hom $$$
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 normHomCompSub : ShortComplex (ModuleCat k) :=
ShortComplex.mk A.norm.hom (applyAsHom A g - 𝟙 A).hom (by ext; simp)
