shortExact_iff_degreewise_shortExact

English

Exchange between short exactness and degreewise short exactness.

Русский

Точность по степеням и точность по коротким точным последовательностям эквивалентны.

LaTeX

$$$S.ShortExact \\iff \\forall i, (S.map (eval C c i)).ShortExact$$$

Lean4

theorem shortExact_iff_degreewise_shortExact : S.ShortExact ↔ ∀ (i : ι), (S.map (eval C c i)).ShortExact :=
  by
  constructor
  · intro hS i
    have := hS.mono_f
    have := hS.epi_g
    exact hS.map (eval C c i)
  · exact shortExact_of_degreewise_shortExact S

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