NYLL
Module

FiniteSurjectiveDescent.lean

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

Module documentation

Descent of sections along arbitrary finite surjections

Čech-compatible sections give germs downstairs. Injectivity of the actual finite direct-image stalk comparison puts the direct-image section in the unit's image on every stalk. The unit is a monomorphism, so these local preimages glue uniquely.

Imports10
Imported by2

Declarations

theorem

exists_global_lift_of_geometricStalk_range

L35 ↗
EtaleCohomology.exists_global_lift_of_geometricStalk_range
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_global_lift_of_geometricStalk_range
    {X : Scheme.{u}} (Λ : Type u) [CommRing Λ]
    {F G : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)} (η : F ⟶ G) [Mono η]
    (a : G.obj.obj (op (Scheme.Etale.mk (𝟙 X))))
    (ha : ∀ (Ω : Type u) [Field Ω] [IsAlgClosed Ω]
      (t : Spec (CommRingCat.of Ω) ⟶ X),
      ∃ b : ToType ((Scheme.pointSmallEtale t).sheafFiber.obj F),
        (Scheme.pointSmallEtale t).sheafFiber.map η b = etaleGlobalSectionsGerm t Λ G a) :
    ∃ b : F.obj.obj (op (Scheme.Etale.mk (𝟙 X))),
      η.hom.app (op (Scheme.Etale.mk (𝟙 X))) b = a
theorem

etaleFiniteSurjective_globalSections_injective

L105 ↗
EtaleCohomology.etaleFiniteSurjective_globalSections_injective
Documentation

Pullback of global sections is injective along a finite surjection.

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 etaleFiniteSurjective_globalSections_injective
    {X Y : Scheme.{u}} (q : Y ⟶ X) [IsFinite q] [Surjective q]
    (Λ : Type u) [CommRing Λ]
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    Function.Injective (etalePullbackGlobalSectionsMap q Λ F)
theorem

existsUnique_globalSections_lift_of_finite_cech_compatible

L120 ↗
EtaleCohomology.existsUnique_globalSections_lift_of_finite_cech_compatible
Documentation

Every global section of inverse image satisfying the actual Čech equation descends uniquely along an arbitrary finite surjection of schemes.

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 existsUnique_globalSections_lift_of_finite_cech_compatible
    {X Y : Scheme.{u}} (q : Y ⟶ X) [IsFinite q] [Surjective q]
    (Λ : 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 : F.obj.obj (op (Scheme.Etale.mk (𝟙 X))),
      etalePullbackGlobalSectionsMap q Λ F b = a

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