NYLL
Module

Centered.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Centered
10 declarations indexed from sourceView source ↗

Module documentation

Prime divisors centered at a rational point

This file supplies the monic-projection form of Fried--Jarden, Lemma 6.2.2(b).

Imports4
Imported by3

Declarations

def

projectionBaseEquivPolynomial

L32 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.projectionBaseEquivPolynomial
Documentation

The one-variable multivariate projection base is the usual polynomial ring.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
def projectionBaseEquivPolynomial :
    ProjectionBase K ≃ₐ[K] Polynomial K
theorem

projectionBase_isPrincipalIdealRing

L39 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.projectionBase_isPrincipalIdealRing
Documentation

In particular, the projection base is a principal ideal domain.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem projectionBase_isPrincipalIdealRing :
    IsPrincipalIdealRing (ProjectionBase K)
theorem

projectionAlgebra_algebraMap_apply

L47 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.projectionAlgebra_algebraMap_apply
Documentation

The projection algebra structure is compatible with the constant K-algebra structures.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem projectionAlgebra_algebraMap_apply
    (f : BivariatePolynomial K) (x : K) :
    @algebraMap (ProjectionBase K) (CoordinateRing f) _ _
        (projectionAlgebra f)
        (algebraMap K (ProjectionBase K) x) =
      algebraMap K (CoordinateRing f) x
abbrev

coordinateRingMap

L63 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.coordinateRingMap
Documentation

The inclusion of the affine coordinate ring in its fraction field.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
abbrev coordinateRingMap
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)] :
    CoordinateRing f →ₐ[K] FractionRing (CoordinateRing f)
structure

CenteredPrimeDivisor

L74 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.CenteredPrimeDivisor
Documentation

A prime divisor finite on the affine coordinate ring and centered at the rational point p. These are exactly the objects counted in the monic-projection form of Fried--Jarden 6.2.2(b).

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · full declaration
structure CenteredPrimeDivisor
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (p : RationalPoint f) where
  /-- The underlying prime divisor of the fraction field of the coordinate ring. -/
  divisor :
    FunctionFieldPrimeDivisor K (FractionRing (CoordinateRing f))
  /-- The divisor is finite along the coordinate-ring inclusion. -/
  finite :
    divisor.FiniteAlong (coordinateRingMap (K := K) (f := f))
  /-- The center of the divisor is the ideal of the rational point p. -/
  center_eq :
    divisor.centerAlong (coordinateRingMap (K := K) (f := f)) finite =
      pointIdeal p
theorem

ext

L94 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.CenteredPrimeDivisor.ext
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisor
variable {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
  {p : RationalPoint f}
Lean source · statement
theorem ext {v w : CenteredPrimeDivisor (K := K) p}
    (h : v.divisor = w.divisor) :
    v = w
def

projectionPointIdeal

L106 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.projectionPointIdeal
Documentation

The prime of K[X] below a rational point of the affine curve.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
def projectionPointIdeal
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    Ideal (ProjectionBase K)
theorem

projectionPointIdeal_isPrime

L113 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.projectionPointIdeal_isPrime
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem projectionPointIdeal_isPrime
    {f : BivariatePolynomial K} (p : RationalPoint f) :
    (projectionPointIdeal (K := K) p).IsPrime
theorem

integralClosure_finrank_eq_of_algebraMap_injective

L127 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.integralClosure_finrank_eq_of_algebraMap_injective
Documentation

Rank comparison for an integral-closure model, with the ambient torsion-freeness supplied by an explicit algebra-map injection.

Keeping this comparison in its own declaration prevents the final rank calculation from reopening the full projection and normalization instance environment.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem integralClosure_finrank_eq_of_algebraMap_injective
    (A K₀ L C : Type*) [CommRing A] [IsDomain A]
    [Field K₀] [Field L] [CommRing C]
    [Algebra A K₀] [IsFractionRing A K₀]
    [Algebra K₀ L] [Algebra A L] [IsScalarTower A K₀ L]
    [Algebra C L] [IsIntegralClosure C A L]
    [Algebra A C] [IsScalarTower A C L]
    [FiniteDimensional K₀ L] [Algebra.IsSeparable K₀ L]
    [IsPrincipalIdealRing A]
    (hL : Function.Injective (algebraMap A L)) :
    Module.finrank A C = Module.finrank K₀ L
theorem

card_centeredPrimeDivisor_le_totalDegree

L151 ↗
FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.card_centeredPrimeDivisor_le_totalDegree
Documentation

For a monic projection whose function-field extension over K(X) is separable, at most totalDegree f prime divisors are finite on the affine coordinate ring and centered at a prescribed rational point.

The separability input is precisely the hypothesis used to make the integral closure of K[X] finite and Dedekind. In particular, it is structural input for the normalization, not an assumed comparison or counting statement.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace CenteredPrimeDivisorBound
open AffinePlaneCurve MonicPlaneCurveProjection
universe u
variable {K : Type u} [Field K]
Lean source · full declaration
theorem card_centeredPrimeDivisor_le_totalDegree
    {f : BivariatePolynomial K} (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) (p : RationalPoint f) :
    letI : IsDomain (CoordinateRing f) :=
      coordinateRing_isDomain hirr
    letI : Algebra (ProjectionFunctionField K)
        (FractionRing (CoordinateRing f)) :=
      functionFieldAlgebra f hirr hmonic
    Algebra.IsSeparable (ProjectionFunctionField K)
        (FractionRing (CoordinateRing f)) →
      Nat.card (CenteredPrimeDivisor (K := K) p) ≤
        MvPolynomial.totalDegree f := by
  let : IsDomain (CoordinateRing f) :=
    coordinateRing_isDomain hirr
  let : Algebra (ProjectionBase K) (CoordinateRing f) :=
    projectionAlgebra f
  let : Algebra (ProjectionBase K)
      (FractionRing (CoordinateRing f)) :=
    inferInstance
  let : IsScalarTower (ProjectionBase K) (CoordinateRing f)
      (FractionRing (CoordinateRing f)) :=
    inferInstance
  have hProjectionFraction_injective :
      Function.Injective
        (algebraMap (ProjectionBase K)
          (FractionRing (CoordinateRing f))) := by
    rw [IsScalarTower.algebraMap_eq
      (ProjectionBase K) (CoordinateRing f)
      (FractionRing (CoordinateRing f))]
    exact
      (IsFractionRing.injective (CoordinateRing f)
          (FractionRing (CoordinateRing f))).comp
        (projectionAlgebra_injective hirr hmonic)
  let : IsScalarTower K (ProjectionBase K)
      (FractionRing (CoordinateRing f)) :=
    IsScalarTower.of_algebraMap_eq fun x => by
      rw [IsScalarTower.algebraMap_apply K (CoordinateRing f)
          (FractionRing (CoordinateRing f)),
        IsScalarTower.algebraMap_apply (ProjectionBase K)
          (CoordinateRing f) (FractionRing (CoordinateRing f)),
        projectionAlgebra_algebraMap_apply f x]
  let : Algebra (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) :=
    functionFieldAlgebra f hirr hmonic
  let : IsScalarTower (ProjectionBase K) (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) :=
    IsScalarTower.of_algebraMap_eq fun x ↦
      (IsFractionRing.lift_algebraMap
        hProjectionFraction_injective x).symm
  intro hseparable
  let : Algebra.IsSeparable (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) :=
    hseparable
  let : Module.Finite (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) :=
    functionField_finiteDimensional f hirr hmonic
  let : IsPrincipalIdealRing (ProjectionBase K) :=
    projectionBase_isPrincipalIdealRing (K := K)
  let S :=
    (integralClosure (ProjectionBase K)
      (FractionRing (CoordinateRing f))).restrictScalars K
  let baseToS : ProjectionBase K →+* S :=
    { toFun := fun r =>
        ⟨algebraMap (ProjectionBase K)
            (FractionRing (CoordinateRing f)) r,
          isIntegral_algebraMap⟩
      map_zero' := Subtype.ext (map_zero _)
      map_one' := Subtype.ext (map_one _)
      map_add' := fun _ _ => Subtype.ext (map_add _ _ _)
      map_mul' := fun _ _ => Subtype.ext (map_mul _ _ _) }
  let : Algebra (ProjectionBase K) S :=
    baseToS.toAlgebra
  let : IsScalarTower (ProjectionBase K) S
      (FractionRing (CoordinateRing f)) :=
    IsScalarTower.of_algebraMap_eq fun _ => rfl
  let : IsScalarTower K S (FractionRing (CoordinateRing f)) :=
    IsScalarTower.subalgebra' K
      (FractionRing (CoordinateRing f))
      (FractionRing (CoordinateRing f)) S
  let : IsIntegralClosure S (ProjectionBase K)
      (FractionRing (CoordinateRing f)) :=
    { algebraMap_injective := fun _ _ h => Subtype.ext h
      isIntegral_iff := by
        intro x
        constructor
        · intro hx
          exact ⟨⟨x, hx⟩, rfl⟩
        · rintro ⟨x, rfl⟩
          exact x.property }
  let : Module.Finite (ProjectionBase K) S :=
    IsIntegralClosure.finite
      (ProjectionBase K) (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) S
  let : IsDedekindDomain S :=
    IsIntegralClosure.isDedekindDomain
      (ProjectionBase K) (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) S
  let : IsFractionRing S (FractionRing (CoordinateRing f)) :=
    IsIntegralClosure.isFractionRing_of_finite_extension
      (ProjectionBase K) (ProjectionFunctionField K)
      (FractionRing (CoordinateRing f)) S
  let hTorsionFreeS : Module.IsTorsionFree (ProjectionBase K) S :=
    FunctionFieldPrimeDivisor.integralClosure_isTorsionFree_of_algebraMap_injective
      (A := ProjectionBase K) (B := S)
      hProjectionFraction_injective
  let hFlat : Module.Flat (ProjectionBase K) S := by
    let : Module.IsTorsionFree (ProjectionBase K) S :=
      hTorsionFreeS
    infer_instance
  let : Module.Flat (ProjectionBase K) S := hFlat
  let : (projectionPointIdeal (K := K) p).IsPrime :=
    projectionPointIdeal_isPrime p
  let toFiniteDivisorOver :
      CenteredPrimeDivisor (K := K) p →
        PrimeDivisorCounting.FiniteDivisorOver
          (K := K) (S := S)
          (F := FractionRing (CoordinateRing f))
          (projectionPointIdeal (K := K) p) :=
    fun v => by
      let ιS :=
        IsScalarTower.toAlgHom K S
          (FractionRing (CoordinateRing f))
      have hfiniteBase :
          v.divisor.FiniteAlong
            (IsScalarTower.toAlgHom K (ProjectionBase K)
              (FractionRing (CoordinateRing f))) := by
        intro r
        change
          algebraMap (ProjectionBase K)
              (FractionRing (CoordinateRing f)) r ∈
            v.divisor.valuationSubring
        rw [IsScalarTower.algebraMap_apply
          (ProjectionBase K) (CoordinateRing f)
          (FractionRing (CoordinateRing f))]
        exact v.finite (algebraMap (ProjectionBase K)
          (CoordinateRing f) r)
      have hfiniteS : v.divisor.FiniteAlong ιS := by
        exact v.divisor.finiteAlong_integralClosure
          (A := ProjectionBase K) (B := S) hfiniteBase
      refine
        { divisor := v.divisor
          finite := hfiniteS
          center_liesOver := ?_ }
      ext r
      change
        algebraMap (ProjectionBase K) (CoordinateRing f) r ∈
            pointIdeal p ↔
          algebraMap (ProjectionBase K) S r ∈
            v.divisor.centerAlong ιS hfiniteS
      rw [← v.center_eq]
      rw [v.divisor.mem_centerAlong_iff_mem_nonunits,
        v.divisor.mem_centerAlong_iff_mem_nonunits]
      change
        algebraMap (CoordinateRing f)
              (FractionRing (CoordinateRing f))
              (algebraMap (ProjectionBase K) (CoordinateRing f) r) ∈
            v.divisor.valuationSubring.nonunits ↔
          algebraMap S (FractionRing (CoordinateRing f))
              (algebraMap (ProjectionBase K) S r) ∈
            v.divisor.valuationSubring.nonunits
      rw [← IsScalarTower.algebraMap_apply
          (ProjectionBase K) (CoordinateRing f)
          (FractionRing (CoordinateRing f)),
        ← IsScalarTower.algebraMap_apply
          (ProjectionBase K) S
          (FractionRing (CoordinateRing f))]
  have toFiniteDivisorOver_injective :
      Function.Injective toFiniteDivisorOver := by
    intro v w h
    apply CenteredPrimeDivisor.ext
    exact congrArg
      PrimeDivisorCounting.FiniteDivisorOver.divisor h
  let toPrimeOver :
      CenteredPrimeDivisor (K := K) p →
        (projectionPointIdeal (K := K) p).primesOver S :=
    fun v ↦
      PrimeDivisorCounting.FiniteDivisorOver.centerMap
        (toFiniteDivisorOver v)
  have toPrimeOver_injective : Function.Injective toPrimeOver :=
    PrimeDivisorCounting.FiniteDivisorOver.centerMap_injective.comp
      toFiniteDivisorOver_injective
  let : Finite
      ((projectionPointIdeal (K := K) p).primesOver S) :=
    Algebra.QuasiFinite.finite_primesOver
      (R := ProjectionBase K) (S := S)
      (projectionPointIdeal (K := K) p)
  calc
    Nat.card (CenteredPrimeDivisor (K := K) p) ≤
        Nat.card ((projectionPointIdeal (K := K) p).primesOver S) :=
      Nat.card_le_card_of_injective
        toPrimeOver toPrimeOver_injective
    _ ≤ Module.finrank (ProjectionBase K) S :=
      PrimeCounting.card_primesOver_le_finrank
        (projectionPointIdeal (K := K) p)
    _ = Module.finrank (ProjectionFunctionField K)
          (FractionRing (CoordinateRing f)) :=
      integralClosure_finrank_eq_of_algebraMap_injective
        (ProjectionBase K) (ProjectionFunctionField K)
        (FractionRing (CoordinateRing f)) S
        hProjectionFraction_injective
    _ ≤ MvPolynomial.totalDegree f :=
      functionField_finrank_le_totalDegree f hirr hmonic

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.