The zero fibre of a rational function #
This file identifies the local order of a rational function with ramification in the zero fibre of its associated projective-line morphism.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.germToFunctionField_rationalFunctionMorphism_app_affineCoordinate
(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)ˣ)
:
let φ := rationalFunctionMorphism K X f g;
let V := (TopologicalSpace.Opens.map φ.base).obj (ProjectiveLine.standardAffineOpen K);
(CategoryTheory.ConcreteCategory.hom (X.germToFunctionField V))
((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app φ (ProjectiveLine.standardAffineOpen K)))
(ProjectiveLine.affineCoordinate K)) = ↑(Additive.toMul g)
On the inverse image of the standard affine chart of ℙ¹, the pullback of X₀ / X₁
represents the rational function used to define the map.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.algebraMap_stalkMap_germ_affineCoordinate_eq
(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.standardAffineOpen K)
:
(algebraMap ↑(X.presheaf.stalk x) ↑X.functionField)
((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (rationalFunctionMorphism K X f g) x))
((CategoryTheory.ConcreteCategory.hom
((ProjectiveLine.scheme K).presheaf.germ (ProjectiveLine.standardAffineOpen K)
((rationalFunctionMorphism K X f g) x) hx))
(ProjectiveLine.affineCoordinate K))) = ↑(Additive.toMul g)
At a point mapping into the standard affine chart, the standard coordinate pulled back to the source stalk maps to the original rational function in the function field.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt_eq_ord_stalkMap_affineCoordinate
(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)
:
(orderAt x) g = ↑(Ring.ord (↑(X.presheaf.stalk ↑x))
((CategoryTheory.ConcreteCategory.hom
(AlgebraicGeometry.Scheme.Hom.stalkMap (rationalFunctionMorphism K X f g) ↑x))
((CategoryTheory.ConcreteCategory.hom
((ProjectiveLine.scheme K).presheaf.germ (ProjectiveLine.standardAffineOpen K)
((rationalFunctionMorphism K X f g) ↑x) hx))
(ProjectiveLine.affineCoordinate K)))).toNat
On the standard affine chart, the scheme-theoretic order of the rational function is the finite order of the pulled-back affine coordinate in the source DVR.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_genericPoint_mem_infinityAffineOpen
(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)ˣ)
:
The generic point of a smooth relative curve maps into the affine chart D₊(X₀) containing
infinity. The inverse coordinate there is the inverse of the nonzero function-field element.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.germToFunctionField_rationalFunctionMorphism_app_inverseAffineCoordinate
(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)ˣ)
:
let φ := rationalFunctionMorphism K X f g;
let V := (TopologicalSpace.Opens.map φ.base).obj (ProjectiveLine.infinityAffineOpen K);
(CategoryTheory.ConcreteCategory.hom (X.germToFunctionField V))
((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app φ (ProjectiveLine.infinityAffineOpen K)))
(ProjectiveLine.inverseAffineCoordinate K)) = (↑(Additive.toMul g))⁻¹
On the inverse image of the chart at infinity, the pullback of X₁ / X₀ represents the
inverse of the rational function used to define the map.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.algebraMap_stalkMap_germ_inverseAffineCoordinate_eq
(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.infinityAffineOpen K)
:
(algebraMap ↑(X.presheaf.stalk x) ↑X.functionField)
((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (rationalFunctionMorphism K X f g) x))
((CategoryTheory.ConcreteCategory.hom
((ProjectiveLine.scheme K).presheaf.germ (ProjectiveLine.infinityAffineOpen K)
((rationalFunctionMorphism K X f g) x) hx))
(ProjectiveLine.inverseAffineCoordinate K))) = (↑(Additive.toMul g))⁻¹
At a point mapping into the affine chart at infinity, the inverse coordinate pulled back to the source stalk maps to the inverse rational function in the function field.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.neg_orderAt_eq_ord_stalkMap_inverseAffineCoordinate
(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)
:
-(orderAt x) g = ↑(Ring.ord (↑(X.presheaf.stalk ↑x))
((CategoryTheory.ConcreteCategory.hom
(AlgebraicGeometry.Scheme.Hom.stalkMap (rationalFunctionMorphism K X f g) ↑x))
((CategoryTheory.ConcreteCategory.hom
((ProjectiveLine.scheme K).presheaf.germ (ProjectiveLine.infinityAffineOpen K)
((rationalFunctionMorphism K X f g) ↑x) hx))
(ProjectiveLine.inverseAffineCoordinate K)))).toNat
On the chart at infinity, the finite order of the pulled-back inverse coordinate is the negative of the scheme-theoretic order of the original rational function.
noncomputable def
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.zeroFibreCodimensionOnePoint
(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.zeroPoint K })
:
A point above zero of a non-global rational function is a codimension-one point of the source curve.
Equations
- TauCeti.AlgebraicGeometry.SchemeWeilDivisor.zeroFibreCodimensionOnePoint K X f g hg x = ⟨↑x, ⋯⟩
Instances For
@[simp]
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.zeroFibreCodimensionOnePoint_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 })
:
The canonical codimension-one point above zero has the original fibre point as its underlying scheme point.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.ramificationIdx_primeIdealOf_zero_eq_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)
(hxzero : (rationalFunctionMorphism K X f g) ↑x = ProjectiveLine.zeroPoint K)
:
let φ := rationalFunctionMorphism K X f g;
let U := ProjectiveLine.standardAffineOpen 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 zero point of the rational-function morphism, the affine ramification index is the scheme-theoretic order of the rational function.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sum_orderAt_residueDegree_zero_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)
:
let φ := rationalFunctionMorphism K X f g;
let U := ProjectiveLine.standardAffineOpen K;
let V := (TopologicalSpace.Opens.map φ.base).obj U;
let a := AlgebraicGeometry.Scheme.Hom.appLE φ U V ⋯;
have hz := ⋯;
let p := (⋯.primeIdealOf ⟨ProjectiveLine.zeroPoint K, hz⟩).asIdeal;
have e := fibrePointPrimesOverEquiv φ U ⋯ (ProjectiveLine.zeroPoint K) hz;
∑ q : ↑(p.primesOver ↑(X.presheaf.obj (Opposite.op V))),
(orderAt (zeroFibreCodimensionOnePoint K X f g hg ((Equiv.symm e) q))) g * ↑(AlgebraicGeometry.Scheme.Hom.residueDegree φ ↑((Equiv.symm e) q)) = ↑(AlgebraicGeometry.Scheme.Hom.finrank φ (ProjectiveLine.zeroPoint K))
The order/residue-degree sum above zero is the finite-flat degree of the rational-function morphism.