Exactness of short complexes in concrete abelian categories #
If an additive concrete category C has an additive forgetful functor to Ab
which preserves homology, then a short complex S in C is exact
if and only if it is so after applying the functor forget₂ C Ab.
@[simp]
theorem
CategoryTheory.ShortComplex.zero_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Functor.PreservesZeroMorphisms (CategoryTheory.forget₂ C Ab)]
(S : CategoryTheory.ShortComplex C)
(x : ↑((CategoryTheory.forget₂ C Ab).obj S.X₁))
:
((CategoryTheory.forget₂ C Ab).map S.g) (((CategoryTheory.forget₂ C Ab).map S.f) x) = 0
theorem
CategoryTheory.Preadditive.mono_iff_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Limits.HasZeroObject C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.Mono f ↔ Function.Injective ⇑((CategoryTheory.forget₂ C Ab).map f)
theorem
CategoryTheory.Preadditive.mono_iff_injective'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Limits.HasZeroObject C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.Mono f ↔ Function.Injective ((CategoryTheory.forget C).map f)
theorem
CategoryTheory.Preadditive.epi_iff_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Limits.HasZeroObject C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.Epi f ↔ Function.Surjective ⇑((CategoryTheory.forget₂ C Ab).map f)
theorem
CategoryTheory.Preadditive.epi_iff_surjective'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Limits.HasZeroObject C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.Epi f ↔ Function.Surjective ((CategoryTheory.forget C).map f)
theorem
CategoryTheory.ShortComplex.exact_iff_exact_map_forget₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.ShortComplex.HasHomology S]
:
theorem
CategoryTheory.ShortComplex.exact_iff_of_concreteCategory
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.ShortComplex.HasHomology S]
:
CategoryTheory.ShortComplex.Exact S ↔ ∀ (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₂)),
((CategoryTheory.forget₂ C Ab).map S.g) x₂ = 0 →
∃ (x₁ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₁)), ((CategoryTheory.forget₂ C Ab).map S.f) x₁ = x₂
theorem
CategoryTheory.ShortComplex.ShortExact.injective_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Limits.HasZeroObject C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.ShortExact S)
:
Function.Injective ⇑((CategoryTheory.forget₂ C Ab).map S.f)
theorem
CategoryTheory.ShortComplex.ShortExact.surjective_g
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Limits.HasZeroObject C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.ShortExact S)
:
Function.Surjective ⇑((CategoryTheory.forget₂ C Ab).map S.g)
theorem
CategoryTheory.ShortComplex.SnakeInput.δ_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[CategoryTheory.Functor.Additive (CategoryTheory.forget₂ C Ab)]
[CategoryTheory.Functor.PreservesHomology (CategoryTheory.forget₂ C Ab)]
(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₁)
(h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃)
(h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂)
:
(CategoryTheory.ShortComplex.SnakeInput.δ D) x₃ = D.v₂₃.τ₁ x₁
This lemma allows the computation of the connecting homomorphism
D.δ when D : SnakeInput C and C is a concrete category.