Module

IsClosed_singleton_of_ne_genericPoint.lean

Nyll.AlgebraicCurves.Geometry.IsClosed_singleton_of_ne_genericPoint

2 declarations indexed from sourceView source ↗

Module documentation

Closed points of an integral smooth curve

On an integral curve smooth of relative dimension one over a field, every point other than the generic point has a closed singleton.

Imports3

Imported by16

theorem

isMaximal_of_isPrime_of_ne_bot

L38 ↗

AlgebraicCurves.Geometry.Proofs.IsClosed_singleton_of_ne_genericPoint.Algebra.IsStandardSmoothOfRelativeDimension.isMaximal_of_isPrime_of_ne_bot

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.IsClosed_singleton_of_ne_genericPoint
universe u v
open CategoryTheory AlgebraicGeometry IsLocalRing Topology
open scoped _root_.Algebra _root_.Algebra.IsStandardSmoothOfRelativeDimension in

Lean source · statement

theorem Algebra.IsStandardSmoothOfRelativeDimension.isMaximal_of_isPrime_of_ne_bot
    {k : Type u} [Field k] {A : Type v} [CommRing A] [IsDomain A] [Algebra k A]
    [Algebra.IsStandardSmoothOfRelativeDimension 1 k A]
    (q : Ideal A) [hq : q.IsPrime] (hq0 : q ≠ ⊥) : q.IsMaximal

theorem