Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.FiniteExtensionCanonicalPlacewiseScaling

Canonical derivation scalings at finite extension places #

This file instantiates the abstract different-annihilator construction for a finite separable extension of K(X). If the Frobenius-constant derivation is normalized by D(X) = 1, the resulting scalar has order equal to the finite coefficient of the canonical different divisor. The quotient-rule bridge then shows that the scaled derivation preserves the complete localized DVR used by the finite-place Wronskian estimates.

source
@[instance_reducible]
noncomputable def BGS.CorvajaZannier.canonicalScalingPolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the finite extension canonical placewise scaling construction.

Equations
Instances For
    source
    theorem BGS.CorvajaZannier.canonicalScalingPolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    IsScalarTower (Polynomial K) (RatFunc K) L
    source
    theorem BGS.CorvajaZannier.canonicalScalingFiniteIntegralClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
    Module.Finite (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.canonicalScalingFiniteIntegralClosureIsIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    Algebra.IsIntegral (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.canonicalScalingPolynomialTorsionFreeTop (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
    Module.IsTorsionFree (Polynomial K) L
    source
    theorem BGS.CorvajaZannier.canonicalScalingFiniteIntegralClosureIsTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
    Module.IsTorsionFree (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.canonicalScalingFiniteBaseFaithfulSmulFractionRing (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    FaithfulSMul (Polynomial K) (FractionRing ↥(RatFuncFiniteIntegralClosure K L))
    source
    @[instance_reducible]
    noncomputable def BGS.CorvajaZannier.canonicalScalingFiniteFractionRingAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    Algebra (FractionRing (Polynomial K)) (FractionRing ↥(RatFuncFiniteIntegralClosure K L))

    The algebra structure from (FractionRing K[X]) to (FractionRing (RatFuncFiniteIntegralClosure K L)) used in the finite extension canonical placewise scaling construction.

    Equations
    Instances For
      source
      theorem BGS.CorvajaZannier.canonicalScalingFiniteFractionRingSeparable (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
      Algebra.IsSeparable (FractionRing (Polynomial K)) (FractionRing ↥(RatFuncFiniteIntegralClosure K L))
      source
      theorem BGS.CorvajaZannier.exists_finiteExtensionFinitePlace_canonicalDifferent_scaling_certificate (K : Type u_1) [Field K] [PerfectField K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] (D : Derivation (↥(frobeniusSubfield L p)) L L) (hDX : D ((algebraMap (RatFunc K) L) RatFunc.X) = 1) (q : FiniteExtensionFinitePlace K L) :
      ∃ (c : L), c ≠ 0 ∧ finitePlaceOrder q c = (finiteExtensionCanonicalDifferentDivisor K L ⋯) (Sum.inl q) ∧ ∀ (r : FiniteExtensionFinitePlaceLocalRing K L q), ∃ (s : FiniteExtensionFinitePlaceLocalRing K L q), (c • D) ((finiteExtensionFinitePlaceLocalizationToField q) r) = (finiteExtensionFinitePlaceLocalizationToField q) s

      At every finite place, the normalized Frobenius-constant derivation admits a scalar whose order is the canonical different coefficient and whose scalar multiple preserves the localized DVR.