Residue degrees in the zero and infinity fibres

This file compares residue degree over the ground field with residue degree along the projective-line morphism attached to a rational function.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.ProjectiveLine.residueDegree_structureMap_zeroPoint (K : Type u) [Field K] : AlgebraicGeometry.Scheme.Hom.residueDegree (ProjectiveLine.structureMap K) (ProjectiveLine.zeroPoint K) = 1

The zero point of the projective line has residue degree one over the base field.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.ProjectiveLine.residueDegree_structureMap_infinityPoint (K : Type u) [Field K] : AlgebraicGeometry.Scheme.Hom.residueDegree (ProjectiveLine.structureMap K) (ProjectiveLine.infinityPoint K) = 1

The point at infinity of the projective line has residue degree one over the base field.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.residueDegree_eq_rationalFunctionMorphism_of_eq_zeroPoint (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (x : ↥X) (hx : (rationalFunctionMorphism K X f g) x = ProjectiveLine.zeroPoint K) : AlgebraicGeometry.Scheme.Hom.residueDegree f x = AlgebraicGeometry.Scheme.Hom.residueDegree (rationalFunctionMorphism K X f g) x

Above zero, residue degree over the base field equals residue degree along the rational-function morphism.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.residueDegree_eq_rationalFunctionMorphism_of_eq_infinityPoint (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (x : ↥X) (hx : (rationalFunctionMorphism K X f g) x = ProjectiveLine.infinityPoint K) : AlgebraicGeometry.Scheme.Hom.residueDegree f x = AlgebraicGeometry.Scheme.Hom.residueDegree (rationalFunctionMorphism K X f g) x

Above infinity, residue degree over the base field equals residue degree along the rational-function morphism.