NYLL
Module

Infinity.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Infinity
39 declarations indexed from sourceView source ↗

Module documentation

Prime divisors at infinity

This file develops the valuation-theoretic input for Fried--Jarden, Lemma 6.2.2(d). If t is a transcendental function, a prime divisor which is not finite on K[t] is finite on K[t⁻¹], and its center there is the unique closed point t⁻¹ = 0. This identifies all such prime divisors with extensions of the single infinite prime of K(t).

The construction is stated for actual subalgebras of the ambient function field. In particular, no auxiliary place or valuation-extension relation is postulated.

Imports7
Imported by1

Declarations

abbrev

PolynomialModel

L46 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.PolynomialModel
Documentation

The affine polynomial model generated by one function t.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
abbrev PolynomialModel (t : F) : Subalgebra K F
abbrev

InfinityModel

L50 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.InfinityModel
Documentation

The affine chart at infinity, generated by the inverse parameter.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
abbrev InfinityModel (t : F) : Subalgebra K F
def

inverseGenerator

L54 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.inverseGenerator
Documentation

The inverse parameter as an element of its affine model.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
def inverseGenerator (t : F) : InfinityModel (K := K) t
def

infinityPrime

L58 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.infinityPrime
Documentation

The point at infinity on K[t⁻¹].

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
def infinityPrime (t : F) : Ideal (InfinityModel (K := K) t)
theorem

finiteOn_polynomialModel_iff

L65 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.finiteOn_polynomialModel_iff
Documentation

A prime divisor is finite on the singly generated model K[t] exactly when its valuation ring contains t.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finiteOn_polynomialModel_iff
    (v : FunctionFieldPrimeDivisor K F) (t : F) :
    v.FiniteOn (PolynomialModel (K := K) t) ↔
      t ∈ v.valuationSubring
theorem

finiteOn_infinityModel_iff

L83 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.finiteOn_infinityModel_iff
Documentation

The corresponding membership criterion on the inverse chart.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finiteOn_infinityModel_iff
    (v : FunctionFieldPrimeDivisor K F) (t : F) :
    v.FiniteOn (InfinityModel (K := K) t) ↔
      t⁻¹ ∈ v.valuationSubring
theorem

finiteOn_infinityModel_of_not_finiteOn_polynomialModel

L93 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.finiteOn_infinityModel_of_not_finiteOn_polynomialModel
Documentation

If a prime divisor is not finite on K[t], it is finite on K[t⁻¹].

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finiteOn_infinityModel_of_not_finiteOn_polynomialModel
    (v : FunctionFieldPrimeDivisor K F) (t : F)
    (h : ¬v.FiniteOn (PolynomialModel (K := K) t)) :
    v.FiniteOn (InfinityModel (K := K) t)
theorem

inverse_mem_nonunits_of_not_finiteOn_polynomialModel

L106 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.inverse_mem_nonunits_of_not_finiteOn_polynomialModel
Documentation

At a prime divisor not finite on K[t], the inverse parameter belongs to the maximal ideal, rather than merely to the valuation ring.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem inverse_mem_nonunits_of_not_finiteOn_polynomialModel
    (v : FunctionFieldPrimeDivisor K F) (t : F)
    (h : ¬v.FiniteOn (PolynomialModel (K := K) t)) :
    t⁻¹ ∈ v.valuationSubring.nonunits
theorem

transcendental_inv

L115 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.transcendental_inv
Documentation

Transcendence is preserved by inversion in a field.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem transcendental_inv {t : F} (ht : Transcendental K t) :
    Transcendental K t⁻¹
theorem

infinityPrime_isMaximal

L120 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.infinityPrime_isMaximal
Documentation

The ideal t⁻¹ = 0 is maximal on the inverse polynomial chart.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem infinityPrime_isMaximal
    {t : F} (ht : Transcendental K t) :
    (infinityPrime (K := K) t).IsMaximal
theorem

center_infinityModel_eq_infinityPrime

L147 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.center_infinityModel_eq_infinityPrime
Documentation

Every prime divisor which is infinite at t has the same center, namely the closed point t⁻¹ = 0 on the inverse chart.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem center_infinityModel_eq_infinityPrime
    (v : FunctionFieldPrimeDivisor K F) {t : F}
    (ht : Transcendental K t)
    (h : ¬v.FiniteOn (PolynomialModel (K := K) t)) :
    v.center (InfinityModel (K := K) t)
        (finiteOn_infinityModel_of_not_finiteOn_polynomialModel v t h) =
      infinityPrime (K := K) t
structure

InfinitePrimeDivisor

L171 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.InfinitePrimeDivisor
Documentation

Prime divisors which are not finite on the polynomial model K[t].

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · full declaration
structure InfinitePrimeDivisor (t : F) where
  /-- The underlying prime divisor of the function field. -/
  divisor : FunctionFieldPrimeDivisor K F
  /-- The divisor is not finite on the polynomial model generated by t. -/
  not_finite :
    ¬divisor.FiniteOn (PolynomialModel (K := K) t)
theorem

ext

L181 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.InfinitePrimeDivisor.ext
Source context 11 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
namespace InfinitePrimeDivisor
Lean source · statement
theorem ext {t : F} {v w : InfinitePrimeDivisor (K := K) t}
    (h : v.divisor = w.divisor) :
    v = w
abbrev

coordinateRingInclusion

L194 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.coordinateRingInclusion
Documentation

The inclusion of an affine plane-curve coordinate ring in its function field.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
abbrev coordinateRingInclusion
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)] :
    CoordinateRing f →ₐ[K] FractionRing (CoordinateRing f)
structure

NonfiniteCoordinatePrimeDivisor

L201 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.NonfiniteCoordinatePrimeDivisor
Documentation

Prime divisors which are not finite on the affine coordinate ring.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · full declaration
structure NonfiniteCoordinatePrimeDivisor
    (f : BivariatePolynomial K) [IsDomain (CoordinateRing f)] where
  /-- The underlying prime divisor of the fraction field of the coordinate ring. -/
  divisor :
    FunctionFieldPrimeDivisor K (FractionRing (CoordinateRing f))
  /-- The divisor is not finite along the coordinate-ring inclusion. -/
  not_finite :
    ¬divisor.FiniteAlong (coordinateRingInclusion (K := K) (f := f))
theorem

ext

L215 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.NonfiniteCoordinatePrimeDivisor.ext
Source context 12 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
namespace NonfiniteCoordinatePrimeDivisor
variable {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
Lean source · statement
theorem ext {v w : NonfiniteCoordinatePrimeDivisor (K := K) f}
    (h : v.divisor = w.divisor) :
    v = w
def

mapCoordinateRingEquiv

L231 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.NonfiniteCoordinatePrimeDivisor.mapCoordinateRingEquiv
Documentation

Transport a nonfinite prime divisor across a coordinate-ring equivalence.

The induced fraction-field equivalence carries the inclusion of the source coordinate ring to the inclusion of the target coordinate ring. Therefore finiteness, and hence its negation, is invariant under transport.

Source context 12 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
namespace NonfiniteCoordinatePrimeDivisor
variable {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
Lean source · statement
def mapCoordinateRingEquiv
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (v : NonfiniteCoordinatePrimeDivisor (K := K) f) :
    NonfiniteCoordinatePrimeDivisor (K := K) g
theorem

divisor_mapCoordinateRingEquiv

L264 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.NonfiniteCoordinatePrimeDivisor.divisor_mapCoordinateRingEquiv
Source context 12 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
namespace NonfiniteCoordinatePrimeDivisor
variable {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
Lean source · statement
theorem divisor_mapCoordinateRingEquiv
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g)
    (v : NonfiniteCoordinatePrimeDivisor (K := K) f) :
    (v.mapCoordinateRingEquiv e).divisor =
      v.divisor.map
        (CenteredPrimeDivisorBound.coordinateFunctionFieldEquiv e)
def

equivCoordinateRingEquiv

L278 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.NonfiniteCoordinatePrimeDivisor.equivCoordinateRingEquiv
Documentation

Nonfinite prime divisors are invariant under arbitrary coordinate-ring K-algebra equivalences.

Source context 12 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
namespace NonfiniteCoordinatePrimeDivisor
variable {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
Lean source · full declaration
def equivCoordinateRingEquiv
    {f g : BivariatePolynomial K}
    [IsDomain (CoordinateRing f)] [IsDomain (CoordinateRing g)]
    (e : CoordinateRing f ≃ₐ[K] CoordinateRing g) :
    NonfiniteCoordinatePrimeDivisor (K := K) f ≃
      NonfiniteCoordinatePrimeDivisor (K := K) g where
  toFun := mapCoordinateRingEquiv e
  invFun := mapCoordinateRingEquiv e.symm
  left_inv v := by
    apply ext
    simp only [divisor_mapCoordinateRingEquiv]
    have he :
        CenteredPrimeDivisorBound.coordinateFunctionFieldEquiv e.symm =
          (CenteredPrimeDivisorBound.coordinateFunctionFieldEquiv e).symm := by
      rfl
    rw [he]
    exact
      FunctionFieldPrimeDivisor.map_symm_map
        (CenteredPrimeDivisorBound.coordinateFunctionFieldEquiv e)
        v.divisor
  right_inv v := by
    apply ext
    simp only [divisor_mapCoordinateRingEquiv]
    have he :
        CenteredPrimeDivisorBound.coordinateFunctionFieldEquiv e.symm =
          (CenteredPrimeDivisorBound.coordinateFunctionFieldEquiv e).symm := by
      rfl
    rw [he]
    simpa using
      (FunctionFieldPrimeDivisor.map_symm_map
        (CenteredPrimeDivisorBound.coordinateFunctionFieldEquiv e).symm
        v.divisor)
theorem

projectionAlgebra_algebraMap_apply

L314 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.projectionAlgebra_algebraMap_apply
Documentation

The projection algebra structure respects the constant-field maps.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
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
def

projectionBaseEquivPolynomial

L330 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.projectionBaseEquivPolynomial
Documentation

The one-variable projection base in ordinary polynomial coordinates.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
def projectionBaseEquivPolynomial :
    ProjectionBase K ≃ₐ[K] Polynomial K
theorem

projectionBaseEquivPolynomial_X

L337 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.projectionBaseEquivPolynomial_X
Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem projectionBaseEquivPolynomial_X :
    projectionBaseEquivPolynomial (K := K)
        (MvPolynomial.X (0 : Fin 1)) =
      Polynomial.X
theorem

intermediateField_adjoin_inv_eq_adjoin

L346 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.intermediateField_adjoin_inv_eq_adjoin
Documentation

A transcendental element and its inverse generate the same intermediate field.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem intermediateField_adjoin_inv_eq_adjoin
    {t : F} (_ht : Transcendental K t) :
    IntermediateField.adjoin K ({t⁻¹} : Set F) =
      IntermediateField.adjoin K ({t} : Set F)
def

infinityProjectionFieldEquiv

L377 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.infinityProjectionFieldEquiv
Documentation

Changing the rational parameter from t⁻¹ to t identifies the two abstract fraction fields.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
def infinityProjectionFieldEquiv
    {t : F} (ht : Transcendental K t) :
    FractionRing (InfinityModel (K := K) t) ≃ₐ[K]
      ProjectionFunctionField K
def

projectionParameter

L402 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.projectionParameter
Documentation

The image of the projection coordinate in the curve's function field.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
def projectionParameter
    (f : BivariatePolynomial K) [IsDomain (CoordinateRing f)] :
    FractionRing (CoordinateRing f)
def

projectionFractionAlgebra

L416 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.projectionFractionAlgebra
Documentation

The projection-base action on the curve's fraction field, written as the literal composite through the coordinate ring. Keeping this map canonical avoids asking typeclass synthesis to reconstruct the same algebra tower in each valuation-counting theorem below.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
def projectionFractionAlgebra
    (f : BivariatePolynomial K) [IsDomain (CoordinateRing f)] :
    Algebra (ProjectionBase K) (FractionRing (CoordinateRing f))
def

projectionFractionAlgHom

L428 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.projectionFractionAlgHom
Documentation

The projection map to the curve's fraction field as a K-algebra map. This packages constant-field compatibility directly, so transcendence and the rational-function lift do not need a synthesized three-level scalar tower.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · full declaration
def projectionFractionAlgHom
    (f : BivariatePolynomial K) [IsDomain (CoordinateRing f)] :
    ProjectionBase K →ₐ[K] FractionRing (CoordinateRing f) where
  toRingHom :=
    @algebraMap (ProjectionBase K) (FractionRing (CoordinateRing f)) _ _
      (projectionFractionAlgebra f)
  commutes' x := by
    change
      algebraMap (CoordinateRing f) (FractionRing (CoordinateRing f))
          (@algebraMap (ProjectionBase K) (CoordinateRing f) _ _
            (projectionAlgebra f) (algebraMap K (ProjectionBase K) x)) =
        algebraMap K (FractionRing (CoordinateRing f)) x
    rw [projectionAlgebra_algebraMap_apply f x,
      ← IsScalarTower.algebraMap_apply K (CoordinateRing f)
        (FractionRing (CoordinateRing f))]
theorem

projectionFractionAlgHom_injective

L444 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.projectionFractionAlgHom_injective
Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem projectionFractionAlgHom_injective
    {f : BivariatePolynomial K} [IsDomain (CoordinateRing f)]
    (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) :
    Function.Injective (projectionFractionAlgHom (K := K) f)
abbrev

InfinityNormalization

L454 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.InfinityNormalization
Documentation

The normalization of the inverse chart inside the ambient field.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
abbrev InfinityNormalization (t : F) : Subalgebra K F
def

infinityModelToNormalization

L459 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.infinityModelToNormalization
Documentation

Inclusion of the inverse chart into its normalization.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
def infinityModelToNormalization (t : F) :
    InfinityModel (K := K) t →ₐ[K] InfinityNormalization (K := K) t
def

infinityNormalizationAlgebra

L470 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.infinityNormalizationAlgebra
Documentation

The algebra structure of the normalization over the inverse polynomial chart. Its algebra map is the literal inclusion in F.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
def infinityNormalizationAlgebra (t : F) :
    Algebra (InfinityModel (K := K) t)
      (InfinityNormalization (K := K) t)
def

infinityFunctionFieldAlgebra

L479 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.infinityFunctionFieldAlgebra
Documentation

The algebra structure on F over the fraction field of the inverse chart.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
def infinityFunctionFieldAlgebra (t : F) :
    Algebra (FractionRing (InfinityModel (K := K) t)) F
theorem

infinityNormalization_finrank_eq_of_algebraMap_injective

L490 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.infinityNormalization_finrank_eq_of_algebraMap_injective
Documentation

Rank comparison for the normalization of an inverse chart. The injectivity of the ambient algebra map is supplied as data, so the comparison does not reopen a FaithfulSMul search through either fraction-field tower.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem infinityNormalization_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

infinityProjectionFieldEquiv_compatible

L509 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.infinityProjectionFieldEquiv_compatible
Documentation

The change-of-parameter equivalence is compatible with embeddings in an ambient field whenever the projection variable maps to t.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem infinityProjectionFieldEquiv_compatible
    {t : F} (ht : Transcendental K t)
    [Algebra (ProjectionFunctionField K) F]
    [IsScalarTower K (ProjectionFunctionField K) F]
    (hX :
      algebraMap (ProjectionFunctionField K) F
          (algebraMap (ProjectionBase K)
            (ProjectionFunctionField K)
            (MvPolynomial.X (0 : Fin 1))) =
        t) :
    letI : Algebra
        (FractionRing (InfinityModel (K := K) t)) F :=
      infinityFunctionFieldAlgebra (K := K) t
    (algebraMap (ProjectionFunctionField K) F).comp
        (infinityProjectionFieldEquiv ht).toRingHom =
      algebraMap (FractionRing (InfinityModel (K := K) t)) F := by
  let B := InfinityModel (K := K) t
  let E := FractionRing B
  let Q := ProjectionFunctionField K
  let Jinv := IntermediateField.adjoin K ({t⁻¹} : Set F)
  let J := IntermediateField.adjoin K ({t} : Set F)
  let : Algebra E F :=
    infinityFunctionFieldAlgebra (K := K) t
  have hBF : Function.Injective (algebraMap B F) :=
    fun _ _ h => Subtype.ext h
  let : IsScalarTower B E F :=
    IsScalarTower.of_algebraMap_eq fun x =>
      (IsFractionRing.lift_algebraMap hBF x).symm
  let eInv :
      E ≃ₐ[K] Jinv :=
    IsFractionRing.algEquivOfAlgEquiv
      (AlgEquiv.refl : B ≃ₐ[K] B)
  let eBase :
      ProjectionBase K ≃ₐ[K] Algebra.adjoin K ({t} : Set F) :=
    (projectionBaseEquivPolynomial (K := K)).trans
      (Polynomial.algEquivOfTranscendental K t ht)
  let eProjection :
      Q ≃ₐ[K] J :=
    IsFractionRing.algEquivOfAlgEquiv eBase
  let eJ : Jinv ≃ₐ[K] J :=
    IntermediateField.equivOfEq
      (intermediateField_adjoin_inv_eq_adjoin ht)
  have hBase :
      (Algebra.adjoin K ({t} : Set F)).val.comp eBase.toAlgHom =
        (IsScalarTower.toAlgHom K Q F).comp
          (IsScalarTower.toAlgHom K (ProjectionBase K) Q) := by
    apply MvPolynomial.algHom_ext
    intro i
    have hi : i = (0 : Fin 1) := Subsingleton.elim _ _
    subst i
    simp only [AlgHom.coe_comp, Function.comp_apply]
    change
      ((eBase (MvPolynomial.X (0 : Fin 1)) :
        Algebra.adjoin K ({t} : Set F)) : F) =
          algebraMap Q F
            (algebraMap (ProjectionBase K) Q
              (MvPolynomial.X (0 : Fin 1)))
    rw [hX]
    simp [eBase]
  have hProjection :
      J.val.toRingHom.comp eProjection.toRingHom =
        (algebraMap Q F) := by
    apply IsLocalization.ringHom_ext
      (nonZeroDivisors (ProjectionBase K))
    apply RingHom.ext
    intro a
    have ha := DFunLike.congr_fun hBase a
    change
      ((eProjection
          (algebraMap (ProjectionBase K) Q a) : J) : F) =
        algebraMap Q F
          (algebraMap (ProjectionBase K) Q a)
    rw [IsFractionRing.algEquivOfAlgEquiv_algebraMap]
    exact ha
  have hProjectionSymm :
      (algebraMap Q F).comp eProjection.symm.toRingHom =
        J.val.toRingHom := by
    apply RingHom.ext
    intro x
    have hx := DFunLike.congr_fun hProjection (eProjection.symm x)
    simpa using hx.symm
  have hInv :
      Jinv.val.toRingHom.comp eInv.toRingHom =
        algebraMap E F := by
    apply IsLocalization.ringHom_ext (nonZeroDivisors B)
    apply RingHom.ext
    intro b
    change
      ((eInv (algebraMap B E b) : Jinv) : F) =
        algebraMap E F (algebraMap B E b)
    rw [IsFractionRing.algEquivOfAlgEquiv_algebraMap]
    rw [← IsScalarTower.algebraMap_apply B E F]
    rfl
  have hJ :
      J.val.toRingHom.comp eJ.toRingHom =
        Jinv.val.toRingHom := by
    apply RingHom.ext
    intro x
    rfl
  apply RingHom.ext
  intro x
  change
    algebraMap Q F
        (eProjection.symm (eJ (eInv x))) =
      algebraMap E F x
  rw [show
      algebraMap Q F
          (eProjection.symm (eJ (eInv x))) =
        ((eJ (eInv x) : J) : F) by
      exact DFunLike.congr_fun hProjectionSymm (eJ (eInv x))]
  rw [show
      ((eJ (eInv x) : J) : F) =
        ((eInv x : Jinv) : F) by
      exact DFunLike.congr_fun hJ (eInv x)]
  exact DFunLike.congr_fun hInv x
theorem

finite_and_card_infinitePrimeDivisor_le_finrank_of_isSeparable

L637 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.finite_and_card_infinitePrimeDivisor_le_finrank_of_isSeparable
Documentation

Separable valuation-extension count at infinity.

This is the exact valuation count used in the separable case of Fried--Jarden 6.2.2(d): all infinite prime divisors inject into the primes of the finite Dedekind normalization above t⁻¹ = 0, and their number is bounded by the degree of the function-field extension.

The separability hypothesis occurs only because Mathlib's current theorem that a Dedekind domain has module-finite normalization in a finite extension is available for separable extensions.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finite_and_card_infinitePrimeDivisor_le_finrank_of_isSeparable
    {t : F} (ht : Transcendental K t)
    (hfinite :
      @Module.Finite (FractionRing (InfinityModel (K := K) t)) F _ _
        (infinityFunctionFieldAlgebra (K := K) t).toModule)
    (hseparable :
      @Algebra.IsSeparable
        (FractionRing (InfinityModel (K := K) t)) F _ _
        (infinityFunctionFieldAlgebra (K := K) t)) :
    Finite (InfinitePrimeDivisor (K := K) t) ∧
      Nat.card (InfinitePrimeDivisor (K := K) t) ≤
        @Module.finrank (FractionRing (InfinityModel (K := K) t)) F _ _
          (infinityFunctionFieldAlgebra (K := K) t).toModule
theorem

card_infinitePrimeDivisor_le_finrank_of_isSeparable

L756 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.card_infinitePrimeDivisor_le_finrank_of_isSeparable
Documentation

The numerical part of the separable valuation-extension count.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem card_infinitePrimeDivisor_le_finrank_of_isSeparable
    {t : F} (ht : Transcendental K t)
    (hfinite :
      @Module.Finite (FractionRing (InfinityModel (K := K) t)) F _ _
        (infinityFunctionFieldAlgebra (K := K) t).toModule)
    (hseparable :
      @Algebra.IsSeparable
        (FractionRing (InfinityModel (K := K) t)) F _ _
        (infinityFunctionFieldAlgebra (K := K) t)) :
    Nat.card (InfinitePrimeDivisor (K := K) t) ≤
      @Module.finrank (FractionRing (InfinityModel (K := K) t)) F _ _
        (infinityFunctionFieldAlgebra (K := K) t).toModule
theorem

card_nonfiniteCoordinatePrimeDivisor_le_finrank_of_isSeparable

L780 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.card_nonfiniteCoordinatePrimeDivisor_le_finrank_of_isSeparable
Documentation

For a monic plane projection, a prime divisor which is not finite on the coordinate ring is already infinite at the projection parameter. Thus the separable valuation-extension count applies directly to the affine curve.

The remaining right-hand side is the degree over K(t⁻¹). Identifying this with the degree over the projection field K(t) is a separate rational function-field change of parameter.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem card_nonfiniteCoordinatePrimeDivisor_le_finrank_of_isSeparable
    {f : BivariatePolynomial K} (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) :
    letI : IsDomain (CoordinateRing f) :=
      coordinateRing_isDomain hirr
    letI : Algebra (ProjectionBase K) (CoordinateRing f) :=
      projectionAlgebra f
    letI : Algebra (ProjectionBase K)
        (FractionRing (CoordinateRing f)) :=
      inferInstance
    letI : Algebra
        (FractionRing
          (InfinityModel (K := K) (projectionParameter (K := K) f)))
        (FractionRing (CoordinateRing f)) :=
      infinityFunctionFieldAlgebra
        (K := K) (projectionParameter (K := K) f)
    Module.Finite
        (FractionRing
          (InfinityModel (K := K) (projectionParameter (K := K) f)))
        (FractionRing (CoordinateRing f)) →
      Algebra.IsSeparable
          (FractionRing
            (InfinityModel (K := K) (projectionParameter (K := K) f)))
          (FractionRing (CoordinateRing f)) →
        Nat.card (NonfiniteCoordinatePrimeDivisor (K := K) f) ≤
          Module.finrank
            (FractionRing
              (InfinityModel (K := K)
                (projectionParameter (K := K) f)))
            (FractionRing (CoordinateRing f)) := by
  let : IsDomain (CoordinateRing f) :=
    coordinateRing_isDomain hirr
  let : Algebra (ProjectionBase K) (CoordinateRing f) :=
    projectionAlgebra f
  let : Algebra (ProjectionBase K)
      (FractionRing (CoordinateRing f)) :=
    projectionFractionAlgebra f
  let : IsScalarTower (ProjectionBase K) (CoordinateRing f)
      (FractionRing (CoordinateRing f)) :=
    inferInstance
  let : Algebra.IsIntegral (ProjectionBase K) (CoordinateRing f) :=
    coordinateRing_isIntegral f hmonic
  let t : FractionRing (CoordinateRing f) :=
    projectionParameter (K := K) f
  let : Algebra
      (FractionRing (InfinityModel (K := K) t))
      (FractionRing (CoordinateRing f)) :=
    infinityFunctionFieldAlgebra (K := K) t
  intro hfinite hseparable
  have hinjective :
      Function.Injective
        (algebraMap (ProjectionBase K)
          (FractionRing (CoordinateRing f))) := by
    change Function.Injective (projectionFractionAlgHom (K := K) f)
    exact projectionFractionAlgHom_injective hirr hmonic
  have ht : Transcendental K t := by
    change Transcendental K
      (projectionFractionAlgHom (K := K) f
        (MvPolynomial.X (0 : Fin 1)))
    simpa only [Transcendental,
      isAlgebraic_algHom_iff
        (projectionFractionAlgHom (K := K) f)
        (projectionFractionAlgHom_injective hirr hmonic)] using
      (MvPolynomial.transcendental_X K (0 : Fin 1))
  have projection_mem_polynomialModel
      (a : ProjectionBase K) :
      algebraMap (ProjectionBase K)
          (FractionRing (CoordinateRing f)) a ∈
        PolynomialModel (K := K) t := by
    have ha :
        a ∈ Algebra.adjoin K
          (Set.range
            (MvPolynomial.X :
              Fin 1 → ProjectionBase K)) := by
      rw [MvPolynomial.adjoin_range_X]
      trivial
    exact
      Algebra.adjoin_induction
        (p := fun z _ =>
          algebraMap (ProjectionBase K)
              (FractionRing (CoordinateRing f)) z ∈
            PolynomialModel (K := K) t)
        (fun z hz => by
          obtain ⟨i, rfl⟩ := hz
          have hi : i = (0 : Fin 1) := Subsingleton.elim _ _
          subst i
          exact
            Algebra.subset_adjoin
              (Set.mem_singleton t))
        (fun c => by
          change
            algebraMap (CoordinateRing f)
                (FractionRing (CoordinateRing f))
                (@algebraMap (ProjectionBase K) (CoordinateRing f) _ _
                  (projectionAlgebra f)
                  (algebraMap K (ProjectionBase K) c)) ∈
              PolynomialModel (K := K) t
          rw [projectionAlgebra_algebraMap_apply f c,
            ← IsScalarTower.algebraMap_apply K (CoordinateRing f)
              (FractionRing (CoordinateRing f))]
          exact
            (PolynomialModel (K := K) t).algebraMap_mem c)
        (fun x y _ _ hx hy => by
          simpa only [map_add] using add_mem hx hy)
        (fun x y _ _ hx hy => by
          simpa only [map_mul] using mul_mem hx hy)
        ha
  have finite_coordinateRing_of_finite_polynomialModel
      (v : FunctionFieldPrimeDivisor K
        (FractionRing (CoordinateRing f)))
      (hpoly : v.FiniteOn (PolynomialModel (K := K) t)) :
      v.FiniteAlong (coordinateRingInclusion (K := K) (f := f)) := by
    have hprojection
        (a : ProjectionBase K) :
        algebraMap (ProjectionBase K)
            (FractionRing (CoordinateRing f)) a ∈
          v.valuationSubring :=
      hpoly
        ⟨algebraMap (ProjectionBase K)
            (FractionRing (CoordinateRing f)) a,
          projection_mem_polynomialModel a⟩
    let g :
        ProjectionBase K →+* v.valuationSubring :=
      { toFun := fun a =>
          ⟨algebraMap (ProjectionBase K)
              (FractionRing (CoordinateRing f)) a,
            hprojection a⟩
        map_zero' := Subtype.ext (map_zero _)
        map_one' := Subtype.ext (map_one _)
        map_add' := fun x y => Subtype.ext (map_add _ x y)
        map_mul' := fun x y => Subtype.ext (map_mul _ x y) }
    let : Algebra (ProjectionBase K) v.valuationSubring :=
      g.toAlgebra
    let : IsScalarTower (ProjectionBase K)
        v.valuationSubring
        (FractionRing (CoordinateRing f)) :=
      IsScalarTower.of_algebraMap_eq fun _ => rfl
    intro x
    have hxProjection :
        IsIntegral (ProjectionBase K)
          (algebraMap (CoordinateRing f)
            (FractionRing (CoordinateRing f)) x) :=
      (Algebra.IsIntegral.isIntegral
        (R := ProjectionBase K) x).map
          (IsScalarTower.toAlgHom
            (ProjectionBase K) (CoordinateRing f)
            (FractionRing (CoordinateRing f)))
    have hxValuation :
        IsIntegral v.valuationSubring
          (algebraMap (CoordinateRing f)
            (FractionRing (CoordinateRing f)) x) :=
      hxProjection.tower_top
    obtain ⟨y, hy⟩ :=
      IsIntegrallyClosed.isIntegral_iff.mp hxValuation
    change
      algebraMap (CoordinateRing f)
          (FractionRing (CoordinateRing f)) x ∈
        v.valuationSubring
    rw [← hy]
    exact y.property
  let toInfinitePrimeDivisor :
      NonfiniteCoordinatePrimeDivisor (K := K) f →
        InfinitePrimeDivisor (K := K) t :=
    fun v =>
      { divisor := v.divisor
        not_finite := fun hpoly =>
          v.not_finite
            (finite_coordinateRing_of_finite_polynomialModel
              v.divisor hpoly) }
  have toInfinitePrimeDivisor_injective :
      Function.Injective toInfinitePrimeDivisor := by
    intro v w h
    apply NonfiniteCoordinatePrimeDivisor.ext
    exact congrArg InfinitePrimeDivisor.divisor h
  have hcount :=
    finite_and_card_infinitePrimeDivisor_le_finrank_of_isSeparable
      ht hfinite hseparable
  let : Finite (InfinitePrimeDivisor (K := K) t) :=
    hcount.1
  calc
    Nat.card (NonfiniteCoordinatePrimeDivisor (K := K) f) ≤
        Nat.card (InfinitePrimeDivisor (K := K) t) :=
      Nat.card_le_card_of_injective
        toInfinitePrimeDivisor
        toInfinitePrimeDivisor_injective
    _ ≤ Module.finrank
          (FractionRing (InfinityModel (K := K) t))
          (FractionRing (CoordinateRing f)) :=
      hcount.2
theorem

card_nonfiniteCoordinatePrimeDivisor_le_totalDegree_of_isSeparable

L980 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.card_nonfiniteCoordinatePrimeDivisor_le_totalDegree_of_isSeparable
Documentation

Separable monic-projection form of Fried--Jarden 6.2.2(d): the number of prime divisors which are not finite on the affine coordinate ring is at most the total degree of the plane equation.

Unlike the intermediate finrank theorem, finiteness over the inverse parameter field is derived here from the already established finite projection K(t) → F; the equivalence K(t⁻¹) ≃ K(t) also identifies the two finranks.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem card_nonfiniteCoordinatePrimeDivisor_le_totalDegree_of_isSeparable
    {f : BivariatePolynomial K} (hirr : Irreducible f)
    (hmonic : (yPolynomial f).Monic) :
    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 (NonfiniteCoordinatePrimeDivisor (K := K) f) ≤
        MvPolynomial.totalDegree f := by
  let : IsDomain (CoordinateRing f) :=
    coordinateRing_isDomain hirr
  let : Algebra (ProjectionBase K)
      (FractionRing (CoordinateRing f)) :=
    projectionFractionAlgebra f
  let Q := ProjectionFunctionField K
  let L := FractionRing (CoordinateRing f)
  have hinjective :
      Function.Injective
        (algebraMap (ProjectionBase K) L) := by
    change Function.Injective (projectionFractionAlgHom (K := K) f)
    exact projectionFractionAlgHom_injective hirr hmonic
  let : Algebra Q L :=
    functionFieldAlgebra f hirr hmonic
  let : IsScalarTower K Q L :=
    IsScalarTower.of_algebraMap_eq fun x => by
      rw [IsScalarTower.algebraMap_apply K (ProjectionBase K) Q x]
      change
        algebraMap K L x =
          IsFractionRing.lift hinjective
            (algebraMap (ProjectionBase K) Q
              (algebraMap K (ProjectionBase K) x))
      rw [IsFractionRing.lift_algebraMap]
      exact
        ((projectionFractionAlgHom (K := K) f).commutes x).symm
  intro hseparableQ
  let : Module.Finite Q L :=
    functionField_finiteDimensional f hirr hmonic
  let : Algebra.IsSeparable Q L :=
    hseparableQ
  let t : L :=
    projectionParameter (K := K) f
  have ht : Transcendental K t := by
    change Transcendental K
      (projectionFractionAlgHom (K := K) f
        (MvPolynomial.X (0 : Fin 1)))
    simpa only [Transcendental,
      isAlgebraic_algHom_iff
        (projectionFractionAlgHom (K := K) f)
        (projectionFractionAlgHom_injective hirr hmonic)] using
      (MvPolynomial.transcendental_X K (0 : Fin 1))
  have hX :
      algebraMap Q L
          (algebraMap (ProjectionBase K) Q
            (MvPolynomial.X (0 : Fin 1))) =
        t := by
    change
      IsFractionRing.lift hinjective
          (algebraMap (ProjectionBase K) Q
            (MvPolynomial.X (0 : Fin 1))) =
        algebraMap (ProjectionBase K) L
          (MvPolynomial.X (0 : Fin 1))
    exact IsFractionRing.lift_algebraMap hinjective _
  let E := FractionRing (InfinityModel (K := K) t)
  let : Algebra E L :=
    infinityFunctionFieldAlgebra (K := K) t
  let e : E ≃ₐ[K] Q :=
    infinityProjectionFieldEquiv ht
  have hcompat :
      (algebraMap Q L).comp e.toRingHom =
        algebraMap E L :=
    infinityProjectionFieldEquiv_compatible ht hX
  have hcompatSymm :
      (algebraMap E L).comp e.symm.toRingHom =
        algebraMap Q L := by
    apply RingHom.ext
    intro x
    have hx := DFunLike.congr_fun hcompat (e.symm x)
    simpa using hx.symm
  have hfiniteE : Module.Finite E L :=
    Module.Finite.of_equiv_equiv
      e.symm.toRingEquiv (RingEquiv.refl L) hcompatSymm
  have hseparableE : Algebra.IsSeparable E L :=
    Algebra.IsSeparable.of_equiv_equiv
      e.symm.toRingEquiv (RingEquiv.refl L) hcompatSymm
  have hcard :
      Nat.card (NonfiniteCoordinatePrimeDivisor (K := K) f) ≤
        Module.finrank E L :=
    card_nonfiniteCoordinatePrimeDivisor_le_finrank_of_isSeparable
      hirr hmonic hfiniteE hseparableE
  have hfinrank :
      Module.finrank E L = Module.finrank Q L :=
    Algebra.finrank_eq_of_equiv_equiv
      e.toRingEquiv (RingEquiv.refl L) hcompat
  exact
    hcard.trans <|
      hfinrank.le.trans <|
        functionField_finrank_le_totalDegree f hirr hmonic
theorem

card_nonfiniteCoordinatePrimeDivisor_le_totalDegree_of_monicRepresentative

L1089 ↗
FieldArithmetic.Chapter06.PrimeDivisorsAtInfinity.card_nonfiniteCoordinatePrimeDivisor_le_totalDegree_of_monicRepresentative
Documentation

Transported separable-projection form of Fried--Jarden 6.2.2(d).

The original irreducible equation need not itself be monic in Y. A chosen linear change and normalization produce a monic representative; the coordinate-ring equivalence transports its nonfinite prime divisors back to the original equation, while total degree is preserved.

Source context 10 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeDivisorsAtInfinity
open IsLocalRing
open FunctionFieldPrimeDivisor
open AffinePlaneCurve MonicPlaneCurveProjection PlaneCurveMonicNormalization
open scoped IntermediateField.algebraAdjoinAdjoin
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem
    card_nonfiniteCoordinatePrimeDivisor_le_totalDegree_of_monicRepresentative
    {f : BivariatePolynomial K} (hirr : Irreducible f)
    (c : Fin 1 → K)
    (h : IsUnit
      (yPolynomial (linearChangeY c f)).leadingCoeff)
    (hseparable :
      CenteredPrimeDivisorBound.MonicRepresentativeProjectionSeparable
        hirr c h) :
    letI : IsDomain (CoordinateRing f) :=
      coordinateRing_isDomain hirr
    Nat.card (NonfiniteCoordinatePrimeDivisor (K := K) f) ≤
      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
      [CenteredPrimeDivisorBound.MonicRepresentativeProjectionSeparable,
        g]
      using hseparable
  let e : CoordinateRing f ≃ₐ[K] CoordinateRing g :=
    coordinateRingEquivMonicRepresentative f c h
  calc
    Nat.card (NonfiniteCoordinatePrimeDivisor (K := K) f) =
        Nat.card (NonfiniteCoordinatePrimeDivisor (K := K) g) :=
      Nat.card_congr
        (NonfiniteCoordinatePrimeDivisor.equivCoordinateRingEquiv
          (K := K) e)
    _ ≤ MvPolynomial.totalDegree g :=
      card_nonfiniteCoordinatePrimeDivisor_le_totalDegree_of_isSeparable
        hg hmonic hseparable'
    _ = MvPolynomial.totalDegree f :=
      totalDegree_monicRepresentative hirr.ne_zero c h

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