Module

H1Extensions.lean

Nyll.EtaleFundamentalGroups.Cohomology.H1Extensions

5 declarations indexed from sourceView source ↗

Module documentation

Extensions representing étale cohomology in degree one

Every class in the existing derived-functor étale cohomology Sheaf.H F 1 is represented by a short exact sequence with kernel F and quotient the constant integer sheaf. The sequence is constructed by embedding F into an injective sheaf, lifting the class through the connecting morphism, and taking an actual pullback. No extension or cohomology comparison is assumed.

This is the extension construction used in the comparison of degree-one cohomology with torsors; it does not yet assert the fundamental-group comparison.

Imports10

Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.CategoryTheory.Abelian.Basic
Mathlib.CategoryTheory.Preadditive.Injective.Basic
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Mathlib.Algebra.Category.Grp.AB
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt

Imported by3

abbrev

pullbackExtension

L39 ↗

EtaleFundamentalGroups.Cohomology.pullbackExtension

Source context 4 commands

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

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

Lean source · statement

abbrev pullbackExtension {C : Type u} [Category.{v} C] [Abelian C]
    (S : ShortComplex C) {Y : C} (f : Y ⟶ S.X₃) : ShortComplex C

lemma

pullbackExtension_shortExact

L45 ↗

EtaleFundamentalGroups.Cohomology.pullbackExtension_shortExact

Source context 4 commands

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

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

Lean source · statement

lemma pullbackExtension_shortExact
    {C : Type u} [Category.{v} C] [Abelian C]
    {S : ShortComplex C} (hS : S.ShortExact) {Y : C} (f : Y ⟶ S.X₃) :
    (pullbackExtension S f).ShortExact

def

pullbackExtensionMap

L72 ↗

EtaleFundamentalGroups.Cohomology.pullbackExtensionMap

Source context 4 commands

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

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

Lean source · full declaration

def pullbackExtensionMap {C : Type u} [Category.{v} C] [Abelian C]
    (S : ShortComplex C) {Y : C} (f : Y ⟶ S.X₃) : pullbackExtension S f ⟶ S where
  τ₁ := 𝟙 S.X₁
  τ₂ := pullback.fst S.g f
  τ₃ := f
  comm₁₂ := by
    change 𝟙 S.X₁ ≫ S.f = _
    rw [Category.id_comp, pullback.lift_fst]
  comm₂₃ := pullback.condition

theorem

exists_extension_of_ext_one

L82 ↗

EtaleFundamentalGroups.Cohomology.exists_extension_of_ext_one

Source context 4 commands

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

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

Lean source · statement

theorem exists_extension_of_ext_one
    {C : Type u} [Category.{v} C] [Abelian C] [EnoughInjectives C] [HasExt.{w} C]
    {X Y : C} (a : Ext.{w} X Y 1) :
    ∃ (E : C) (i : Y ⟶ E) (p : E ⟶ X) (h : i ≫ p = 0)
      (hs : (ShortComplex.mk i p h).ShortExact), hs.extClass = a

theorem

exists_h1_extension

L110 ↗

EtaleFundamentalGroups.Cohomology.exists_h1_extension

Documentation

Every actual étale H¹ class is represented by a short exact extension of the constant integer sheaf. This needs no connectedness, finiteness, normality, or hypothesis on the characteristic of the scheme.

Source context 4 commands

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

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

Lean source · statement

theorem exists_h1_extension (X : Scheme.{u})
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}) (a : Sheaf.H.{u} F 1) :
    ∃ (E : Sheaf X.smallEtaleTopology AddCommGrpCat.{u})
      (i : F ⟶ E)
      (p : E ⟶ (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (ULift.{u} ℤ)))
      (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact), hs.extClass = a

Module documentation

Extensions representing étale cohomology in degree one

Declarations

pullbackExtension

pullbackExtension_shortExact

pullbackExtensionMap

exists_extension_of_ext_one

exists_h1_extension