NYLL
Module

OpenFunctionField.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenFunctionField
7 declarations indexed from sourceView source ↗

Module documentation

Function fields of dense open subschemes

An open immersion between integral schemes identifies their function fields. The equivalence below is the literal function-field map induced by the open immersion, so it can be used in scalar-tower comparisons.

Imports2
Imported by7

Declarations

theorem

denseRange_of_isOpenImmersion

L28 ↗
AlgebraicGeometry.Scheme.Hom.denseRange_of_isOpenImmersion
Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X U : Scheme.{u}}
Lean source · statement
theorem denseRange_of_isOpenImmersion
    [IsIntegral X] [IsIntegral U]
    (j : U ⟶ X) [IsOpenImmersion j] :
    DenseRange j
theorem

functionFieldMap_bijective_of_isOpenImmersion

L36 ↗
AlgebraicGeometry.Scheme.Hom.functionFieldMap_bijective_of_isOpenImmersion
Documentation

The canonical function-field map of an open immersion of integral schemes is bijective.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X U : Scheme.{u}}
Lean source · statement
theorem functionFieldMap_bijective_of_isOpenImmersion
    [IsIntegral X] [IsIntegral U]
    (j : U ⟶ X) [IsOpenImmersion j] :
    Function.Bijective
      (j.functionFieldMap (denseRange_of_isOpenImmersion j))
def

functionFieldRingEquivOfIsOpenImmersion

L46 ↗
AlgebraicGeometry.Scheme.Hom.functionFieldRingEquivOfIsOpenImmersion
Documentation

A dense open subscheme has canonically the same function field as its ambient integral scheme.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X U : Scheme.{u}}
Lean source · statement
def functionFieldRingEquivOfIsOpenImmersion
    [IsIntegral X] [IsIntegral U]
    (j : U ⟶ X) [IsOpenImmersion j] :
    X.functionField ≃+* U.functionField
theorem

functionFieldRingEquivOfIsOpenImmersion_apply

L55 ↗
AlgebraicGeometry.Scheme.Hom.functionFieldRingEquivOfIsOpenImmersion_apply
Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X U : Scheme.{u}}
Lean source · statement
theorem functionFieldRingEquivOfIsOpenImmersion_apply
    [IsIntegral X] [IsIntegral U]
    (j : U ⟶ X) [IsOpenImmersion j] (a : X.functionField) :
    j.functionFieldRingEquivOfIsOpenImmersion a =
      j.functionFieldMap (denseRange_of_isOpenImmersion j) a
def

functionFieldAlgebraOfIsOpenImmersionSpec

L65 ↗
AlgebraicGeometry.Scheme.Hom.functionFieldAlgebraOfIsOpenImmersionSpec
Documentation

The algebra structure on the function field of an integral open subscheme of Spec R, induced from the canonical fraction-field algebra of the ambient affine scheme.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X U : Scheme.{u}}
Lean source · statement
def functionFieldAlgebraOfIsOpenImmersionSpec
    (R : CommRingCat.{u}) [IsDomain R]
    {U : Scheme.{u}} [IsIntegral U]
    (j : U ⟶ Spec R) [IsOpenImmersion j] :
    Algebra R U.functionField
def

functionFieldAlgEquivOfIsOpenImmersionSpec

L75 ↗
AlgebraicGeometry.Scheme.Hom.functionFieldAlgEquivOfIsOpenImmersionSpec
Documentation

The function-field equivalence of an integral open subscheme of an affine integral scheme, as an equivalence over the literal affine ring.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X U : Scheme.{u}}
Lean source · full declaration
def functionFieldAlgEquivOfIsOpenImmersionSpec
    (R : CommRingCat.{u}) [IsDomain R]
    {U : Scheme.{u}} [IsIntegral U]
    (j : U ⟶ Spec R) [IsOpenImmersion j] :
    letI : Algebra R U.functionField :=
      j.functionFieldAlgebraOfIsOpenImmersionSpec R
    (Spec R).functionField ≃ₐ[R] U.functionField := by
  letI : Algebra R U.functionField :=
    j.functionFieldAlgebraOfIsOpenImmersionSpec R
  exact
    { j.functionFieldRingEquivOfIsOpenImmersion with
      commutes' := fun _ ↦ rfl }
theorem

functionField_isFractionRing_of_isOpenImmersionSpec

L90 ↗
AlgebraicGeometry.Scheme.Hom.functionField_isFractionRing_of_isOpenImmersionSpec
Documentation

The function field of a nonempty integral open subscheme of Spec R is a fraction field of the literal domain R.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X U : Scheme.{u}}
Lean source · full declaration
theorem functionField_isFractionRing_of_isOpenImmersionSpec
    (R : CommRingCat.{u}) [IsDomain R]
    {U : Scheme.{u}} [IsIntegral U]
    (j : U ⟶ Spec R) [IsOpenImmersion j] :
    letI : Algebra R U.functionField :=
      j.functionFieldAlgebraOfIsOpenImmersionSpec R
    IsFractionRing R U.functionField := by
  let : Algebra R U.functionField :=
    j.functionFieldAlgebraOfIsOpenImmersionSpec R
  let : IsFractionRing R (Spec R).functionField :=
    AlgebraicGeometry.functionField_isFractionRing_of_affine R
  exact IsFractionRing.of_algEquiv
    (j.functionFieldAlgEquivOfIsOpenImmersionSpec R)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.