exact_and_epi_g_iff_of_iso — Mathlib

English

For an iso e : S1 ≅ S2, S1.Exact ∧ Epi S1.g ⇔ S2.Exact ∧ Epi S2.g.

Русский

Для изоморфизма e : S1 ≅ S2 выполняется S1.Exact ∧ Epi S1.g ⇔ S2.Exact ∧ Epi S2.g.

LaTeX

$$$S_1.Exact \\land \\operatorname{Epi}(S_1.g) \\iff S_2.Exact \\land \\operatorname{Epi}(S_2.g)$$$

Lean4

theorem exact_and_epi_g_iff_of_iso (e : S₁ ≅ S₂) : S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g :=
  by
  have : Epi S₁.g ↔ Epi S₂.g :=
    (MorphismProperty.epimorphisms C).arrow_mk_iso_iff
      (Arrow.isoMk (ShortComplex.π₂.mapIso e) (ShortComplex.π₃.mapIso e) e.hom.comm₂₃)
  rw [exact_iff_of_iso e, this]

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