English
The sequence L₀.X₂ → L₀.X₃ → L₃.X₁ is exact.
Русский
Последовательность L₀.X₂ → L₀.X₃ → L₃.X₁ точна.
LaTeX
$$$\\operatorname{Exact}(L_0.X_2 \to L_0.X_3 \to L_3.X_1)$$$
Lean4
/-- Exactness of `L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁`. -/
theorem L₁'_exact : S.L₁'.Exact :=
by
rw [ShortComplex.exact_iff_exact_up_to_refinements]
intro A₀ x₃ hx₃
dsimp at x₃ hx₃
obtain ⟨A₁, π₁, hπ₁, p, hp⟩ := surjective_up_to_refinements_of_epi S.L₀'.g x₃
dsimp [L₀'] at p hp
have hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0 := by rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]
obtain ⟨A₂, π₂, hπ₂, x₁, hx₁⟩ := S.exact_C₁_down.exact_up_to_refinements (p ≫ S.φ₁) hp'
dsimp at x₁ hx₁
let x₂' := x₁ ≫ S.L₁.f
let x₂ := π₂ ≫ p ≫ pullback.fst _ _
have hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0 := by
simp only [x₂, x₂', sub_comp, assoc, ← S.v₁₂.comm₁₂, ← reassoc_of% hx₁, φ₂, φ₁_L₂_f, sub_self]
let k₂ : A₂ ⟶ S.L₀.X₂ := S.exact_C₂_up.lift _ hx₂'
have hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂' := S.exact_C₂_up.lift_f _ _
have hk₂' : k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd _ _ := by
simp only [x₂, x₂', ← cancel_mono S.v₀₁.τ₃, assoc, ← S.v₀₁.comm₂₃, reassoc_of% hk₂, sub_comp, S.L₁.zero, comp_zero,
sub_zero, pullback.condition]
exact ⟨A₂, π₂ ≫ π₁, epi_comp _ _, k₂, by simp only [assoc, L₁'_f, ← hk₂', hp]⟩
