English
In a concrete category, the forgetful image of δ equals the forgetful image of v23.τ1 when the corresponding x3,x2,x1 satisfy the forgetful relations h2 and h1.
Русский
В конкретной категории изображение забывающей functor δ равно изображению забывающей функции v23.τ1 при условиях совместимости h2 и h1.
LaTeX
$$$(\\forget_2 C Ab).map D.\\delta x_3 = (\\forget_2 C Ab).map D.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₃ : (forget₂ C Ab).obj D.L₀.X₃) (x₂ : (forget₂ C Ab).obj D.L₁.X₂) (x₁ : (forget₂ C Ab).obj D.L₂.X₁)
(h₂ : (forget₂ C Ab).map D.L₁.g x₂ = (forget₂ C Ab).map D.v₀₁.τ₃ x₃)
(h₁ : (forget₂ C Ab).map D.L₂.f x₁ = (forget₂ C Ab).map D.v₁₂.τ₂ x₂) :
(forget₂ C Ab).map D.δ x₃ = (forget₂ C Ab).map D.v₂₃.τ₁ x₁ :=
by
have e : forget₂ C Ab ⋙ forget Ab ≅ forget C := eqToIso (HasForget₂.forget_comp)
apply (mono_iff_injective (e.hom.app _)).1 inferInstance
refine
(congr_hom (e.hom.naturality D.δ) x₃).trans
((D.δ_apply (e.hom.app _ x₃) (e.hom.app _ x₂) (e.hom.app _ x₁) ?_ ?_).trans
(congr_hom (e.hom.naturality D.v₂₃.τ₁).symm x₁))
· refine ((congr_fun (e.hom.naturality D.L₁.g) x₂).symm.trans ?_).trans (congr_fun (e.hom.naturality D.v₀₁.τ₃) x₃)
dsimp
rw [h₂]
· refine ((congr_fun (e.hom.naturality D.L₂.f) x₁).symm.trans ?_).trans (congr_fun (e.hom.naturality D.v₁₂.τ₂) x₂)
dsimp
rw [h₁]
