Module

GenericComplementCoverExtension.lean

Nyll.EtaleFundamentalGroups.Purity.GenericComplementCoverExtension

4 declarations indexed from sourceView source ↗

Module documentation

Local cover extensions at generic boundary points

At a generic point of an irreducible component of the complement, the actual overlap of the local spectrum with the open is its puncture. Local purity therefore supplies an extending cover, retaining an isomorphism on the original overlap. This is the local input for Stacks 0EY7.

Imports3

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrum
Nyll.SchemeTheory.LocalGeometry.GenericComplementPuncture
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Imported by2

instance

finiteEtaleOverCategoryGenericCover

L28 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryGenericCover

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

instance finiteEtaleOverCategoryGenericCover (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X)

instance

finiteEtaleHasPullbacksAlongGenericCover

L32 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongGenericCover

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryGenericCover (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X

Lean source · statement

instance finiteEtaleHasPullbacksAlongGenericCover
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

instance

finiteEtaleStableUnderBaseChangeAlongGenericCover

L38 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongGenericCover

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryGenericCover (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongGenericCover
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩

Lean source · statement

instance finiteEtaleStableUnderBaseChangeAlongGenericCover
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f

theorem

exists_stalk_cover_extension_of_generic_complement

L47 ↗

AlgebraicGeometry.FiniteEtale.exists_stalk_cover_extension_of_generic_complement

Documentation

Purity at a generic boundary point extends the actual pulled-back cover over its local spectrum, with the comparison on the original open overlap.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryGenericCover (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongGenericCover
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongGenericCover
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩

Lean source · statement

theorem exists_stalk_cover_extension_of_generic_complement
    {X : Scheme.{u}} (U : X.Opens)
    (x : genericPoints {z : X // z ∉ U})
    (hpurity : HasPuncturedPurity (X.presheaf.stalk x.1.1))
    (V : FiniteEtale U.toScheme) :
    ∃ W : FiniteEtale (Spec (X.presheaf.stalk x.1.1)),
      Nonempty
        ((pullback (Limits.pullback.fst (X.fromSpecStalk x.1.1) U.ι)).obj W ≅
          (pullback (Limits.pullback.snd (X.fromSpecStalk x.1.1) U.ι)).obj V)

Module documentation

Local cover extensions at generic boundary points

Declarations

finiteEtaleOverCategoryGenericCover

finiteEtaleHasPullbacksAlongGenericCover

finiteEtaleStableUnderBaseChangeAlongGenericCover

exists_stalk_cover_extension_of_generic_complement