Module

jacobsonSpace_of_locallyOfFiniteType.lean

Nyll.AlgebraicCurves.Geometry.Schemes.jacobsonSpace_of_locallyOfFiniteType

1 declaration indexed from sourceView source ↗

Module documentation

jacobson Space of locally Of Finite Type

Imports1

Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Imported by2

Nyll.AlgebraicCurves.Geometry.Schemes.All
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_tensorPow_three_of_forall_nonempty_pullback_tensor_iso

theorem

jacobsonSpace_of_locallyOfFiniteType

L27 ↗

AlgebraicGeometry.jacobsonSpace_of_locallyOfFiniteType

Source context 4 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.jacobsonSpace_of_locallyOfFiniteType
    {k : Type u} [Field k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k)) [LocallyOfFiniteType
      t] :
    JacobsonSpace X

Module documentation

jacobson Space of locally Of Finite Type

Declarations

jacobsonSpace_of_locallyOfFiniteType