Module

Functoriality.lean

Nyll.SchemeTheory.FunctionFields.Functoriality

6 declarations indexed from sourceView source ↗

Module documentation

Function fields of dominant morphisms

A morphism with dense image between integral schemes sends the generic point to the generic point. Its map on local rings therefore gives the canonical embedding of function fields.

Imports1

Mathlib.AlgebraicGeometry.FunctionField

Imported by12

theorem

eqToHom_stalk_eq_stalkCongr

L29 ↗

AlgebraicGeometry.Scheme.Hom.eqToHom_stalk_eq_stalkCongr

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.Hom
variable {X Y : Scheme.{u}}

Lean source · full declaration

theorem eqToHom_stalk_eq_stalkCongr
    (Z : Scheme.{u}) {z z' : Z} (h : z = z') :
    eqToHom (congrArg (fun w ↦ Z.presheaf.stalk w) h) =
      (Z.presheaf.stalkCongr (.of_eq h)).hom := by
  subst z'
  simp

theorem

map_genericPoint_of_denseRange

L38 ↗

AlgebraicGeometry.Scheme.Hom.map_genericPoint_of_denseRange

Documentation

A dense morphism between irreducible schemes sends the generic point to the generic point.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.Hom
variable {X Y : Scheme.{u}}

Lean source · statement

theorem map_genericPoint_of_denseRange
    (f : Y ⟶ X) [IrreducibleSpace X] [IrreducibleSpace Y]
    (hf : DenseRange f) :
    f (genericPoint Y) = genericPoint X

def

functionFieldMap

L48 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldMap

Documentation

The canonical map on function fields induced by a dense morphism of integral schemes.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.Hom
variable {X Y : Scheme.{u}}

Lean source · statement

def functionFieldMap
    (f : Y ⟶ X) [IsIntegral X] [IsIntegral Y]
    (hf : DenseRange f) :
    X.functionField →+* Y.functionField

theorem

functionFieldMap_injective

L60 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldMap_injective

Documentation

The function-field map of a dense morphism of integral schemes is injective.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.Hom
variable {X Y : Scheme.{u}}

Lean source · statement

theorem functionFieldMap_injective
    (f : Y ⟶ X) [IsIntegral X] [IsIntegral Y]
    (hf : DenseRange f) :
    Function.Injective (functionFieldMap f hf)

theorem

functionFieldMap_comp_germToFunctionField_top

L69 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldMap_comp_germToFunctionField_top

Documentation

On global sections, the function-field map of a dense morphism is the map obtained by first pulling back the section and then taking its germ at the generic point.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.Hom
variable {X Y : Scheme.{u}}

Lean source · full declaration

theorem functionFieldMap_comp_germToFunctionField_top
    (f : Y ⟶ X) [IsIntegral X] [IsIntegral Y]
    (hf : DenseRange f) :
    letI : Nonempty (⊤ : X.Opens) :=
      ⟨⟨Classical.choice (inferInstance : Nonempty X), by simp⟩⟩
    letI : Nonempty (⊤ : Y.Opens) :=
      ⟨⟨Classical.choice (inferInstance : Nonempty Y), by simp⟩⟩
    (functionFieldMap f hf).comp (X.germToFunctionField ⊤).hom =
      (Y.germToFunctionField ⊤).hom.comp f.appTop.hom := by
  let : Nonempty (⊤ : X.Opens) :=
    ⟨⟨Classical.choice (inferInstance : Nonempty X), by simp⟩⟩
  let : Nonempty (⊤ : Y.Opens) :=
    ⟨⟨Classical.choice (inferInstance : Nonempty Y), by simp⟩⟩
  let h : genericPoint X = f (genericPoint Y) :=
    (map_genericPoint_of_denseRange f hf).symm
  have hEq : eqToHom (show
      X.presheaf.stalk (genericPoint X) =
        X.presheaf.stalk (f (genericPoint Y)) by
      rw [map_genericPoint_of_denseRange f hf]) =
      (X.presheaf.stalkCongr (.of_eq h)).hom := by
    convert eqToHom_stalk_eq_stalkCongr X h
  unfold functionFieldMap
  rw [← CommRingCat.hom_comp, ← CommRingCat.hom_comp]
  apply congrArg CommRingCat.Hom.hom
  rw [hEq]
  simp only [TopCat.Presheaf.stalkCongr_hom]
  rw [← Category.assoc]
  erw [TopCat.Presheaf.germ_stalkSpecializes]
  exact f.germ_stalkMap ⊤ (genericPoint Y) (by simp)

def

functionFieldAlgebraOfDenseRange

L101 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldAlgebraOfDenseRange

Documentation

The algebra structure on the target function field induced by a dense morphism of integral schemes.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.Hom
variable {X Y : Scheme.{u}}

Lean source · statement

def functionFieldAlgebraOfDenseRange
    (f : Y ⟶ X) [IsIntegral X] [IsIntegral Y]
    (hf : DenseRange f) :
    Algebra X.functionField Y.functionField

Module documentation

Function fields of dominant morphisms

Declarations

eqToHom_stalk_eq_stalkCongr

map_genericPoint_of_denseRange

functionFieldMap

functionFieldMap_injective

functionFieldMap_comp_germToFunctionField_top

functionFieldAlgebraOfDenseRange