Module

AffineLimit.lean

Nyll.AlgebraicCurves.Geometry.Schemes.AffineLimit

6 declarations indexed from sourceView source ↗

Module documentation

Relative affine spectra and finite-subalgebra descent and equality-detection conditions.

Imports1

Mathlib.AlgebraicGeometry.Scheme

Imported by18

abbrev

specOver

L28 ↗

AlgebraicGeometry.AffineLimit.specOver

Documentation

The affine spectrum of an R-algebra, viewed as an object over Spec R.

Source context 4 commands

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

universe w u
open CategoryTheory Opposite
namespace AlgebraicGeometry.AffineLimit
variable (R : Type u) [CommRing R]

Lean source · statement

abbrev specOver (A : Type u) [CommRing A] [Algebra R A] :
    Over (Spec (CommRingCat.of R))

abbrev

specOverOfSubalgebra

L33 ↗

AlgebraicGeometry.AffineLimit.specOverOfSubalgebra

Documentation

The morphism of relative affine spectra induced by a subalgebra inclusion.

Source context 4 commands

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

universe w u
open CategoryTheory Opposite
namespace AlgebraicGeometry.AffineLimit
variable (R : Type u) [CommRing R]

Lean source · statement

abbrev specOverOfSubalgebra {A : Type u} [CommRing A] [Algebra R A]
    (A₀ : Subalgebra R A) :
    specOver R A ⟶ specOver R A₀

abbrev

specOverOfLE

L41 ↗

AlgebraicGeometry.AffineLimit.specOverOfLE

Documentation

The morphism of relative affine spectra induced by an inclusion of two subalgebras.

Source context 4 commands

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

universe w u
open CategoryTheory Opposite
namespace AlgebraicGeometry.AffineLimit
variable (R : Type u) [CommRing R]

Lean source · statement

abbrev specOverOfLE {A : Type u} [CommRing A] [Algebra R A]
    (A₀ A₁ : Subalgebra R A) (h : A₀ ≤ A₁) :
    specOver R A₁ ⟶ specOver R A₀

def

IsLFPSurj

L51 ↗

AlgebraicGeometry.AffineLimit.IsLFPSurj

Documentation

Every functor-valued point descends to a finitely generated subalgebra.

Source context 5 commands

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

universe w u
open CategoryTheory Opposite
namespace AlgebraicGeometry.AffineLimit
variable (R : Type u) [CommRing R]
variable {R}

Lean source · statement

def IsLFPSurj (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type w) : Prop

def

IsLFPInj

L57 ↗

AlgebraicGeometry.AffineLimit.IsLFPInj

Documentation

Equality of functor-valued points is detected at a larger finitely generated subalgebra.

Source context 5 commands

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

universe w u
open CategoryTheory Opposite
namespace AlgebraicGeometry.AffineLimit
variable (R : Type u) [CommRing R]
variable {R}

Lean source · statement

def IsLFPInj (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type w) : Prop

def

HomIsLFP

L65 ↗

AlgebraicGeometry.AffineLimit.HomIsLFP

Documentation

Finite-subalgebra descent and equality detection for a morphism to an affine spectrum.

Source context 5 commands

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

universe w u
open CategoryTheory Opposite
namespace AlgebraicGeometry.AffineLimit
variable (R : Type u) [CommRing R]
variable {R}

Lean source · statement

def HomIsLFP {X : Scheme.{u}} (ξ : X ⟶ Spec (CommRingCat.of R)) : Prop

Module documentation

Declarations

specOver

specOverOfSubalgebra

specOverOfLE

IsLFPSurj

IsLFPInj

HomIsLFP