exact_of_iso — Mathlib

English

Given an iso e : S1 ≅ S2, exactness is transported along e: if S1 is exact, then S2 is exact.

Русский

Пусть дано изоморфизм e : S1 ≅ S2; точность переносится: если S1 точен, то и S2 точен.

LaTeX

$$$\\text{Exact}(S_1) \\Rightarrow \\text{Exact}(S_2)$$$

Lean4

theorem exact_of_iso (e : S₁ ≅ S₂) (h : S₁.Exact) : S₂.Exact :=
  by
  obtain ⟨⟨h, z⟩⟩ := h
  exact ⟨⟨HomologyData.ofIso e h, z⟩⟩

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