English
The internal Hom functor preserves action compatibility: the functorial map respects the G-action via conjugation by g.
Русский
Внутренний композиционный гомоморфизм сохраняет совместимость действия: ковariantная карта сохраняет действие G через сопряжение g.
LaTeX
$$$$ (\\Rep.ihom A).obj B \\, ρ \\, g = B.ρ\\, g \\circ (\\, - \\,) \\circ A.ρ g^{-1}. $$$$
Lean4
/-- Auxiliary lemma for defining group cohomology, used to show that the isomorphism
`diagonalHomEquiv` commutes with the differentials in two complexes which compute
group cohomology. -/
@[deprecated "We no longer use `diagonalHomEquiv` to define group cohomology" (since := "2025-06-08")]
theorem diagonalHomEquiv_symm_partialProd_succ (f : (Fin n → G) → A) (g : Fin (n + 1) → G) (a : Fin (n + 1)) :
((diagonalHomEquiv n A).symm f).hom (Finsupp.single (Fin.partialProd g ∘ a.succ.succAbove) 1) =
f (Fin.contractNth a (· * ·) g) :=
by
rw [diagonalHomEquiv_symm_apply]
simp only [Function.comp_apply, Fin.succ_succAbove_zero, Fin.partialProd_zero, map_one, Fin.succ_succAbove_succ,
Module.End.one_apply, Fin.partialProd_succ]
congr
ext
rw [← Fin.partialProd_succ, Fin.inv_partialProd_mul_eq_contractNth]
