Module

LaurentNormalizationRamification.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.LaurentNormalizationRamification

4 declarations indexed from sourceView source ↗

Module documentation

Ramification outside the two missing points of the Laurent chart

We use the actual Laurent evaluation into the rational function field. Its fraction-field property follows from localization of the polynomial ring, and its image is regular at every place except zero and infinity. Thus an etale normalization of this chart has ramification index one at every other place. No ramification comparison is assumed.

Imports5

Nyll.AnabelianGeometry.GeometricFundamentalGroup.AffineNormalizationRamification
Nyll.AlgebraicCurves.Models.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
Mathlib.Algebra.Polynomial.Laurent
Mathlib.RingTheory.Localization.LocalizationLocalization
Mathlib.RingTheory.DedekindDomain.Dvr

Imported by3

abbrev

laurentRatFuncAlgebra

L36 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentRatFuncAlgebra

Documentation

The actual Laurent evaluation, retaining its algebra dictionary as a single value.

Source context 8 commands

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

noncomputable section
open AlgebraicCurve
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
open AlgebraicCurves.Models.Proofs
open CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open AlgebraicCurve.S1c
universe u

Lean source · statement

abbrev laurentRatFuncAlgebra (K : Type u) [Field K] :
    Algebra (LaurentPolynomial K) (RatFunc K)

theorem

laurentPolynomial_isDedekindDomain

L40 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentPolynomial_isDedekindDomain

Documentation

The Laurent polynomial ring over a field is Dedekind, by its actual localization at X.

Source context 8 commands

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

noncomputable section
open AlgebraicCurve
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
open AlgebraicCurves.Models.Proofs
open CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open AlgebraicCurve.S1c
universe u

Lean source · statement

theorem laurentPolynomial_isDedekindDomain (K : Type u) [Field K] :
    IsDedekindDomain (LaurentPolynomial K)

theorem

laurentRatFunc_isFractionRing

L48 ↗

AnabelianGeometry.GeometricFundamentalGroup.laurentRatFunc_isFractionRing

Documentation

The rational function field is the fraction field of the Laurent evaluation algebra.

Source context 8 commands

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

noncomputable section
open AlgebraicCurve
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
open AlgebraicCurves.Models.Proofs
open CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open AlgebraicCurve.S1c
universe u

Lean source · full declaration

theorem laurentRatFunc_isFractionRing (K : Type u) [Field K] :
    let : Algebra (LaurentPolynomial K) (RatFunc K) := laurentRatFuncAlgebra K
    IsFractionRing (LaurentPolynomial K) (RatFunc K) := by
  intro rationalAlgebra
  have polynomialTower : IsScalarTower K[X] (LaurentPolynomial K) (RatFunc K) :=
    IsScalarTower.of_algebraMap_eq fun p => by
      change algebraMap K[X] (RatFunc K) p = ι K (Polynomial.toLaurent p)
      exact (ι_toLaurent K p).symm
  exact IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
    (Submonoid.powers (Polynomial.X : K[X])) (LaurentPolynomial K) (RatFunc K)

theorem

ramificationIndex_eq_one_of_etale_laurent_normalization

L62 ↗

AnabelianGeometry.GeometricFundamentalGroup.ramificationIndex_eq_one_of_etale_laurent_normalization

Documentation

An etale normalization of the actual Laurent chart is unramified outside zero and infinity. The evaluation algebra in the statement is shared by the proof.

Source context 9 commands

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

noncomputable section
open AlgebraicCurve
open scoped Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
open AlgebraicCurves.Models.Proofs
open CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open AlgebraicCurve.S1c
universe u
open Classical in

Lean source · full declaration

theorem ramificationIndex_eq_one_of_etale_laurent_normalization
    {K E : Type u} [Field K] [Field E] [Algebra K E] [Algebra (RatFunc K) E]
    [Algebra (LaurentPolynomial K) E]
    [IsScalarTower K (RatFunc K) E] [FiniteDimensional (RatFunc K) E]
    [Algebra.IsSeparable (RatFunc K) E] :
    let : Algebra (LaurentPolynomial K) (RatFunc K) := laurentRatFuncAlgebra K
    IsScalarTower (LaurentPolynomial K) (RatFunc K) E →
      Algebra.Etale (LaurentPolynomial K) (integralClosure (LaurentPolynomial K) E) →
      ∀ w : Place K E, w.restrict (RatFunc K) ≠ RationalFunctionField.placeInfty K →
        w.restrict (RatFunc K) ≠ RationalFunctionField.placeOfPoint K 0 →
        w.ramificationIndex (RatFunc K) = 1 := by
  intro rationalAlgebra extensionTower hEtale w hInfty hZero
  classical
  have fractionField : IsFractionRing (LaurentPolynomial K) (RatFunc K) :=
    laurentRatFunc_isFractionRing K
  have dedekind : IsDedekindDomain (LaurentPolynomial K) := laurentPolynomial_isDedekindDomain K
  apply ramificationIndex_eq_one_of_etale_affine_normalization hEtale w
  intro f
  have hmem : ι K f ∈ (ι K).range := ⟨f, rfl⟩
  rw [← iInf_ne_ne_eq K] at hmem
  exact (Subring.mem_iInf.mp (Subring.mem_iInf.mp
    (Subring.mem_iInf.mp hmem (w.restrict (RatFunc K))) hInfty)) hZero

Module documentation

Ramification outside the two missing points of the Laurent chart

Declarations

laurentRatFuncAlgebra

laurentPolynomial_isDedekindDomain

laurentRatFunc_isFractionRing

ramificationIndex_eq_one_of_etale_laurent_normalization