English
The symmetric version of the hom-equivalence applied to f equals the inverse composition as in the previous statement.
Русский
Симметрическая версия применения гом-эквивалентности к f равна соответствующей обратной композиции как ранее.
LaTeX
$$$ (\mathrm{coindResAdjunction}_{k,S}).\mathrm{homEquiv}_{A,B}^{-1} \; f = (\mathrm{indCoindIso}_{A}).inv \circ (\mathrm{indResHomEquiv}_{S.subtype,A,B})^{-1} (f) $$$
Lean4
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the periodic chain complex in `ModuleCat k` given by
`... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0` where `N` is the norm map.
Its homology is the group homology of `A`. -/
noncomputable abbrev moduleCatChainComplex : ChainComplex (ModuleCat k) ℕ :=
HomologicalComplex.alternatingConst A.V (φ := A.norm.hom) (ψ := (applyAsHom A g - 𝟙 A).hom) (by ext; simp)
(by ext; simp) fun _ _ => ComplexShape.down_nat_odd_add
