Module

ResidueField.lean

Nyll.SchemeTheory.Fibers.ResidueField

5 declarations indexed from sourceView source ↗

Module documentation

Residue fields in scheme-theoretic fibres

The inclusion of a scheme-theoretic fibre is surjective on stalks and hence does not change residue fields. For a dominant morphism of integral schemes, the generic point of the generic fibre maps to the generic point of the source. Together these facts give the canonical residue-field comparison used by divisorial generic-fibre arguments.

Imports2

Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.AlgebraicGeometry.FunctionField

Imported by2

theorem

residueFieldMap_bijective_of_surjectiveOnStalks

L31 ↗

AlgebraicGeometry.Scheme.Hom.residueFieldMap_bijective_of_surjectiveOnStalks

Documentation

A morphism surjective on stalks induces bijections on residue fields.

Source context 5 commands

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

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

Lean source · statement

theorem Scheme.Hom.residueFieldMap_bijective_of_surjectiveOnStalks
    (f : X ⟶ Y) [SurjectiveOnStalks f] (x : X) :
    Function.Bijective (f.residueFieldMap x)

theorem

fiberι_residueFieldMap_bijective

L43 ↗

AlgebraicGeometry.Scheme.Hom.fiberι_residueFieldMap_bijective

Documentation

The inclusion of a scheme-theoretic fibre does not change residue fields.

Source context 5 commands

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

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

Lean source · statement

theorem Scheme.Hom.fiberι_residueFieldMap_bijective
    (f : X ⟶ Y) (y : Y) (z : f.fiber y) :
    Function.Bijective ((f.fiberι y).residueFieldMap z)

def

fiberιResidueFieldRingEquiv

L50 ↗

AlgebraicGeometry.Scheme.Hom.fiberιResidueFieldRingEquiv

Documentation

The residue-field equivalence induced by the inclusion of a scheme-theoretic fibre.

Source context 5 commands

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

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

Lean source · statement

def Scheme.Hom.fiberιResidueFieldRingEquiv
    (f : X ⟶ Y) (y : Y) (z : f.fiber y) :
    X.residueField (f.fiberι y z) ≃+* (f.fiber y).residueField z

theorem

fiberι_genericPoint_eq_genericPoint

L59 ↗

AlgebraicGeometry.Scheme.Hom.fiberι_genericPoint_eq_genericPoint

Documentation

If the generic point of an integral source maps to the generic point of an integral target, the generic point of the generic fibre maps back to the generic point of the source.

Source context 5 commands

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

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

Lean source · statement

theorem Scheme.Hom.fiberι_genericPoint_eq_genericPoint
    [IsIntegral X] [IsIntegral Y]
    (f : X ⟶ Y) (hη : f (genericPoint X) = genericPoint Y)
    [IsIntegral (f.fiber (genericPoint Y))] :
    f.fiberι (genericPoint Y) (genericPoint (f.fiber (genericPoint Y))) =
      genericPoint X

def

genericFiberResidueFieldRingEquiv

L91 ↗

AlgebraicGeometry.Scheme.Hom.genericFiberResidueFieldRingEquiv

Documentation

The generic fibre and the source have canonically equivalent residue fields at their generic points.

Source context 5 commands

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

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

Lean source · statement

def Scheme.Hom.genericFiberResidueFieldRingEquiv
    [IsIntegral X] [IsIntegral Y]
    (f : X ⟶ Y) (hη : f (genericPoint X) = genericPoint Y)
    [IsIntegral (f.fiber (genericPoint Y))] :
    X.residueField (genericPoint X) ≃+*
      (f.fiber (genericPoint Y)).residueField
        (genericPoint (f.fiber (genericPoint Y)))

Module documentation

Residue fields in scheme-theoretic fibres

Declarations

residueFieldMap_bijective_of_surjectiveOnStalks

fiberι_residueFieldMap_bijective

fiberιResidueFieldRingEquiv

fiberι_genericPoint_eq_genericPoint

genericFiberResidueFieldRingEquiv