Degree-zero assembly for the divisor product formula

This file assembles the zero- and infinity-fibre calculations into the residue-degree-weighted product formula for rational functions on smooth proper curves.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.instNonemptyCarrierCarrierCommRingCatToSchemeTopOpensOfIsIntegral_5 {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : Nonempty ↥↑⊤

@[instance_reducible]

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.positiveOrderFintype (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (b : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) b) : Fintype { x : CodimensionOnePoint X // 0 < (orderAt x) g }

The positive-order locus of a non-global rational function is finite, with its canonical fintype transported from the finite zero fibre.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.negativeOrderFintype (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (b : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) b) : Fintype { x : CodimensionOnePoint X // (orderAt x) g < 0 }

The negative-order locus of a non-global rational function is finite, with its canonical fintype transported from the finite infinity fibre.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sum_positiveOrder_residueDegree_eq_finrank (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (b : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) b) : have φ := rationalFunctionMorphism K X f g; ∑ x : { x : CodimensionOnePoint X // 0 < (orderAt x) g }, (orderAt ↑x) g * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑↑x) = ↑(AlgebraicGeometry.Scheme.Hom.finrank φ (ProjectiveLine.zeroPoint K))

The residue-degree-weighted sum of the positive orders is the finite-flat degree of the zero fibre.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sum_negativeOrder_residueDegree_eq_neg_finrank (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (b : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) b) : have φ := rationalFunctionMorphism K X f g; ∑ x : { x : CodimensionOnePoint X // (orderAt x) g < 0 }, (orderAt ↑x) g * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑↑x) = -↑(AlgebraicGeometry.Scheme.Hom.finrank φ (ProjectiveLine.infinityPoint K))

The residue-degree-weighted sum of the negative orders is the negative finite-flat degree of the infinity fibre.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sum_support_eq_sum_positive_add_sum_negative (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (b : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) b) : ∑ x ∈ ((orderSystem X).principalDivisor g).support, (orderAt x) g * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x) = ∑ x : { x : CodimensionOnePoint X // 0 < (orderAt x) g }, (orderAt ↑x) g * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑↑x) + ∑ x : { x : CodimensionOnePoint X // (orderAt x) g < 0 }, (orderAt ↑x) g * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑↑x)

The finite support sum of a non-global rational function splits into its positive-order and negative-order loci.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_principalDivisor_eq_zero_of_nonGlobal (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (b : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) b) : (relativeDegree f) ((orderSystem X).principalDivisor g) = 0

The principal divisor of a non-global rational function on a smooth proper curve has relative degree zero.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderSystem_isWeightedDegreeZero (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] : (orderSystem X).IsWeightedDegreeZero fun (x : CodimensionOnePoint X) => ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)

Product formula for the scheme-theoretic order system of a smooth proper curve: every principal divisor has residue-degree-weighted degree zero.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.divisorProductFormula (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] : (orderSystem X).IsWeightedDegreeZero fun (x : CodimensionOnePoint X) => ↑(AlgebraicGeometry.Scheme.Hom.residueDegree f ↑x)

Public adapter name for the divisor product formula on smooth proper curves.