noncomputable def
LongExactSequence.cohomologyδ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i j : ι)
(hij : c.Rel i j)
:
The connecting homomorphism H_i(C) → H_j(A) of the long exact homology
sequence arising from a short exact sequence of complexes.
Instances For
theorem
LongExactSequence.long_exact_sequence_exact_at_Hi_B
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i : ι)
:
Exactness of the long exact sequence at H_i(B).
theorem
LongExactSequence.long_exact_sequence_exact_at_Hi_C
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i j : ι)
(hij : c.Rel i j)
:
Exactness of the long exact sequence at H_i(C).
theorem
LongExactSequence.long_exact_sequence_exact_at_Hj_A
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i j : ι)
(hij : c.Rel i j)
:
Exactness of the long exact sequence at H_j(A).
theorem
LongExactSequence.long_exact_sequence
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i j : ι)
(hij : c.Rel i j)
:
{ X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact ∧ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
g := hS.δ i j hij, zero := ⋯ }.Exact ∧ { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.Exact
The long exact (co)homology sequence: from a short exact sequence of complexes,
exactness holds at H_i(B), H_i(C), and H_j(A).
theorem
LongExactSequence.mono_cohomologyδ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i j : ι)
(hij : c.Rel i j)
(hi : CategoryTheory.Limits.IsZero (S.X₂.homology i))
:
CategoryTheory.Mono (cohomologyδ hS i j hij)
If H_i(B) = 0, the connecting homomorphism δ is a monomorphism.
theorem
LongExactSequence.epi_cohomologyδ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i j : ι)
(hij : c.Rel i j)
(hj : CategoryTheory.Limits.IsZero (S.X₂.homology j))
:
CategoryTheory.Epi (cohomologyδ hS i j hij)
If H_j(B) = 0, the connecting homomorphism δ is an epimorphism.
theorem
LongExactSequence.isIso_cohomologyδ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{ι : Type u_1}
{c : ComplexShape ι}
{S : CategoryTheory.ShortComplex (HomologicalComplex C c)}
(hS : S.ShortExact)
(i j : ι)
(hij : c.Rel i j)
(hi : CategoryTheory.Limits.IsZero (S.X₂.homology i))
(hj : CategoryTheory.Limits.IsZero (S.X₂.homology j))
:
CategoryTheory.IsIso (cohomologyδ hS i j hij)
If both H_i(B) and H_j(B) vanish, the connecting δ is an isomorphism.