NYLL
Module

StalkFiber.lean

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

Module documentation

Translation torsors in geometric stalks of extensions

A fiber of a short exact sequence of abelian groups is a torsor for its actual kernel. Applying the exact geometric stalk functor gives this structure for extensions of étale abelian sheaves. No splitting of the extension is assumed: a point of each fiber is obtained from the surjective quotient map.

Imports7
  • Mathlib.Algebra.Category.Grp.AB
  • Mathlib.Algebra.Category.Grp.EpiMono
  • Mathlib.Algebra.Homology.ShortComplex.Ab
  • Mathlib.Algebra.Torsor.Basic
  • Mathlib.AlgebraicGeometry.Sites.EtalePoint
  • Mathlib.AlgebraicGeometry.Sites.AffineEtale
  • Mathlib.CategoryTheory.Sites.Point.Skyscraper
Imported by3

Declarations

abbrev

abelianExtensionFiber

L35 ↗
EtaleFundamentalGroups.Cohomology.abelianExtensionFiber
Documentation

The fiber of the actual quotient homomorphism in an abelian extension.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · statement
abbrev abelianExtensionFiber
def

fiberTranslate

L37 ↗
EtaleFundamentalGroups.Cohomology.fiberTranslate
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · statement
def fiberTranslate (a : S.X₁) (e : abelianExtensionFiber S z) :
    abelianExtensionFiber S z
theorem

exists_fiberDifference

L41 ↗
EtaleFundamentalGroups.Cohomology.exists_fiberDifference
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · statement
theorem exists_fiberDifference (hS : S.ShortExact)
    (e f : abelianExtensionFiber S z) :
    ∃ a : S.X₁, S.f a = e.val - f.val
def

fiberDifference

L47 ↗
EtaleFundamentalGroups.Cohomology.fiberDifference
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · statement
def fiberDifference (e f : abelianExtensionFiber S z) : S.X₁
theorem

fiberDifference_spec

L50 ↗
EtaleFundamentalGroups.Cohomology.fiberDifference_spec
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · statement
theorem fiberDifference_spec (hS : S.ShortExact)
    (e f : abelianExtensionFiber S z) :
    S.f (fiberDifference S hS z e f) = e.val - f.val
def

abelianExtensionFiberTorsor

L58 ↗
EtaleFundamentalGroups.Cohomology.abelianExtensionFiberTorsor
Documentation

Translation and the unique kernel difference make every quotient fiber a torsor. Both existence and uniqueness use the given short exact sequence.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · full declaration
def abelianExtensionFiberTorsor : AddTorsor S.X₁ (abelianExtensionFiber S z) where
  vadd := fiberTranslate S z
  zero_vadd e := Subtype.ext (by
    change S.f 0 + e.val = e.val
    rw [map_zero, zero_add])
  add_vadd a b e := Subtype.ext (by
    change S.f (a + b) + e.val = S.f a + (S.f b + e.val)
    rw [map_add, add_assoc])
  vsub := fiberDifference S hS z
  nonempty := by
    obtain ⟨e, he⟩ := (AddCommGrpCat.epi_iff_surjective S.g).mp hS.epi_g z
    exact ⟨⟨e, he⟩⟩
  vsub_vadd' e f := Subtype.ext (by
    change S.f (fiberDifference S hS z e f) + f.val = e.val
    rw [fiberDifference_spec S z hS, sub_add_cancel])
  vadd_vsub' a e := by
    apply (AddCommGrpCat.mono_iff_injective S.f).mp hS.mono_f
    exact (fiberDifference_spec S z hS (fiberTranslate S z a e) e).trans
      (add_sub_cancel_right (S.f a) e.val)
theorem

abelianExtensionFiberTorsor_vadd

L79 ↗
EtaleFundamentalGroups.Cohomology.abelianExtensionFiberTorsor_vadd
Documentation

The torsor action is the original inclusion followed by addition.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · full declaration
theorem abelianExtensionFiberTorsor_vadd (a : S.X₁) (e : abelianExtensionFiber S z) :
    let := abelianExtensionFiberTorsor S hS z
    (a +ᵥ e).val = S.f a + e.val := rfl
theorem

shortExact_geometricStalk

L84 ↗
EtaleFundamentalGroups.Cohomology.shortExact_geometricStalk
Documentation

Geometric stalks preserve the short exact sequence itself.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · statement
theorem shortExact_geometricStalk {X : Scheme.{u}} {Ω : Type u}
    [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
    (E : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
    (hE : E.ShortExact) :
    (E.map (Scheme.pointSmallEtale ξ).sheafFiber).ShortExact
def

geometricStalkFiberTorsor

L94 ↗
EtaleFundamentalGroups.Cohomology.geometricStalkFiberTorsor
Documentation

A quotient fiber in the actual geometric stalk is a torsor for the actual kernel stalk; the required exactness is proved by the stalk functor.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · statement
def geometricStalkFiberTorsor {X : Scheme.{u}} {Ω : Type u}
    [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)
    (E : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
    (hE : E.ShortExact)
    (z : (Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj E.X₃) :
    AddTorsor ((Scheme.pointSmallEtale ξ).sheafFiber (A := AddCommGrpCat.{u}) |>.obj E.X₁)
      (abelianExtensionFiber (E.map (Scheme.pointSmallEtale ξ).sheafFiber) z)
def

extensionFiberTransportTorsor

L107 ↗
EtaleFundamentalGroups.Cohomology.extensionFiberTransportTorsor
Documentation

Transfer the actual kernel translations along specified coefficient and fiber isomorphisms. The multiplicative tag permits a group action to commute with these additive translations without changing the coefficient group.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · statement
def extensionFiberTransportTorsor (A : AddCommGrpCat.{u}) (eA : A ≅ S.X₁)
    {P : Type u} (eP : P ≃ abelianExtensionFiber S z) :
    Torsor (Multiplicative A) P
theorem

extensionFiberTransportTorsor_smul

L136 ↗
EtaleFundamentalGroups.Cohomology.extensionFiberTransportTorsor_smul
Documentation

The transferred action still translates by the same original inclusion.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable (S : ShortComplex AddCommGrpCat.{u}) (hS : S.ShortExact) (z : S.X₃)
Lean source · full declaration
theorem extensionFiberTransportTorsor_smul (A : AddCommGrpCat.{u}) (eA : A ≅ S.X₁)
    {P : Type u} (eP : P ≃ abelianExtensionFiber S z) (a : Multiplicative A) (p : P) :
    let := extensionFiberTransportTorsor S hS z A eA eP
    (eP (a • p)).val = S.f (eA.hom a.toAdd) + (eP p).val := by
  change (eP (eP.symm (fiberTranslate S z (eA.hom a.toAdd) (eP p)))).val = _
  rw [eP.apply_symm_apply]
  rfl

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