English
Let k be a commutative ring, G and H groups, A a representation of H and B a representation of G. If f: G → H is injective and φ: Res_f(A) ⟶ B is an epimorphism, then for every natural number i, the i-th component of the induced cochains map is epi (i.e., surjective in the module category).
Русский
Пусть k — коммутативное кольцо, G и H — группы, A — репрезентация H, B — репрезентация G. Пусть f: G → H инъективно, и φ: Res_f(A) ⟶ B — эпиморфизм. Тогда для каждого натурального i соответствующий i-й компонент индуцированного отображения коцепонов является эпиморфизмом (то есть сюръекция в соответствующей категориальной структуре).
LaTeX
$$$\\\\forall i \\\\\\in \\\\mathbb{N}, \\\\mathrm{Epi}\\\\big( (\\\\mathrm{cochainsMap} f \\\\varphi).f i \\\\big)$$$$
Lean4
theorem cochainsMap_f_map_epi (hf : Function.Injective f) [Epi φ] (i : ℕ) : Epi ((cochainsMap f φ).f i) := by
simpa [ModuleCat.epi_iff_surjective] using
((Rep.epi_iff_surjective φ).1 inferInstance).comp_left.comp <|
LinearMap.funLeft_surjective_of_injective k A _ hf.comp_left
