Module

ExtensionFiberSquare.lean

Nyll.EtaleFundamentalGroups.Cohomology.ExtensionFiberSquare

4 declarations indexed from sourceView source ↗

Module documentation

The sheaf of lifts is an actual categorical fiber

The sectionwise construction used for extension monodromy satisfies the pullback universal property in the category of étale sheaves. This allows exact inverse image to transport the original sheaf of lifts.

Imports5

Nyll.EtaleFundamentalGroups.Cohomology.ExtensionFibers
Mathlib.CategoryTheory.Limits.Types.Products
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Sites.Whiskering

Imported by3

def

extensionFiberTerminal

L30 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberTerminal

Documentation

The actual singleton sheaf, used as the source of a global section.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology

Lean source · statement

def extensionFiberTerminal (X : Scheme.{u}) : Sheaf X.smallEtaleTopology (Type u)

def

extensionFiberSection

L38 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberSection

Documentation

The original global quotient section, as a morphism from the singleton sheaf.

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

def extensionFiberSection :
    extensionFiberTerminal X ⟶
      (sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj S.X₃

def

extensionFiberInclusion

L44 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberInclusion

Documentation

Forget the condition on a section of the sheaf of lifts.

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

def extensionFiberInclusion :
    extensionFiber S t ⟶
      (sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj S.X₂

theorem

extensionFiber_isPullback

L50 ↗

EtaleFundamentalGroups.Cohomology.extensionFiber_isPullback

Documentation

The existing lift sheaf is the categorical inverse image of its 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

theorem extensionFiber_isPullback :
    IsPullback (extensionFiberInclusion S t)
      ((Sheaf.isTerminalTerminal X.smallEtaleTopology Types.isTerminalPUnit).from
        (extensionFiber S t))
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).map S.g)
      (extensionFiberSection S t)

Module documentation

The sheaf of lifts is an actual categorical fiber

Declarations

extensionFiberTerminal

extensionFiberSection

extensionFiberInclusion

extensionFiber_isPullback