NYLL
Module

PuncturedSpectrumDirectedRefinement.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumDirectedRefinement
35 declarations indexed from sourceView source ↗

Module documentation

A directed principal-open refinement of a punctured spectrum

The nonempty finite subsets of a chosen finite generating set, ordered by reverse inclusion, index the principal opens obtained by inverting the product of the selected generators. Singleton subsets recover the original cover, while union represents intersection. This makes the refinement locally directed and suitable as the base cover of relative gluing data.

Imports2
Imported by2

Declarations

abbrev

puncturedSpectrumRefinementIndex

L34 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementIndex
Documentation

Nonempty finite subsets of the chosen generators, ordered by reverse inclusion. Thus a morphism of indices points from a smaller principal open to a larger one.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
abbrev puncturedSpectrumRefinementIndex
def

puncturedSpectrumRefinementSingleton

L39 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementSingleton
Documentation

The index corresponding to one member of the original principal cover.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumRefinementSingleton
    (i : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumRefinementIndex R
def

puncturedSpectrumRefinementUnion

L45 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementUnion
Documentation

Union is a common lower bound for the reverse-inclusion order.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumRefinementUnion
    (s t : puncturedSpectrumRefinementIndex R) :
    puncturedSpectrumRefinementIndex R
theorem

puncturedSpectrumRefinementUnion_le_left

L52 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementUnion_le_left
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementUnion_le_left
    (s t : puncturedSpectrumRefinementIndex R) :
    puncturedSpectrumRefinementUnion R s t ≤ s
theorem

puncturedSpectrumRefinementUnion_le_right

L59 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementUnion_le_right
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementUnion_le_right
    (s t : puncturedSpectrumRefinementIndex R) :
    puncturedSpectrumRefinementUnion R s t ≤ t
def

puncturedSpectrumGeneratorProduct

L66 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumGeneratorProduct
Documentation

The product of the generators selected by an index.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumGeneratorProduct
    (s : puncturedSpectrumRefinementIndex R) : R
def

puncturedSpectrumAmbientRefinementOpen

L71 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientRefinementOpen
Documentation

The ambient principal open belonging to a finite generator product.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumAmbientRefinementOpen
    (s : puncturedSpectrumRefinementIndex R) :
    (Spec (.of R)).Opens
theorem

mem_puncturedSpectrumAmbientRefinementOpen_iff

L77 ↗
AlgebraicGeometry.Scheme.mem_puncturedSpectrumAmbientRefinementOpen_iff
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem mem_puncturedSpectrumAmbientRefinementOpen_iff
    (s : puncturedSpectrumRefinementIndex R) (x : Spec (.of R)) :
    x ∈ puncturedSpectrumAmbientRefinementOpen R s ↔
      ∀ i ∈ s.1, puncturedSpectrumGenerator R i ∉ x.asIdeal
theorem

puncturedSpectrumAmbientRefinementOpen_singleton

L87 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientRefinementOpen_singleton
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumAmbientRefinementOpen_singleton
    (i : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumAmbientRefinementOpen R
        (puncturedSpectrumRefinementSingleton R i) =
      puncturedSpectrumAmbientBasicOpen R i
theorem

puncturedSpectrumAmbientRefinementOpen_union

L98 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientRefinementOpen_union
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumAmbientRefinementOpen_union
    (s t : puncturedSpectrumRefinementIndex R) :
    puncturedSpectrumAmbientRefinementOpen R
        (puncturedSpectrumRefinementUnion R s t) =
      puncturedSpectrumAmbientRefinementOpen R s ⊓
        puncturedSpectrumAmbientRefinementOpen R t
theorem

puncturedSpectrumAmbientRefinementOpen_le

L130 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientRefinementOpen_le
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumAmbientRefinementOpen_le
    (s : puncturedSpectrumRefinementIndex R) :
    puncturedSpectrumAmbientRefinementOpen R s ≤
      puncturedSpectrumOpen R
def

puncturedSpectrumRefinementOpen

L144 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementOpen
Documentation

A product principal open, regarded inside the punctured spectrum.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumRefinementOpen
    (s : puncturedSpectrumRefinementIndex R) :
    (puncturedSpectrum R).Opens
theorem

puncturedSpectrumRefinementOpen_singleton

L151 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementOpen_singleton
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementOpen_singleton
    (i : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumRefinementOpen R
        (puncturedSpectrumRefinementSingleton R i) =
      puncturedSpectrumBasicOpen R i
theorem

puncturedSpectrumRefinementOpen_union

L161 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementOpen_union
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementOpen_union
    (s t : puncturedSpectrumRefinementIndex R) :
    puncturedSpectrumRefinementOpen R
        (puncturedSpectrumRefinementUnion R s t) =
      puncturedSpectrumRefinementOpen R s ⊓
        puncturedSpectrumRefinementOpen R t
theorem

puncturedSpectrumAmbientRefinementOpen_mono

L173 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientRefinementOpen_mono
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumAmbientRefinementOpen_mono
    {s t : puncturedSpectrumRefinementIndex R} (hst : s ≤ t) :
    puncturedSpectrumAmbientRefinementOpen R s ≤
      puncturedSpectrumAmbientRefinementOpen R t
theorem

puncturedSpectrumRefinementOpen_mono

L183 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementOpen_mono
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementOpen_mono
    {s t : puncturedSpectrumRefinementIndex R} (hst : s ≤ t) :
    puncturedSpectrumRefinementOpen R s ≤
      puncturedSpectrumRefinementOpen R t
def

puncturedSpectrumRefinementOpenIsoSpecAway

L192 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementOpenIsoSpecAway
Documentation

Every product chart is canonically the spectrum of the localization away from the corresponding generator product.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumRefinementOpenIsoSpecAway
    (s : puncturedSpectrumRefinementIndex R) :
    (puncturedSpectrumRefinementOpen R s).toScheme ≅
      Spec (.of (Localization.Away
        (puncturedSpectrumGeneratorProduct R s)))
theorem

puncturedSpectrumRefinementOpen_isAffine

L207 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementOpen_isAffine
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementOpen_isAffine
    (s : puncturedSpectrumRefinementIndex R) :
    IsAffineOpen (puncturedSpectrumRefinementOpen R s)
theorem

puncturedSpectrumRefinementOpen_isOpenCover

L216 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementOpen_isOpenCover
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementOpen_isOpenCover :
    IsOpenCover (puncturedSpectrumRefinementOpen R)
abbrev

puncturedSpectrumDirectedOpenCover

L227 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumDirectedOpenCover
Documentation

The open cover by all nonempty finite products of chosen generators.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
abbrev puncturedSpectrumDirectedOpenCover :
    (puncturedSpectrum R).OpenCover
def

puncturedSpectrumRefinementTransition

L238 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementTransition
Documentation

The inclusion associated to an inequality in the reverse-inclusion indexing order.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumRefinementTransition
    {s t : puncturedSpectrumRefinementIndex R} (hst : s ≤ t) :
    (puncturedSpectrumRefinementOpen R s).toScheme ⟶
      (puncturedSpectrumRefinementOpen R t).toScheme
def

puncturedSpectrumRefinementUnionToLeft

L246 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementUnionToLeft
Documentation

The union chart maps to the left member of the intersection.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumRefinementUnionToLeft
    (s t : puncturedSpectrumRefinementIndex R) :
    (puncturedSpectrumRefinementOpen R
      (puncturedSpectrumRefinementUnion R s t)).toScheme ⟶
        (puncturedSpectrumRefinementOpen R s).toScheme
def

puncturedSpectrumRefinementUnionToRight

L255 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementUnionToRight
Documentation

The union chart maps to the right member of the intersection.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumRefinementUnionToRight
    (s t : puncturedSpectrumRefinementIndex R) :
    (puncturedSpectrumRefinementOpen R
      (puncturedSpectrumRefinementUnion R s t)).toScheme ⟶
        (puncturedSpectrumRefinementOpen R t).toScheme
theorem

puncturedSpectrumRefinementTransition_comp_ι

L265 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementTransition_comp_ι
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementTransition_comp_ι
    {s t : puncturedSpectrumRefinementIndex R} (hst : s ≤ t) :
    puncturedSpectrumRefinementTransition R hst ≫
        (puncturedSpectrumRefinementOpen R t).ι =
      (puncturedSpectrumRefinementOpen R s).ι
theorem

puncturedSpectrumRefinementTransition_id

L273 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementTransition_id
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementTransition_id
    (s : puncturedSpectrumRefinementIndex R) :
    puncturedSpectrumRefinementTransition R (le_refl s) = 𝟙 _
theorem

puncturedSpectrumRefinementTransition_comp

L279 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementTransition_comp
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementTransition_comp
    {s t v : puncturedSpectrumRefinementIndex R}
    (hst : s ≤ t) (htv : t ≤ v) :
    puncturedSpectrumRefinementTransition R (hst.trans htv) =
      puncturedSpectrumRefinementTransition R hst ≫
        puncturedSpectrumRefinementTransition R htv
theorem

puncturedSpectrumRefinementUnion_maps_comm

L288 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementUnion_maps_comm
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementUnion_maps_comm
    (s t : puncturedSpectrumRefinementIndex R) :
    puncturedSpectrumRefinementUnionToLeft R s t ≫
        (puncturedSpectrumRefinementOpen R s).ι =
      puncturedSpectrumRefinementUnionToRight R s t ≫
        (puncturedSpectrumRefinementOpen R t).ι
theorem

puncturedSpectrumRefinementOpen_union_singleton

L302 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementOpen_union_singleton
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumRefinementOpen_union_singleton
    (i j : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumRefinementOpen R
        (puncturedSpectrumRefinementUnion R
          (puncturedSpectrumRefinementSingleton R i)
          (puncturedSpectrumRefinementSingleton R j)) =
      puncturedSpectrumOverlap R i j
theorem

puncturedSpectrumRefinementUnion_exists_pullback_lift

L315 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumRefinementUnion_exists_pullback_lift
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · full declaration
theorem puncturedSpectrumRefinementUnion_exists_pullback_lift
    (s t : puncturedSpectrumRefinementIndex R)
    (x : (pullback
      (puncturedSpectrumRefinementOpen R s).ι
      (puncturedSpectrumRefinementOpen R t).ι).carrier) :
    ∃ y : (puncturedSpectrumRefinementOpen R
        (puncturedSpectrumRefinementUnion R s t)).toScheme,
      pullback.lift
        (puncturedSpectrumRefinementTransition R
          (puncturedSpectrumRefinementUnion_le_left R s t))
        (puncturedSpectrumRefinementTransition R
          (puncturedSpectrumRefinementUnion_le_right R s t))
        (by simp only [puncturedSpectrumRefinementTransition_comp_ι]) y = x := by
  let xs := pullback.fst
    (puncturedSpectrumRefinementOpen R s).ι
    (puncturedSpectrumRefinementOpen R t).ι x
  let xt := pullback.snd
    (puncturedSpectrumRefinementOpen R s).ι
    (puncturedSpectrumRefinementOpen R t).ι x
  have hbase : xs.1 = xt.1 := by
    change
      (puncturedSpectrumRefinementOpen R s).ι xs =
        (puncturedSpectrumRefinementOpen R t).ι xt
    dsimp only [xs, xt]
    have hcondition :
        pullback.fst
            (puncturedSpectrumRefinementOpen R s).ι
            (puncturedSpectrumRefinementOpen R t).ι ≫
              (puncturedSpectrumRefinementOpen R s).ι =
          pullback.snd
            (puncturedSpectrumRefinementOpen R s).ι
            (puncturedSpectrumRefinementOpen R t).ι ≫
              (puncturedSpectrumRefinementOpen R t).ι :=
      pullback.condition
    simpa only [Scheme.Hom.comp_apply] using
      congrArg (fun f :
        pullback
            (puncturedSpectrumRefinementOpen R s).ι
            (puncturedSpectrumRefinementOpen R t).ι ⟶
          puncturedSpectrum R ↦ f x) hcondition
  have hxt : xs.1 ∈ puncturedSpectrumRefinementOpen R t := by
    rw [hbase]
    exact xt.2
  let y : (puncturedSpectrumRefinementOpen R
      (puncturedSpectrumRefinementUnion R s t)).toScheme :=
    ⟨xs.1, by
      rw [puncturedSpectrumRefinementOpen_union]
      exact ⟨xs.2, hxt⟩⟩
  refine ⟨y, ?_⟩
  apply ((pullback.fst
    (puncturedSpectrumRefinementOpen R s).ι
    (puncturedSpectrumRefinementOpen R t).ι) ≫
      (puncturedSpectrumRefinementOpen R s).ι).isOpenEmbedding.injective
  rw [← Scheme.Hom.comp_apply, pullback.lift_fst_assoc,
    puncturedSpectrumRefinementTransition_comp_ι]
  rfl
instance

puncturedSpectrumDirectedOpenCover_locallyDirected

L372 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumDirectedOpenCover_locallyDirected
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · full declaration
instance puncturedSpectrumDirectedOpenCover_locallyDirected :
    (puncturedSpectrumDirectedOpenCover R).LocallyDirected where
  trans {s t} hst :=
    puncturedSpectrumRefinementTransition R (leOfHom hst)
  trans_id s := by
    rw [← cancel_mono
      (puncturedSpectrumRefinementOpen R s).ι]
    simp only [puncturedSpectrumRefinementTransition_comp_ι,
      Category.id_comp]
  trans_comp {s t v} hst htv := by
    rw [← cancel_mono
      (puncturedSpectrumRefinementOpen R v).ι]
    simp only [Category.assoc,
      puncturedSpectrumRefinementTransition_comp_ι]
  w {s t} hst := by
    exact puncturedSpectrumRefinementTransition_comp_ι R (leOfHom hst)
  directed {s t} x := by
    let k := puncturedSpectrumRefinementUnion R s t
    let hks : k ⟶ s := homOfLE
      (puncturedSpectrumRefinementUnion_le_left R s t)
    let hkt : k ⟶ t := homOfLE
      (puncturedSpectrumRefinementUnion_le_right R s t)
    refine ⟨k, hks, hkt, ?_⟩
    simpa only [k, hks, hkt] using
      puncturedSpectrumRefinementUnion_exists_pullback_lift R s t x
  property_trans {s t} hst := by
    dsimp only [puncturedSpectrumRefinementTransition]
    infer_instance
theorem

puncturedSpectrumDirectedOpenCover_index_finite

L401 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumDirectedOpenCover_index_finite
Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem puncturedSpectrumDirectedOpenCover_index_finite :
    Finite (puncturedSpectrumDirectedOpenCover R).I₀
theorem

puncturedSpectrumDirectedOpenCover_chart_isAffine

L406 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumDirectedOpenCover_chart_isAffine
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumDirectedOpenCover_chart_isAffine
    (s : (puncturedSpectrumDirectedOpenCover R).I₀) :
    IsAffine ((puncturedSpectrumDirectedOpenCover R).X s)
theorem

puncturedSpectrumDirectedOpenCover_trans

L413 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumDirectedOpenCover_trans
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumDirectedOpenCover_trans
    {s t : (puncturedSpectrumDirectedOpenCover R).I₀} (hst : s ≤ t) :
    (puncturedSpectrumDirectedOpenCover R).trans (homOfLE hst) =
      puncturedSpectrumRefinementTransition R hst
theorem

puncturedSpectrumDirectedOpenCover_trans_comp_ι

L420 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumDirectedOpenCover_trans_comp_ι
Source context 7 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumDirectedOpenCover_trans_comp_ι
    {s t : (puncturedSpectrumDirectedOpenCover R).I₀}
    (hst : s ⟶ t) :
    (puncturedSpectrumDirectedOpenCover R).trans hst ≫
        (puncturedSpectrumRefinementOpen R t).ι =
      (puncturedSpectrumRefinementOpen R s).ι
def

puncturedSpectrumDirectedOpenCoverBaseRelativeGluingData

L431 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumDirectedOpenCoverBaseRelativeGluingData
Documentation

The canonical cartesian diagram of the base charts, expressed in the exact format consumed by relative gluing. This contains no descent or effectivity hypothesis: its natural transformation is the identity.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · full declaration
def puncturedSpectrumDirectedOpenCoverBaseRelativeGluingData :
    Cover.RelativeGluingData (puncturedSpectrumDirectedOpenCover R) where
  functor :=
    (puncturedSpectrumDirectedOpenCover R).functorOfLocallyDirected
  natTrans := 𝟙 _
  equifibered := NatTrans.Equifibered.of_isIso _

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