NYLL
Module

StalkFactorization.lean

Nyll.SchemeTheory.FunctionFields.StalkFactorization
5 declarations indexed from sourceView source ↗

Module documentation

Function fields of morphisms factoring through a stalk spectrum

An injective map out of an integral scheme's stalk gives a dominant morphism from the spectrum of its target back to the scheme. The induced function-field map restricts to the original ring map on that stalk.

Imports2
Imported by2

Declarations

theorem

eqToHom_stalk_eq_stalkCongr

L26 ↗
AlgebraicGeometry.Scheme.Hom.eqToHom_stalk_eq_stalkCongr
Source context 4 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe 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

SpecMap_genericPoint_of_injective

L33 ↗
AlgebraicGeometry.Scheme.Hom.SpecMap_genericPoint_of_injective
Source context 4 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
Lean source · statement
theorem SpecMap_genericPoint_of_injective
    {R S : CommRingCat.{u}} [IsDomain R] [IsDomain S]
    (phi : R ⟶ S) (hphi : Function.Injective phi) :
    Spec.map phi (genericPoint (Spec S)) = genericPoint (Spec R)
theorem

fromSpecStalk_genericPoint_eq

L42 ↗
AlgebraicGeometry.Scheme.Hom.fromSpecStalk_genericPoint_eq
Source context 4 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
Lean source · statement
theorem fromSpecStalk_genericPoint_eq
    {X : Scheme.{u}} [IsIntegral X] (x : X) :
    X.fromSpecStalk x (genericPoint (Spec (X.presheaf.stalk x))) =
      genericPoint X
theorem

denseRange_specMap_comp_fromSpecStalk_of_injective

L69 ↗
AlgebraicGeometry.Scheme.Hom.denseRange_specMap_comp_fromSpecStalk_of_injective
Documentation

An injective map from a stalk of an integral scheme defines a dominant morphism from the target spectrum back to the scheme.

Source context 4 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
Lean source · statement
theorem denseRange_specMap_comp_fromSpecStalk_of_injective
    {X : Scheme.{u}} [IsIntegral X] (x : X)
    {S : Type u} [CommRing S] [IsDomain S]
    (phi : X.presheaf.stalk x →+* S) (hphi : Function.Injective phi) :
    DenseRange
      (Spec.map (CommRingCat.ofHom phi) ≫ X.fromSpecStalk x)
theorem

functionFieldMap_comp_stalkFunctionField_of_injective

L94 ↗
AlgebraicGeometry.Scheme.Hom.functionFieldMap_comp_stalkFunctionField_of_injective
Documentation

The function-field map of a morphism presented by an injective map out of a stalk restricts to that ring map, followed by the canonical map to the target fraction field.

Source context 4 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u
Lean source · full declaration
theorem functionFieldMap_comp_stalkFunctionField_of_injective
    {X : Scheme.{u}} [IsIntegral X] (x : X)
    {S : Type u} [CommRing S] [IsDomain S]
    (phi : X.presheaf.stalk x →+* S) (hphi : Function.Injective phi) :
    let g := Spec.map (CommRingCat.ofHom phi) ≫ X.fromSpecStalk x
    let hg : DenseRange g :=
      denseRange_specMap_comp_fromSpecStalk_of_injective x phi hphi
    letI : Algebra S (Spec (.of S)).functionField :=
      AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of S)
    (g.functionFieldMap hg).comp
        (algebraMap (X.presheaf.stalk x) X.functionField) =
      (algebraMap S (Spec (.of S)).functionField).comp phi := by
  dsimp only
  let : Algebra S (Spec (.of S)).functionField :=
    AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (.of S)
  let g : Spec (.of S) ⟶ X :=
    Spec.map (CommRingCat.ofHom phi) ≫ X.fromSpecStalk x
  let hg : DenseRange g :=
    denseRange_specMap_comp_fromSpecStalk_of_injective x phi hphi
  have hgeneric : g (genericPoint (Spec (.of S))) = genericPoint X :=
    g.map_genericPoint_of_denseRange hg
  let lhs : X.presheaf.stalk x →+* (Spec (.of S)).functionField :=
    (g.functionFieldMap hg).comp
      (algebraMap (X.presheaf.stalk x) X.functionField)
  let rhs : X.presheaf.stalk x →+* (Spec (.of S)).functionField :=
    (algebraMap S (Spec (.of S)).functionField).comp phi
  change lhs = rhs
  have hspec : Spec.map (CommRingCat.ofHom lhs) =
      Spec.map (CommRingCat.ofHom rhs) := by
    apply (cancel_mono (X.fromSpecStalk x)).mp
    dsimp only [lhs, rhs]
    rw [show
      CommRingCat.ofHom
          ((g.functionFieldMap hg).comp
              (algebraMap (X.presheaf.stalk x) X.functionField)) =
        CommRingCat.ofHom
            (algebraMap (X.presheaf.stalk x) X.functionField) ≫
          CommRingCat.ofHom (g.functionFieldMap hg) by rfl]
    rw [show
      CommRingCat.ofHom
          ((algebraMap S (Spec (.of S)).functionField).comp phi) =
        CommRingCat.ofHom phi ≫
          CommRingCat.ofHom
            (algebraMap S (Spec (.of S)).functionField) by rfl]
    rw [Spec.map_comp, Spec.map_comp]
    simp only [Category.assoc]
    rw [show
      CommRingCat.ofHom
          (algebraMap (X.presheaf.stalk x) X.functionField) =
        X.presheaf.stalkSpecializes (genericPoint_specializes x) by rfl]
    rw [Scheme.SpecMap_stalkSpecializes_fromSpecStalk]
    rw [show
      Spec.map (CommRingCat.ofHom
          (algebraMap S (Spec (.of S)).functionField)) =
        (Spec (.of S)).fromSpecStalk (genericPoint (Spec (.of S))) from
      (Spec.fromSpecStalk_eq' (.of S) (genericPoint (Spec (.of S)))).symm]
    unfold functionFieldMap
    rw [show
      CommRingCat.ofHom
          (CommRingCat.Hom.hom
            (eqToHom _ ≫
              g.stalkMap (genericPoint (Spec (.of S))))) =
        eqToHom _ ≫
          g.stalkMap (genericPoint (Spec (.of S))) by rfl]
    rw [Spec.map_comp]
    simp only [Category.assoc]
    rw [eqToHom_stalk_eq_stalkCongr]
    all_goals try exact hgeneric.symm
    dsimp only [TopCat.Presheaf.stalkCongr]
    change Spec.map (g.stalkMap (genericPoint (Spec (.of S)))) ≫
      Spec.map (X.presheaf.stalkSpecializes (specializes_of_eq hgeneric)) ≫
        X.fromSpecStalk (genericPoint X) = _
    rw [Scheme.SpecMap_stalkSpecializes_fromSpecStalk]
    rw [Scheme.SpecMap_stalkMap_fromSpecStalk]
  have hhom :
      CommRingCat.Hom.hom (CommRingCat.ofHom lhs) =
        CommRingCat.Hom.hom (CommRingCat.ofHom rhs) :=
    congrArg CommRingCat.Hom.hom (Spec.map_injective hspec)
  exact hhom

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