NYLL
Module

GenericPointNaturality.lean

Nyll.AnabelianGeometry.WeightFiltration.GenericPointNaturality
2 declarations indexed from sourceView source ↗

Module documentation

Naturality of the actual generic point

The canonical function-field map commutes with the maps from the generic stalk spectra. This is used when comparing the actual Kummer characters on an open curve with geometric pullback from its compactification.

Imports2
Imported by2

Declarations

theorem

specMap_stalk_eqToHom_comp

L24 ↗
AnabelianGeometry.WeightFiltration.specMap_stalk_eqToHom_comp
Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace AnabelianGeometry.WeightFiltration
Lean source · full declaration
theorem specMap_stalk_eqToHom_comp
    {X : Scheme} {x y : X} (h : x = y) :
    Spec.map (eqToHom (congrArg (fun z => X.presheaf.stalk z) h)) ≫
      X.fromSpecStalk x = X.fromSpecStalk y := by
  subst y
  simp only [eqToHom_refl, Spec.map_id, Category.id_comp]
theorem

functionFieldMap_genericPoint

L32 ↗
AnabelianGeometry.WeightFiltration.functionFieldMap_genericPoint
Documentation

The actual generic-point square of a dominant morphism commutes.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace AnabelianGeometry.WeightFiltration
Lean source · statement
theorem functionFieldMap_genericPoint
    {X Y : Scheme} [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

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