Module

StalkFunctoriality.lean

Nyll.SchemeTheory.FunctionFields.StalkFunctoriality

4 declarations indexed from sourceView source ↗

Module documentation

Function-field maps and local rings

The canonical map on function fields commutes with every stalk map, not only with global sections. For an open immersion it therefore identifies the actual local-ring subrings. This supplies the local equations needed when restricting a Kummer construction to an open curve.

Imports2

Nyll.SchemeTheory.FunctionFields.Functoriality
Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Imported by4

theorem

eqToHom_stalk_eq_stalkCongr'

L30 ↗

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.Scheme.Hom
universe u
variable {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
omit [IsIntegral X] in

Lean source · full declaration

theorem eqToHom_stalk_eq_stalkCongr'
    {x x' : X} (h : x = x') :
    eqToHom (congrArg (fun z => X.presheaf.stalk z) h) =
      (X.presheaf.stalkCongr (.of_eq h)).hom := by
  subst x'
  simp only [eqToHom_refl, TopCat.Presheaf.stalkCongr_hom,
    TopCat.Presheaf.stalkSpecializes_refl]

theorem

functionFieldMap_comp_germToFunctionField

L40 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldMap_comp_germToFunctionField

Documentation

Function-field pullback commutes with taking the generic germ of a section over any nonempty open, with nonempty inverse image.

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 Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem functionFieldMap_comp_germToFunctionField
    (f : Y ⟶ X) (hf : DenseRange f) (U : X.Opens)
    [Nonempty U] [Nonempty (f ⁻¹ᵁ U)] :
    (f.functionFieldMap hf).comp (X.germToFunctionField U).hom =
      (Y.germToFunctionField (f ⁻¹ᵁ U)).hom.comp (f.app U).hom

theorem

functionFieldMap_algebraMap_stalk

L66 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldMap_algebraMap_stalk

Documentation

The actual map on function fields commutes with the actual map on local rings at every point.

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 Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem functionFieldMap_algebraMap_stalk
    (f : Y ⟶ X) (hf : DenseRange f) (y : Y) (a : X.presheaf.stalk (f y)) :
    f.functionFieldMap hf (algebraMap (X.presheaf.stalk (f y)) X.functionField a) =
      algebraMap (Y.presheaf.stalk y) Y.functionField (f.stalkMap y a)

theorem

functionFieldMap_mem_stalk_range_iff_of_isOpenImmersion

L85 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldMap_mem_stalk_range_iff_of_isOpenImmersion

Documentation

An open immersion identifies, inside the identified function fields, the actual local-ring images at corresponding points.

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 Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]

Lean source · statement

theorem functionFieldMap_mem_stalk_range_iff_of_isOpenImmersion
    (f : Y ⟶ X) [IsOpenImmersion f] (hf : DenseRange f) (y : Y)
    (a : X.functionField) :
    f.functionFieldMap hf a ∈ (algebraMap (Y.presheaf.stalk y) Y.functionField).range ↔
      a ∈ (algebraMap (X.presheaf.stalk (f y)) X.functionField).range

Module documentation

Function-field maps and local rings

Declarations

eqToHom_stalk_eq_stalkCongr'

functionFieldMap_comp_germToFunctionField

functionFieldMap_algebraMap_stalk

functionFieldMap_mem_stalk_range_iff_of_isOpenImmersion