English
In an abelian category, a short complex S is exact iff for every A and every x2: A → S.X2 with x2 ≫ g = 0 there exists A', π, epi, x1 with π ≫ x2 = x1 ≫ f.
Русский
В абелевой категории короткий комплекс S точный тогда и только тогда, когда для каждого A и каждого x2: A → S.X2 с x2 ≫ g = 0 существует A', π, эпиморфизм, x1 с выполняющим π ≫ x2 = x1 ≫ f.
LaTeX
$$$S.Exact \\iff \\forall A\\,(x_2:A\\to S.X_2)\\; (x_2\\,\\gg\,S.g=0)\\ \\exists A',\\pi:A'\\to A\\; (\\pi\\ epi)\\; (x_1:A'\\to S.X_1),\\; \\pi\\, x_2 = x_1\\, S.f$$$
Lean4
theorem exact_iff_exact_up_to_refinements :
S.Exact ↔
∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂) (_ : x₂ ≫ S.g = 0),
∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f :=
by
rw [S.exact_iff_epi_toCycles, epi_iff_surjective_up_to_refinements]
constructor
· intro hS A a ha
obtain ⟨A', π, hπ, x₁, fac⟩ := hS (S.liftCycles a ha)
exact ⟨A', π, hπ, x₁, by simpa only [assoc, liftCycles_i, toCycles_i] using fac =≫ S.iCycles⟩
· intro hS A a
obtain ⟨A', π, hπ, x₁, fac⟩ := hS (a ≫ S.iCycles) (by simp)
exact ⟨A', π, hπ, x₁, by simp only [← cancel_mono S.iCycles, assoc, toCycles_i, fac]⟩
