Core.lean

def padicChangedUniformizerThetaValue
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicCompletedLevelCompleteDVF p n).valuationSubring

theorem padicChangedUniformizerThetaValue_hasEval
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    PowerSeries.HasEval (padicChangedUniformizerThetaValue p u n)

def padicCompletedChangedStandardScalarEndomorphismValue
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a : (padicLocalField p).valuationSubring) :
    (padicCompletedLevelCompleteDVF p n).valuationSubring

theorem padicCompletedChangedStandardScalarEndomorphismValue_hasEval
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.HasEval
      (padicCompletedChangedStandardScalarEndomorphismValue
        p u n x hx a)

theorem padicCompletedChangedStandardScalarEndomorphismValue_mul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a b : (padicLocalField p).valuationSubring) :
    padicCompletedChangedStandardScalarEndomorphismValue
        p u n x hx (a * b) =
      padicCompletedChangedStandardScalarEndomorphismValue p u n
        (padicCompletedChangedStandardScalarEndomorphismValue
          p u n x hx b)
        (padicCompletedChangedStandardScalarEndomorphismValue_hasEval
          p u n x hx b) a

theorem padicCompletedChangedStandardScalarEndomorphismValue_one
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    padicCompletedChangedStandardScalarEndomorphismValue
        p u n x hx 1 =
      x

theorem
    padicCompletedChangedStandardScalarEndomorphismValue_uniformizer_pow
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) (r : ℕ) :
    padicCompletedChangedStandardScalarEndomorphismValue p u n x hx
        ((standardLubinTateChangedUniformizer
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) u) ^ r) =
      Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n) x
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (standardLubinTateChangedUniformizer
            (padicLocalField p)
            (padicIntEquivValuationSubring p (p : ℤ_[p])) u) r)

theorem padicChangedUniformizerIntertwiner_endomorphism_evaluation
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a : (padicLocalField p).valuationSubring) (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    padicCompletedLevelPowerSeriesEval p n
        (padicCompletedMultiplicativeScalarEndomorphismValue
          p n x hx a)
        (padicCompletedMultiplicativeScalarEndomorphismValue_hasEval
          p n x hx a)
        (padicChangedUniformizerIntertwiner p u) =
      padicCompletedChangedStandardScalarEndomorphismValue p u n
        (padicCompletedLevelPowerSeriesEval p n x hx
          (padicChangedUniformizerIntertwiner p u))
        (padicCompletedLevelPowerSeriesEval_hasEval p n x hx
          (padicChangedUniformizerIntertwiner p u)
          (padicChangedUniformizerIntertwiner_hasSubst p u))
        a

theorem padicChangedUniformizerIntertwiner_changedSeries_evaluation
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    padicCompletedLevelPowerSeriesEval p n
        (padicCompletedMultiplicativeScalarEndomorphismValue p n x hx
          (standardLubinTateChangedUniformizer
            (padicLocalField p)
            (padicIntEquivValuationSubring p (p : ℤ_[p])) u))
        (padicCompletedMultiplicativeScalarEndomorphismValue_hasEval
          p n x hx
          (standardLubinTateChangedUniformizer
            (padicLocalField p)
            (padicIntEquivValuationSubring p (p : ℤ_[p])) u))
        (padicChangedUniformizerIntertwiner p u) =
      padicCompletedLevelPowerSeriesEval p n
        (padicCompletedLevelPowerSeriesEval p n x hx
          (padicChangedUniformizerIntertwiner p u))
        (padicCompletedLevelPowerSeriesEval_hasEval p n x hx
          (padicChangedUniformizerIntertwiner p u)
          (padicChangedUniformizerIntertwiner_hasSubst p u))
        (padicCompletedChangedStandardSeries p u)

theorem padicChangedUniformizerIntertwiner_eval_injective
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    {x y : (padicCompletedLevelCompleteDVF p n).valuationSubring}
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy :
      padicCompletedLevelPowerSeriesEval p n x hx
          (padicChangedUniformizerIntertwiner p u) =
        padicCompletedLevelPowerSeriesEval p n y hy
          (padicChangedUniformizerIntertwiner p u)) :
    x = y

theorem padicChangedUniformizerIntertwiner_eval_zero
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedLevelPowerSeriesEval p n
        0 PowerSeries.HasEval.zero
        (padicChangedUniformizerIntertwiner p u) =
      0

theorem padicChangedUniformizerThetaValue_iterate_succ_eq_zero
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n)
        (padicChangedUniformizerThetaValue p u n)
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (standardLubinTateChangedUniformizer
            (padicLocalField p)
            (padicIntEquivValuationSubring p (p : ℤ_[p])) u)
          (n + 1)) =
      0

theorem padicChangedUniformizerThetaValue_iterate_ne_zero
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n)
        (padicChangedUniformizerThetaValue p u n)
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (standardLubinTateChangedUniformizer
            (padicLocalField p)
            (padicIntEquivValuationSubring p (p : ℤ_[p])) u) n) ≠
      0

theorem padicChangedUniformizerThetaValue_isRoot
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    ((standardLubinTatePrimitivePolynomial
        (padicLocalField p)
        (standardLubinTateChangedUniformizer
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) u) n).map
      (padicCompletedLevelPadicIntegerCoefficientHom p n)).IsRoot
        (padicChangedUniformizerThetaValue p u n)

theorem padicChangedUniformizerThetaValue_field_isRoot
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    ((standardLubinTatePrimitivePolynomialOverField
        (padicLocalField p)
        (standardLubinTateChangedUniformizer
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) u) n).map
      (algebraMap ℚ_[p] (padicCompletedLevelField p n))).IsRoot
        ((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n)

theorem padicChangedUniformizerThetaValue_aeval_levelMinpoly
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    let hπ :=
      standardLubinTateChangedUniformizer_isUniformizer
        (padicMultiplicativeLubinTateSeries_isUniformizer p) u
    Polynomial.aeval
        ((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n)
        (minpoly ℚ_[p] (standardLubinTateLevelPowerBasis hπ n).gen) =
      0 := by
  let hπ :=
    standardLubinTateChangedUniformizer_isUniformizer
      (padicMultiplicativeLubinTateSeries_isUniformizer p) u
  change
    Polynomial.aeval
        ((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n)
        (minpoly ℚ_[p] (standardLubinTateLevelPowerBasis hπ n).gen) =
      0
  rw [standardLubinTateLevelPowerBasis_minpoly hπ n,
    Polynomial.aeval_def]
  simpa only [Polynomial.IsRoot, Polynomial.eval_map] using
    padicChangedUniformizerThetaValue_field_isRoot p u n

def padicChangedUniformizerLevelEmbedding
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    let hπ :=
      standardLubinTateChangedUniformizer_isUniformizer
        (padicMultiplicativeLubinTateSeries_isUniformizer p) u
    standardLubinTateLevelField hπ n →ₐ[ℚ_[p]]
      padicCompletedLevelField p n := by
  let hπ :=
    standardLubinTateChangedUniformizer_isUniformizer
      (padicMultiplicativeLubinTateSeries_isUniformizer p) u
  let theta : padicCompletedLevelField p n :=
    ((padicChangedUniformizerThetaValue p u n :
      (padicCompletedLevelCompleteDVF p n).valuationSubring) :
        padicCompletedLevelField p n)
  change
    standardLubinTateLevelField hπ n →ₐ[ℚ_[p]]
      padicCompletedLevelField p n
  exact
    (standardLubinTateLevelPowerBasis hπ n).lift theta
      (by
        simpa only [theta] using
          padicChangedUniformizerThetaValue_aeval_levelMinpoly p u n)

theorem padicChangedUniformizerLevelEmbedding_apply_gen
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    let hπ :=
      standardLubinTateChangedUniformizer_isUniformizer
        (padicMultiplicativeLubinTateSeries_isUniformizer p) u
    padicChangedUniformizerLevelEmbedding p u n
        (standardLubinTateLevelPowerBasis hπ n).gen =
      ((padicChangedUniformizerThetaValue p u n :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n) := by
  let hπ :=
    standardLubinTateChangedUniformizer_isUniformizer
      (padicMultiplicativeLubinTateSeries_isUniformizer p) u
  let theta : padicCompletedLevelField p n :=
    ((padicChangedUniformizerThetaValue p u n :
      (padicCompletedLevelCompleteDVF p n).valuationSubring) :
        padicCompletedLevelField p n)
  change
    (standardLubinTateLevelPowerBasis hπ n).lift
        theta
        (padicChangedUniformizerThetaValue_aeval_levelMinpoly p u n)
        (standardLubinTateLevelPowerBasis hπ n).gen =
      theta
  exact
    (standardLubinTateLevelPowerBasis hπ n).lift_gen _ _

theorem padicChangedUniformizerIntertwiner_frobenius_evaluation
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    padicCompletedLevelPowerSeriesEval p n x hx
        (PowerSeries.map WittVector.frobenius
          (padicChangedUniformizerIntertwiner p u)) =
      padicCompletedLevelPowerSeriesEval p n
        (padicCompletedLevelPowerSeriesEval p n x hx
          (padicCompletedMultiplicativeUnitEndomorphism p u))
        (padicCompletedLevelPowerSeriesEval_hasEval p n x hx
          (padicCompletedMultiplicativeUnitEndomorphism p u)
          (padicCompletedMultiplicativeUnitEndomorphism_hasSubst p u))
        (padicChangedUniformizerIntertwiner p u)

theorem
    padicChangedUniformizerThetaValue_frobeniusCoefficients
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedLevelPowerSeriesEval p n
        (padicCompletedMultiplicativePrimitivePoint p n)
        (padicCompletedMultiplicativePrimitivePoint_hasEval p n)
        (PowerSeries.map WittVector.frobenius
          (padicChangedUniformizerIntertwiner p u)) =
      padicCompletedLevelPowerSeriesEval p n
        (padicCompletedMultiplicativePrimitivePointUnitAction p u n)
        (padicCompletedMultiplicativePrimitivePointUnitAction_hasEval p u n)
        (padicChangedUniformizerIntertwiner p u)