The infinity fibre and sign loci of a rational function

This file treats the infinity fibre and identifies the positive and negative order loci with the zero and infinity fibres of the associated projective-line morphism.

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

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.infinityFibreCodimensionOnePoint (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)ˣ) (hg : ¬∃ (b : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) b) (x : { x : ↥X // (rationalFunctionMorphism K X f g) x = ProjectiveLine.infinityPoint K }) : CodimensionOnePoint X

A point above infinity of a non-global rational function is a codimension-one point of the source curve.

Equations

• TauCeti.AlgebraicGeometry.SchemeWeilDivisor.infinityFibreCodimensionOnePoint K X f g hg x = ⟨↑x, ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.infinityFibreCodimensionOnePoint_val (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 : { x : ↥X // (rationalFunctionMorphism K X f g) x = ProjectiveLine.infinityPoint K }) : ↑(infinityFibreCodimensionOnePoint K X f g hg x) = ↑x

The canonical codimension-one point above infinity has the original fibre point as its underlying scheme point.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.ramificationIdx_primeIdealOf_infinity_eq_neg_orderAt (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 : CodimensionOnePoint X) (hxinf : (rationalFunctionMorphism K X f g) ↑x = ProjectiveLine.infinityPoint K) : let φ := rationalFunctionMorphism K X f g; let U := ProjectiveLine.infinityAffineOpen K; have hxU := ⋯; let V := (TopologicalSpace.Opens.map φ.base).obj U; have hV := ⋯; have a := AlgebraicGeometry.Scheme.Hom.appLE φ U V ⋯; have q := (hV.primeIdealOf ⟨↑x, hxU⟩).asIdeal; ↑(q.ramificationIdx ↑((ProjectiveLine.scheme K).presheaf.obj (Opposite.op U))) = -(orderAt x) g

Above the point at infinity, the affine ramification index is the negative of the scheme-theoretic order of the rational function.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sum_orderAt_residueDegree_infinity_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) : let φ := rationalFunctionMorphism K X f g; let U := ProjectiveLine.infinityAffineOpen K; let V := (TopologicalSpace.Opens.map φ.base).obj U; let a := AlgebraicGeometry.Scheme.Hom.appLE φ U V ⋯; have hinf := ⋯; let p := (⋯.primeIdealOf ⟨ProjectiveLine.infinityPoint K, hinf⟩).asIdeal; have e := fibrePointPrimesOverEquiv φ U ⋯ (ProjectiveLine.infinityPoint K) hinf; ∑ q : ↑(p.primesOver ↑(X.presheaf.obj (Opposite.op V))), (orderAt (infinityFibreCodimensionOnePoint K X f g hg ((Equiv.symm e) q))) g * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree φ ↑((Equiv.symm e) q)) = -↑(AlgebraicGeometry.Scheme.Hom.finrank φ (ProjectiveLine.infinityPoint K))

The order/residue-degree sum above infinity is the negative finite-flat degree of the rational-function morphism.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt_nonneg_of_mem_standardAffineOpen (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (x : CodimensionOnePoint X) (hx : (rationalFunctionMorphism K X f g) ↑x ∈ ProjectiveLine.standardAffineOpen K) : 0 ≤ (orderAt x) g

The order of a rational function is nonnegative at every point lying in the standard affine chart of its map to ℙ¹.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt_eq_zero_of_mem_standardAffineOpen_of_ne_zeroPoint (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (x : CodimensionOnePoint X) (hx : (rationalFunctionMorphism K X f g) ↑x ∈ ProjectiveLine.standardAffineOpen K) (hne : (rationalFunctionMorphism K X f g) ↑x ≠ ProjectiveLine.zeroPoint K) : (orderAt x) g = 0

Away from the zero point, the standard affine coordinate is a unit in the target stalk, so the corresponding rational-function order is zero.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt_eq_zero_of_mem_infinityAffineOpen_of_ne_infinityPoint (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (x : CodimensionOnePoint X) (hx : (rationalFunctionMorphism K X f g) ↑x ∈ ProjectiveLine.infinityAffineOpen K) (hne : (rationalFunctionMorphism K X f g) ↑x ≠ ProjectiveLine.infinityPoint K) : (orderAt x) g = 0

Away from the point at infinity, the inverse affine coordinate is a unit in the target stalk, so the corresponding rational-function order is zero.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_eq_zero_or_infinity_of_orderAt_ne_zero (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (x : CodimensionOnePoint X) (hne : (orderAt x) g ≠ 0) : (rationalFunctionMorphism K X f g) ↑x = ProjectiveLine.zeroPoint K ∨ (rationalFunctionMorphism K X f g) ↑x = ProjectiveLine.infinityPoint K

Every nonzero order occurs above either zero or infinity of the projective-line morphism.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_eq_zeroPoint_of_orderAt_pos (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (x : CodimensionOnePoint X) (hpos : 0 < (orderAt x) g) : (rationalFunctionMorphism K X f g) ↑x = ProjectiveLine.zeroPoint K

Positive orders are exactly on the zero fibre.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_eq_infinityPoint_of_orderAt_neg (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (x : CodimensionOnePoint X) (hneg : (orderAt x) g < 0) : (rationalFunctionMorphism K X f g) ↑x = ProjectiveLine.infinityPoint K

Negative orders are exactly on the infinity fibre.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.zeroFibreEquivPositiveOrder (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 : ↥X // (rationalFunctionMorphism K X f g) x = ProjectiveLine.zeroPoint K } ≃ { x : CodimensionOnePoint X // 0 < (orderAt x) g }

The zero fibre of a non-global rational function is canonically equivalent to the codimension-one points where its order is positive.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.zeroFibreEquivPositiveOrder_apply_val (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 : { x : ↥X // (rationalFunctionMorphism K X f g) x = ProjectiveLine.zeroPoint K }) : ↑((zeroFibreEquivPositiveOrder K X f g hg) x) = zeroFibreCodimensionOnePoint K X f g hg x

The positive-order point underlying the zero-fibre equivalence is the canonical codimension-one point attached to the fibre point.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.infinityFibreEquivNegativeOrder (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 : ↥X // (rationalFunctionMorphism K X f g) x = ProjectiveLine.infinityPoint K } ≃ { x : CodimensionOnePoint X // (orderAt x) g < 0 }

The infinity fibre of a non-global rational function is canonically equivalent to the codimension-one points where its order is negative.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.infinityFibreEquivNegativeOrder_apply_val (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 : { x : ↥X // (rationalFunctionMorphism K X f g) x = ProjectiveLine.infinityPoint K }) : ↑((infinityFibreEquivNegativeOrder K X f g hg) x) = infinityFibreCodimensionOnePoint K X f g hg x

The negative-order point underlying the infinity-fibre equivalence is the canonical codimension-one point attached to the fibre point.