CompletedChangedUniformizerPrimitive.lean

def padicChangedCompletedPrimitivePolynomialInteger
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Polynomial
      (padicCompletedUnramifiedCompleteDVF p).valuationSubring

def padicChangedCompletedPrimitivePolynomial
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Polynomial (padicCompletedUnramifiedField p)

theorem padicChangedCompletedPrimitivePolynomialInteger_map
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicChangedCompletedPrimitivePolynomialInteger p u n).map
        (algebraMap
          (padicCompletedUnramifiedCompleteDVF p).valuationSubring
          (padicCompletedUnramifiedField p)) =
      padicChangedCompletedPrimitivePolynomial p u n

theorem padicChangedCompletedPrimitivePolynomialInteger_monic
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicChangedCompletedPrimitivePolynomialInteger p u n).Monic

theorem padicChangedCompletedPrimitivePolynomial_monic
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicChangedCompletedPrimitivePolynomial p u n).Monic

theorem padicChangedCompletedPrimitivePolynomialInteger_natDegree
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicChangedCompletedPrimitivePolynomialInteger p u n).natDegree =
      (p - 1) * p ^ n

theorem padicChangedCompletedPrimitivePolynomial_natDegree
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicChangedCompletedPrimitivePolynomial p u n).natDegree =
      (p - 1) * p ^ n

theorem padicChangedCompletedUniformizer_isUniformizer
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    let π :=
      padicIntEquivValuationSubring p (p : ℤ_[p])
    let πu :=
      standardLubinTateChangedUniformizer
        (padicLocalField p) π u
    (padicCompletedUnramifiedCompleteDVF p).valuation.IsUniformizer
      ((padicCompletedUnramifiedIntegerMap p πu :
        (padicCompletedUnramifiedCompleteDVF p).valuationSubring) :
          padicCompletedUnramifiedField p) := by
  let target := padicCompletedUnramifiedCompleteDVF p
  let π := padicIntEquivValuationSubring p (p : ℤ_[p])
  let πu :=
    standardLubinTateChangedUniformizer
      (padicLocalField p) π u
  let πE : target.valuationSubring :=
    padicCompletedUnramifiedIntegerMap p π
  let uE : target.valuationSubring :=
    padicCompletedUnramifiedIntegerMap p
      (u : (padicLocalField p).valuationSubring)
  have hπ :
      target.valuation.IsUniformizer
        (πE : padicCompletedUnramifiedField p) := by
    simpa only [target, π, πE] using
      padicCompletedUnramifiedIntegerMap_isUniformizer p
  have huE : IsUnit uE :=
    u.isUnit.map (padicCompletedUnramifiedIntegerMap p)
  apply hπ.of_associated
  have hmul : padicCompletedUnramifiedIntegerMap p πu = uE * πE :=
    map_mul (padicCompletedUnramifiedIntegerMap p)
      (u : (padicLocalField p).valuationSubring) π
  exact hmul.symm ▸ (associated_unit_mul_right πE uE huE)

theorem
    padicChangedCompletedPrimitivePolynomialInteger_isWeaklyEisensteinAt
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicChangedCompletedPrimitivePolynomialInteger p u n).IsWeaklyEisensteinAt
      (padicCompletedUnramifiedCompleteDVF p).maximalIdeal

theorem padicChangedCompletedPrimitivePolynomialInteger_isEisensteinAt
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicChangedCompletedPrimitivePolynomialInteger p u n).IsEisensteinAt
      (padicCompletedUnramifiedCompleteDVF p).maximalIdeal

theorem padicChangedCompletedPrimitivePolynomialInteger_irreducible
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Irreducible
      (padicChangedCompletedPrimitivePolynomialInteger p u n)

theorem padicChangedCompletedPrimitivePolynomial_irreducible
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Irreducible (padicChangedCompletedPrimitivePolynomial p u n)

theorem padicChangedUniformizerThetaValue_isRoot_completedPrimitivePolynomial
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    ((padicChangedCompletedPrimitivePolynomial p u n).map
      (algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n))).IsRoot
      ((padicChangedUniformizerThetaValue p u n :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n)

theorem padicChangedUniformizerThetaValue_isIntegral_completedBase
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IsIntegral (padicCompletedUnramifiedField p)
      ((padicChangedUniformizerThetaValue p u n :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n)

theorem padicChangedUniformizerThetaValue_minpoly_completedBase
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    minpoly (padicCompletedUnramifiedField p)
        ((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n) =
      padicChangedCompletedPrimitivePolynomial p u n

theorem padicChangedUniformizerThetaValue_adjoin_completedBase_eq_top
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IntermediateField.adjoin
        (padicCompletedUnramifiedField p)
        ({((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n)} :
          Set (padicCompletedLevelField p n)) =
      ⊤

def padicChangedUniformizerThetaPowerBasis
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    PowerBasis (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)

theorem padicChangedUniformizerThetaPowerBasis_gen
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    (padicChangedUniformizerThetaPowerBasis p u n).gen =
      ((padicChangedUniformizerThetaValue p u n :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n)