NYLL
Module

PuncturedSpectrumCech.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumCech
30 declarations indexed from sourceView source ↗

Module documentation

Pairwise intersections in the principal cover of a punctured spectrum

This file gives the first Cech-level data for the finite principal affine cover of a punctured local spectrum. A pairwise intersection is identified with the spectrum of the localization away from the product of the two generators. The two projections and the associated pullback functors on finite etale covers are exposed explicitly for later descent constructions.

Imports2
Imported by2

Declarations

instance

finiteEtaleHasPullbacksAlongCech

L28 ↗
AlgebraicGeometry.Scheme.finiteEtaleHasPullbacksAlongCech
Source context 4 commands

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

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

finiteEtaleStableUnderBaseChangeAlongCech

L34 ↗
AlgebraicGeometry.Scheme.finiteEtaleStableUnderBaseChangeAlongCech
Source context 5 commands

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

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

puncturedSpectrumOverlap

L45 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlap
Documentation

The pairwise intersection of two members of the principal cover of the punctured spectrum.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumOverlap
    (i j : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrum R).Opens
def

puncturedSpectrumAmbientOverlap

L52 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientOverlap
Documentation

The corresponding ambient principal open, cut out by the product of the two chosen generators.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumAmbientOverlap
    (i j : puncturedSpectrumGeneratorIndex R) :
    (Spec (.of R)).Opens
theorem

puncturedSpectrumAmbientOverlap_le

L60 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientOverlap_le
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumAmbientOverlap_le
    (i j : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumAmbientOverlap R i j ≤ puncturedSpectrumOpen R
theorem

puncturedSpectrumOverlap_eq_preimage_ambient

L71 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlap_eq_preimage_ambient
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumOverlap_eq_preimage_ambient
    (i j : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumOverlap R i j =
      (puncturedSpectrumOpen R).ι ⁻¹ᵁ
        puncturedSpectrumAmbientOverlap R i j
def

puncturedSpectrumOverlapIsoSpecAwayMul

L93 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapIsoSpecAwayMul
Documentation

The pairwise intersection is canonically the spectrum of the localization away from the product of its two indexing generators.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumOverlapIsoSpecAwayMul
    (i j : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumOverlap R i j).toScheme ≅
      Spec (.of (Localization.Away
        (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j)))
theorem

puncturedSpectrumOverlapIsoSpecAwayMul_hom_SpecMap

L108 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapIsoSpecAwayMul_hom_SpecMap
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumOverlapIsoSpecAwayMul_hom_SpecMap
    (i j : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumOverlapIsoSpecAwayMul R i j).hom ≫
        Spec.map (CommRingCat.ofHom (algebraMap (CommRingCat.of R)
          (Localization.Away
            (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j)))) =
      (puncturedSpectrumOverlap R i j).ι ≫ puncturedSpectrumInclusion R
abbrev

puncturedSpectrumDoubleLocalization

L159 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumDoubleLocalization
Documentation

The actual iterated localization: first invert the left generator and then invert the image of the right generator.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
abbrev puncturedSpectrumDoubleLocalization
    (i j : puncturedSpectrumGeneratorIndex R)
def

puncturedSpectrumAwayMulEquivDoubleLocalization

L167 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAwayMulEquivDoubleLocalization
Documentation

Localizing at the product is canonically equivalent to the corresponding iterated localization.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumAwayMulEquivDoubleLocalization
    (i j : puncturedSpectrumGeneratorIndex R) :
    Localization.Away
        (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j) ≃ₐ[R]
      puncturedSpectrumDoubleLocalization R i j
def

puncturedSpectrumOverlapIsoSpecDoubleLocalization

L178 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapIsoSpecDoubleLocalization
Documentation

The pairwise intersection as the spectrum of an actual iterated localization.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumOverlapIsoSpecDoubleLocalization
    (i j : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumOverlap R i j).toScheme ≅
      Spec (.of (puncturedSpectrumDoubleLocalization R i j))
def

puncturedSpectrumOverlapToLeft

L188 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapToLeft
Documentation

The inclusion of a pairwise intersection into its left chart.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumOverlapToLeft
    (i j : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumOverlap R i j).toScheme ⟶
      (puncturedSpectrumBasicOpen R i).toScheme
def

puncturedSpectrumOverlapToRight

L195 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapToRight
Documentation

The inclusion of a pairwise intersection into its right chart.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumOverlapToRight
    (i j : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumOverlap R i j).toScheme ⟶
      (puncturedSpectrumBasicOpen R j).toScheme
theorem

puncturedSpectrumBasicOpenIsoSpecAway_hom_SpecMap

L205 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumBasicOpenIsoSpecAway_hom_SpecMap
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumBasicOpenIsoSpecAway_hom_SpecMap
    (i : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumBasicOpenIsoSpecAway R i).hom ≫
        Spec.map (CommRingCat.ofHom (algebraMap R
          (Localization.Away (puncturedSpectrumGenerator R i)))) =
      (puncturedSpectrumBasicOpen R i).ι ≫ puncturedSpectrumInclusion R
def

puncturedSpectrumAwayToOverlapLeft

L226 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAwayToOverlapLeft
Documentation

The canonical ring map from the left localization to the common product localization.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumAwayToOverlapLeft
    (i j : puncturedSpectrumGeneratorIndex R) :
    Localization.Away (puncturedSpectrumGenerator R i) →+*
      Localization.Away
        (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j)
def

puncturedSpectrumAwayToOverlapRight

L236 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAwayToOverlapRight
Documentation

The canonical ring map from the right localization to the common product localization.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumAwayToOverlapRight
    (i j : puncturedSpectrumGeneratorIndex R) :
    Localization.Away (puncturedSpectrumGenerator R j) →+*
      Localization.Away
        (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j)
def

puncturedSpectrumOverlapSpecMapLeft

L246 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapSpecMapLeft
Documentation

On affine spectra, the left projection of the Cech overlap is induced by the canonical map to the product localization.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumOverlapSpecMapLeft
    (i j : puncturedSpectrumGeneratorIndex R) :
    Spec (.of (Localization.Away
      (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j))) ⟶
        Spec (.of (Localization.Away (puncturedSpectrumGenerator R i)))
def

puncturedSpectrumOverlapSpecMapRight

L255 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapSpecMapRight
Documentation

On affine spectra, the right projection of the Cech overlap is induced by the canonical map to the product localization.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumOverlapSpecMapRight
    (i j : puncturedSpectrumGeneratorIndex R) :
    Spec (.of (Localization.Away
      (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j))) ⟶
        Spec (.of (Localization.Away (puncturedSpectrumGenerator R j)))
theorem

puncturedSpectrumOverlapSpecMapLeft_comp_SpecMap

L265 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapSpecMapLeft_comp_SpecMap
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumOverlapSpecMapLeft_comp_SpecMap
    (i j : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumOverlapSpecMapLeft R i j ≫
        Spec.map (CommRingCat.ofHom (algebraMap R
          (Localization.Away (puncturedSpectrumGenerator R i)))) =
      Spec.map (CommRingCat.ofHom (algebraMap R
        (Localization.Away
          (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j))))
theorem

puncturedSpectrumOverlapSpecMapRight_comp_SpecMap

L283 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapSpecMapRight_comp_SpecMap
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumOverlapSpecMapRight_comp_SpecMap
    (i j : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumOverlapSpecMapRight R i j ≫
        Spec.map (CommRingCat.ofHom (algebraMap R
          (Localization.Away (puncturedSpectrumGenerator R j)))) =
      Spec.map (CommRingCat.ofHom (algebraMap R
        (Localization.Away
          (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j))))
theorem

puncturedSpectrumOverlapIsoSpecAwayMul_hom_comp_left

L302 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapIsoSpecAwayMul_hom_comp_left
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumOverlapIsoSpecAwayMul_hom_comp_left
    (i j : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumOverlapIsoSpecAwayMul R i j).hom ≫
        puncturedSpectrumOverlapSpecMapLeft R i j =
      puncturedSpectrumOverlapToLeft R i j ≫
        (puncturedSpectrumBasicOpenIsoSpecAway R i).hom
theorem

puncturedSpectrumOverlapIsoSpecAwayMul_hom_comp_right

L326 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapIsoSpecAwayMul_hom_comp_right
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumOverlapIsoSpecAwayMul_hom_comp_right
    (i j : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumOverlapIsoSpecAwayMul R i j).hom ≫
        puncturedSpectrumOverlapSpecMapRight R i j =
      puncturedSpectrumOverlapToRight R i j ≫
        (puncturedSpectrumBasicOpenIsoSpecAway R j).hom
theorem

puncturedSpectrumOverlapSpecMapLeft_comp_chartIso_inv

L349 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapSpecMapLeft_comp_chartIso_inv
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumOverlapSpecMapLeft_comp_chartIso_inv
    (i j : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumOverlapSpecMapLeft R i j ≫
        (puncturedSpectrumBasicOpenIsoSpecAway R i).inv =
      (puncturedSpectrumOverlapIsoSpecAwayMul R i j).inv ≫
        puncturedSpectrumOverlapToLeft R i j
theorem

puncturedSpectrumOverlapSpecMapRight_comp_chartIso_inv

L363 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOverlapSpecMapRight_comp_chartIso_inv
Source context 8 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumOverlapSpecMapRight_comp_chartIso_inv
    (i j : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumOverlapSpecMapRight R i j ≫
        (puncturedSpectrumBasicOpenIsoSpecAway R j).inv =
      (puncturedSpectrumOverlapIsoSpecAwayMul R i j).inv ≫
        puncturedSpectrumOverlapToRight R i j
def

puncturedSpectrumFiniteEtaleRestrictionLeft

L376 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleRestrictionLeft
Documentation

Restriction of finite etale covers from the left principal chart to the pairwise overlap.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumFiniteEtaleRestrictionLeft
    (i j : puncturedSpectrumGeneratorIndex R) :
    FiniteEtale ((puncturedSpectrumBasicOpen R i).toScheme) ⥤
      FiniteEtale ((puncturedSpectrumOverlap R i j).toScheme)
def

puncturedSpectrumFiniteEtaleRestrictionRight

L384 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleRestrictionRight
Documentation

Restriction of finite etale covers from the right principal chart to the pairwise overlap.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumFiniteEtaleRestrictionRight
    (i j : puncturedSpectrumGeneratorIndex R) :
    FiniteEtale ((puncturedSpectrumBasicOpen R j).toScheme) ⥤
      FiniteEtale ((puncturedSpectrumOverlap R i j).toScheme)
def

puncturedSpectrumFiniteEtaleAwayRestrictionLeft

L391 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleAwayRestrictionLeft
Documentation

The affine source version of restriction from the left chart.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumFiniteEtaleAwayRestrictionLeft
    (i j : puncturedSpectrumGeneratorIndex R) :
    FiniteEtale
        (Spec (.of (Localization.Away (puncturedSpectrumGenerator R i)))) ⥤
      FiniteEtale
        (Spec (.of (Localization.Away
          (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j))))
def

puncturedSpectrumFiniteEtaleAwayRestrictionRight

L401 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleAwayRestrictionRight
Documentation

The affine source version of restriction from the right chart.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumFiniteEtaleAwayRestrictionRight
    (i j : puncturedSpectrumGeneratorIndex R) :
    FiniteEtale
        (Spec (.of (Localization.Away (puncturedSpectrumGenerator R j)))) ⥤
      FiniteEtale
        (Spec (.of (Localization.Away
          (puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j))))
def

puncturedSpectrumFiniteEtaleRestrictionLeftIso

L412 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleRestrictionLeftIso
Documentation

Restriction on the geometric charts and restriction on their affine localization models are canonically naturally isomorphic on the left.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumFiniteEtaleRestrictionLeftIso
    (i j : puncturedSpectrumGeneratorIndex R) :
    FiniteEtale.pullback (puncturedSpectrumBasicOpenIsoSpecAway R i).inv ⋙
        puncturedSpectrumFiniteEtaleAwayRestrictionLeft R i j ≅
      puncturedSpectrumFiniteEtaleRestrictionLeft R i j ⋙
        FiniteEtale.pullback
          (puncturedSpectrumOverlapIsoSpecAwayMul R i j).inv
def

puncturedSpectrumFiniteEtaleRestrictionRightIso

L440 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleRestrictionRightIso
Documentation

Restriction on the geometric charts and restriction on their affine localization models are canonically naturally isomorphic on the right.

Source context 7 commands

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

noncomputable section
open CategoryTheory IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
local instance finiteEtaleHasPullbacksAlongCech
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCech
    {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⟩
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumFiniteEtaleRestrictionRightIso
    (i j : puncturedSpectrumGeneratorIndex R) :
    FiniteEtale.pullback (puncturedSpectrumBasicOpenIsoSpecAway R j).inv ⋙
        puncturedSpectrumFiniteEtaleAwayRestrictionRight R i j ≅
      puncturedSpectrumFiniteEtaleRestrictionRight R i j ⋙
        FiniteEtale.pullback
          (puncturedSpectrumOverlapIsoSpecAwayMul R i j).inv

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