Module

ExtensionPresentation.lean

Nyll.EtaleCohomology.Constructible.ExtensionPresentation

1 declaration indexed from sourceView source ↗

Module documentation

A cokernel presentation of an extension

If an epimorphism onto the quotient of a short exact sequence lifts to its middle term, the middle term is a cokernel of a map from the kernel of that epimorphism to the sum of its source and the subobject. This supplies the presentation used in the local constancy proof for extensions.

Imports3

Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.CategoryTheory.Abelian.Basic
Mathlib.CategoryTheory.Preadditive.Biproducts

Imported by2

theorem

exists_extension_cokernel_presentation

L25 ↗

EtaleCohomology.exists_extension_cokernel_presentation

Documentation

A lifted epimorphism gives an actual cokernel presentation of the middle term.

Source context 3 commands

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

noncomputable section
open CategoryTheory Limits
namespace EtaleCohomology

Lean source · statement

theorem exists_extension_cokernel_presentation
    {C : Type*} [Category* C] [Abelian C]
    (S : ShortComplex C) (hS : S.ShortExact)
    {P : C} (q : P ⟶ S.X₃) [Epi q] (t : P ⟶ S.X₂) (ht : t ≫ S.g = q) :
    ∃ a : kernel q ⟶ S.X₁ ⊞ P, Nonempty (cokernel a ≅ S.X₂)

Module documentation

A cokernel presentation of an extension

Declarations

exists_extension_cokernel_presentation