Module

AffineIntegralLimit.lean

Nyll.SchemeTheory.Descent.AffineIntegralLimit

11 declarations indexed from sourceView source ↗

Module documentation

Affine integral morphisms as limits of finite-FP schemes

Apply the native Spec limit-preservation theorem to the actual small finite-FP ring-model colimit. The resulting scheme diagram has its genuine maps to the original affine base, with finite and locally finitely presented stage maps and the actual limit cone. Surjectivity of the original morphism implies surjectivity of each stage map by the proved factorization.

The existing finitely generated subalgebra limit family uses inclusion maps and does not supply arbitrary-base finite presentation. Here the finite-FP model diagram is used directly; no global relative-Spec or gluing comparison is assumed.

Imports11

Nyll.SchemeTheory.RingTheory.IntegralFinitePresentationColimit
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.Limits.Opposites
Mathlib.CategoryTheory.Limits.Preserves.Basic
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.FinitePresentation

Imported by2

def

diagram

L46 ↗

AlgebraicGeometry.AffineIntegralLimit.diagram

Documentation

The actual cofiltered affine scheme diagram dual to the small ring diagram.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

def diagram : (FinitePresentationModel R B)ᵒᵖ ⥤ Scheme.{u}

def

cone

L50 ↗

AlgebraicGeometry.AffineIntegralLimit.cone

Documentation

The actual cone with vertex Spec B.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

def cone : Cone (diagram R B)

def

coneIsLimit

L54 ↗

AlgebraicGeometry.AffineIntegralLimit.coneIsLimit

Documentation

Native Spec preservation turns the proved ring colimit into a scheme limit.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

def coneIsLimit [Algebra.IsIntegral R B] : IsLimit (cone R B)

def

baseMap

L58 ↗

AlgebraicGeometry.AffineIntegralLimit.baseMap

Documentation

The algebra structure maps give the diagram's morphism to the original base.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · full declaration

def baseMap : diagram R B ⟶
    (Functor.const (FinitePresentationModel R B)ᵒᵖ).obj (Spec (CommRingCat.of R)) where
  app i := Spec.map (CommRingCat.ofHom (algebraMap R i.unop.stage))
  naturality i j f := by
    let α : j.unop.presentation.eval.obj →ₐ[R] i.unop.presentation.eval.obj :=
      f.unop.hom.left.hom
    change Spec.map (CommRingCat.ofHom α.toRingHom) ≫
        Spec.map (CommRingCat.ofHom (algebraMap R j.unop.stage)) =
      Spec.map (CommRingCat.ofHom (algebraMap R i.unop.stage)) ≫ 𝟙 _
    rw [Category.comp_id, ← Spec.map_comp, ← CommRingCat.ofHom_comp]
    exact congrArg (fun ψ : R →+* i.unop.stage => Spec.map (CommRingCat.ofHom ψ))
      α.comp_algebraMap

theorem

projection_comp_base

L72 ↗

AlgebraicGeometry.AffineIntegralLimit.projection_comp_base

Documentation

Each cone projection is an actual factorization of the original affine morphism.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

theorem projection_comp_base (i : (FinitePresentationModel R B)ᵒᵖ) :
    (cone R B).π.app i ≫ (baseMap R B).app i =
      Spec.map (CommRingCat.ofHom (algebraMap R B))

theorem

cone_π_comp_baseMap

L83 ↗

AlgebraicGeometry.AffineIntegralLimit.cone_π_comp_baseMap

Documentation

The factorization holds for the complete cone morphism over the base.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

theorem cone_π_comp_baseMap :
    (cone R B).π ≫ baseMap R B =
      (Functor.const (FinitePresentationModel R B)ᵒᵖ).map
        (Spec.map (CommRingCat.ofHom (algebraMap R B)))

instance

(anonymous instance)

L91 ↗

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

instance (i : (FinitePresentationModel R B)ᵒᵖ) : IsAffine ((diagram R B).obj i)

instance

(anonymous instance)

L94 ↗

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

instance {i j : (FinitePresentationModel R B)ᵒᵖ} (f : i ⟶ j) :
    IsAffineHom ((diagram R B).map f)

instance

(anonymous instance)

L99 ↗

Documentation

Every actual stage morphism is finite over the original base.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

instance (i : (FinitePresentationModel R B)ᵒᵖ) : IsFinite ((baseMap R B).app i)

instance

(anonymous instance)

L105 ↗

Documentation

Every stage morphism is locally of finite presentation; together with finiteness this gives a finite morphism of finite presentation.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

instance (i : (FinitePresentationModel R B)ᵒᵖ) :
    LocallyOfFinitePresentation ((baseMap R B).app i)

instance

(anonymous instance)

L113 ↗

Documentation

Surjectivity of the original affine morphism descends to every stage map.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry.AffineIntegralLimit
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

instance [hSurj : Surjective (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
    (i : (FinitePresentationModel R B)ᵒᵖ) : Surjective ((baseMap R B).app i)

Module documentation

Affine integral morphisms as limits of finite-FP schemes

Declarations