EtaleFundamentalGroups.Cohomology.extClass_eq_zero_iff_exists_section
The connecting class is zero exactly when the short exact sequence splits on its quotient. The section is obtained from the actual Ext exact sequence.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Abelian
universe w v u
namespace EtaleFundamentalGroups.CohomologyLean source · statement
theorem extClass_eq_zero_iff_exists_section
{C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
{S : ShortComplex C} (hS : S.ShortExact) :
hS.extClass = 0 ↔ ∃ s : S.X₃ ⟶ S.X₂, s ≫ S.g = 𝟙 S.X₃