NYLL
Module

PuncturedSpectrumCechTriple.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumCechTriple
22 declarations indexed from sourceView source ↗

Module documentation

Triple intersections in the principal cover of a punctured spectrum

This file constructs the triple-intersection level of the principal Cech cover. It identifies a triple intersection with the spectrum of both the product localization and the corresponding three-stage localization, exposes the three maps to pairwise intersections, and records the natural isomorphisms needed for the finite-etale cocycle condition.

Imports1
Imported by2

Declarations

instance

finiteEtaleHasPullbacksAlongCechTriple

L27 ↗
AlgebraicGeometry.Scheme.finiteEtaleHasPullbacksAlongCechTriple
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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
instance

finiteEtaleStableUnderBaseChangeAlongCechTriple

L33 ↗
AlgebraicGeometry.Scheme.finiteEtaleStableUnderBaseChangeAlongCechTriple
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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
Lean source · statement
instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
def

puncturedSpectrumTripleOverlap

L43 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlap
Documentation

The intersection of three principal charts 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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlap
    (i j k : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrum R).Opens
def

puncturedSpectrumAmbientTripleOverlap

L50 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientTripleOverlap
Documentation

The ambient basic open belonging to the product of three 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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumAmbientTripleOverlap
    (i j k : puncturedSpectrumGeneratorIndex R) :
    (Spec (.of R)).Opens
theorem

puncturedSpectrumAmbientTripleOverlap_le

L59 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientTripleOverlap_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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumAmbientTripleOverlap_le
    (i j k : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumAmbientTripleOverlap R i j k ≤
      puncturedSpectrumOpen R
theorem

puncturedSpectrumTripleOverlap_eq_preimage_ambient

L71 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlap_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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlap_eq_preimage_ambient
    (i j k : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumTripleOverlap R i j k =
      (puncturedSpectrumOpen R).ι ⁻¹ᵁ
        puncturedSpectrumAmbientTripleOverlap R i j k
def

puncturedSpectrumTripleOverlapIsoSpecAwayMul

L98 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlapIsoSpecAwayMul
Documentation

A triple intersection is canonically the spectrum of the localization away from the product of its three 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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlapIsoSpecAwayMul
    (i j k : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumTripleOverlap R i j k).toScheme ≅
      Spec (.of (Localization.Away
        ((puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j) *
          puncturedSpectrumGenerator R k)))
abbrev

puncturedSpectrumTripleLocalization

L114 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleLocalization
Documentation

The actual three-stage localization: first invert i, then j, and finally the image of k.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleLocalization
    (i j k : puncturedSpectrumGeneratorIndex R)
def

puncturedSpectrumAwayTripleEquivTripleLocalization

L122 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAwayTripleEquivTripleLocalization
Documentation

Localization at the triple product is canonically equivalent to the corresponding three-stage 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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumAwayTripleEquivTripleLocalization
    (i j k : puncturedSpectrumGeneratorIndex R) :
    Localization.Away
        ((puncturedSpectrumGenerator R i * puncturedSpectrumGenerator R j) *
          puncturedSpectrumGenerator R k) ≃ₐ[R]
      puncturedSpectrumTripleLocalization R i j k
def

puncturedSpectrumTripleOverlapIsoSpecTripleLocalization

L139 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlapIsoSpecTripleLocalization
Documentation

The triple intersection as the spectrum of an actual three-stage 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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlapIsoSpecTripleLocalization
    (i j k : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumTripleOverlap R i j k).toScheme ≅
      Spec (.of (puncturedSpectrumTripleLocalization R i j k))
def

puncturedSpectrumTripleOverlapToIJ

L149 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlapToIJ
Documentation

The triple intersection maps to the (i,j) pairwise intersection.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlapToIJ
    (i j k : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumTripleOverlap R i j k).toScheme ⟶
      (puncturedSpectrumOverlap R i j).toScheme
def

puncturedSpectrumTripleOverlapToIK

L156 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlapToIK
Documentation

The triple intersection maps to the (i,k) pairwise intersection.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlapToIK
    (i j k : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumTripleOverlap R i j k).toScheme ⟶
      (puncturedSpectrumOverlap R i k).toScheme
def

puncturedSpectrumTripleOverlapToJK

L164 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlapToJK
Documentation

The triple intersection maps to the (j,k) pairwise intersection.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlapToJK
    (i j k : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumTripleOverlap R i j k).toScheme ⟶
      (puncturedSpectrumOverlap R j k).toScheme
theorem

puncturedSpectrumTripleOverlap_comp_toChartI

L173 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlap_comp_toChartI
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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlap_comp_toChartI
    (i j k : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumTripleOverlapToIJ R i j k ≫
        puncturedSpectrumOverlapToLeft R i j =
      puncturedSpectrumTripleOverlapToIK R i j k ≫
        puncturedSpectrumOverlapToLeft R i k
theorem

puncturedSpectrumTripleOverlap_comp_toChartJ

L191 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlap_comp_toChartJ
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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlap_comp_toChartJ
    (i j k : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumTripleOverlapToIJ R i j k ≫
        puncturedSpectrumOverlapToRight R i j =
      puncturedSpectrumTripleOverlapToJK R i j k ≫
        puncturedSpectrumOverlapToLeft R j k
theorem

puncturedSpectrumTripleOverlap_comp_toChartK

L209 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumTripleOverlap_comp_toChartK
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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumTripleOverlap_comp_toChartK
    (i j k : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumTripleOverlapToIK R i j k ≫
        puncturedSpectrumOverlapToRight R i k =
      puncturedSpectrumTripleOverlapToJK R i j k ≫
        puncturedSpectrumOverlapToRight R j k
def

puncturedSpectrumFiniteEtaleTripleRestrictionIJ

L228 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleTripleRestrictionIJ
Documentation

Restriction of finite-etale covers from the (i,j) overlap to the triple intersection.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumFiniteEtaleTripleRestrictionIJ
    (i j k : puncturedSpectrumGeneratorIndex R) :
    FiniteEtale ((puncturedSpectrumOverlap R i j).toScheme) ⥤
      FiniteEtale ((puncturedSpectrumTripleOverlap R i j k).toScheme)
def

puncturedSpectrumFiniteEtaleTripleRestrictionIK

L236 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleTripleRestrictionIK
Documentation

Restriction of finite-etale covers from the (i,k) overlap to the triple intersection.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumFiniteEtaleTripleRestrictionIK
    (i j k : puncturedSpectrumGeneratorIndex R) :
    FiniteEtale ((puncturedSpectrumOverlap R i k).toScheme) ⥤
      FiniteEtale ((puncturedSpectrumTripleOverlap R i j k).toScheme)
def

puncturedSpectrumFiniteEtaleTripleRestrictionJK

L244 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleTripleRestrictionJK
Documentation

Restriction of finite-etale covers from the (j,k) overlap to the triple intersection.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumFiniteEtaleTripleRestrictionJK
    (i j k : puncturedSpectrumGeneratorIndex R) :
    FiniteEtale ((puncturedSpectrumOverlap R j k).toScheme) ⥤
      FiniteEtale ((puncturedSpectrumTripleOverlap R i j k).toScheme)
def

puncturedSpectrumFiniteEtaleTripleRestrictionIsoI

L252 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleTripleRestrictionIsoI
Documentation

The two finite-etale restriction routes from chart i to the triple intersection are naturally isomorphic.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumFiniteEtaleTripleRestrictionIsoI
    (i j k : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumFiniteEtaleRestrictionLeft R i j ⋙
        puncturedSpectrumFiniteEtaleTripleRestrictionIJ R i j k ≅
      puncturedSpectrumFiniteEtaleRestrictionLeft R i k ⋙
        puncturedSpectrumFiniteEtaleTripleRestrictionIK R i j k
def

puncturedSpectrumFiniteEtaleTripleRestrictionIsoJ

L278 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleTripleRestrictionIsoJ
Documentation

The two finite-etale restriction routes from chart j to the triple intersection are naturally isomorphic.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumFiniteEtaleTripleRestrictionIsoJ
    (i j k : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumFiniteEtaleRestrictionRight R i j ⋙
        puncturedSpectrumFiniteEtaleTripleRestrictionIJ R i j k ≅
      puncturedSpectrumFiniteEtaleRestrictionLeft R j k ⋙
        puncturedSpectrumFiniteEtaleTripleRestrictionJK R i j k
def

puncturedSpectrumFiniteEtaleTripleRestrictionIsoK

L304 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumFiniteEtaleTripleRestrictionIsoK
Documentation

The two finite-etale restriction routes from chart k to the triple intersection are naturally isomorphic.

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 finiteEtaleHasPullbacksAlongCechTriple
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongCechTriple
    {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 puncturedSpectrumFiniteEtaleTripleRestrictionIsoK
    (i j k : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumFiniteEtaleRestrictionRight R i k ⋙
        puncturedSpectrumFiniteEtaleTripleRestrictionIK R i j k ≅
      puncturedSpectrumFiniteEtaleRestrictionRight R j k ⋙
        puncturedSpectrumFiniteEtaleTripleRestrictionJK R i j k

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