Rank of a finite flat morphism of schemes

In this file we define the rank AlgebraicGeometry.Scheme.Hom.finrank of a finite flat morphism of schemes f : X ⟶ Y. It is locally constant and is characterized by the condition that the rank of Spec S ⟶ Spec R at some prime p of R is the rank of S as an R-algebra at p.

Main definitions

• AlgebraicGeometry.Scheme.Hom.finrank: For a morphism f : X ⟶ Y of schemes, the function Y → ℕ sending y to the rank of f_* 𝒪_X over 𝒪_Y at y. Instead of talking about sheaves, we define it by choosing an open neighbourhood of y. This is sometimes also called the degree of a morphism in the literature.

Main results

• AlgebraicGeometry.Scheme.Hom.isLocallyConstant_finrank: The rank function of a finite flat locally finitely presented morphism is locally constant.
• AlgebraicGeometry.Scheme.Hom.one_le_finrank_iff_surjective: The rank function is at least 1 everywhere if and only if the morphism is surjective.
• AlgebraicGeometry.Scheme.Hom.isIso_iff_finrank_eq: A finite flat locally finitely presented morphism is an isomorphism if and only if its rank is constant equal to 1.

TODO

• Relate Hom.finrank f y to the rank of f_* 𝒪_X over 𝒪_Y at y when the API for locally free sheaves of modules is developed.

noncomputable def AlgebraicGeometry.Scheme.Hom.finrank {X S : Scheme} (f : X ⟶ S) (s : ↥S) : ℕ

The rank of a morphism f : X ⟶ S of schemes at a point s : S. When f is finite, flat and locally of finite presentation, this is a locally constant function (see AlgebraicGeometry.isLocallyConstant_finrank).

Equations

• AlgebraicGeometry.Scheme.Hom.finrank f s = AlgebraicGeometry.IsAffine.finrank✝ (CategoryTheory.Limits.pullback.snd f (S.affineOpenCover.f (S.affineOpenCover.idx s))) (Exists.choose ⋯)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank {R S : CommRingCat} {f : R ⟶ S} (hf₁ : (CommRingCat.Hom.hom f).Finite) (hf₂ : (CommRingCat.Hom.hom f).Flat) : finrank (Spec.map f) = (CommRingCat.Hom.hom f).finrank

theorem AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_algebraMap (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] (x : PrimeSpectrum R) : finrank (Spec.map (CommRingCat.ofHom (algebraMap R S))) x = Module.rankAtStalk S x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso {X S Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ S) [CategoryTheory.IsIso f] [Flat g] [IsFinite g] : finrank (CategoryTheory.CategoryStruct.comp f g) = finrank g

theorem AlgebraicGeometry.Scheme.Hom.finrank_pullback_snd {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [Flat f] [IsFinite f] (y : ↥Y) : finrank (CategoryTheory.Limits.pullback.snd f g) y = finrank f (g y)

theorem AlgebraicGeometry.Scheme.Hom.finrank_of_isPullback {P X Y Z : Scheme} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) (h : CategoryTheory.IsPullback fst snd f g) [Flat f] [IsFinite f] (y : ↥Y) : finrank snd y = finrank f (g y)

theorem AlgebraicGeometry.Scheme.Hom.finrank_pullback_fst {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [Flat f] [IsFinite f] (y : ↥Y) : finrank (CategoryTheory.Limits.pullback.fst g f) y = finrank f (g y)

theorem AlgebraicGeometry.Scheme.Hom.one_le_finrank_map {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X) : 1 ≤ finrank f (f x)

theorem AlgebraicGeometry.Scheme.Hom.one_le_finrank_iff_surjective {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] : 1 ≤ finrank f ↔ Surjective f

A finite flat locally finitely presented morphism is surjective if and only if its rank function is at least 1 everywhere.

theorem AlgebraicGeometry.Scheme.Hom.isLocallyConstant_finrank {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f] : IsLocallyConstant (finrank f)

The rank of a finite flat locally finitely presented morphism is locally constant.

theorem AlgebraicGeometry.Scheme.Hom.finrank_eq_one_of_isIso {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : finrank f = 1

The rank of an isomorphism is 1.

theorem AlgebraicGeometry.Scheme.Hom.isIso_iff_finrank_eq {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] : CategoryTheory.IsIso f ↔ finrank f = 1

A finite flat locally finitely presented morphism is an isomorphism if and only if its rank is constant equal to 1.