CategoryTheory.ShortComplex.SnakeInput.δ_apply
theorem CategoryTheory.ShortComplex.SnakeInput.δ_apply :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C]
[inst_2 : CategoryTheory.HasForget₂ C Ab] [inst_3 : CategoryTheory.Abelian C]
[inst_4 : (CategoryTheory.forget₂ C Ab).Additive] [inst_5 : (CategoryTheory.forget₂ C Ab).PreservesHomology]
(D : CategoryTheory.ShortComplex.SnakeInput C) (x₃ : (CategoryTheory.forget C).obj D.L₀.X₃)
(x₂ : (CategoryTheory.forget C).obj D.L₁.X₂) (x₁ : (CategoryTheory.forget C).obj D.L₂.X₁),
D.L₁.g x₂ = D.v₀₁.τ₃ x₃ → D.L₂.f x₁ = D.v₁₂.τ₂ x₂ → D.δ x₃ = D.v₂₃.τ₁ x₁
This theorem, `CategoryTheory.ShortComplex.SnakeInput.δ_apply`, establishes a computation rule for the connecting homomorphism, denoted `D.δ`, in a certain context. Given a Short Complex `D` that takes in a category `C` as input where `C` is a concrete category, and given elements `x₃`, `x₂`, `x₁` from different objects in the complex, if the morphism `D.L₁.g` applied to `x₂` equals the morphism `D.v₀₁.τ₃` applied to `x₃` and the morphism `D.L₂.f` applied to `x₁` equals the morphism `D.v₁₂.τ₂` applied to `x₂`, then the connecting homomorphism `D.δ` applied to `x₃` equals the morphism `D.v₂₃.τ₁` applied to `x₁`. In other words, this theorem provides a way to compute the value of the connecting homomorphism under certain conditions.
More concisely: Given a Short Complex `D` in a concrete category and elements `x₁, x₂, x₃` such that `D.L₁.g(x₂) = D.v₀₁.τ₃(x₃)` and `D.L₂.f(x₁) = D.v₁₂.τ₂(x₂)`, then `D.δ(x₃) = D.v₂₃.τ₁(x₁)`.
|
CategoryTheory.ShortComplex.SnakeInput.δ_apply'
theorem CategoryTheory.ShortComplex.SnakeInput.δ_apply' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C]
[inst_2 : CategoryTheory.HasForget₂ C Ab] [inst_3 : CategoryTheory.Abelian C]
[inst_4 : (CategoryTheory.forget₂ C Ab).Additive] [inst_5 : (CategoryTheory.forget₂ C Ab).PreservesHomology]
(D : CategoryTheory.ShortComplex.SnakeInput C) (x₃ : ↑((CategoryTheory.forget₂ C Ab).obj D.L₀.X₃))
(x₂ : ↑((CategoryTheory.forget₂ C Ab).obj D.L₁.X₂)) (x₁ : ↑((CategoryTheory.forget₂ C Ab).obj D.L₂.X₁)),
((CategoryTheory.forget₂ C Ab).map D.L₁.g) x₂ = ((CategoryTheory.forget₂ C Ab).map D.v₀₁.τ₃) x₃ →
((CategoryTheory.forget₂ C Ab).map D.L₂.f) x₁ = ((CategoryTheory.forget₂ C Ab).map D.v₁₂.τ₂) x₂ →
((CategoryTheory.forget₂ C Ab).map D.δ) x₃ = ((CategoryTheory.forget₂ C Ab).map D.v₂₃.τ₁) x₁
This theorem provides a way to compute the connecting homomorphism `D.δ` in the context of a concrete category `C`. Given a `SnakeInput` object `D` in the category `C`, and elements `x₃`, `x₂`, and `x₁` from the objects of the short complex `D`, if the image of `x₂` under the map `D.L₁.g` equals to the image of `x₃` under the map `D.v₀₁.τ₃`, and the image of `x₁` under the map `D.L₂.f` equals to the image of `x₂` under the map `D.v₁₂.τ₂`, then the image of `x₃` under the connecting homomorphism `D.δ` equals the image of `x₁` under the map `D.v₂₃.τ₁`. The category `C` is assumed to be an abelian category, and it also has a forgetful functor to the category of abelian groups that is both additive and preserves homology.
More concisely: Given an abelian category `C` with forgetful functor preserving homology, if in a short exact sequence `D: 0 -> D₁ -> D₂ -> D₃ -> 0` in `C`, the images of `x₁`, `x₂`, and `x₃` under corresponding maps satisfy `D.v₁₂.τ₂(x₂) = D.L₁.g(x₃)` and `D.L₂.f(x₁) = D.v₁₂.τ₂(x₂)`, then `D.δ(x₃) = D.v₂₃.τ₁(x₁)`.
|