theorem LongExactCohomology.up_rel (n : ℤ) : (ComplexShape.up ℤ).Rel n (n + 1)

The cochain shape relates n to n + 1.

noncomputable def LongExactCohomology.connectingHomomorphism {𝒜 : Type u} [CategoryTheory.Category.{v, u} 𝒜] [CategoryTheory.Abelian 𝒜] {S : CategoryTheory.ShortComplex (CochainComplex 𝒜 ℤ)} (hS : S.ShortExact) (n : ℤ) : HomologicalComplex.homology S.X₃ n ⟶ HomologicalComplex.homology S.X₁ (n + 1)

The connecting homomorphism H^n(C) → H^{n+1}(A) in cohomology arising from a short exact sequence of cochain complexes.

theorem LongExactCohomology.long_exact_seq_exact_at_H_A {𝒜 : Type u} [CategoryTheory.Category.{v, u} 𝒜] [CategoryTheory.Abelian 𝒜] {S : CategoryTheory.ShortComplex (CochainComplex 𝒜 ℤ)} (hS : S.ShortExact) (n : ℤ) : { X₁ := HomologicalComplex.homology S.X₃ n, X₂ := HomologicalComplex.homology S.X₁ (n + 1), X₃ := HomologicalComplex.homology S.X₂ (n + 1), f := connectingHomomorphism hS n, g := HomologicalComplex.homologyMap S.f (n + 1), zero := ⋯ }.Exact

Exactness of the long exact cohomology sequence at H^{n+1}(A) (Prop 42, Lec 23).

theorem LongExactCohomology.long_exact_seq_exact_at_H_B {𝒜 : Type u} [CategoryTheory.Category.{v, u} 𝒜] [CategoryTheory.Abelian 𝒜] {S : CategoryTheory.ShortComplex (CochainComplex 𝒜 ℤ)} (hS : S.ShortExact) (n : ℤ) : { X₁ := HomologicalComplex.homology S.X₁ n, X₂ := HomologicalComplex.homology S.X₂ n, X₃ := HomologicalComplex.homology S.X₃ n, f := HomologicalComplex.homologyMap S.f n, g := HomologicalComplex.homologyMap S.g n, zero := ⋯ }.Exact

Exactness of the long exact cohomology sequence at H^n(B).

theorem LongExactCohomology.long_exact_seq_exact_at_H_C {𝒜 : Type u} [CategoryTheory.Category.{v, u} 𝒜] [CategoryTheory.Abelian 𝒜] {S : CategoryTheory.ShortComplex (CochainComplex 𝒜 ℤ)} (hS : S.ShortExact) (n : ℤ) : { X₁ := HomologicalComplex.homology S.X₂ n, X₂ := HomologicalComplex.homology S.X₃ n, X₃ := HomologicalComplex.homology S.X₁ (n + 1), f := HomologicalComplex.homologyMap S.g n, g := connectingHomomorphism hS n, zero := ⋯ }.Exact

Exactness of the long exact cohomology sequence at H^n(C).

theorem LongExactCohomology.long_exact_cohomology_sequence {𝒜 : Type u} [CategoryTheory.Category.{v, u} 𝒜] [CategoryTheory.Abelian 𝒜] {S : CategoryTheory.ShortComplex (CochainComplex 𝒜 ℤ)} (hS : S.ShortExact) (n : ℤ) : { X₁ := HomologicalComplex.homology S.X₁ n, X₂ := HomologicalComplex.homology S.X₂ n, X₃ := HomologicalComplex.homology S.X₃ n, f := HomologicalComplex.homologyMap S.f n, g := HomologicalComplex.homologyMap S.g n, zero := ⋯ }.Exact ∧ { X₁ := HomologicalComplex.homology S.X₂ n, X₂ := HomologicalComplex.homology S.X₃ n, X₃ := HomologicalComplex.homology S.X₁ (n + 1), f := HomologicalComplex.homologyMap S.g n, g := connectingHomomorphism hS n, zero := ⋯ }.Exact ∧ { X₁ := HomologicalComplex.homology S.X₃ n, X₂ := HomologicalComplex.homology S.X₁ (n + 1), X₃ := HomologicalComplex.homology S.X₂ (n + 1), f := connectingHomomorphism hS n, g := HomologicalComplex.homologyMap S.f (n + 1), zero := ⋯ }.Exact

The long exact cohomology sequence: from a short exact sequence of cochain complexes, exactness holds at H^n(B), H^n(C), and H^{n+1}(A) (the snake lemma, Prop 42, Lec 23).