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]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[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]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
[Limits.HasZeroObject C]
{X Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.Preadditive.mono_iff_injective'
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
[Limits.HasZeroObject C]
{X Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.Preadditive.epi_iff_surjective
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
[Limits.HasZeroObject C]
{X Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.Preadditive.epi_iff_surjective'
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
[Limits.HasZeroObject C]
{X Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.ShortComplex.exact_iff_exact_map_forget₂
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[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]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[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]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
{S : ShortComplex C}
[Limits.HasZeroObject C]
(hS : S.ShortExact)
:
Function.Injective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map S.f))
theorem
CategoryTheory.ShortComplex.ShortExact.surjective_g
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasForget₂ C Ab]
[Preadditive C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
{S : ShortComplex C}
[Limits.HasZeroObject C]
(hS : S.ShortExact)
:
Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map S.g))
noncomputable def
CategoryTheory.ShortComplex.cyclesMk
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[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₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0)
:
Constructor for cycles of short complexes in a concrete category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.i_cyclesMk
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[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₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0)
:
theorem
CategoryTheory.ShortComplex.SnakeInput.δ_apply
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[HasForget₂ C Ab]
[Abelian C]
[(forget₂ C Ab).Additive]
[(forget₂ C Ab).PreservesHomology]
(D : SnakeInput C)
(x₃ : ToType D.L₀.X₃)
(x₂ : ToType D.L₁.X₂)
(x₁ : ToType D.L₂.X₁)
(h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃)
(h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom 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]
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[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₂ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃)
(h₁ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₂.f)) x₁ = (ConcreteCategory.hom ((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.