Module

FunctionFieldResidueAtSourceGeneric.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.FunctionFieldResidueAtSourceGeneric

2 declarations indexed from sourceView source ↗

Module documentation

Function fields at the image of a source generic point

For a dense morphism of integral schemes, the function field of the target is canonically the residue field at the image of the source generic point. The resulting equivalence is compatible with the residue-field map to the source generic point.

Imports1

Nyll.EtaleFundamentalGroups.GaloisCovers.FunctionFieldResidueNaturality

Imported by2

def

functionFieldResidueFieldRingEquivAtSourceGeneric

L31 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldResidueFieldRingEquivAtSourceGeneric

Documentation

The target function field, identified with the residue field at the image of the source generic point of a dense morphism.

Source context 6 commands

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

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

Lean source · statement

def functionFieldResidueFieldRingEquivAtSourceGeneric
    [IsIntegral X] [IsIntegral Z]
    (g : Z ⟶ X) (hg : DenseRange g) :
    X.functionField ≃+* X.residueField (g (genericPoint Z))

theorem

functionFieldResidueFieldRingEquivAtSourceGeneric_naturality

L40 ↗

AlgebraicGeometry.Scheme.Hom.functionFieldResidueFieldRingEquivAtSourceGeneric_naturality