Module

FiniteExtensionPoint.lean

Nyll.AlgebraicCurves.Geometry.Schemes.FiniteExtensionPoint

5 declarations indexed from sourceView source ↗

Module documentation

A point after a finite extension of the ground field

A closed point of a nonempty scheme locally of finite type has a finite residue field. Its actual residue-field morphism gives a section after base change. No separability or characteristic assumption enters the construction.

Imports6

Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Mathlib.RingTheory.Jacobson.Ring
Mathlib.Topology.JacobsonSpace
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurveBase

Imported by2

def

pointResidueAlgebra

L40 ↗

AlgebraicGeometry.Scheme.pointResidueAlgebra

Documentation

The ground-field algebra structure on the residue field induced by the structure map.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace AlgebraicGeometry.Scheme
variable {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K))

Lean source · statement

def pointResidueAlgebra (x : X) : Algebra K (X.residueField x)

theorem

pointResidueAlgebra_specMap

L43 ↗

AlgebraicGeometry.Scheme.pointResidueAlgebra_specMap

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace AlgebraicGeometry.Scheme
variable {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K))

Lean source · full declaration

theorem pointResidueAlgebra_specMap (x : X) :
    let _ : Algebra K (X.residueField x) := pointResidueAlgebra f x
    specMap K (X.residueField x) = X.fromSpecResidueField x ≫ f := by
  intro a
  exact Spec.map_preimage (X.fromSpecResidueField x ≫ f)

def

pointResidueSection

L50 ↗

AlgebraicGeometry.Scheme.pointResidueSection

Documentation

The residue-field point gives an actual section of the base-changed scheme.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace AlgebraicGeometry.Scheme
variable {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K))

Lean source · full declaration

def pointResidueSection (x : X) :
    let _ : Algebra K (X.residueField x) := pointResidueAlgebra f x
    SchemeHomOver (𝟙 (Spec (CommRingCat.of (X.residueField x))))
      (baseChange K f (X.residueField x)) := by
  intro a
  exact ⟨pullback.lift (X.fromSpecResidueField x) (𝟙 _)
    (by rw [Category.id_comp, pointResidueAlgebra_specMap f x]), pullback.lift_snd _ _ _⟩

theorem

pointResidueAlgebra_finite

L58 ↗

AlgebraicGeometry.Scheme.pointResidueAlgebra_finite

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace AlgebraicGeometry.Scheme
variable {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K))

Lean source · full declaration

theorem pointResidueAlgebra_finite [LocallyOfFiniteType f] (x : X)
    (hx : IsClosed ({x} : Set X)) :
    let _ : Algebra K (X.residueField x) := pointResidueAlgebra f x
    Module.Finite K (X.residueField x) := by
  intro a
  have : JacobsonSpace X := LocallyOfFiniteType.jacobsonSpace f
  have : LocallyOfFiniteType (X.fromSpecResidueField x) :=
    isClosed_singleton_iff_locallyOfFiniteType.1 hx
  have hφ : LocallyOfFiniteType (Spec.map (Spec.preimage (X.fromSpecResidueField x ≫ f))) := by
    rw [Spec.map_preimage]
    infer_instance
  have hft : RingHom.FiniteType (Spec.preimage (X.fromSpecResidueField x ≫ f)).hom :=
    HasRingHomProperty.Spec_iff.mp hφ
  have : Algebra.FiniteType K (X.residueField x) := hft
  exact finite_of_finite_type_of_isJacobsonRing K (X.residueField x)

theorem

exists_finite_pointResidueAlgebra

L76 ↗

AlgebraicGeometry.Scheme.exists_finite_pointResidueAlgebra

Documentation

A nonempty scheme locally of finite type over a field has a closed point with finite residue extension, with the algebra structure fixed by its actual point map.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace AlgebraicGeometry.Scheme
variable {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K))

Lean source · full declaration

theorem exists_finite_pointResidueAlgebra [LocallyOfFiniteType f] [Nonempty X] :
    ∃ x : X, IsClosed ({x} : Set X) ∧
      let _ : Algebra K (X.residueField x) := pointResidueAlgebra f x
      Module.Finite K (X.residueField x) := by
  have : JacobsonSpace X := LocallyOfFiniteType.jacobsonSpace f
  obtain ⟨x, -, hx⟩ := nonempty_inter_closedPoints
    (Set.univ_nonempty : (Set.univ : Set X).Nonempty) isClosed_univ.isLocallyClosed
  exact ⟨x, hx, pointResidueAlgebra_finite f x hx⟩

Module documentation

A point after a finite extension of the ground field

Declarations

pointResidueAlgebra

pointResidueAlgebra_specMap

pointResidueSection

pointResidueAlgebra_finite

exists_finite_pointResidueAlgebra