NYLL
Module

FiberStalkComparison.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiberStalkComparison
11 declarations indexed from sourceView source ↗

Module documentation

The geometric stalk of an extension fiber

The sheaf of lifts is the actual pullback over the chosen quotient section. Since geometric stalks preserve finite limits, its stalk is the fiber of the stalk homomorphism. The comparison uses the forgetful functor's filtered colimit comparison, preserving the original abelian group structures.

Imports8
  • Nyll.EtaleFundamentalGroups.Cohomology.ExtensionFibers
  • Mathlib.Algebra.Category.Grp.AB
  • Mathlib.Algebra.Category.Grp.Limits
  • Mathlib.AlgebraicGeometry.Sites.EtalePoint
  • Mathlib.CategoryTheory.Limits.Connected
  • Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
  • Mathlib.CategoryTheory.Limits.Types.Pullbacks
  • Mathlib.CategoryTheory.Sites.Point.Basic
Imported by2

Declarations

abbrev

fiberInclusion

L37 ↗
EtaleFundamentalGroups.Cohomology.fiberInclusion
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 fiberInclusion
def

fiberToPoint

L39 ↗
EtaleFundamentalGroups.Cohomology.fiberToPoint
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
def fiberToPoint :
    (extensionFiber S t).obj ⟶ (Functor.const X.Etaleᵒᵖ).obj PUnit where
  app _ := ↾fun _ => PUnit.unit
theorem

fiber_square

L43 ↗
EtaleFundamentalGroups.Cohomology.fiber_square
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 fiber_square :
    fiberInclusion S t ≫ Functor.whiskerRight S.g.hom (forget AddCommGrpCat.{u}) =
      fiberToPoint S t ≫ t
abbrev

fiberCone

L49 ↗
EtaleFundamentalGroups.Cohomology.fiberCone
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 fiberCone :
    PullbackCone (Functor.whiskerRight S.g.hom (forget AddCommGrpCat.{u})) t
def

fiberConeIsLimit

L53 ↗
EtaleFundamentalGroups.Cohomology.fiberConeIsLimit
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 fiberConeIsLimit : IsLimit (fiberCone S t)
def

constantUnitPresheafStalkIso

L80 ↗
EtaleFundamentalGroups.Cohomology.constantUnitPresheafStalkIso
Source context 6 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})
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def constantUnitPresheafStalkIso :
    (Scheme.pointSmallEtale ξ).presheafFiber.obj
      ((Functor.const X.Etaleᵒᵖ).obj PUnit.{u + 1}) ≅ PUnit.{u + 1}
def

quotientSectionSetStalk

L86 ↗
EtaleFundamentalGroups.Cohomology.quotientSectionSetStalk
Source context 6 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})
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def quotientSectionSetStalk :
    (Scheme.pointSmallEtale ξ).presheafFiber.obj (S.X₃.obj ⋙ forget AddCommGrpCat.{u})
def

fiberSetStalkEquiv

L91 ↗
EtaleFundamentalGroups.Cohomology.fiberSetStalkEquiv
Source context 6 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})
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def fiberSetStalkEquiv :
    (Scheme.pointSmallEtale ξ).sheafFiber.obj (extensionFiber S t) ≃
      {b : (Scheme.pointSmallEtale ξ).presheafFiber.obj
        (S.X₂.obj ⋙ forget AddCommGrpCat.{u}) //
        (Scheme.pointSmallEtale ξ).presheafFiber.map
          (Functor.whiskerRight S.g.hom (forget AddCommGrpCat.{u})) b =
            quotientSectionSetStalk S t ξ}
def

quotientSectionStalk

L117 ↗
EtaleFundamentalGroups.Cohomology.quotientSectionStalk
Documentation

The chosen global quotient section, evaluated in the actual abelian stalk.

Source context 6 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})
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · full declaration
def quotientSectionStalk :
    (Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj S.X₃ :=
  ((Scheme.pointSmallEtale ξ).sheafFiberCompIso (forget AddCommGrpCat.{u})).hom.app S.X₃
    (quotientSectionSetStalk S t ξ)
def

extensionFiberStalkEquiv

L123 ↗
EtaleFundamentalGroups.Cohomology.extensionFiberStalkEquiv
Documentation

Taking the geometric stalk commutes with taking the actual extension fiber.

Source context 6 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})
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
def extensionFiberStalkEquiv :
    (Scheme.pointSmallEtale ξ).sheafFiber.obj (extensionFiber S t) ≃
      {b : (Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj S.X₂ //
        (Scheme.pointSmallEtale ξ).sheafFiber.map S.g b = quotientSectionStalk S t ξ}
theorem

extensionFiberStalkEquiv_toFiber

L151 ↗
EtaleFundamentalGroups.Cohomology.extensionFiberStalkEquiv_toFiber
Documentation

On a representative germ the comparison is the canonical map into the original abelian stalk, applied to the original section.

Source context 6 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})
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
Lean source · statement
theorem extensionFiberStalkEquiv_toFiber (U : X.Etale)
    (x : (Scheme.pointSmallEtale ξ).fiber.obj U)
    (e : (extensionFiber S t).obj.obj (op U)) :
    (extensionFiberStalkEquiv S t ξ
      ((Scheme.pointSmallEtale ξ).toPresheafFiber U x (extensionFiber S t).obj e)).val =
      (Scheme.pointSmallEtale ξ).toPresheafFiber U x S.X₂.obj e.val

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.