ChangedUniformizerCoefficient.lean

abbrev padicCompletedUnramifiedWittRing (p : ℕ) [Fact p.Prime]

def padicIntToCompletedUnramifiedWittRing
    (p : ℕ) [Fact p.Prime] :
    ℤ_[p] →+* padicCompletedUnramifiedWittRing p

theorem padicIntToCompletedUnramifiedWittRing_frobenius
    (p : ℕ) [Fact p.Prime] (z : ℤ_[p]) :
    WittVector.frobenius
        (padicIntToCompletedUnramifiedWittRing p z) =
      padicIntToCompletedUnramifiedWittRing p z

def padicValuationSubringToCompletedUnramifiedWittRing
    (p : ℕ) [Fact p.Prime] :
    (padicLocalField p).valuationSubring →+*
      padicCompletedUnramifiedWittRing p

theorem padicValuationSubringToCompletedUnramifiedWittRing_uniformizer
    (p : ℕ) [Fact p.Prime] :
    padicValuationSubringToCompletedUnramifiedWittRing p
        (padicIntEquivValuationSubring p (p : ℤ_[p])) =
      (p : padicCompletedUnramifiedWittRing p)

theorem padicValuationSubringToCompletedUnramifiedWittRing_frobenius
    (p : ℕ) [Fact p.Prime]
    (z : (padicLocalField p).valuationSubring) :
    WittVector.frobenius
        (padicValuationSubringToCompletedUnramifiedWittRing p z) =
      padicValuationSubringToCompletedUnramifiedWittRing p z

def padicValuationUnitToCompletedUnramifiedWittUnit
    (p : ℕ) [Fact p.Prime] :
    (padicLocalField p).valuationSubringˣ →*
      (padicCompletedUnramifiedWittRing p)ˣ

theorem completedUnramifiedWittUnit_coeff_zero_ne_zero
    (p : ℕ) [Fact p.Prime]
    (u : (padicCompletedUnramifiedWittRing p)ˣ) :
    ((u : padicCompletedUnramifiedWittRing p).coeff 0) ≠ 0

theorem padicChangedUniformizerRotation_coeff_zero_ne_zero
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    (WittVector.frobeniusRotation p
      (show
        ((1 : padicCompletedUnramifiedWittRing p).coeff 0) ≠ 0 by
        simp)
      (completedUnramifiedWittUnit_coeff_zero_ne_zero p
        (padicValuationUnitToCompletedUnramifiedWittUnit p u))).coeff 0 ≠ 0 := by
  simpa only [WittVector.frobeniusRotation,
    WittVector.coeff_mk, WittVector.frobeniusRotationCoeff] using
    (WittVector.RecursionBase.solution_nonzero p
      (show
        ((1 : padicCompletedUnramifiedWittRing p).coeff 0) ≠ 0 by
        simp)
      (completedUnramifiedWittUnit_coeff_zero_ne_zero p
        (padicValuationUnitToCompletedUnramifiedWittUnit p u)))

def padicChangedUniformizerLinearCoefficient
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    (padicCompletedUnramifiedWittRing p)ˣ

theorem padicChangedUniformizerLinearCoefficient_coe
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    (padicChangedUniformizerLinearCoefficient p u :
        padicCompletedUnramifiedWittRing p) =
      WittVector.frobeniusRotation p
        (show
          ((1 : padicCompletedUnramifiedWittRing p).coeff 0) ≠ 0 by
          simp)
        (completedUnramifiedWittUnit_coeff_zero_ne_zero p
          (padicValuationUnitToCompletedUnramifiedWittUnit p u)) :=
  Classical.choose_spec
    (WittVector.isUnit_of_coeff_zero_ne_zero
      (WittVector.frobeniusRotation p
        (show
          ((1 : padicCompletedUnramifiedWittRing p).coeff 0) ≠ 0 by
          simp)
        (completedUnramifiedWittUnit_coeff_zero_ne_zero p
          (padicValuationUnitToCompletedUnramifiedWittUnit p u)))
      (padicChangedUniformizerRotation_coeff_zero_ne_zero p u))

theorem padicChangedUniformizerLinearCoefficient_frobenius
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    WittVector.frobenius
        (padicChangedUniformizerLinearCoefficient p u :
          padicCompletedUnramifiedWittRing p) =
      (padicChangedUniformizerLinearCoefficient p u :
          padicCompletedUnramifiedWittRing p) *
        (padicValuationUnitToCompletedUnramifiedWittUnit p u :
          padicCompletedUnramifiedWittRing p)

def padicChangedUniformizerCoefficientOperator
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (m : ℕ) :
    padicCompletedUnramifiedWittRing p →+
      padicCompletedUnramifiedWittRing p where
  toFun a :=
    (↑((padicValuationUnitToCompletedUnramifiedWittUnit p u)⁻¹) :
        padicCompletedUnramifiedWittRing p) *
      (p : padicCompletedUnramifiedWittRing p) ^ (m - 1) *
      WittVector.frobenius a
  map_zero' := by simp
  map_add' a b := by
    simp only [map_add, mul_add]

theorem padicChangedUniformizerCoefficientOperator_maps_pow_succ
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (m : ℕ) (hm : 2 ≤ m) :
    let I : Ideal (padicCompletedUnramifiedWittRing p) :=
      Ideal.span ({(p : padicCompletedUnramifiedWittRing p)} : Set _)
    ∀ (n : ℕ) {x : padicCompletedUnramifiedWittRing p},
      x ∈ I ^ n →
        padicChangedUniformizerCoefficientOperator p u m x ∈
          I ^ (n + 1) := by
  dsimp only
  let W := padicCompletedUnramifiedWittRing p
  let I : Ideal W := Ideal.span ({(p : W)} : Set W)
  let φ : W →+* W := WittVector.frobenius
  have hφI : I.map φ = I := by
    dsimp only [I]
    rw [Ideal.map_span, Set.image_singleton]
    dsimp only [φ]
    rw [map_natCast]
  have hpI : (p : W) ∈ I :=
    Ideal.subset_span (Set.mem_singleton (p : W))
  have hmPos : 0 < m - 1 := by omega
  have hpPowI : (p : W) ^ (m - 1) ∈ I :=
    I.pow_mem_of_mem hpI (m - 1) hmPos
  have hcI :
      (↑((padicValuationUnitToCompletedUnramifiedWittUnit p u)⁻¹) : W) *
          (p : W) ^ (m - 1) ∈ I :=
    I.mul_mem_left
      (↑((padicValuationUnitToCompletedUnramifiedWittUnit p u)⁻¹) : W)
      hpPowI
  intro n x hx
  have hφxMap : φ x ∈ (I ^ n).map φ :=
    Ideal.mem_map_of_mem φ hx
  have hφx : φ x ∈ I ^ n := by
    rw [Ideal.map_pow φ I n, hφI] at hφxMap
    exact hφxMap
  have hmul :
      ((↑((padicValuationUnitToCompletedUnramifiedWittUnit p u)⁻¹) : W) *
          (p : W) ^ (m - 1)) * φ x ∈ I * I ^ n :=
    Ideal.mul_mem_mul hcI hφx
  change
    ((↑((padicValuationUnitToCompletedUnramifiedWittUnit p u)⁻¹) : W) *
          (p : W) ^ (m - 1)) * φ x ∈ I ^ (n + 1)
  rw [pow_succ, mul_comm (I ^ n) I]
  exact hmul

theorem existsUnique_padicChangedUniformizerCoefficient
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (m : ℕ) (hm : 2 ≤ m)
    (b : padicCompletedUnramifiedWittRing p) :
    ∃! a : padicCompletedUnramifiedWittRing p,
      a =
        b +
          (↑((padicValuationUnitToCompletedUnramifiedWittUnit p u)⁻¹) :
              padicCompletedUnramifiedWittRing p) *
            (p : padicCompletedUnramifiedWittRing p) ^ (m - 1) *
            WittVector.frobenius a