ThetaFirstIdentity.lean

def equalCharacteristicSourceUniformizer
    (u : k⟦X⟧ˣ) : k⟦X⟧

def equalCharacteristicSourceBracketGamma
    (u : k⟦X⟧ˣ) (j : ℕ) : k⟦X⟧

theorem equalCharacteristicSourceBracketGamma_constantCoeff
    (u : k⟦X⟧ˣ) (j : ℕ) (hj : 0 < j) :
    PowerSeries.coeff 0 (equalCharacteristicSourceBracketGamma u j) = 0

def equalCharacteristicSourceBracketNumerator
    (a : k⟦X⟧) : k⟦X⟧

theorem equalCharacteristicSourceBracketNumerator_constantCoeff
    (a : k⟦X⟧) :
    PowerSeries.coeff 0 (equalCharacteristicSourceBracketNumerator a) = 0

def equalCharacteristicSourceBracketBeta
    (u : k⟦X⟧ˣ) (a : k⟦X⟧) : k⟦X⟧

def equalCharacteristicSourceBracketCoefficient
    (u : k⟦X⟧ˣ) : ℕ → k⟦X⟧
  | 0 => (u : k⟦X⟧)
  | j + 1 =>
      contractingFrobeniusEquationSolution (R := k)
        (RingHom.id k)
        (equalCharacteristicSourceBracketGamma u (j + 1))
        (equalCharacteristicSourceBracketBeta u
          (equalCharacteristicSourceBracketCoefficient u j))

theorem equalCharacteristicSourceBracketCoefficient_zero
    (u : k⟦X⟧ˣ) :
    equalCharacteristicSourceBracketCoefficient u 0 = (u : k⟦X⟧)

theorem equalCharacteristicSourceBracketCoefficient_succ_equation
    (u : k⟦X⟧ˣ) (j : ℕ) :
    equalCharacteristicSourceBracketCoefficient u (j + 1) -
        equalCharacteristicSourceBracketGamma u (j + 1) *
          equalCharacteristicSourceBracketCoefficient u (j + 1) =
      equalCharacteristicSourceBracketBeta u
        (equalCharacteristicSourceBracketCoefficient u j)

theorem equalCharacteristicSourceBracketCoefficient_succ_comparison
    (u : k⟦X⟧ˣ) (j : ℕ) :
    equalCharacteristicSourceUniformizer u *
          equalCharacteristicSourceBracketCoefficient u (j + 1) -
        equalCharacteristicSourceUniformizer u ^
            (Nat.card k ^ (j + 1)) *
          equalCharacteristicSourceBracketCoefficient u (j + 1) =
      equalCharacteristicSourceBracketCoefficient u j -
        equalCharacteristicSourceBracketCoefficient u j ^ Nat.card k

def equalCharacteristicSourceBracket
    (u : k⟦X⟧ˣ) : (k⟦X⟧)⟦X⟧

theorem equalCharacteristicSourceBracket_coeff_pow
    (u : k⟦X⟧ˣ) (j : ℕ) :
    PowerSeries.coeff (Nat.card k ^ j)
        (equalCharacteristicSourceBracket u) =
      equalCharacteristicSourceBracketCoefficient u j

theorem equalCharacteristicSourceBracket_constantCoeff
    (u : k⟦X⟧ˣ) :
    PowerSeries.constantCoeff (equalCharacteristicSourceBracket u) = 0

theorem equalCharacteristicSourceBracket_hasSubst
    (u : k⟦X⟧ˣ) :
    PowerSeries.HasSubst (equalCharacteristicSourceBracket u)

def equalCharacteristicCompletedSourceBracketCoefficient
    (u : k⟦X⟧ˣ) (j : ℕ) : (AlgebraicClosure k)⟦X⟧

def equalCharacteristicCompletedSourceBracket
    (u : k⟦X⟧ˣ) : ((AlgebraicClosure k)⟦X⟧)⟦X⟧

theorem equalCharacteristicCompletedSourceBracket_coeff_pow
    (u : k⟦X⟧ˣ) (j : ℕ) :
    PowerSeries.coeff (Nat.card k ^ j)
        (equalCharacteristicCompletedSourceBracket u) =
      equalCharacteristicCompletedSourceBracketCoefficient u j

theorem equalCharacteristicCompletedSourceBracket_constantCoeff
    (u : k⟦X⟧ˣ) :
    PowerSeries.constantCoeff
        (equalCharacteristicCompletedSourceBracket u) = 0

theorem equalCharacteristicCompletedSourceBracket_hasSubst
    (u : k⟦X⟧ˣ) :
    PowerSeries.HasSubst (equalCharacteristicCompletedSourceBracket u)

theorem equalCharacteristicCompletedSourceBracketCoefficient_zero
    (u : k⟦X⟧ˣ) :
    equalCharacteristicCompletedSourceBracketCoefficient u 0 =
      PowerSeries.map (algebraMap k (AlgebraicClosure k)) (u : k⟦X⟧)

theorem equalCharacteristicSourceUniformizer_map
    (u : k⟦X⟧ˣ) :
    PowerSeries.map (algebraMap k (AlgebraicClosure k))
        (equalCharacteristicSourceUniformizer u) =
      equalCharacteristicCompletedSourceUniformizer u

theorem equalCharacteristicPowerSeriesFrobenius_map_algebraMap
    (a : k⟦X⟧) :
    equalCharacteristicPowerSeriesFrobenius k
        (PowerSeries.map (algebraMap k (AlgebraicClosure k)) a) =
      PowerSeries.map (algebraMap k (AlgebraicClosure k)) a

theorem equalCharacteristicCompletedSourceBracket_frobenius
    (u : k⟦X⟧ˣ) :
    PowerSeries.map (equalCharacteristicPowerSeriesFrobenius k)
        (equalCharacteristicCompletedSourceBracket u) =
      equalCharacteristicCompletedSourceBracket u

theorem equalCharacteristicCompletedSourceBracketCoefficient_succ_comparison
    (u : k⟦X⟧ˣ) (j : ℕ) :
    equalCharacteristicCompletedSourceUniformizer u *
          equalCharacteristicCompletedSourceBracketCoefficient u (j + 1) -
        equalCharacteristicCompletedSourceUniformizer u ^
            (Nat.card k ^ (j + 1)) *
          equalCharacteristicCompletedSourceBracketCoefficient u (j + 1) =
      equalCharacteristicCompletedSourceBracketCoefficient u j -
        equalCharacteristicCompletedSourceBracketCoefficient u j ^ Nat.card k

theorem equalCharacteristicCompletedSourceBracket_commutes
    (u : k⟦X⟧ˣ) :
    PowerSeries.subst (equalCharacteristicCompletedSourceBracket u)
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (equalCharacteristicCompletedSourceUniformizer u)) =
      PowerSeries.subst
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (equalCharacteristicCompletedSourceUniformizer u))
        (equalCharacteristicCompletedSourceBracket u)

theorem equalCharacteristicQAdditiveSeries_pow_card_pow
    (a : ℕ → R) (i : ℕ) :
    equalCharacteristicQAdditiveSeries k a ^ (Nat.card k ^ i) =
      equalCharacteristicQAdditiveSeries k (fun n ↦
        if i ≤ n then a (n - i) ^ (Nat.card k ^ i) else 0) := by
  induction i with
  | zero =>
      simp
  | succ i ih =>
      rw [pow_succ, pow_mul, ih,
        equalCharacteristicQAdditiveSeries_pow_card]
      congr 1
      funext n
      cases n with
      | zero =>
          simp [equalCharacteristicQAdditiveShift]
      | succ n =>
          by_cases hin : i ≤ n
          · have hisucc : i + 1 ≤ n + 1 := Nat.succ_le_succ hin
            simp [equalCharacteristicQAdditiveShift, hin, hisucc,
              pow_mul]
          · have hisucc : ¬ i + 1 ≤ n + 1 := by omega
            simp [equalCharacteristicQAdditiveShift, hin, hisucc,
              Nat.card_pos.ne']

theorem equalCharacteristicQAdditiveSeries_pow_card_pow_coeff
    (a : ℕ → R) (i n : ℕ) :
    PowerSeries.coeff (Nat.card k ^ n)
        (equalCharacteristicQAdditiveSeries k a ^ (Nat.card k ^ i)) =
      if i ≤ n then a (n - i) ^ (Nat.card k ^ i) else 0 := by
  rw [equalCharacteristicQAdditiveSeries_pow_card_pow,
    equalCharacteristicQAdditiveSeries_coeff_pow]

def equalCharacteristicQAdditiveCompositionCoefficient
    (b a : ℕ → R) (n : ℕ) : R

theorem equalCharacteristicQAdditiveSeries_subst_qAdditiveSeries
    (b a : ℕ → R) :
    PowerSeries.subst (equalCharacteristicQAdditiveSeries k a)
        (equalCharacteristicQAdditiveSeries k b) =
      equalCharacteristicQAdditiveSeries k
        (equalCharacteristicQAdditiveCompositionCoefficient (k := k) b a)

def equalCharacteristicThetaAfterBracketCoefficient
    (u : k⟦X⟧ˣ) : ℕ → (AlgebraicClosure k)⟦X⟧

theorem equalCharacteristicThetaSeries_subst_sourceBracket
    (u : k⟦X⟧ˣ) :
    PowerSeries.subst (equalCharacteristicCompletedSourceBracket u)
        (equalCharacteristicThetaSeries u) =
      equalCharacteristicQAdditiveSeries k
        (equalCharacteristicThetaAfterBracketCoefficient u)

theorem equalCharacteristicThetaAfterBracketCoefficient_zero
    (u : k⟦X⟧ˣ) :
    equalCharacteristicThetaAfterBracketCoefficient u 0 =
      equalCharacteristicPowerSeriesFrobenius k
        (equalCharacteristicThetaCoefficient u 0)

theorem equalCharacteristicThetaSeries_subst_sourceBracket_intertwines
    (u : k⟦X⟧ˣ) :
    PowerSeries.subst
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (equalCharacteristicCompletedSourceUniformizer u))
        (PowerSeries.map (equalCharacteristicPowerSeriesFrobenius k)
          (PowerSeries.subst (equalCharacteristicCompletedSourceBracket u)
            (equalCharacteristicThetaSeries u))) =
      PowerSeries.subst
        (PowerSeries.subst (equalCharacteristicCompletedSourceBracket u)
          (equalCharacteristicThetaSeries u))
        (equalCharacteristicCompletedLubinTateSeries
          (k := k) PowerSeries.X)

theorem equalCharacteristicQAdditiveIntertwiner_succ_comparison
    (u : k⟦X⟧ˣ)
    (c : ℕ → (AlgebraicClosure k)⟦X⟧)
    (hintertwines :
      PowerSeries.subst
          (equalCharacteristicCompletedLubinTateSeries (k := k)
            (equalCharacteristicCompletedSourceUniformizer u))
          (equalCharacteristicQAdditiveSeries k
            (fun i ↦ equalCharacteristicPowerSeriesFrobenius k (c i))) =
        PowerSeries.subst (equalCharacteristicQAdditiveSeries k c)
          (equalCharacteristicCompletedLubinTateSeries
            (k := k) PowerSeries.X))
    (j : ℕ) :
    PowerSeries.X * c (j + 1) -
        equalCharacteristicCompletedSourceUniformizer u ^
            (Nat.card k ^ (j + 1)) *
          equalCharacteristicPowerSeriesFrobenius k (c (j + 1)) =
      equalCharacteristicPowerSeriesFrobenius k (c j) -
        c j ^ Nat.card k := by
  rw [equalCharacteristicQAdditiveSeries_subst_completedLubinTateSeries,
    equalCharacteristicCompletedLubinTateSeries_subst_qAdditiveSeries]
    at hintertwines
  have hcoeff := congrArg
    (PowerSeries.coeff (Nat.card k ^ (j + 1))) hintertwines
  rw [equalCharacteristicQAdditiveSeries_coeff_pow,
    equalCharacteristicQAdditiveSeries_coeff_pow,
    equalCharacteristicLubinTateSubstitutionCoefficient,
    equalCharacteristicLubinTatePostcompositionCoefficient] at hcoeff
  linear_combination -hcoeff

theorem equalCharacteristicQAdditiveIntertwinerCoefficient_unique
    (u : k⟦X⟧ˣ)
    (c d : ℕ → (AlgebraicClosure k)⟦X⟧)
    (hzero : c 0 = d 0)
    (hc : ∀ j : ℕ,
      PowerSeries.X * c (j + 1) -
          equalCharacteristicCompletedSourceUniformizer u ^
              (Nat.card k ^ (j + 1)) *
            equalCharacteristicPowerSeriesFrobenius k (c (j + 1)) =
        equalCharacteristicPowerSeriesFrobenius k (c j) -
          c j ^ Nat.card k)
    (hd : ∀ j : ℕ,
      PowerSeries.X * d (j + 1) -
          equalCharacteristicCompletedSourceUniformizer u ^
              (Nat.card k ^ (j + 1)) *
            equalCharacteristicPowerSeriesFrobenius k (d (j + 1)) =
        equalCharacteristicPowerSeriesFrobenius k (d j) -
          d j ^ Nat.card k) :
    c = d

theorem equalCharacteristicCompletedSourceUniformizer_frobenius
    (u : k⟦X⟧ˣ) :
    equalCharacteristicPowerSeriesFrobenius k
        (equalCharacteristicCompletedSourceUniformizer u) =
      equalCharacteristicCompletedSourceUniformizer u

theorem equalCharacteristicThetaFrobeniusCoefficient_succ_comparison
    (u : k⟦X⟧ˣ) (j : ℕ) :
    PowerSeries.X *
          equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicThetaCoefficient u (j + 1)) -
        equalCharacteristicCompletedSourceUniformizer u ^
            (Nat.card k ^ (j + 1)) *
          equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicPowerSeriesFrobenius k
              (equalCharacteristicThetaCoefficient u (j + 1))) =
      equalCharacteristicPowerSeriesFrobenius k
          (equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicThetaCoefficient u j)) -
        equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicThetaCoefficient u j) ^ Nat.card k

theorem equalCharacteristicThetaAfterBracketCoefficient_succ_comparison
    (u : k⟦X⟧ˣ) (j : ℕ) :
    PowerSeries.X *
          equalCharacteristicThetaAfterBracketCoefficient u (j + 1) -
        equalCharacteristicCompletedSourceUniformizer u ^
            (Nat.card k ^ (j + 1)) *
          equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicThetaAfterBracketCoefficient u (j + 1)) =
      equalCharacteristicPowerSeriesFrobenius k
          (equalCharacteristicThetaAfterBracketCoefficient u j) -
        equalCharacteristicThetaAfterBracketCoefficient u j ^ Nat.card k

theorem equalCharacteristicThetaSeriesFrobenius_eq_subst_sourceBracket
    (u : k⟦X⟧ˣ) :
    equalCharacteristicThetaSeriesFrobenius u =
      PowerSeries.subst (equalCharacteristicCompletedSourceBracket u)
        (equalCharacteristicThetaSeries u)