English
For a SnakeInput D in an abelian, concrete category, δ evaluated at x3 is the composite v23.τ1 applied to x1, given the compatibility relations h2 and h1.
Русский
Для SnakeInput D в абелевой, конкретной категории δ на x3 равняется композиции v23.τ1 на x1 при соблюдении совместимости h2 и h1.
LaTeX
$$$\\delta x_3 = (v_{23}.\\tau_1)(x_1)$$$
Lean4
/-- This lemma allows the computation of the connecting homomorphism
`D.δ` when `D : SnakeInput C` and `C` is a concrete category. -/
theorem δ_apply (x₃ : ToType (D.L₀.X₃)) (x₂ : ToType (D.L₁.X₂)) (x₁ : ToType (D.L₂.X₁)) (h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃)
(h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂) : D.δ x₃ = D.v₂₃.τ₁ x₁ :=
by
have := (forget₂ C Ab).preservesFiniteLimits_of_preservesHomology
have : PreservesFiniteLimits (forget C) :=
by
have : forget₂ C Ab ⋙ forget Ab = forget C := HasForget₂.forget_comp
simpa only [← this] using comp_preservesFiniteLimits _ _
have eq := CategoryTheory.congr_fun (D.snd_δ) (Limits.Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)
have eq₁ := Concrete.pullbackMk_fst D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
have eq₂ := Concrete.pullbackMk_snd D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply] at eq
rw [eq₂] at eq
refine eq.trans (CategoryTheory.congr_arg (D.v₂₃.τ₁) ?_)
apply (Preadditive.mono_iff_injective' D.L₂.f).1 inferInstance
rw [← ConcreteCategory.comp_apply, φ₁_L₂_f]
dsimp [φ₂]
rw [ConcreteCategory.comp_apply, eq₁]
exact h₁.symm
