FiniteLevelPrimitiveRoot.lean

theorem padicMultiplicativeScalarEndomorphism_nat
    (p : ℕ) [Fact p.Prime] (m : ℕ) :
    recursiveIntertwiner
        (padicMultiplicativeLubinTateSeries_isUniformizer p)
        (padicMultiplicativeLubinTateSeries p)
        (padicMultiplicativeLubinTateSeries p)
        (fun _ : Unit =>
          (m : (padicLocalField p).valuationSubring)) =
      (1 + PowerSeries.X) ^ m - 1 := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let A :
      PowerSeries (padicLocalField p).valuationSubring :=
    (1 + PowerSeries.X) ^ m - 1
  let Eps :
      PowerSeries (padicLocalField p).valuationSubring :=
    (padicMultiplicativeLubinTateSeries p).toPowerSeries
  have hEps :
      Eps =
        PowerSeries.binomialSeries
            (padicLocalField p).valuationSubring (p : ℤ) -
          1 :=
    rfl
  have hAconstant : PowerSeries.constantCoeff A = 0 := by
    simp [A]
  have hAcoeffOne :
      PowerSeries.coeff 1 A =
        (m : (padicLocalField p).valuationSubring) := by
    dsimp only [A]
    simp only [map_sub, PowerSeries.coeff_one]
    rw [PowerSeries.coeff_one_pow]
    simp
  have hAlinear :
      HasLinearTerm A
        (fun _ : Unit =>
          (m : (padicLocalField p).valuationSubring)) := by
    rw [HasLinearTerm]
    apply MvPowerSeries.nat_le_order
    intro d hd
    have hdNat : d.degree < 2 := by
      exact_mod_cast hd
    have hdegree : d.degree = d () := by
      simp [Finsupp.degree_eq_sum]
    have hd' : d () < 2 := by omega
    by_cases hd0 : d () = 0
    · have hdeq : d = 0 := by
        apply Finsupp.ext
        intro i
        cases i
        simp [hd0]
      subst d
      change
        PowerSeries.constantCoeff A -
            MvPowerSeries.constantCoeff
              (linearForm
                (fun _ : Unit =>
                  (m : (padicLocalField p).valuationSubring))) =
          0
      rw [hAconstant, constantCoeff_linearForm, sub_self]
    · have hd1 : d () = 1 := by omega
      have hdeq : d = Finsupp.single () 1 := by
        apply Finsupp.ext
        intro i
        cases i
        simp [hd1]
      subst d
      have hlinearForm :
          linearForm
              (fun _ : Unit =>
                (m : (padicLocalField p).valuationSubring)) =
            MvPowerSeries.C
                (m : (padicLocalField p).valuationSubring) *
              MvPowerSeries.X () := by
        simp [linearForm]
      change
        PowerSeries.coeff 1 A -
            MvPowerSeries.coeff (Finsupp.single () 1)
              (linearForm
                (fun _ : Unit =>
                  (m : (padicLocalField p).valuationSubring))) =
          0
      classical
      rw [hAcoeffOne, hlinearForm, MvPowerSeries.coeff_C_mul,
        MvPowerSeries.coeff_index_single_self_X, mul_one, sub_self]
  have hAsubst : PowerSeries.HasSubst A :=
    hAlinear.hasSubst
  have hEsubst :
      PowerSeries.HasSubst Eps := by
    apply PowerSeries.HasSubst.of_constantCoeff_zero
    exact (padicMultiplicativeLubinTateSeries p).constantCoeff_eq_zero
  have hAsubstOne :
      PowerSeries.subst A
          (1 : PowerSeries (padicLocalField p).valuationSubring) =
        1 := by
    change
      PowerSeries.subst A
          (PowerSeries.C
            (1 : (padicLocalField p).valuationSubring)) =
        1
    rw [PowerSeries.subst_C]
    rfl
  have hEsubstOne :
      PowerSeries.subst Eps
          (1 : PowerSeries (padicLocalField p).valuationSubring) =
        1 := by
    change
      PowerSeries.subst Eps
          (PowerSeries.C
            (1 : (padicLocalField p).valuationSubring)) =
        1
    rw [PowerSeries.subst_C]
    rfl
  have hAone :
      1 + A = (1 + PowerSeries.X) ^ m := by
    dsimp only [A]
    ring
  have hEone :
      1 + Eps =
        (1 + PowerSeries.X) ^ p := by
    rw [hEps, PowerSeries.binomialSeries_nat (R := ℤ)]
    ring
  have hcommutes :
      PowerSeries.subst A Eps =
        PowerSeries.subst Eps A := by
    calc
      PowerSeries.subst A Eps =
          (1 + A) ^ p - 1 := by
        rw [hEps, PowerSeries.binomialSeries_nat (R := ℤ),
          PowerSeries.subst_sub hAsubst,
          PowerSeries.subst_pow hAsubst,
          PowerSeries.subst_add hAsubst,
          PowerSeries.subst_X hAsubst, hAsubstOne]
      _ = ((1 + PowerSeries.X) ^ m) ^ p - 1 := by
        rw [hAone]
      _ = (1 + PowerSeries.X) ^ (m * p) - 1 := by
        rw [← pow_mul]
      _ = (1 + PowerSeries.X) ^ (p * m) - 1 := by
        rw [mul_comm m p]
      _ = ((1 + PowerSeries.X) ^ p) ^ m - 1 := by
        rw [pow_mul]
      _ =
          (1 + Eps) ^ m - 1 := by
        rw [hEone]
      _ =
          PowerSeries.subst Eps
            ((1 +
              (PowerSeries.X :
                PowerSeries (padicLocalField p).valuationSubring)) ^ m -
              1) := by
        symm
        rw [PowerSeries.subst_sub hEsubst,
          PowerSeries.subst_pow hEsubst,
          PowerSeries.subst_add hEsubst,
          PowerSeries.subst_X hEsubst, hEsubstOne]
      _ =
          PowerSeries.subst Eps A :=
        rfl
  have hAintertwines :
      Intertwines
        (padicMultiplicativeLubinTateSeries p)
        (padicMultiplicativeLubinTateSeries p) A := by
    change
      PowerSeries.subst A Eps =
        MvPowerSeries.subst
          (fun i : Unit =>
            inVariable (padicMultiplicativeLubinTateSeries p) i) A
    calc
      PowerSeries.subst A Eps =
          PowerSeries.subst Eps A :=
        hcommutes
      _ =
          MvPowerSeries.subst
            (fun i : Unit =>
              inVariable (padicMultiplicativeLubinTateSeries p) i) A := by
        symm
        rw [PowerSeries.subst_def]
        congr 1
        funext i
        cases i
        change
          PowerSeries.subst PowerSeries.X Eps = Eps
        exact PowerSeries.X_subst Eps
  exact
    eq_of_hasLinearTerm_of_intertwines hπ
      (padicMultiplicativeLubinTateSeries p)
      (padicMultiplicativeLubinTateSeries p)
      (fun _ : Unit =>
        (m : (padicLocalField p).valuationSubring))
      (recursiveIntertwiner_hasLinearTerm hπ
        (padicMultiplicativeLubinTateSeries p)
        (padicMultiplicativeLubinTateSeries p)
        (fun _ : Unit =>
          (m : (padicLocalField p).valuationSubring)))
      (recursiveIntertwiner_intertwines hπ
        (padicMultiplicativeLubinTateSeries p)
        (padicMultiplicativeLubinTateSeries p)
        (fun _ : Unit =>
          (m : (padicLocalField p).valuationSubring)))
      hAlinear hAintertwines

theorem
    padicValuationSubring_sub_toZModPow_val_mem_maximalIdeal_pow
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : (padicLocalField p).valuationSubring) :
    let z :=
      (padicIntEquivValuationSubring p).symm
        a
    let m := (PadicInt.toZModPow (p := p) (n + 1) z).val
    a - (m : (padicLocalField p).valuationSubring) ∈
      (padicLocalField p).toCompleteDVF.maximalIdeal ^ (n + 1) := by
  change (padicDVRValuation p).valuationSubring at a
  let e := padicIntEquivValuationSubring p
  let z : ℤ_[p] :=
    e.symm a
  let m := (PadicInt.toZModPow (p := p) (n + 1) z).val
  have hz :
      z - (m : ℤ_[p]) ∈
        Ideal.span ({(p : ℤ_[p]) ^ (n + 1)} : Set ℤ_[p]) := by
    rw [← PadicInt.ker_toZModPow, RingHom.mem_ker]
    rw [map_sub, map_natCast]
    dsimp only [m]
    rw [ZMod.natCast_zmod_val, sub_self]
  have hzmax :
      z - (m : ℤ_[p]) ∈
        IsLocalRing.maximalIdeal ℤ_[p] ^ (n + 1) := by
    rw [PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow]
    exact hz
  have hmapped :
      e (z - (m : ℤ_[p])) ∈
        IsLocalRing.maximalIdeal
            (padicDVRValuation p).valuationSubring ^ (n + 1) :=
    (ValuationTheory.ringEquiv_mem_maximalIdeal_pow_iff
      e (n + 1) (z - (m : ℤ_[p]))).2 hzmax
  change
    a - (m : (padicDVRValuation p).valuationSubring) ∈
      IsLocalRing.maximalIdeal
          (padicDVRValuation p).valuationSubring ^ (n + 1)
  simpa only [map_sub, map_natCast, e, z, m,
    RingEquiv.apply_symm_apply] using hmapped

theorem
    padicStandardPrimitivePointIntegerAction_eq_toZModPow_val
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let m :=
      (PadicInt.toZModPow (p := p) (n + 1)
        ((padicIntEquivValuationSubring p).symm
          (u : (padicLocalField p).valuationSubring))).val
    standardLubinTatePrimitivePointIntegerAction
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n u =
      standardLubinTateEndomorphismValue
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (m : (padicLocalField p).valuationSubring) := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let m :=
    (PadicInt.toZModPow (p := p) (n + 1)
      ((padicIntEquivValuationSubring p).symm
        (u : (padicLocalField p).valuationSubring))).val
  let d : (padicLocalField p).valuationSubring :=
    (u : (padicLocalField p).valuationSubring) - m
  have hd :
      d ∈ (padicLocalField p).toCompleteDVF.maximalIdeal ^ (n + 1) := by
    simpa only [d, m] using
      padicValuationSubring_sub_toZModPow_val_mem_maximalIdeal_pow p n
        (u : (padicLocalField p).valuationSubring)
  have hdzero :
      standardLubinTateEndomorphismValue hπ n d = 0 :=
    (standardLubinTateEndomorphismValue_eq_zero_iff_mem_maximalIdeal_pow
      hπ n d).2 hd
  change
    standardLubinTateEndomorphismValue hπ n
        (u : (padicLocalField p).valuationSubring) =
      standardLubinTateEndomorphismValue hπ n
        (m : (padicLocalField p).valuationSubring)
  calc
    standardLubinTateEndomorphismValue hπ n
        (u : (padicLocalField p).valuationSubring) =
        standardLubinTateEndomorphismValue hπ n
          ((m : (padicLocalField p).valuationSubring) + d) := by
      congr 1
      dsimp only [d]
      ring
    _ =
        standardLubinTateFormalAdd hπ n
          (standardLubinTateEndomorphismValue hπ n
            (m : (padicLocalField p).valuationSubring))
          (standardLubinTateEndomorphismValue hπ n d) :=
      standardLubinTateEndomorphismValue_add hπ n m d
    _ =
        standardLubinTateFormalAdd hπ n
          (standardLubinTateEndomorphismValue hπ n
            (m : (padicLocalField p).valuationSubring))
          (standardLubinTateEndomorphismValue hπ n 0) := by
      exact congrArg
        (standardLubinTateFormalAdd hπ n
          (standardLubinTateEndomorphismValue hπ n
            (m : (padicLocalField p).valuationSubring)))
        (hdzero.trans (standardLubinTateEndomorphismValue_zero hπ n).symm)
    _ =
        standardLubinTateEndomorphismValue hπ n
          ((m : (padicLocalField p).valuationSubring) + 0) :=
      (standardLubinTateEndomorphismValue_add hπ n m 0).symm
    _ =
        standardLubinTateEndomorphismValue hπ n
          (m : (padicLocalField p).valuationSubring) := by
      rw [add_zero]

theorem padicStandardLubinTateSeries_eval_iterate
    (p : ℕ) [Fact p.Prime] (n i : ℕ) :
    standardLubinTateLevelPowerSeriesEval
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (standardLubinTatePrimitivePointIterateInteger
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n i)
        (standardLubinTatePrimitivePointIterateInteger_hasEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n i)
        (standardLubinTateSeries
          (padicMultiplicativeLubinTateSeries_isUniformizer p)).toPowerSeries =
      standardLubinTatePrimitivePointIterateInteger
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n (i + 1)

theorem
    padicStandardLubinTatePrimitivePointIterateInteger_ne_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    standardLubinTatePrimitivePointIterateInteger
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n n ≠
      0

theorem padicMultiplicativePrimitivePoint_pow_primePower
    (p : ℕ) [Fact p.Prime] (n i : ℕ) :
    (1 + padicMultiplicativePrimitivePoint p n) ^ (p ^ i) =
      1 +
        standardLubinTateLevelPowerSeriesEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n
          (standardLubinTatePrimitivePointIterateInteger
            (padicMultiplicativeLubinTateSeries_isUniformizer p) n i)
          (standardLubinTatePrimitivePointIterateInteger_hasEval
            (padicMultiplicativeLubinTateSeries_isUniformizer p) n i)
          (padicStandardToMultiplicativeIntertwiner p)

def padicMultiplicativePrimitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    standardLubinTateLevelField
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n

theorem padicMultiplicativePrimitiveRoot_unitAction
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    1 +
        (standardLubinTateLevelPowerSeriesEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n
          (standardLubinTatePrimitivePointIntegerAction
            (padicMultiplicativeLubinTateSeries_isUniformizer p) n u)
          (standardLubinTatePrimitivePointIntegerAction_hasEval
            (padicMultiplicativeLubinTateSeries_isUniformizer p) n u)
          (padicStandardToMultiplicativeIntertwiner p)).val =
      padicMultiplicativePrimitiveRoot p n ^
        (PadicInt.toZModPow (p := p) (n + 1)
          ((padicIntEquivValuationSubring p).symm
            (u : (padicLocalField p).valuationSubring))).val

theorem padicMultiplicativeLevelAlgEquiv_mem_valuationSubring_iff
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (σ : Gal((standardLubinTateLevelField
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)/ℚ_[p]))
    (x : standardLubinTateLevelField
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n) :
    x ∈ (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuation.valuationSubring ↔
      σ x ∈ (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuation.valuationSubring

def
    padicMultiplicativeLevelAutomorphismIntegerRingEquiv
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (σ : Gal((standardLubinTateLevelField
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)/ℚ_[p])) :
    (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring ≃+*
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring

theorem
    padicMultiplicativeLevelAutomorphismIntegerRingEquiv_apply
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (σ : Gal((standardLubinTateLevelField
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)/ℚ_[p]))
    (x : (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring) :
    (padicMultiplicativeLevelAutomorphismIntegerRingEquiv p n σ x).val =
      σ x.val

theorem
    padicMultiplicativeLevelAutomorphismIntegerRingEquiv_continuous
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (σ : Gal((standardLubinTateLevelField
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)/ℚ_[p])) :
    Continuous (padicMultiplicativeLevelAutomorphismIntegerRingEquiv p n σ)

theorem
    padicMultiplicativeLevelAutomorphismIntegerRingEquiv_comp_coefficientHom
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (σ : Gal((standardLubinTateLevelField
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)/ℚ_[p])) :
    (padicMultiplicativeLevelAutomorphismIntegerRingEquiv p n σ :
        (standardLubinTateLevelCompleteDVF
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring →+*
        (standardLubinTateLevelCompleteDVF
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring).comp
      (standardLubinTateLevelCoefficientHom
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n) =
      standardLubinTateLevelCoefficientHom
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n

theorem
    padicMultiplicativeLevelAutomorphismIntegerRingEquiv_primitivePointEvaluation
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    padicMultiplicativeLevelAutomorphismIntegerRingEquiv p n
        ((standardLubinTateUnitParameterEquivGal
          (padicLocalField p)
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u))⁻¹)
        (padicMultiplicativePrimitivePoint p n) =
      standardLubinTateLevelPowerSeriesEval
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (standardLubinTatePrimitivePointIntegerAction
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n u⁻¹)
        (standardLubinTatePrimitivePointIntegerAction_hasEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n u⁻¹)
        (padicStandardToMultiplicativeIntertwiner p)

theorem padicMultiplicativePrimitiveRoot_galoisAction
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    (standardLubinTateUnitParameterEquivGal
        (padicLocalField p)
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (standardLubinTateUnitParameterClass
          (padicLocalField p) n u))⁻¹
        (padicMultiplicativePrimitiveRoot p n) =
      padicMultiplicativePrimitiveRoot p n ^
        (PadicInt.toZModPow (p := p) (n + 1)
          ((padicIntEquivValuationSubring p).symm
            ((u⁻¹ : (padicLocalField p).valuationSubringˣ) :
              (padicLocalField p).valuationSubring))).val

theorem padicMultiplicativePrimitiveRoot_unitParameterGaloisAction
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    standardLubinTateUnitParameterEquivGal
        (padicLocalField p)
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (standardLubinTateUnitParameterClass
          (padicLocalField p) n u)
        (padicMultiplicativePrimitiveRoot p n) =
      padicMultiplicativePrimitiveRoot p n ^
        (PadicInt.toZModPow (p := p) (n + 1)
          ((padicIntEquivValuationSubring p).symm
            ((u : (padicLocalField p).valuationSubringˣ) :
              (padicLocalField p).valuationSubring))).val

theorem padicMultiplicativePrimitiveRoot_isPrimitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsPrimitiveRoot (padicMultiplicativePrimitiveRoot p n) (p ^ (n + 1))