Module

GeometricIntegrality.lean

Nyll.SchemeTheory.FunctionFields.GeometricIntegrality

10 declarations indexed from sourceView source ↗

Module documentation

Geometric integrality of function fields

This file proves that passing from a geometrically integral domain over a field to its fraction field preserves geometric integrality. It then applies this ring-theoretic fact to the function field of an integral scheme.

Imports4

Nyll.SchemeTheory.Morphisms.EtalePostcomposition
Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.RingTheory.Localization.BaseChange

Imported by2

theorem

isDomain_of_isFractionRing_left

L31 ↗

Algebra.TensorProduct.isDomain_of_isFractionRing_left

Documentation

Base change of a domain along a fraction field remains a domain whenever the base change of the original domain is a domain.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace Algebra
namespace TensorProduct

Lean source · statement

theorem isDomain_of_isFractionRing_left
    {k R K L : Type u}
    [Field k] [CommRing R] [IsDomain R] [Algebra k R]
    [Field K] [Algebra k K] [Algebra R K] [IsScalarTower k R K]
    [IsFractionRing R K] [Field L] [Algebra k L]
    [IsDomain (TensorProduct k R L)] :
    IsDomain (TensorProduct k K L)

theorem

comp_of_isOpenImmersion

L91 ↗

AlgebraicGeometry.GeometricallyIntegral.comp_of_isOpenImmersion

Documentation

A surjective open subscheme of a geometrically integral scheme is geometrically integral over the same base.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

theorem GeometricallyIntegral.comp_of_isOpenImmersion
    {U X S : Scheme.{u}} (i : U ⟶ X) (f : X ⟶ S)
    [IsOpenImmersion i] [GeometricallyIntegral f] [Surjective (i ≫ f)] :
    GeometricallyIntegral (i ≫ f)

theorem

spec_of_isFractionRing

L101 ↗

AlgebraicGeometry.GeometricallyIntegral.spec_of_isFractionRing

Documentation

If K is a fraction field of a geometrically integral k-domain R, then Spec K is geometrically integral over k.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

theorem GeometricallyIntegral.spec_of_isFractionRing
    {k R K : Type u}
    [Field k] [CommRing R] [IsDomain R] [Algebra k R]
    [Field K] [Algebra k K] [Algebra R K] [IsScalarTower k R K]
    [IsFractionRing R K]
    [GeometricallyIntegral
      (Spec.map (CommRingCat.ofHom (algebraMap k R)))] :
    GeometricallyIntegral
      (Spec.map (CommRingCat.ofHom (algebraMap k K)))

def

functionFieldAlgebra

L135 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldAlgebra

Documentation

The algebra structure on the function field induced by a morphism to an affine base.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

def Scheme.Hom.functionFieldAlgebra
    {R : Type u} [CommRing R] {X : Scheme.{u}} [IrreducibleSpace X]
    (f : X ⟶ Spec (.of R)) : Algebra R X.functionField

def

sectionAlgebra

L141 ↗

AlgebraicGeometry.sectionAlgebra

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

def sectionAlgebra
    {k : Type u} [CommRing k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (U : X.Opens) :
    Algebra k Γ(X, U)

lemma

hom_eq_isoSpec_hom_comp_specMap

L148 ↗

AlgebraicGeometry.hom_eq_isoSpec_hom_comp_specMap

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

lemma hom_eq_isoSpec_hom_comp_specMap
    {R : Type u} [CommRing R] {Z : Scheme.{u}} [IsAffine Z]
    (p : Z ⟶ Spec (.of R)) :
    p = Z.isoSpec.hom ≫ Spec.map
      ((Scheme.ΓSpecIso (.of R)).inv ≫ p.appTop)

lemma

comp_open_eq_isoSpec_hom_comp_specMap_algebraMap

L180 ↗

AlgebraicGeometry.comp_open_eq_isoSpec_hom_comp_specMap_algebraMap

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

lemma comp_open_eq_isoSpec_hom_comp_specMap_algebraMap
    {k : Type u} [CommRing k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (U : X.Opens) (hU : IsAffineOpen U) :
    U.ι ≫ f = hU.isoSpec.hom ≫
      Spec.map (CommRingCat.ofHom
        (@algebraMap k Γ(X, U) _ _ (sectionAlgebra f U)))

lemma

comp_open_appTop_topIso

L207 ↗

AlgebraicGeometry.comp_open_appTop_topIso

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · full declaration

lemma comp_open_appTop_topIso
    {k : Type u} [CommRing k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (U : X.Opens) :
    (U.ι ≫ f).appTop ≫ U.topIso.hom =
      f.appTop ≫ X.presheaf.map (homOfLE (show U ≤ ⊤ from le_top)).op := by
  rw [Scheme.Hom.comp_appTop, Category.assoc]
  congr 1
  change X.presheaf.map (homOfLE (x := U.ι ''ᵁ ⊤) le_top).op ≫
      X.presheaf.map (eqToHom U.ι_image_top.symm).op = _
  rw [← Functor.map_comp]
  rfl

lemma

functionFieldAlgebra_eq_comp_sectionAlgebra

L219 ↗

AlgebraicGeometry.functionFieldAlgebra_eq_comp_sectionAlgebra

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

lemma functionFieldAlgebra_eq_comp_sectionAlgebra
    {k : Type u} [CommRing k] {X : Scheme.{u}} [IrreducibleSpace X]
    (f : X ⟶ Spec (.of k)) (U : X.Opens) [Nonempty U] :
    @algebraMap k X.functionField _ _ f.functionFieldAlgebra =
      (@algebraMap Γ(X, U) X.functionField _ _
        (inferInstance : Algebra Γ(X, U) X.functionField)).comp
        (@algebraMap k Γ(X, U) _ _ (sectionAlgebra f U))

theorem

spec_functionField

L253 ↗

AlgebraicGeometry.GeometricallyIntegral.spec_functionField

Documentation

The function field of an integral, geometrically integral scheme over a field is geometrically integral over that field.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
open Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

theorem GeometricallyIntegral.spec_functionField
    {k : Type u} [Field k] {X : Scheme.{u}} [IsIntegral X]
    (f : X ⟶ Spec (.of k)) [GeometricallyIntegral f] :
    GeometricallyIntegral
      (Spec.map (CommRingCat.ofHom
        (@algebraMap k X.functionField _ _ f.functionFieldAlgebra)))

Module documentation

Geometric integrality of function fields

Declarations