Nyll.EtaleFundamentalGroups.Cohomology.ExtensionComparison

Module documentation

Comparing representatives of a degree-one extension class

Compatibility of the actual derived extension classes with a kernel map gives a morphism of short exact sequences which is the identity on the quotient. The morphism is constructed using the two Ext exact sequences: first extend the kernel map, then correct the induced quotient endomorphism. Thus independence of a chosen extension representative does not require an additional comparison assumption.

theorem

exists_extension_comparison_of_extClass_naturality

L32 ↗

EtaleFundamentalGroups.Cohomology.exists_extension_comparison_of_extClass_naturality

Documentation

Compatibility of derived extension classes gives a comparison with the specified kernel map and identity quotient map. In particular, equal classes have an isomorphism inducing the identity on both endpoints.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.Abelian
universe w v u
namespace EtaleFundamentalGroups.Cohomology

Lean source · statement

theorem exists_extension_comparison_of_extClass_naturality
    {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
    {K₁ K₂ Q E₁ E₂ : C} (α : K₁ ⟶ K₂)
    (i₁ : K₁ ⟶ E₁) (p₁ : E₁ ⟶ Q) (z₁ : i₁ ≫ p₁ = 0)
    (i₂ : K₂ ⟶ E₂) (p₂ : E₂ ⟶ Q) (z₂ : i₂ ≫ p₂ = 0)
    (h₁ : (ShortComplex.mk i₁ p₁ z₁).ShortExact)
    (h₂ : (ShortComplex.mk i₂ p₂ z₂).ShortExact)
    (he : h₁.extClass.comp (Ext.mk₀ α) (add_zero 1) = h₂.extClass) :
    ∃ f : E₁ ⟶ E₂, i₁ ≫ f = α ≫ i₂ ∧ f ≫ p₂ = p₁

Module documentation

Comparing representatives of a degree-one extension class

Declarations

exists_extension_comparison_of_extClass_naturality