Fibre degrees of the rational-function morphism

This file compares the local orders of a rational function with the finite-flat fibres of its associated morphism to the projective line. The first bridge identifies the pullback of the standard affine coordinate with the original element of the function field.

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

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.residueDegree_SpecMap_eq_inertiaDeg (R S : CommRingCat) (a : R ⟶ S) (q : PrimeSpectrum ↑S) : AlgebraicGeometry.Scheme.Hom.residueDegree (AlgebraicGeometry.Spec.map a) q = q.asIdeal.inertiaDeg ↑R

The residue degree of a morphism between affine spectra is the inertia degree of the corresponding prime ideal.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.ramificationIdx_eq_ord_algebraMap_of_eq_span_singleton {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p] (t : R) (hp : p = Ideal.span {t}) : q.ramificationIdx R = (Ring.ord (Localization.AtPrime q) ((algebraMap R (Localization.AtPrime q)) t)).toNat

If the prime downstairs is generated by one element, the ramification index is the order of the image of that generator in the localization upstairs.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.ord_ringEquiv {R S : Type u} [CommRing R] [CommRing S] (e : R ≃+* S) (x : R) : Ring.ord R x = Ring.ord S (e x)

The order defined by quotient length is invariant under a ring equivalence.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.fibrePointPrimesOverEquiv {X Y : AlgebraicGeometry.Scheme} (φ : X ⟶ Y) [AlgebraicGeometry.IsAffineHom φ] (U : Y.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) (y : ↥Y) (hy : y ∈ U) : let V := (TopologicalSpace.Opens.map φ.base).obj U; have a := AlgebraicGeometry.Scheme.Hom.appLE φ U V ⋯; have p := (hU.primeIdealOf ⟨y, hy⟩).asIdeal; { x : ↥X // φ x = y } ≃ ↑(p.primesOver ↑(X.presheaf.obj (Opposite.op V)))

Points of a fibre over a point in an affine chart correspond to prime ideals of the affine preimage lying over the target prime.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.fibrePointPrimesOverEquiv_apply_val {X Y : AlgebraicGeometry.Scheme} (φ : X ⟶ Y) [AlgebraicGeometry.IsAffineHom φ] (U : Y.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) (y : ↥Y) (hy : y ∈ U) (x : { x : ↥X // φ x = y }) : let V := (TopologicalSpace.Opens.map φ.base).obj U; have hV := ⋯; have a := AlgebraicGeometry.Scheme.Hom.appLE φ U V ⋯; ↑((fibrePointPrimesOverEquiv φ U hU y hy) x) = (hV.primeIdealOf ⟨↑x, ⋯⟩).asIdeal

The prime ideal underlying the fibre-point equivalence is the affine-chart prime of the source point.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.inertiaDeg_primeIdealOf_app_eq_residueDegree {X Y : AlgebraicGeometry.Scheme} (φ : X ⟶ Y) [AlgebraicGeometry.IsAffineHom φ] (U : Y.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥X) (hx : x ∈ (TopologicalSpace.Opens.map φ.base).obj U) : let V := (TopologicalSpace.Opens.map φ.base).obj U; have hV := ⋯; have a := AlgebraicGeometry.Scheme.Hom.appLE φ U V ⋯; (hV.primeIdealOf ⟨x, hx⟩).asIdeal.inertiaDeg ↑(Y.presheaf.obj (Opposite.op U)) = AlgebraicGeometry.Scheme.Hom.residueDegree φ x

In an affine chart, the inertia degree of the prime corresponding to a source point is the residue degree of the original scheme morphism at that point.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sum_ramification_inertia_app_eq_finrank {X Y : AlgebraicGeometry.Scheme} (φ : X ⟶ Y) [AlgebraicGeometry.IsFinite φ] [AlgebraicGeometry.Flat φ] (U : Y.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) (y : ↥Y) (hy : y ∈ U) : let V := (TopologicalSpace.Opens.map φ.base).obj U; let a := AlgebraicGeometry.Scheme.Hom.appLE φ U V ⋯; have p := (hU.primeIdealOf ⟨y, hy⟩).asIdeal; ∑ q : ↑(p.primesOver ↑(X.presheaf.obj (Opposite.op V))), (↑q).ramificationIdx ↑(Y.presheaf.obj (Opposite.op U)) * (↑q).inertiaDeg ↑(Y.presheaf.obj (Opposite.op U)) = AlgebraicGeometry.Scheme.Hom.finrank φ y

For a finite flat morphism, the ramification-index/inertia-degree sum over an affine fibre is the scheme-theoretic finite-flat rank at the target point.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sum_ramification_residueDegree_app_eq_finrank {X Y : AlgebraicGeometry.Scheme} (φ : X ⟶ Y) [AlgebraicGeometry.IsFinite φ] [AlgebraicGeometry.Flat φ] (U : Y.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) (y : ↥Y) (hy : y ∈ U) : let V := (TopologicalSpace.Opens.map φ.base).obj U; let a := AlgebraicGeometry.Scheme.Hom.appLE φ U V ⋯; let p := (hU.primeIdealOf ⟨y, hy⟩).asIdeal; have e := fibrePointPrimesOverEquiv φ U hU y hy; ∑ q : ↑(p.primesOver ↑(X.presheaf.obj (Opposite.op V))), (↑q).ramificationIdx ↑(Y.presheaf.obj (Opposite.op U)) * AlgebraicGeometry.Scheme.Hom.residueDegree φ ↑((Equiv.symm e) q) = AlgebraicGeometry.Scheme.Hom.finrank φ y

The affine finite-flat fibre formula with the inertia degrees replaced by geometric residue degrees. The equivalence with the fibre is kept explicit so the summation still uses the canonical primesOver fintype.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sum_ramification_inertia_zero_eq_finrank_rationalFunctionMorphism (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 p := Ideal.span {ProjectiveLine.affineCoordinate K}; ∑ q : ↑(p.primesOver ↑(X.presheaf.obj (Opposite.op V))), (↑q).ramificationIdx ↑((ProjectiveLine.scheme K).presheaf.obj (Opposite.op U)) * (↑q).inertiaDeg ↑((ProjectiveLine.scheme K).presheaf.obj (Opposite.op U)) = AlgebraicGeometry.Scheme.Hom.finrank φ (ProjectiveLine.zeroPoint K)

For a non-global rational function, the ramification/inertia sum above the zero point of ℙ¹ is the finite-flat degree of its projective-line morphism. The target prime is normalized to the principal ideal generated by X₀ / X₁.