Module

FGSubalgebra_nonempty_isLimit_specCone.lean

Nyll.AlgebraicCurves.Geometry.Schemes.FGSubalgebra_nonempty_isLimit_specCone

1 declaration indexed from sourceView source ↗

Module documentation

Spectra of finitely generated subalgebras form an inverse limit

Applying the spectrum functor to the colimit presentation by finitely generated subalgebras gives the canonical limit cone with the spectrum of the original algebra as its vertex.

Imports2

Imported by4

theorem

nonempty_isLimit_specCone

L31 ↗

AlgebraicGeometry.FGSubalgebra.nonempty_isLimit_specCone

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.FGSubalgebra_nonempty_isLimit_specCone
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u

Lean source · statement

theorem _root_.AlgebraicGeometry.FGSubalgebra.nonempty_isLimit_specCone
    (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] :
    Nonempty (IsLimit (FGSubalgebra.specCone R A))

Module documentation

Spectra of finitely generated subalgebras form an inverse limit

Declarations

nonempty_isLimit_specCone