NYLL
Module

NoetherianImageResidueLimit.lean

Nyll.SchemeTheory.Descent.NoetherianImageResidueLimit
29 declarations indexed from sourceView source ↗

Module documentation

Actual residue fibers of the Noetherian image approximation

The fibers of the actual stage images over the contracted primes form an inverse system. Its limit is the actual fiber of the original closed subscheme. The three limits used here are supplied by the image construction, the exhaustive subalgebra construction, and the residue-field colimit theorem.

Imports6
Imported by2

Declarations

abbrev

residueSpecDiagram

L37 ↗
AlgebraicGeometry.SubalgebraStages.residueSpecDiagram
Documentation

The spectra of the actual residue fields at the contracted stage primes.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
abbrev residueSpecDiagram : ιᵒᵖ ⥤ Scheme.{u}
instance

(anonymous instance)

L40 ↗
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
instance (i : ιᵒᵖ) : IsAffine ((residueSpecDiagram S p).obj i)
instance

(anonymous instance)

L43 ↗
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
instance (i : ιᵒᵖ) : CompactSpace ((residueSpecDiagram S p).obj i)
instance

(anonymous instance)

L46 ↗
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
instance (i : ιᵒᵖ) : QuasiSeparatedSpace ((residueSpecDiagram S p).obj i)
abbrev

residueSpecCone

L51 ↗
AlgebraicGeometry.SubalgebraStages.residueSpecCone
Documentation

The cone from the spectrum of the original residue field.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
abbrev residueSpecCone : Cone (residueSpecDiagram S p)
abbrev

residueSpecBase

L55 ↗
AlgebraicGeometry.SubalgebraStages.residueSpecBase
Documentation

The residue point of a stage is its actual algebra-map spectrum morphism.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
abbrev residueSpecBase (i : ιᵒᵖ) :
    (residueSpecDiagram S p).obj i ⟶ (specDiagram S).obj i
abbrev

residueSpecBaseTop

L61 ↗
AlgebraicGeometry.SubalgebraStages.residueSpecBaseTop
Documentation

The original residue point, before approximation.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
abbrev residueSpecBaseTop : Spec (CommRingCat.of p.ResidueField) ⟶ Spec (CommRingCat.of A)
lemma

residueSpecBase_naturality

L65 ↗
AlgebraicGeometry.SubalgebraStages.residueSpecBase_naturality
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueSpecBase_naturality {i j : ιᵒᵖ} (h : i ⟶ j) :
    (residueSpecDiagram S p).map h ≫ residueSpecBase S p j =
      residueSpecBase S p i ≫ (specDiagram S).map h
def

residueSpecBaseMaps

L80 ↗
AlgebraicGeometry.SubalgebraStages.residueSpecBaseMaps
Documentation

The actual residue points constitute a natural transformation over the stage spectra.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · full declaration
def residueSpecBaseMaps : residueSpecDiagram S p ⟶ specDiagram S where
  app i := residueSpecBase S p i
  naturality _ _ h := residueSpecBase_naturality S p h
lemma

residueSpecCone_projection_base

L85 ↗
AlgebraicGeometry.SubalgebraStages.residueSpecCone_projection_base
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueSpecCone_projection_base (i : ιᵒᵖ) :
    (residueSpecCone S p).π.app i ≫ residueSpecBase S p i =
      residueSpecBaseTop p ≫ (specCone S).π.app i
def

residueSpecConeIsLimit

L100 ↗
AlgebraicGeometry.SubalgebraStages.residueSpecConeIsLimit
Documentation

Spectra turn the actual residue-field colimit into the actual residue-point limit.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
def residueSpecConeIsLimit [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (hS : ∀ a : A, ∃ i, a ∈ S i) : IsLimit (residueSpecCone S p)
abbrev

residueFiberObj

L117 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberObj
Documentation

The actual fiber of a stage image at the contraction of the original prime.

Source context 9 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)
variable (p : Ideal A) [p.IsPrime]
open SubalgebraStages in
Lean source · statement
abbrev residueFiberObj (i : (FGSubalgebra A₀ A)ᵒᵖ) : Scheme.{u}
instance

(anonymous instance)

L120 ↗
Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
instance (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    IsAffineHom (pullback.fst (baseMap A₀ A f₀ j i)
      (SubalgebraStages.residueSpecBase (subalgebras A₀ A) p i))
def

residueFiberTrans

L132 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberTrans
Documentation

The actual fiber transition induced by the image and residue-field maps.

Source context 9 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)
variable (p : Ideal A) [p.IsPrime]
open SubalgebraStages in
Lean source · statement
def residueFiberTrans {i k : (FGSubalgebra A₀ A)ᵒᵖ} (h : i ⟶ k) :
    residueFiberObj A₀ A f₀ j p i ⟶ residueFiberObj A₀ A f₀ j p k
lemma

residueFiberTrans_fst

L141 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberTrans_fst
Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueFiberTrans_fst {i k : (FGSubalgebra A₀ A)ᵒᵖ} (h : i ⟶ k) :
    residueFiberTrans A₀ A f₀ j p h ≫
        pullback.fst (baseMap A₀ A f₀ j k)
          (SubalgebraStages.residueSpecBase (subalgebras A₀ A) p k) =
      pullback.fst (baseMap A₀ A f₀ j i)
        (SubalgebraStages.residueSpecBase (subalgebras A₀ A) p i) ≫
          (diagram A₀ A f₀ j).map h
lemma

residueFiberTrans_snd

L151 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberTrans_snd
Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueFiberTrans_snd {i k : (FGSubalgebra A₀ A)ᵒᵖ} (h : i ⟶ k) :
    residueFiberTrans A₀ A f₀ j p h ≫
        pullback.snd (baseMap A₀ A f₀ j k)
          (SubalgebraStages.residueSpecBase (subalgebras A₀ A) p k) =
      pullback.snd (baseMap A₀ A f₀ j i)
        (SubalgebraStages.residueSpecBase (subalgebras A₀ A) p i) ≫
          (SubalgebraStages.residueSpecDiagram (subalgebras A₀ A) p).map h
def

residueFiberDiagram

L161 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberDiagram
Documentation

The inverse system of actual residue fibers of the actual image stages.

Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · full declaration
def residueFiberDiagram : (FGSubalgebra A₀ A)ᵒᵖ ⥤ Scheme.{u} where
  obj i := residueFiberObj A₀ A f₀ j p i
  map h := residueFiberTrans A₀ A f₀ j p h
  map_id i := by
    apply pullback.hom_ext
    · rw [residueFiberTrans_fst, CategoryTheory.Functor.map_id,
        Category.comp_id, Category.id_comp]
    · rw [residueFiberTrans_snd, CategoryTheory.Functor.map_id,
        Category.comp_id, Category.id_comp]
  map_comp h h' := by
    apply pullback.hom_ext
    · rw [residueFiberTrans_fst, Category.assoc, residueFiberTrans_fst,
        residueFiberTrans_fst_assoc, CategoryTheory.Functor.map_comp]
    · rw [residueFiberTrans_snd, Category.assoc, residueFiberTrans_snd,
        residueFiberTrans_snd_assoc, CategoryTheory.Functor.map_comp]
      simp only [SubalgebraStages.residueSpecDiagram, CategoryTheory.Functor.comp_map]
def

residueFiberFst

L179 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberFst
Documentation

Projection of the actual fiber system to the image system.

Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · full declaration
def residueFiberFst : residueFiberDiagram A₀ A f₀ j p ⟶ diagram A₀ A f₀ j where
  app i := pullback.fst (baseMap A₀ A f₀ j i)
    (SubalgebraStages.residueSpecBase (subalgebras A₀ A) p i)
  naturality _ _ h := residueFiberTrans_fst A₀ A f₀ j p h
def

residueFiberSnd

L185 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberSnd
Documentation

Projection of the actual fiber system to the residue-field spectrum system.

Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · full declaration
def residueFiberSnd : residueFiberDiagram A₀ A f₀ j p ⟶
    SubalgebraStages.residueSpecDiagram (subalgebras A₀ A) p where
  app i := pullback.snd (baseMap A₀ A f₀ j i)
    (SubalgebraStages.residueSpecBase (subalgebras A₀ A) p i)
  naturality _ _ h := residueFiberTrans_snd A₀ A f₀ j p h
abbrev

originalBaseMap

L192 ↗
AlgebraicGeometry.NoetherianImageApproximation.originalBaseMap
Documentation

The actual structure map of the original closed subscheme to the ambient ring.

Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
abbrev originalBaseMap : Z ⟶ Spec (CommRingCat.of A)
abbrev

originalResidueFiber

L196 ↗
AlgebraicGeometry.NoetherianImageApproximation.originalResidueFiber
Documentation

The original fiber over the actual original residue field.

Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
abbrev originalResidueFiber : Scheme.{u}
def

residueFiberLeg

L201 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberLeg
Documentation

The original fiber maps to each actual stage fiber.

Source context 9 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)
variable (p : Ideal A) [p.IsPrime]
open SubalgebraStages in
Lean source · statement
def residueFiberLeg (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    originalResidueFiber A₀ A f₀ j p ⟶ residueFiberObj A₀ A f₀ j p i
lemma

residueFiberLeg_fst

L210 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberLeg_fst
Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueFiberLeg_fst (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    residueFiberLeg A₀ A f₀ j p i ≫
        pullback.fst (baseMap A₀ A f₀ j i)
          (SubalgebraStages.residueSpecBase (subalgebras A₀ A) p i) =
      pullback.fst (originalBaseMap A₀ A f₀ j) (SubalgebraStages.residueSpecBaseTop p) ≫
        (cone A₀ A f₀ j).π.app i
lemma

residueFiberLeg_snd

L219 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberLeg_snd
Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueFiberLeg_snd (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    residueFiberLeg A₀ A f₀ j p i ≫
        pullback.snd (baseMap A₀ A f₀ j i)
          (SubalgebraStages.residueSpecBase (subalgebras A₀ A) p i) =
      pullback.snd (originalBaseMap A₀ A f₀ j) (SubalgebraStages.residueSpecBaseTop p) ≫
        (SubalgebraStages.residueSpecCone (subalgebras A₀ A) p).π.app i
def

residueFiberCone

L228 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberCone
Documentation

The actual original fiber is a cone over the actual stage fibers.

Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · full declaration
def residueFiberCone : Cone (residueFiberDiagram A₀ A f₀ j p) where
  pt := originalResidueFiber A₀ A f₀ j p
  π :=
    { app i := residueFiberLeg A₀ A f₀ j p i
      naturality i k h := by
        simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]
        apply pullback.hom_ext
        · rw [Category.assoc, residueFiberTrans_fst, residueFiberLeg_fst_assoc,
            (cone A₀ A f₀ j).w h, residueFiberLeg_fst]
        · rw [Category.assoc, residueFiberTrans_snd, residueFiberLeg_snd_assoc,
            (SubalgebraStages.residueSpecCone (subalgebras A₀ A) p).w h,
            residueFiberLeg_snd] }
instance

(anonymous instance)

L242 ↗
Documentation

Each actual residue-fiber transition is affine.

Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
instance {i k : (FGSubalgebra A₀ A)ᵒᵖ} (h : i ⟶ k) :
    IsAffineHom ((residueFiberDiagram A₀ A f₀ j p).map h)
instance

(anonymous instance)

L258 ↗
Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
instance [IsProper f₀] (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    CompactSpace ((residueFiberDiagram A₀ A f₀ j p).obj i)
instance

(anonymous instance)

L264 ↗
Source context 8 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)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
instance [IsProper f₀] (i : (FGSubalgebra A₀ A)ᵒᵖ) :
    QuasiSeparatedSpace ((residueFiberDiagram A₀ A f₀ j p).obj i)
def

residueFiberConeIsLimit

L273 ↗
AlgebraicGeometry.NoetherianImageApproximation.residueFiberConeIsLimit
Documentation

The original residue fiber is the limit of the actual contracted residue fibers.

Source context 10 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)
variable (p : Ideal A) [p.IsPrime]
open AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone in
open SubalgebraStages in
Lean source · statement
def residueFiberConeIsLimit [IsProper f₀] [IsClosedImmersion j] :
    IsLimit (residueFiberCone A₀ A f₀ j p)

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