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.forget₂ C Ab).PreservesZeroMorphisms]
(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.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
[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.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
[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_surjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
[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.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
[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.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
(S : CategoryTheory.ShortComplex C)
[S.HasHomology]
:
S.Exact ↔ (S.map (CategoryTheory.forget₂ C Ab)).Exact
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.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
(S : CategoryTheory.ShortComplex C)
[S.HasHomology]
:
S.Exact ↔ ∀ (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.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
[CategoryTheory.Limits.HasZeroObject C]
{S : CategoryTheory.ShortComplex C}
(hS : S.ShortExact)
:
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.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
[CategoryTheory.Limits.HasZeroObject C]
{S : CategoryTheory.ShortComplex C}
(hS : S.ShortExact)
:
Function.Surjective ⇑((CategoryTheory.forget₂ C Ab).map S.g)
noncomputable def
CategoryTheory.ShortComplex.cyclesMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
(S : CategoryTheory.ShortComplex C)
[S.HasHomology]
(x₂ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₂))
(hx₂ : ((CategoryTheory.forget₂ C Ab).map S.g) x₂ = 0)
:
↑((CategoryTheory.forget₂ C Ab).obj S.cycles)
Constructor for cycles of short complexes in a concrete category.
Equations
- S.cyclesMk x₂ hx₂ = (S.mapCyclesIso (CategoryTheory.forget₂ C Ab)).hom ((S.map (CategoryTheory.forget₂ C Ab)).abCyclesIso.inv ⟨x₂, hx₂⟩)
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.i_cyclesMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Preadditive C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(CategoryTheory.forget₂ C Ab).PreservesHomology]
(S : CategoryTheory.ShortComplex C)
[S.HasHomology]
(x₂ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₂))
(hx₂ : ((CategoryTheory.forget₂ C Ab).map S.g) x₂ = 0)
:
((CategoryTheory.forget₂ C Ab).map S.iCycles) (S.cyclesMk x₂ hx₂) = x₂
theorem
CategoryTheory.ShortComplex.SnakeInput.δ_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(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₁)
(h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃)
(h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂)
:
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.
theorem
CategoryTheory.ShortComplex.SnakeInput.δ_apply'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.HasForget₂ C Ab]
[CategoryTheory.Abelian C]
[(CategoryTheory.forget₂ C Ab).Additive]
[(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₁))
(h₂ : ((CategoryTheory.forget₂ C Ab).map D.L₁.g) x₂ = ((CategoryTheory.forget₂ C Ab).map D.v₀₁.τ₃) x₃)
(h₁ : ((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 lemma allows the computation of the connecting homomorphism
D.δ when D : SnakeInput C and C is a concrete category.