Residue degrees of scheme morphisms

This file develops the elementary functorial API for Mathlib's AlgebraicGeometry.Scheme.Hom.residueDegree. For a scheme morphism f : X ⟶ Y and a point x : X, this is the degree [κ(x) : κ(f(x))], with value zero when the field extension is infinite.

The main result is the tower law residueDegree_comp. It identifies the residue degree of a composite with the product of the two successive residue degrees. We also characterize when a residue degree is positive and when it is one. These facts supply the residue-field weights used in the degree and pushforward parts of Layer A of the Jacobian challenge roadmap.

The construction follows the residue-degree convention for pushforward of cycles in the Stacks Project, Tag 02R4. The proofs reuse Mathlib's residue-field maps and the field-extension tower law Module.finrank_mul_finrank.

@[simp]

theorem TauCeti.AlgebraicGeometry.residueDegree_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X) : AlgebraicGeometry.Scheme.Hom.residueDegree (CategoryTheory.CategoryStruct.comp f g) x = AlgebraicGeometry.Scheme.Hom.residueDegree g (f x) * AlgebraicGeometry.Scheme.Hom.residueDegree f x

The residue degree of a composite is the product of the successive residue degrees: [κ(x) : κ(g(f(x)))] = [κ(f(x)) : κ(g(f(x)))] [κ(x) : κ(f(x))].

theorem TauCeti.AlgebraicGeometry.residueDegree_pos_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) : 0 < AlgebraicGeometry.Scheme.Hom.residueDegree f x ↔ (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)).Finite

A residue degree is positive exactly when the associated residue-field extension is finite.

theorem TauCeti.AlgebraicGeometry.residueDegree_ne_zero_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) : AlgebraicGeometry.Scheme.Hom.residueDegree f x ≠ 0 ↔ (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)).Finite

A residue degree is nonzero exactly when the associated residue-field extension is finite.

theorem TauCeti.AlgebraicGeometry.residueDegree_eq_one_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) : AlgebraicGeometry.Scheme.Hom.residueDegree f x = 1 ↔ Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x))

A residue-field map is bijective exactly when its residue degree is one.

@[simp]

theorem TauCeti.AlgebraicGeometry.residueDegree_eq_one_of_isIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (x : ↥X) : AlgebraicGeometry.Scheme.Hom.residueDegree f x = 1

An isomorphism of schemes has residue degree one at every point.