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}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Limits.HasZeroMorphisms C]
[(forget₂ C Ab).PreservesZeroMorphisms]
(S : ShortComplex C)
(x : ↑((forget₂ C Ab).obj S.X₁))
:
theorem
CategoryTheory.Preadditive.mono_iff_injective
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
[Limits.HasZeroObject C]
{X Y : C}
(f : X ⟶ Y)
:
Mono f ↔ Function.Injective ⇑((forget₂ C Ab).map f)
theorem
CategoryTheory.Preadditive.mono_iff_injective'
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
[Limits.HasZeroObject C]
{X Y : C}
(f : X ⟶ Y)
:
Mono f ↔ Function.Injective ((forget C).map f)
theorem
CategoryTheory.Preadditive.epi_iff_surjective
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
[Limits.HasZeroObject C]
{X Y : C}
(f : X ⟶ Y)
:
Epi f ↔ Function.Surjective ⇑((forget₂ C Ab).map f)
theorem
CategoryTheory.Preadditive.epi_iff_surjective'
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
[Limits.HasZeroObject C]
{X Y : C}
(f : X ⟶ Y)
:
Epi f ↔ Function.Surjective ((forget C).map f)
theorem
CategoryTheory.ShortComplex.exact_iff_exact_map_forget₂
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
(S : ShortComplex C)
[S.HasHomology]
:
theorem
CategoryTheory.ShortComplex.exact_iff_of_hasForget
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
(S : ShortComplex C)
[S.HasHomology]
:
theorem
CategoryTheory.ShortComplex.ShortExact.injective_f
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
{S : ShortComplex C}
[Limits.HasZeroObject C]
(hS : S.ShortExact)
:
Function.Injective ⇑((forget₂ C Ab).map S.f)
theorem
CategoryTheory.ShortComplex.ShortExact.surjective_g
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
{S : ShortComplex C}
[Limits.HasZeroObject C]
(hS : S.ShortExact)
:
Function.Surjective ⇑((forget₂ C Ab).map S.g)
noncomputable def
CategoryTheory.ShortComplex.cyclesMk
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
(S : ShortComplex C)
[S.HasHomology]
(x₂ : ↑((forget₂ C Ab).obj S.X₂))
(hx₂ : ((forget₂ C Ab).map S.g) x₂ = 0)
:
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}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
(S : ShortComplex C)
[S.HasHomology]
(x₂ : ↑((forget₂ C Ab).obj S.X₂))
(hx₂ : ((forget₂ C Ab).map S.g) x₂ = 0)
:
theorem
CategoryTheory.ShortComplex.SnakeInput.δ_apply
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Abelian C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
(D : SnakeInput C)
(x₃ : (forget C).obj D.L₀.X₃)
(x₂ : (forget C).obj D.L₁.X₂)
(x₁ : (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}
[Category.{v, u} C]
[HasForget C]
[HasForget₂ C Ab]
[Abelian C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
(D : SnakeInput C)
(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₂)
:
This lemma allows the computation of the connecting homomorphism
D.δ when D : SnakeInput C and C is a concrete category.