Module

CenteredTransport.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.CenteredTransport

14 declarations indexed from sourceView source ↗

Module documentation

Transport of centered prime divisors

Coordinate-ring equivalences transport rational points and centered prime divisors. Applied to the monic representative of a plane equation, this removes the literal monicity assumption from the separable-projection form of Fried--Jarden, Lemma 6.2.2(b).

Imports4

Imported by2

theorem

centerAlong_comap_comp

L36 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.centerAlong_comap_comp

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace FunctionFieldPrimeDivisor

Lean source · full declaration

theorem centerAlong_comap_comp
    {F A B : Type*} [Field F] [CommRing A] [CommRing B]
    [Algebra K F] [Algebra K A] [Algebra K B]
    (v : FunctionFieldPrimeDivisor K F)
    (j : B →ₐ[K] F) (hj : v.FiniteAlong j)
    (e : A →ₐ[K] B) :
    (v.centerAlong j hj).comap e.toRingHom =
      v.centerAlong (j.comp e) (fun a => hj (e a)) := by
  rfl

theorem

centerAlong_congr

L50 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.centerAlong_congr

Documentation

The center along a model map depends only on the underlying map into the function field, not on the proof that the map lands in the valuation ring.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace FunctionFieldPrimeDivisor

Lean source · statement

theorem centerAlong_congr
    {F A : Type*} [Field F] [CommRing A]
    [Algebra K F] [Algebra K A]
    (v : FunctionFieldPrimeDivisor K F)
    {ι κ : A →ₐ[K] F}
    (hι : v.FiniteAlong ι) (hκ : v.FiniteAlong κ)
    (h : ∀ a, ι a = κ a) :
    v.centerAlong ι hι = v.centerAlong κ hκ

theorem

ext

L67 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.RationalPoint.ext

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace AffinePlaneCurve

Lean source · statement

theorem RationalPoint.ext
    {f : BivariatePolynomial K} {p q : RationalPoint f}
    (h : p.coords = q.coords) :
    p = q

theorem

mapCoordinateRingEquiv_symm

L77 ↗

FieldArithmetic.Chapter06.AffinePlaneCurve.RationalPoint.mapCoordinateRingEquiv_symm

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace AffinePlaneCurve

Lean source · statement

theorem RationalPoint.mapCoordinateRingEquiv_symm
    {f g : BivariatePolynomial K}
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (p : RationalPoint f) :
    (p.mapCoordinateRingEquiv e).mapCoordinateRingEquiv e.symm = p

def

coordinateFunctionFieldEquiv

L96 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.coordinateFunctionFieldEquiv

Documentation

The fraction-field equivalence induced by a coordinate-ring equivalence.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · statement

def coordinateFunctionFieldEquiv
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g) :
    FractionRing (CoordinateRing f) ≃ₐ[K]
      FractionRing (CoordinateRing g)

theorem

coordinateFunctionFieldEquiv_algebraMap

L105 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.coordinateFunctionFieldEquiv_algebraMap

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · statement

theorem coordinateFunctionFieldEquiv_algebraMap
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (x : CoordinateRing f) :
    coordinateFunctionFieldEquiv e
        (algebraMap (CoordinateRing f)
          (FractionRing (CoordinateRing f)) x) =
      algebraMap (CoordinateRing g)
        (FractionRing (CoordinateRing g)) (e x)

def

mapCoordinateRingEquiv

L121 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.CenteredPrimeDivisor.mapCoordinateRingEquiv

Documentation

Transport a divisor centered at p to the corresponding point under a coordinate-ring equivalence.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · statement

def CenteredPrimeDivisor.mapCoordinateRingEquiv
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (p : RationalPoint f)
    (v : CenteredPrimeDivisor (K := K) p) :
    CenteredPrimeDivisor (K := K)
      (p.mapCoordinateRingEquiv e)

theorem

divisor_mapCoordinateRingEquiv

L187 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.CenteredPrimeDivisor.divisor_mapCoordinateRingEquiv

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · statement

theorem CenteredPrimeDivisor.divisor_mapCoordinateRingEquiv
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (p : RationalPoint f)
    (v : CenteredPrimeDivisor (K := K) p) :
    (v.mapCoordinateRingEquiv e p).divisor =
      v.divisor.map (coordinateFunctionFieldEquiv e)

theorem

divisor_cast

L198 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.CenteredPrimeDivisor.divisor_cast

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · statement

theorem CenteredPrimeDivisor.divisor_cast
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    {p q : RationalPoint f} (h : p = q)
    (v : CenteredPrimeDivisor (K := K) p) :
    ((h ▸ v) : CenteredPrimeDivisor (K := K) q).divisor =
      v.divisor

theorem

mapCoordinateRingEquiv_injective

L207 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.CenteredPrimeDivisor.mapCoordinateRingEquiv_injective

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · statement

theorem CenteredPrimeDivisor.mapCoordinateRingEquiv_injective
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (p : RationalPoint f) :
    Function.Injective
      (CenteredPrimeDivisor.mapCoordinateRingEquiv
        (K := K) e p)

theorem

mapCoordinateRingEquiv_surjective

L222 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.CenteredPrimeDivisor.mapCoordinateRingEquiv_surjective

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · statement

theorem CenteredPrimeDivisor.mapCoordinateRingEquiv_surjective
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (p : RationalPoint f) :
    Function.Surjective
      (CenteredPrimeDivisor.mapCoordinateRingEquiv
        (K := K) e p)

def

equivCoordinateRingEquiv

L247 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.CenteredPrimeDivisor.equivCoordinateRingEquiv

Documentation

Centered prime divisors are invariant under coordinate-ring equivalence.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · statement

def CenteredPrimeDivisor.equivCoordinateRingEquiv
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (p : RationalPoint f) :
    CenteredPrimeDivisor (K := K) p ≃
      CenteredPrimeDivisor (K := K)
        (p.mapCoordinateRingEquiv e)

def

MonicRepresentativeProjectionSeparable

L269 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.MonicRepresentativeProjectionSeparable

Documentation

The projection attached to a chosen monic representative is separable.

This packages the local domain and algebra structures used by card_centeredPrimeDivisor_le_totalDegree_of_monicRepresentative.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · statement

def MonicRepresentativeProjectionSeparable
    {f : BivariatePolynomial K} (hirr : Irreducible f)
    (c : Fin 1 → K)
    (h : IsUnit
      (yPolynomial (linearChangeY c f)).leadingCoeff) : Prop

theorem

card_centeredPrimeDivisor_le_totalDegree_of_monicRepresentative

L296 ↗

FieldArithmetic.Chapter06.CenteredPrimeDivisorBound.card_centeredPrimeDivisor_le_totalDegree_of_monicRepresentative

Documentation

After an invertible linear coordinate change and unit rescaling, the separable-projection bound for a monic equation bounds the centered prime divisors of the original plane curve.

Thus literal monicity is a choice of coordinates rather than a hypothesis on the original equation.

Source context 9 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open AffinePlaneCurve
open MonicPlaneCurveProjection PlaneCurveMonicNormalization
open CenteredPrimeDivisorBound
universe u
variable {K : Type u} [Field K]
namespace CenteredPrimeDivisorBound

Lean source · full declaration

theorem card_centeredPrimeDivisor_le_totalDegree_of_monicRepresentative
    {f : BivariatePolynomial K} (hirr : Irreducible f)
    (c : Fin 1 → K)
    (h : IsUnit
      (yPolynomial (linearChangeY c f)).leadingCoeff)
    (p : RationalPoint f)
    (hseparable :
      MonicRepresentativeProjectionSeparable hirr c h) :
    letI : IsDomain (CoordinateRing f) :=
      coordinateRing_isDomain hirr
    Nat.card (CenteredPrimeDivisor (K := K) p) ≤
      MvPolynomial.totalDegree f := by
  let : IsDomain (CoordinateRing f) :=
    coordinateRing_isDomain hirr
  let g := monicRepresentative f c h
  have hg : Irreducible g :=
    monicRepresentative_irreducible hirr c h
  have hmonic : (yPolynomial g).Monic :=
    monicRepresentative_monic f c h
  let : IsDomain (CoordinateRing g) :=
    coordinateRing_isDomain hg
  let : Algebra (ProjectionFunctionField K)
      (FractionRing (CoordinateRing g)) :=
    functionFieldAlgebra g hg hmonic
  have hseparable' :
      Algebra.IsSeparable (ProjectionFunctionField K)
        (FractionRing (CoordinateRing g)) := by
    simpa [MonicRepresentativeProjectionSeparable, g] using
      hseparable
  let e : CoordinateRing f ≃ₐ[K] CoordinateRing g :=
    coordinateRingEquivMonicRepresentative f c h
  calc
    Nat.card (CenteredPrimeDivisor (K := K) p) =
        Nat.card
          (CenteredPrimeDivisor (K := K)
            (p.mapCoordinateRingEquiv e)) :=
      Nat.card_congr
        (CenteredPrimeDivisor.equivCoordinateRingEquiv
          (K := K) e p)
    _ ≤ MvPolynomial.totalDegree g :=
      card_centeredPrimeDivisor_le_totalDegree
        hg hmonic (p.mapCoordinateRingEquiv e) hseparable'
    _ = MvPolynomial.totalDegree f :=
      totalDegree_monicRepresentative hirr.ne_zero c h

Module documentation

Transport of centered prime divisors

Declarations