Module

GaloisSections.lean

Nyll.EtaleCohomology.Sites.GaloisSections

8 declarations indexed from sourceView source ↗

Module documentation

Actual Galois descent of small-etale sheaf sections

A section on a finite etale Galois cover descends exactly when it is fixed by its deck transformations. The proof uses actual sheaf descent and the proved decomposition of the cover's self-product into deck graphs. No Galois/etale cohomology comparison is assumed.

Imports7

Nyll.EtaleFundamentalGroups.GaloisCovers.SelfProduct
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
Nyll.SchemeTheory.FiniteEtale.Forget.FiniteLimits
Nyll.SchemeTheory.FiniteEtale.Forget.FiniteCoproducts
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Imported by2

abbrev

finiteEtaleInclusion

L32 ↗

EtaleCohomology.finiteEtaleInclusion

Documentation

The canonical inclusion of finite etale objects into the small etale site.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace EtaleCohomology

Lean source · statement

abbrev finiteEtaleInclusion (X : Scheme.{u}) : FiniteEtale X ⥤ X.Etale

instance

finiteEtaleInclusion_preservesFiniteLimits

L38 ↗

EtaleCohomology.finiteEtaleInclusion_preservesFiniteLimits

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace EtaleCohomology

Lean source · statement

instance finiteEtaleInclusion_preservesFiniteLimits (X : Scheme.{u}) :
    PreservesFiniteLimits (finiteEtaleInclusion X)

abbrev

finiteEtaleCoverBaseMap

L50 ↗

EtaleCohomology.finiteEtaleCoverBaseMap

Documentation

The actual structure map of a finite etale object to the base site object.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace EtaleCohomology

Lean source · statement

abbrev finiteEtaleCoverBaseMap (X : Scheme.{u}) (Y : FiniteEtale X) :
    (finiteEtaleInclusion X).obj Y ⟶ Scheme.Etale.mk (𝟙 X)

theorem

finiteEtaleCoverBaseMap_covering

L55 ↗

EtaleCohomology.finiteEtaleCoverBaseMap_covering

Documentation

A surjective finite etale structure map is a singleton cover of the base.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace EtaleCohomology

Lean source · statement

theorem finiteEtaleCoverBaseMap_covering (X : Scheme.{u}) (Y : FiniteEtale X)
    [Surjective Y.hom] :
    Sieve.generate (Presieve.singleton (finiteEtaleCoverBaseMap X Y)) ∈
      X.smallEtaleTopology (Scheme.Etale.mk (𝟙 X))

theorem

finiteEtaleSheaf_restrict_injective

L76 ↗

EtaleCohomology.finiteEtaleSheaf_restrict_injective

Documentation

Restriction to an actual finite etale surjective cover is injective.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace EtaleCohomology

Lean source · statement

theorem finiteEtaleSheaf_restrict_injective
    (X : Scheme.{u}) (F : Sheaf X.smallEtaleTopology (Type u))
    (Y : FiniteEtale X) [Surjective Y.hom] :
    Function.Injective (F.obj.map (finiteEtaleCoverBaseMap X Y).op)

theorem

finiteEtaleSheaf_restrict_invariant

L88 ↗

EtaleCohomology.finiteEtaleSheaf_restrict_invariant

Documentation

A section pulled back from the base is fixed by every actual deck transformation.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace EtaleCohomology

Lean source · statement

theorem finiteEtaleSheaf_restrict_invariant
    (X : Scheme.{u}) (F : Sheaf X.smallEtaleTopology (Type u))
    (Y : FiniteEtale X) (t : F.obj.obj (op (Scheme.Etale.mk (𝟙 X))))
    (σ : Aut Y) :
    F.obj.map ((finiteEtaleInclusion X).map σ.hom).op
      (F.obj.map (finiteEtaleCoverBaseMap X Y).op t) =
        F.obj.map (finiteEtaleCoverBaseMap X Y).op t

theorem

finiteEtale_sheaf_coproduct_sections_ext

L103 ↗

EtaleCohomology.finiteEtale_sheaf_coproduct_sections_ext

Documentation

Sections on the actual finite coproduct are determined by their restrictions to its summands. Covering is proved on the underlying schemes.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace EtaleCohomology

Lean source · statement

theorem finiteEtale_sheaf_coproduct_sections_ext
    (X : Scheme.{u}) (F : Sheaf X.smallEtaleTopology (Type u))
    {ι : Type v} [Finite ι] (A : ι → FiniteEtale X)
    (s t : F.obj.obj (op ((finiteEtaleInclusion X).obj (∐ A))))
    (h : ∀ i, F.obj.map ((finiteEtaleInclusion X).map (Sigma.ι A i)).op s =
      F.obj.map ((finiteEtaleInclusion X).map (Sigma.ι A i)).op t) : s = t

theorem

existsUnique_section_of_galois_invariant

L129 ↗

EtaleCohomology.existsUnique_section_of_galois_invariant

Documentation

Every deck-invariant section on an actual finite etale Galois cover descends uniquely to the base in the actual small etale sheaf.

Source context 5 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory Limits Opposite
open CategoryTheory.PreGaloisCategory
namespace EtaleCohomology

Lean source · statement

theorem existsUnique_section_of_galois_invariant
    (X : Scheme.{u}) [ConnectedSpace X]
    (F : Sheaf X.smallEtaleTopology (Type u))
    (Y : FiniteEtale X) [IsGalois Y]
    (s : F.obj.obj (op ((finiteEtaleInclusion X).obj Y)))
    (hs : ∀ σ : Aut Y,
      F.obj.map ((finiteEtaleInclusion X).map σ.hom).op s = s) :
    ∃! t : F.obj.obj (op (Scheme.Etale.mk (𝟙 X))),
      F.obj.map (finiteEtaleCoverBaseMap X Y).op t = s

Module documentation

Actual Galois descent of small-etale sheaf sections

Declarations