cochainsMap_id_f_map_epi — Mathlib

English

In the identity case f is the identity on G and φ is still epi, so the induced i-th component of the cochains map is epi for all i. This specializes the previous statement to the identity group homomorphism.

Русский

В случае, когда f — тождественное отображение на G и φ всё ещё эпиморфизм, i-й компонент отображения коцепонов остаётся эпиморфизмом для всех i. Это частный случай предыдущего высказывания для тождественного гомоморфизма группы.

LaTeX

$$$\\\\forall i \\\\\\in \\\\mathbb{N}, \\\\mathrm{Epi}((\\\\mathrm{cochainsMap} (\\\\mathrm{id}_G) \\\\varphi).f i)$$$$

Lean4

instance cochainsMap_id_f_map_epi {A B : Rep k G} (φ : A ⟶ B) [Epi φ] (i : ℕ) :
    Epi ((cochainsMap (MonoidHom.id G) φ).f i) :=
  cochainsMap_f_map_epi (MonoidHom.id G) φ (fun _ _ h => h) i

Похожие утверждения