Module

ExtensionFibers.lean

Nyll.EtaleFundamentalGroups.Cohomology.ExtensionFibers

7 declarations indexed from sourceView source ↗

Module documentation

Fibers of extensions of étale abelian sheaves

The inverse image of a global section of the quotient of a short exact sequence is an actual sheaf of sets. It has sections étale locally, and any section identifies that fiber with the kernel by translation. These are the local torsor constructions for the comparison with degree-one cohomology.

Imports9

Nyll.EtaleFundamentalGroups.Cohomology.H1Extensions
Mathlib.Algebra.Category.Grp.EpiMono
Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Mathlib.Algebra.Homology.ShortComplex.Ab
Mathlib.CategoryTheory.Sites.EpiMono
Mathlib.CategoryTheory.Sites.Limits
Mathlib.CategoryTheory.Sites.LocallySurjective
Mathlib.CategoryTheory.Sites.Subsheaf
Mathlib.CategoryTheory.Sites.Whiskering

Imported by5

lemma

section_naturality

L37 ↗

EtaleFundamentalGroups.Cohomology.section_naturality

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (S : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ S.X₃.obj ⋙ forget AddCommGrpCat.{u})

Lean source · statement

lemma section_naturality {U V : X.Etaleᵒᵖ} (f : U ⟶ V) :
    S.X₃.obj.map f (t.app U PUnit.unit) = t.app V PUnit.unit

abbrev

extensionFiberSubfunctor

L42 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberSubfunctor

Documentation

The sectionwise fiber of the quotient map over a global section.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (S : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ S.X₃.obj ⋙ forget AddCommGrpCat.{u})

Lean source · full declaration

abbrev extensionFiberSubfunctor : Subfunctor (S.X₂.obj ⋙ forget AddCommGrpCat.{u}) where
  obj U := {e | S.g.hom.app U e = t.app U PUnit.unit}
  map {U V} f e he := by
    change S.g.hom.app V (S.X₂.obj.map f e) = t.app V PUnit.unit
    have hn := ConcreteCategory.congr_hom (S.g.hom.naturality f) e
    change S.g.hom.app V (S.X₂.obj.map f e) =
      S.X₃.obj.map f (S.g.hom.app U e) at hn
    exact hn.trans ((congrArg (S.X₃.obj.map f) he).trans (section_naturality S t f))

theorem

extensionFiber_isSheaf

L53 ↗

EtaleFundamentalGroups.Cohomology.extensionFiber_isSheaf

Documentation

Equality with a fixed quotient section is local, so the sectionwise fiber is a sheaf, not merely a presheaf.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (S : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ S.X₃.obj ⋙ forget AddCommGrpCat.{u})

Lean source · statement

theorem extensionFiber_isSheaf :
    Presheaf.IsSheaf X.smallEtaleTopology (extensionFiberSubfunctor S t).toFunctor

abbrev

extensionFiber

L75 ↗

EtaleFundamentalGroups.Cohomology.extensionFiber

Documentation

The actual étale sheaf obtained as the inverse image of the quotient section.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (S : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ S.X₃.obj ⋙ forget AddCommGrpCat.{u})

Lean source · statement

abbrev extensionFiber : Sheaf X.smallEtaleTopology (Type u)

theorem

extensionFiber_locally_nonempty

L79 ↗

EtaleFundamentalGroups.Cohomology.extensionFiber_locally_nonempty

Documentation

Every quotient section of a short exact sequence lifts on an étale cover.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (S : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ S.X₃.obj ⋙ forget AddCommGrpCat.{u})

Lean source · statement

theorem extensionFiber_locally_nonempty (hS : S.ShortExact) (U : X.Etaleᵒᵖ) :
    Presheaf.imageSieve S.g.hom (t.app U PUnit.unit) ∈ X.smallEtaleTopology U.unop

lemma

sections_exact

L86 ↗

EtaleFundamentalGroups.Cohomology.sections_exact

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (S : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ S.X₃.obj ⋙ forget AddCommGrpCat.{u})

Lean source · statement

lemma sections_exact (hS : S.ShortExact) (U : X.Etaleᵒᵖ) :
    (S.map ((sheafSections X.smallEtaleTopology AddCommGrpCat).obj U)).Exact

theorem

extensionFiber_translation_bijective

L95 ↗

EtaleFundamentalGroups.Cohomology.extensionFiber_translation_bijective

Documentation

Translation by a chosen lift is bijective from the kernel sections to the fiber. The inverse is supplied by the actual kernel universal property.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (S : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ S.X₃.obj ⋙ forget AddCommGrpCat.{u})

Lean source · full declaration

theorem extensionFiber_translation_bijective (hS : S.ShortExact) (U : X.Etaleᵒᵖ)
    (e : {b : S.X₂.obj.obj U // S.g.hom.app U b = t.app U PUnit.unit}) :
    Function.Bijective (fun a : S.X₁.obj.obj U =>
      (⟨S.f.hom.app U a + e.val, by
        rw [map_add]
        have hz := ConcreteCategory.congr_hom
          (congrArg (fun k : S.X₁ ⟶ S.X₃ => k.hom.app U) S.zero) a
        change S.g.hom.app U (S.f.hom.app U a) = 0 at hz
        rw [hz, zero_add]
        exact e.property⟩ : {b : S.X₂.obj.obj U // S.g.hom.app U b = t.app U PUnit.unit})) := by
  have : Mono S.f := hS.mono_f
  have hm : Mono (S.f.hom.app U) := inferInstance
  have hi := (AddCommGrpCat.mono_iff_injective (S.f.hom.app U)).mp hm
  constructor
  · intro a b hab
    exact hi (add_right_cancel (congrArg Subtype.val hab))
  · intro z
    have hz : S.g.hom.app U (z.val - e.val) = 0 := by
      rw [map_sub, z.property, e.property, sub_self]
    obtain ⟨a, ha⟩ :=
      (ShortComplex.ab_exact_iff _).mp (sections_exact S hS U) (z.val - e.val) hz
    refine ⟨a, Subtype.ext ?_⟩
    change S.f.hom.app U a + e.val = z.val
    exact (congrArg (fun q => q + e.val) ha).trans (sub_add_cancel z.val e.val)

Module documentation

Fibers of extensions of étale abelian sheaves

Declarations

section_naturality

extensionFiberSubfunctor

extensionFiber_isSheaf

extensionFiber

extensionFiber_locally_nonempty

sections_exact

extensionFiber_translation_bijective