NYLL
Module

FiniteCechStalkLift.lean

Nyll.EtaleCohomology.Sites.FiniteCechStalkLift
3 declarations indexed from sourceView source ↗

Module documentation

A Čech-compatible section determines a germ downstairs

For a finite surjection, lift an algebraically closed geometric point using the same field. Invert the actual pullback stalk map at one lift. The Čech equation on the pair of any two lifts shows that this germ works at every lift, without assuming descent or a stalk-product surjectivity theorem.

Imports4
Imported by2

Declarations

theorem

unit_stalkComponent_isIso_of_lift

L29 ↗
EtaleCohomology.unit_stalkComponent_isIso_of_lift
Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
theorem unit_stalkComponent_isIso_of_lift
    {X Y : Scheme.{u}} (q : Y ⟶ X)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (t : Spec (CommRingCat.of Ω) ⟶ X)
    (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
    (Λ : Type u) [CommRing Λ]
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    IsIso ((Scheme.pointSmallEtale t).sheafFiber.map
        ((etalePullbackPushforwardAdjunction q Λ).unit.app F) ≫
      etalePushforwardStalkComponent q t s ((etalePullback q Λ).obj F))
theorem

globalSectionsMap_germ_of_lift

L42 ↗
EtaleCohomology.globalSectionsMap_germ_of_lift
Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
theorem globalSectionsMap_germ_of_lift
    {X Y : Scheme.{u}} (q : Y ⟶ X)
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (t : Spec (CommRingCat.of Ω) ⟶ X)
    (s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t})
    (Λ : Type u) [CommRing Λ]
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    etalePullbackGlobalSectionsMap q Λ F ≫
        etaleGlobalSectionsGerm s.val Λ ((etalePullback q Λ).obj F) =
      etaleGlobalSectionsGerm t Λ F ≫
        (Scheme.pointSmallEtale t).sheafFiber.map
          ((etalePullbackPushforwardAdjunction q Λ).unit.app F) ≫
        etalePushforwardStalkComponent q t s ((etalePullback q Λ).obj F)
theorem

exists_stalk_lift_of_finite_cech_compatible

L61 ↗
EtaleCohomology.exists_stalk_lift_of_finite_cech_compatible
Documentation

Every Čech-compatible global section on a finite surjective pullback comes from one germ downstairs at each algebraically closed geometric point. That germ agrees with the section at all lifts with the same field.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
theorem exists_stalk_lift_of_finite_cech_compatible
    {X Y : Scheme.{u}} (q : Y ⟶ X) [IsFinite q] [Surjective q]
    {Ω : Type u} [Field Ω] [IsAlgClosed Ω]
    (t : Spec (CommRingCat.of Ω) ⟶ X)
    (Λ : Type u) [CommRing Λ]
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ))
    (a : ((etalePullback q Λ).obj F).obj.obj (op (Scheme.Etale.mk (𝟙 Y))))
    (ha : etaleCechFirstSectionsMap q Λ F a = etaleCechSecondSectionsMap q Λ F a) :
    ∃ b : ToType ((Scheme.pointSmallEtale t).sheafFiber.obj F),
      ∀ s : {s : Spec (CommRingCat.of Ω) ⟶ Y // s ≫ q = t},
        ((Scheme.pointSmallEtale t).sheafFiber.map
            ((etalePullbackPushforwardAdjunction q Λ).unit.app F) ≫
          etalePushforwardStalkComponent q t s ((etalePullback q Λ).obj F)) b =
        etaleGlobalSectionsGerm s.val Λ ((etalePullback q Λ).obj F) a

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