The rank of a finite flat morphism is the degree of its function-field extension

For a finite flat affine morphism with integral target, the rank at every target point equals the dimension after passing to compatible fraction rings. When the source is also integral, these fraction rings are fields, and the dimension is the function-field extension degree.

Globally, let f : X ⟶ Y be a finite flat dominant morphism of integral schemes, and f^* : K(Y) ⟶ K(X) its pullback of rational functions (AlgebraicGeometry.Scheme.Hom.functionFieldMap). Then the rank of f at every point of Y is the degree [K(X) : f^* K(Y)]. In particular the rank is constant, with no noetherian or finite presentation hypothesis. For instance, a finite dominant morphism from an integral scheme to an integral curve smooth over a field is flat (AlgebraicGeometry.Scheme.Hom.flat_of_isDominant_of_smooth), so its constant fibre length is the degree of its function-field extension.

The local rank is Mathlib's Scheme.Hom.finrank. Its affine formula reduces the result to Mathlib's fibre-rank calculation for finite flat modules and the invariance of dimension under passage to fraction rings. The global statement restricts f over an affine open of Y, whose preimage is affine because f is finite. Both coordinate rings are domains whose fraction fields are the function fields, and f^* extends the map of coordinate rings.

The degree is stated as the dimension of K(X) over the subfield f^* K(Y), as for the degree of an isogeny of Weierstrass curves (TauCeti.Isogeny.degree). This avoids putting an algebra structure on K(X) over K(Y), which would clash with Algebra.id for an endomorphism.

Main results

• TauCeti.AlgebraicGeometry.finrank_SpecMap_eq_finrank_fractionRing: the affine statement, for any compatible fraction rings.
• AlgebraicGeometry.Scheme.Hom.finrank_eq_finrank_fieldRange_functionFieldMap: the rank of a finite flat dominant morphism of integral schemes is the degree [K(X) : f^* K(Y)] at every point.

References

• Stacks Project, Tag 02KA.

theorem TauCeti.AlgebraicGeometry.finrank_SpecMap_eq_finrank_fractionRing {R S : Type u} {K : Type v} {L : Type w} [CommRing R] [IsDomain R] [CommRing S] [CommRing K] [CommRing L] [Algebra R S] [Algebra R K] [Algebra S L] [Algebra R L] [Module K L] [IsScalarTower R K L] [IsScalarTower R S L] [IsFractionRing R K] [IsFractionRing S L] [Module.Flat R S] [Module.Finite R S] (p : PrimeSpectrum R) : AlgebraicGeometry.Scheme.Hom.finrank (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) p = Module.finrank K L

The rank of a finite flat affine morphism with integral target is the dimension after passing to fraction rings. If S is a domain, K and L are fields and this is the degree of the induced function-field extension. The scalar towers record compatibility with the map of coordinate rings.

theorem AlgebraicGeometry.Scheme.Hom.finrank_eq_finrank_fieldRange_functionFieldMap {X Y : Scheme} (f : X ⟶ Y) [IsIntegral X] [IsIntegral Y] [IsFinite f] [Flat f] [IsDominant f] (y : ↥Y) : finrank f y = Module.finrank ↥(CommRingCat.Hom.hom (functionFieldMap f)).fieldRange ↑X.functionField

The rank of a finite flat morphism is its function-field degree. For a finite flat dominant morphism f : X ⟶ Y of integral schemes, the rank of f at every point of Y is the degree [K(X) : f^* K(Y)] of the function field of X over the image of the pullback of rational functions f^* (Scheme.Hom.functionFieldMap). In particular the rank is constant.