Module

Infinite_setOf_isClosed_singleton.lean

Nyll.AlgebraicCurves.FunctionFields.Infinite_setOf_isClosed_singleton

3 declarations indexed from sourceView source ↗

Module documentation

Infinite setOf isClosed singleton

An integral curve locally of finite type over a field has infinitely many closed points.

Imports2

Imported by3

theorem

isField_of_isMaximal_bot

L35 ↗

AlgebraicCurves.FunctionFields.Proofs.Infinite_setOf_isClosed_singleton.AlgebraicCurve.LInf.isField_of_isMaximal_bot

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Infinite_setOf_isClosed_singleton
open CategoryTheory AlgebraicGeometry IsLocalRing
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace LInf
open _root_.AlgebraicCurve

Lean source · statement

theorem isField_of_isMaximal_bot (A : Type*) [CommRing A] [Nontrivial A]
    (h : (⊥ : Ideal A).IsMaximal) : IsField A

theorem

isField_of_finite_maximalSpectrum

L39 ↗

AlgebraicCurves.FunctionFields.Proofs.Infinite_setOf_isClosed_singleton.AlgebraicCurve.LInf.isField_of_finite_maximalSpectrum

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Infinite_setOf_isClosed_singleton
open CategoryTheory AlgebraicGeometry IsLocalRing
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace LInf
open _root_.AlgebraicCurve

Lean source · statement

theorem isField_of_finite_maximalSpectrum (A : Type*) [CommRing A] [IsDomain A] [IsJacobsonRing A]
    [Finite (MaximalSpectrum A)] : IsField A

theorem

infinite_setOf_isClosed_singleton

L56 ↗

AlgebraicCurve.infinite_setOf_isClosed_singleton

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Infinite_setOf_isClosed_singleton
open CategoryTheory AlgebraicGeometry IsLocalRing
universe u
open AlgebraicCurve.LInf in

Lean source · statement

theorem _root_.AlgebraicCurve.infinite_setOf_isClosed_singleton
    {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
    [IsIntegral C] [SmoothOfRelativeDimension 1 c] :
    {x : C | IsClosed ({x} : Set C)}.Infinite

Module documentation

Infinite setOf isClosed singleton

Declarations

isField_of_isMaximal_bot

isField_of_finite_maximalSpectrum

infinite_setOf_isClosed_singleton