Module

FiberRank.lean

Nyll.SchemeTheory.Morphisms.FiberRank

2 declarations indexed from sourceView source ↗

Module documentation

Rank comparisons on actual generic and scheme-theoretic fibers

For finite flat morphisms, the literal scheme-theoretic fiber has the rank of the original morphism at the chosen point. Over an integral base, finite presentation makes this rank equal to the rank on any specified actual generic-stalk pullback square. These comparisons are proved at the scheme level, before introducing a field extension or its scalar structures.

Imports4

Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Mathlib.Topology.LocallyConstant.Basic
Mathlib.AlgebraicGeometry.Fiber
Mathlib.AlgebraicGeometry.FunctionField

Imported by2

theorem

finrank_eq_genericStalkPullback

L32 ↗

AlgebraicGeometry.Scheme.Hom.finrank_eq_genericStalkPullback

Documentation

A finite flat finitely presented morphism over an integral base has the rank of its actual generic-stalk pullback at every base point.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u

Lean source · statement

theorem finrank_eq_genericStalkPullback
    {X Y Z : Scheme.{u}} [IsIntegral X]
    (f : Y ⟶ X) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (i : Z ⟶ Y) (g : Z ⟶ Spec X.functionField)
    (H : IsPullback i g f (X.fromSpecStalk (genericPoint X))) (x : X) :
    f.finrank x = g.finrank (IsLocalRing.closedPoint X.functionField)

theorem

finrank_fiberToSpecResidueField

L51 ↗

AlgebraicGeometry.Scheme.Hom.finrank_fiberToSpecResidueField