Module

ExtensionFiberPullback.lean

Nyll.EtaleFundamentalGroups.Cohomology.ExtensionFiberPullback

5 declarations indexed from sourceView source ↗

Module documentation

Inverse image of the actual sheaf of lifts

The lift sheaf of an abelian extension is pulled back using its categorical fiber square. The comparison uses the actual abelian inverse image and the actual underlying-set comparison; no compatibility is imposed as a hypothesis. The quotient section is transported explicitly.

Imports4

Nyll.EtaleFundamentalGroups.Cohomology.ExtensionFiberSquare
Nyll.EtaleFundamentalGroups.Cohomology.AbelianPullbackMate
Nyll.EtaleCohomology.Sites.SetPullbackExact
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Imported by2

def

extensionFiberTerminalPullbackIso

L32 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberTerminalPullbackIso

Documentation

The singleton sheaf is preserved by the actual inverse image.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits EtaleCohomology Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

def extensionFiberTerminalPullbackIso :
    (etaleSetPullback f).obj (extensionFiberTerminal Y) ≅ extensionFiberTerminal X

def

extensionFiberPullbackSection

L42 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberPullbackSection

Documentation

Transport the original quotient section through the actual inverse image.

Source context 6 commands

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

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

Lean source · statement

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

theorem

extensionFiber_pullback_isPullback

L51 ↗

EtaleFundamentalGroups.Cohomology.extensionFiber_pullback_isPullback

Documentation

The transported lift square remains a pullback.

Source context 6 commands

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

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

Lean source · statement

theorem extensionFiber_pullback_isPullback :
    IsPullback
      ((etaleSetPullback f).map (extensionFiberInclusion S t) ≫
        (abelianPullbackUnderlyingMateIso f).inv.app S.X₂)
      ((Sheaf.isTerminalTerminal X.smallEtaleTopology Types.isTerminalPUnit).from
        ((etaleSetPullback f).obj (extensionFiber S t)))
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).map
        ((etaleAbelianPullback f).map S.g))
      (extensionFiberPullbackSection f S t)

def

extensionFiberPullbackIso

L75 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberPullbackIso

Documentation

Actual set inverse image of the lift sheaf is the lift sheaf of the actual abelian inverse-image extension, over the transported quotient section.

Source context 6 commands

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

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

Lean source · statement

def extensionFiberPullbackIso :
    (etaleSetPullback f).obj (extensionFiber S t) ≅
      extensionFiber (S.map (etaleAbelianPullback f))
        (extensionFiberPullbackSection f S t).hom

theorem

extensionFiberPullbackIso_hom_inclusion

L84 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberPullbackIso_hom_inclusion

Documentation

The comparison preserves the original section of the middle sheaf.

Source context 6 commands

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

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

Lean source · statement

theorem extensionFiberPullbackIso_hom_inclusion :
    (extensionFiberPullbackIso f S t).hom ≫
        extensionFiberInclusion (S.map (etaleAbelianPullback f))
          (extensionFiberPullbackSection f S t).hom =
      (etaleSetPullback f).map (extensionFiberInclusion S t) ≫
        (abelianPullbackUnderlyingMateIso f).inv.app S.X₂

Module documentation

Inverse image of the actual sheaf of lifts

Declarations

extensionFiberTerminalPullbackIso

extensionFiberPullbackSection

extensionFiber_pullback_isPullback

extensionFiberPullbackIso

extensionFiberPullbackIso_hom_inclusion