Module

GenericFieldSourceNaturality.lean

Nyll.EtaleFundamentalGroups.Normalization.GenericFieldSourceNaturality

5 declarations indexed from sourceView source ↗

Module documentation

Naturality of the actual generic-field source identification

Imports2

Imported by4

theorem

eqToHom_stalk_eq_specializes

L20 ↗

EtaleFundamentalGroups.eqToHom_stalk_eq_specializes

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem eqToHom_stalk_eq_specializes
    (X : Scheme.{u}) {x y : X} (h : x = y) :
    eqToHom (congrArg (fun z => X.presheaf.stalk z) h) =
      X.presheaf.stalkSpecializes (specializes_of_eq h.symm) := by
  subst y
  simp only [eqToHom_refl, TopCat.Presheaf.stalkSpecializes_refl]

theorem

Spec_functionFieldMap_fromSpecStalk

L29 ↗

EtaleFundamentalGroups.Spec_functionFieldMap_fromSpecStalk

Documentation

The canonical function-field map is compatible with the original generic-point morphisms of schemes.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem Spec_functionFieldMap_fromSpecStalk
    {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
    (f : Y ⟶ X) (hf : DenseRange f) :
    Spec.map (CommRingCat.ofHom (f.functionFieldMap hf)) ≫
        X.fromSpecStalk (genericPoint X) =
      Y.fromSpecStalk (genericPoint Y) ≫ f

theorem

functionFieldMap_comp_of_dense

L46 ↗

EtaleFundamentalGroups.functionFieldMap_comp_of_dense

Documentation

Composition of the literal function-field maps, detected at the actual generic-point morphism.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem functionFieldMap_comp_of_dense
    {X Y Z : Scheme.{u}} [IsIntegral X] [IsIntegral Y] [IsIntegral Z]
    (f : Y ⟶ X) (hf : DenseRange f) (g : Z ⟶ Y) (hg : DenseRange g) :
    let hgf : DenseRange (g ≫ f) := hf.comp hg f.continuous
    (g.functionFieldMap hg).comp (f.functionFieldMap hf) =
      (g ≫ f).functionFieldMap hgf := by
  intro hgf
  have h : CommRingCat.ofHom ((g.functionFieldMap hg).comp (f.functionFieldMap hf)) =
      CommRingCat.ofHom ((g ≫ f).functionFieldMap hgf) := by
    apply Spec.map_injective
    apply (cancel_mono (X.fromSpecStalk (genericPoint X))).mp
    change Spec.map (CommRingCat.ofHom (f.functionFieldMap hf) ≫
      CommRingCat.ofHom (g.functionFieldMap hg)) ≫ _ = _
    rw [Spec.map_comp, Category.assoc, Spec_functionFieldMap_fromSpecStalk f hf,
      ← Category.assoc, Spec_functionFieldMap_fromSpecStalk g hg,
      Category.assoc, Spec_functionFieldMap_fromSpecStalk (g ≫ f) hgf]
  exact congrArg CommRingCat.Hom.hom h

theorem

genericFieldSourceRingEquiv_comp_functionFieldMap

L66 ↗

EtaleFundamentalGroups.genericFieldSourceRingEquiv_comp_functionFieldMap

Documentation

Identifying an actual generic field source with the function field of its target respects the actual extension map from the base.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem genericFieldSourceRingEquiv_comp_functionFieldMap
    {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
    (f : Y ⟶ X) (hf : DenseRange f)
    {L : Type u} [Field L] [Algebra X.functionField L]
    (p : Spec (.of L) ⟶ Y) [IsDominant p] [IsPreimmersion p]
    (hp : p ≫ f = Spec.map (CommRingCat.ofHom (algebraMap X.functionField L)) ≫
      X.fromSpecStalk (genericPoint X)) :
    (genericFieldSourceRingEquiv p).toRingHom.comp (f.functionFieldMap hf) =
      algebraMap X.functionField L

theorem

genericFieldSourceRingEquiv_symm_pow

L93 ↗

EtaleFundamentalGroups.genericFieldSourceRingEquiv_symm_pow

Documentation

An actual root in the generic source field becomes an actual root in the covering scheme's function field under this proved comparison.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem genericFieldSourceRingEquiv_symm_pow
    {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y]
    (f : Y ⟶ X) (hf : DenseRange f)
    {L : Type u} [Field L] [Algebra X.functionField L]
    (p : Spec (.of L) ⟶ Y) [IsDominant p] [IsPreimmersion p]
    (hp : p ≫ f = Spec.map (CommRingCat.ofHom (algebraMap X.functionField L)) ≫
      X.fromSpecStalk (genericPoint X))
    (a : X.functionField) (b : L) (n : ℕ)
    (hb : b ^ n = algebraMap X.functionField L a) :
    ((genericFieldSourceRingEquiv p).symm b) ^ n = f.functionFieldMap hf a

Module documentation

Naturality of the actual generic-field source identification

Declarations

eqToHom_stalk_eq_specializes

Spec_functionFieldMap_fromSpecStalk

functionFieldMap_comp_of_dense

genericFieldSourceRingEquiv_comp_functionFieldMap

genericFieldSourceRingEquiv_symm_pow