NYLL
Module

NoetherianImageApproximation.lean

Nyll.SchemeTheory.Descent.NoetherianImageApproximation
17 declarations indexed from sourceView source ↗

Module documentation

Proper Noetherian images of a closed subscheme in a fixed ambient model

A closed subscheme of the base change of a proper scheme over a Noetherian ring is recovered as the limit of its actual images over finitely generated subalgebras. Every image is proper over its actual Noetherian stage ring. No finite-presentation hypothesis is imposed on the closed subscheme.

Imports6
Imported by2

Declarations

def

subalgebras

L35 ↗
AlgebraicGeometry.NoetherianImageApproximation.subalgebras
Documentation

The exhaustive ordered family of actual finitely generated subalgebras.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
Lean source · full declaration
def subalgebras : FGSubalgebra A₀ A →o Subalgebra A₀ A where
  toFun B := B.1
  monotone' _ _ h := h
theorem

exhaustive

L40 ↗
AlgebraicGeometry.NoetherianImageApproximation.exhaustive
Documentation

Every element occurs in its actual singleton-generated subalgebra.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
Lean source · statement
theorem exhaustive (a : A) : ∃ B, a ∈ subalgebras A₀ A B
abbrev

ambientDiagram

L49 ↗
AlgebraicGeometry.NoetherianImageApproximation.ambientDiagram
Documentation

The actual ambient schemes over the finitely generated subalgebras.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
abbrev ambientDiagram : (FGSubalgebra A₀ A)ᵒᵖ ⥤ Scheme.{u}
abbrev

ambientCone

L53 ↗
AlgebraicGeometry.NoetherianImageApproximation.ambientCone
Documentation

The actual ambient cone with vertex the base change to A.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
abbrev ambientCone : Cone (ambientDiagram A₀ A f₀)
def

ambientConeIsLimit

L57 ↗
AlgebraicGeometry.NoetherianImageApproximation.ambientConeIsLimit
Documentation

Exhaustiveness of the ring stages gives the actual ambient limit.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
Lean source · statement
def ambientConeIsLimit : IsLimit (ambientCone A₀ A f₀)
abbrev

diagram

L64 ↗
AlgebraicGeometry.NoetherianImageApproximation.diagram
Documentation

The proper approximation consists of the actual stage images of j.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
abbrev diagram : (FGSubalgebra A₀ A)ᵒᵖ ⥤ Scheme.{u}
abbrev

cone

L68 ↗
AlgebraicGeometry.NoetherianImageApproximation.cone
Documentation

The cone whose source is the original closed subscheme.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
abbrev cone : Cone (diagram A₀ A f₀ j)
def

baseMap

L72 ↗
AlgebraicGeometry.NoetherianImageApproximation.baseMap
Documentation

The actual map from a stage image to its finitely generated base ring.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
def baseMap (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    (diagram A₀ A f₀ j).obj i ⟶ Spec (CommRingCat.of i.unop.1)
lemma

transition_baseMap

L79 ↗
AlgebraicGeometry.NoetherianImageApproximation.transition_baseMap
Documentation

The actual stage maps commute with the inclusions of their base rings.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
lemma transition_baseMap {i k : (FGSubalgebra A₀ A)ᵒᵖ} (f : i ⟶ k) :
    (diagram A₀ A f₀ j).map f ≫ baseMap A₀ A f₀ j k =
      baseMap A₀ A f₀ j i ≫
        (SubalgebraStages.specDiagram (subalgebras A₀ A)).map f
def

baseMaps

L92 ↗
AlgebraicGeometry.NoetherianImageApproximation.baseMaps
Documentation

The actual image diagram lies over the diagram of spectra of its stage rings.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · full declaration
def baseMaps : diagram A₀ A f₀ j ⟶
    SubalgebraStages.specDiagram (subalgebras A₀ A) where
  app i := baseMap A₀ A f₀ j i
  naturality _ _ f := transition_baseMap A₀ A f₀ j f
instance

(anonymous instance)

L97 ↗
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
instance [IsProper f₀] (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    IsProper (baseMap A₀ A f₀ j i)
instance

(anonymous instance)

L102 ↗
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
instance [IsProper f₀] (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    CompactSpace ((diagram A₀ A f₀ j).obj i)
instance

(anonymous instance)

L106 ↗
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
instance [IsProper f₀] (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    QuasiSeparatedSpace ((diagram A₀ A f₀ j).obj i)
theorem

stageRing_isNoetherian

L111 ↗
AlgebraicGeometry.NoetherianImageApproximation.stageRing_isNoetherian
Documentation

Every actual ring stage is Noetherian.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
theorem stageRing_isNoetherian [IsNoetherianRing A₀] (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    IsNoetherianRing i.unop.1
theorem

stage_isNoetherian

L118 ↗
AlgebraicGeometry.NoetherianImageApproximation.stage_isNoetherian
Documentation

Every image stage is an actual proper Noetherian scheme.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
theorem stage_isNoetherian [IsNoetherianRing A₀] [IsProper f₀]
    (i : (FGSubalgebra A₀ A)ᵒᵖ) : IsNoetherian ((diagram A₀ A f₀ j).obj i)
def

coneIsLimit

L126 ↗
AlgebraicGeometry.NoetherianImageApproximation.coneIsLimit
Documentation

The original closed subscheme is the limit of the actual proper image stages.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
def coneIsLimit [IsProper f₀] [IsClosedImmersion j] :
    IsLimit (cone A₀ A f₀ j)
lemma

cone_projection_baseMap

L132 ↗
AlgebraicGeometry.NoetherianImageApproximation.cone_projection_baseMap
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀))
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt)
Lean source · statement
lemma cone_projection_baseMap (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    (cone A₀ A f₀ j).π.app i ≫ baseMap A₀ A f₀ j i =
      j ≫ pullback.snd f₀ (SubalgebraStages.specHomTop (A₀ := A₀) (A := A)) ≫
        SubalgebraStages.specLeg (subalgebras A₀ A) i.unop

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