epi_δ_of_isZero

Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

URI: https://scilib.ai/kg/mathlib#groupHomology.epi_δ_of_isZero

English

If H_n(G, X2) = 0, then δ: H_{n+1}(G, X3) → H_n(G, X1) is an epimorphism.

Русский

Если H_n(G, X2) = 0, тогда δ: H_{n+1}(G, X_3) → H_n(G, X_1) является эпиморфизмом.

LaTeX

$$$\mathrm{IsZero}\bigl(H_n(G, X_2)\bigr) \Rightarrow \mathrm{Epi}\bigl(\delta hX (n+1) n rfl\bigr)$$$

Lean4

theorem epi_δ_of_isZero (n : ℕ) (h : IsZero (groupHomology X.X₂ n)) : Epi (δ hX (n + 1) n rfl) :=
  SnakeInput.epi_δ _ h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru