NYLL
Module

PuncturedSpectrumCompletionDescentFrontier.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumCompletionDescentFrontier
11 declarations indexed from sourceView source ↗

Module documentation

Punctured spectra under maximal-adic completion

A local ring map which carries the source maximal ideal onto the target maximal ideal pulls the punctured spectrum back to the target punctured spectrum. This file packages the resulting cartesian square and its finite-etale pullback comparison.

For maximal-adic completion, purity of the completed ring therefore extends every cover from the original puncture after completion. Descending that completed extension is a separate algebraization problem; it is not assumed here.

Imports2
Imported by3

Declarations

instance

finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier

L32 ↗
AlgebraicGeometry.Scheme.finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier
Source context 4 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
Lean source · statement
instance finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
instance

finiteEtaleStableUnderBaseChangeAlongPuncturedSpectrumCompletionDescentFrontier

L38 ↗
AlgebraicGeometry.Scheme.finiteEtaleStableUnderBaseChangeAlongPuncturedSpectrumCompletionDescentFrontier
Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
Lean source · statement
instance finiteEtaleStableUnderBaseChangeAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
theorem

preimage_puncturedSpectrumOpen_of_map_maximalIdeal_eq

L47 ↗
AlgebraicGeometry.Scheme.preimage_puncturedSpectrumOpen_of_map_maximalIdeal_eq
Documentation

A local ring map which maps the maximal ideal onto the maximal ideal pulls the punctured open back to the punctured open.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
Lean source · statement
theorem preimage_puncturedSpectrumOpen_of_map_maximalIdeal_eq
    {R S : Type u} [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S]
    (f : R →+* S) [IsLocalHom f]
    (hmax : (maximalIdeal R).map f = maximalIdeal S) :
    Spec.map (CommRingCat.ofHom f) ⁻¹ᵁ puncturedSpectrumOpen R =
      puncturedSpectrumOpen S
def

puncturedSpectrumMorphismOfMapMaximalIdealEq

L87 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumMorphismOfMapMaximalIdealEq
Documentation

The morphism between punctured spectra induced by a local ring map whose maximal ideal extension is the target maximal ideal.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
Lean source · statement
def puncturedSpectrumMorphismOfMapMaximalIdealEq
    {R S : Type u} [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S]
    (f : R →+* S) [IsLocalHom f]
    (hmax : (maximalIdeal R).map f = maximalIdeal S) :
    puncturedSpectrum S ⟶ puncturedSpectrum R
theorem

puncturedSpectrumMorphismOfMapMaximalIdealEq_comp_inclusion

L100 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumMorphismOfMapMaximalIdealEq_comp_inclusion
Documentation

The punctured-spectrum morphism commutes with the two canonical open immersions into affine spectra.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
Lean source · statement
theorem puncturedSpectrumMorphismOfMapMaximalIdealEq_comp_inclusion
    {R S : Type u} [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S]
    (f : R →+* S) [IsLocalHom f]
    (hmax : (maximalIdeal R).map f = maximalIdeal S) :
    puncturedSpectrumMorphismOfMapMaximalIdealEq f hmax ≫
        puncturedSpectrumInclusion R =
      puncturedSpectrumInclusion S ≫
        Spec.map (CommRingCat.ofHom f)
theorem

puncturedSpectrumMorphismOfMapMaximalIdealEq_isPullback

L114 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumMorphismOfMapMaximalIdealEq_isPullback
Documentation

The square of a local affine morphism and the induced punctured-spectrum morphism is cartesian when the maximal ideal is obtained by extension.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
Lean source · statement
theorem puncturedSpectrumMorphismOfMapMaximalIdealEq_isPullback
    {R S : Type u} [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S]
    (f : R →+* S) [IsLocalHom f]
    (hmax : (maximalIdeal R).map f = maximalIdeal S) :
    IsPullback
      (puncturedSpectrumMorphismOfMapMaximalIdealEq f hmax)
      (puncturedSpectrumInclusion S)
      (puncturedSpectrumInclusion R)
      (Spec.map (CommRingCat.ofHom f))
def

puncturedSpectrumPullbackIsoOfMapMaximalIdealEq

L139 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumPullbackIsoOfMapMaximalIdealEq
Documentation

Restriction to the puncture commutes naturally with base change along a local map carrying the maximal ideal onto the maximal ideal.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
Lean source · statement
def puncturedSpectrumPullbackIsoOfMapMaximalIdealEq
    {R S : Type u} [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S]
    (f : R →+* S) [IsLocalHom f]
    (hmax : (maximalIdeal R).map f = maximalIdeal S) :
    AlgebraicGeometry.FiniteEtale.pullback
          (puncturedSpectrumInclusion R) ⋙
        AlgebraicGeometry.FiniteEtale.pullback
          (puncturedSpectrumMorphismOfMapMaximalIdealEq f hmax) ≅
      AlgebraicGeometry.FiniteEtale.pullback
          (Spec.map (CommRingCat.ofHom f)) ⋙
        AlgebraicGeometry.FiniteEtale.pullback
          (puncturedSpectrumInclusion S)
theorem

exists_extension_after_baseChange_of_hasPuncturedPurity

L167 ↗
AlgebraicGeometry.Scheme.exists_extension_after_baseChange_of_hasPuncturedPurity
Documentation

Purity on the target of a local map extends every cover of the source puncture after base change to the target puncture.

Source context 6 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongPuncturedSpectrumCompletionDescentFrontier
    {S T : Scheme.{u}} (f : S ⟶ T) :
    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_extension_after_baseChange_of_hasPuncturedPurity
    {R S : Type u} [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S]
    (f : R →+* S) [IsLocalHom f]
    (hmax : (maximalIdeal R).map f = maximalIdeal S)
    (hpurity : AlgebraicGeometry.FiniteEtale.HasPuncturedPurity S)
    (Y : AlgebraicGeometry.FiniteEtale (puncturedSpectrum R)) :
    ∃ X : AlgebraicGeometry.FiniteEtale (Spec (.of S)),
      Nonempty
        ((AlgebraicGeometry.FiniteEtale.pullback
            (puncturedSpectrumInclusion S)).obj X ≅
          (AlgebraicGeometry.FiniteEtale.pullback
            (puncturedSpectrumMorphismOfMapMaximalIdealEq f hmax)).obj Y)
def

maximalAdicCompletionPuncturedSpectrumMorphism

L195 ↗
EtaleFundamentalGroups.maximalAdicCompletionPuncturedSpectrumMorphism
Documentation

The map from the puncture of the maximal-adic completion to the original punctured spectrum.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace EtaleFundamentalGroups
universe u
open AlgebraicGeometry AlgebraicGeometry.Scheme
Lean source · statement
def maximalAdicCompletionPuncturedSpectrumMorphism
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    Scheme.puncturedSpectrum (AdicCompletion (maximalIdeal R) R) ⟶
      Scheme.puncturedSpectrum R
theorem

maximalAdicCompletionPuncturedSpectrumMorphism_isPullback

L205 ↗
EtaleFundamentalGroups.maximalAdicCompletionPuncturedSpectrumMorphism_isPullback
Documentation

The maximal-adic completion square with the two punctured-spectrum inclusions is cartesian.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace EtaleFundamentalGroups
universe u
open AlgebraicGeometry AlgebraicGeometry.Scheme
Lean source · statement
theorem maximalAdicCompletionPuncturedSpectrumMorphism_isPullback
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    IsPullback
      (maximalAdicCompletionPuncturedSpectrumMorphism R)
      (Scheme.puncturedSpectrumInclusion
        (AdicCompletion (maximalIdeal R) R))
      (Scheme.puncturedSpectrumInclusion R)
      (Spec.map (CommRingCat.ofHom
        (algebraMap R (AdicCompletion (maximalIdeal R) R))))
theorem

exists_maximalAdicCompletion_extension_of_hasPuncturedPurity

L221 ↗
EtaleFundamentalGroups.exists_maximalAdicCompletion_extension_of_hasPuncturedPurity
Documentation

If the maximal-adic completion has punctured purity, every finite-etale cover of the original puncture acquires an extension over the completed local spectrum after base change.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace EtaleFundamentalGroups
universe u
open AlgebraicGeometry AlgebraicGeometry.Scheme
Lean source · statement
theorem exists_maximalAdicCompletion_extension_of_hasPuncturedPurity
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hpurity : AlgebraicGeometry.FiniteEtale.HasPuncturedPurity
      (AdicCompletion (maximalIdeal R) R))
    (Y : AlgebraicGeometry.FiniteEtale (Scheme.puncturedSpectrum R)) :
    ∃ X : AlgebraicGeometry.FiniteEtale
        (Spec (.of (AdicCompletion (maximalIdeal R) R))),
      Nonempty
        ((AlgebraicGeometry.FiniteEtale.pullback
            (Scheme.puncturedSpectrumInclusion
              (AdicCompletion (maximalIdeal R) R))).obj X ≅
          (AlgebraicGeometry.FiniteEtale.pullback
            (maximalAdicCompletionPuncturedSpectrumMorphism R)).obj Y)

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