ScalarEndomorphisms.lean

def padicCompletedMultiplicativeScalarEndomorphism
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries (padicCompletedUnramifiedWittRing p)

theorem padicMultiplicativeScalarEndomorphism_mul
    (p : ℕ) [Fact p.Prime]
    (a b : (padicLocalField p).valuationSubring) :
    recursiveIntertwiner
        (padicMultiplicativeLubinTateSeries_isUniformizer p)
        (padicMultiplicativeLubinTateSeries p)
        (padicMultiplicativeLubinTateSeries p)
        (fun _ : Unit => a * b) =
      PowerSeries.subst
        (recursiveIntertwiner
          (padicMultiplicativeLubinTateSeries_isUniformizer p)
          (padicMultiplicativeLubinTateSeries p)
          (padicMultiplicativeLubinTateSeries p)
          (fun _ : Unit => b))
        (recursiveIntertwiner
          (padicMultiplicativeLubinTateSeries_isUniformizer p)
          (padicMultiplicativeLubinTateSeries p)
          (padicMultiplicativeLubinTateSeries p)
          (fun _ : Unit => a)) := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let E := padicMultiplicativeLubinTateSeries p
  let A :=
    recursiveIntertwiner hπ E E (fun _ : Unit => a)
  let B :=
    recursiveIntertwiner hπ E E (fun _ : Unit => b)
  have hAlinear :=
    recursiveIntertwiner_hasLinearTerm hπ E E
      (fun _ : Unit => a)
  have hBlinear :=
    recursiveIntertwiner_hasLinearTerm hπ E E
      (fun _ : Unit => b)
  have hcomp :=
    hAlinear.subst
      (G := fun _ : Unit => B)
      (M := fun _ : Unit => fun _ : Unit => b)
      (fun _ => hBlinear)
  have hcomp' :
      HasLinearTerm (PowerSeries.subst B A)
        (fun _ : Unit => a * b) := by
    simpa only [A, B, PowerSeries.subst_def, Finset.univ_unique,
      Finset.sum_singleton] using hcomp
  have hIntertwines :=
    (recursiveIntertwiner_intertwines hπ E E
      (fun _ : Unit => a)).powerSeries_subst
        hAlinear.hasSubst
        (recursiveIntertwiner_intertwines hπ E E
          (fun _ : Unit => b))
        hBlinear.hasSubst
  exact
    eq_of_hasLinearTerm_of_intertwines hπ E E
      (fun _ : Unit => a * b)
      (recursiveIntertwiner_hasLinearTerm hπ E E
        (fun _ : Unit => a * b))
      (recursiveIntertwiner_intertwines hπ E E
        (fun _ : Unit => a * b))
      hcomp' hIntertwines

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

theorem powerSeries_hasLinearTerm_of_constantCoeff_coeff_one
    {R : Type*} [CommRing R]
    (H : PowerSeries R) (a : R)
    (hconstant : PowerSeries.constantCoeff H = 0)
    (hone : PowerSeries.coeff 1 H = a) :
    SameUniformizer.HasLinearTerm H (fun _ : Unit => a) := by
  rw [SameUniformizer.HasLinearTerm]
  apply MvPowerSeries.nat_le_order
  intro d hd
  have hdegree : d.degree = d () :=
    by simp [Finsupp.degree_eq_sum]
  have hd' : d () < 2 := by
    simpa only [hdegree] using hd
  by_cases hd0 : d () = 0
  · have hdeq : d = 0 := by
      apply Finsupp.ext
      intro i
      cases i
      simp [hd0]
    subst d
    simp only [map_sub,
      MvPowerSeries.coeff_zero_eq_constantCoeff_apply,
      ← PowerSeries.constantCoeff_eq, hconstant,
      SameUniformizer.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
    change
      PowerSeries.coeff 1 H -
          MvPowerSeries.coeff (Finsupp.single () 1)
            (SameUniformizer.linearForm (fun _ : Unit => a)) =
        0
    rw [hone]
    classical
    simp [SameUniformizer.linearForm]

theorem
    padicCompletedMultiplicativeScalarEndomorphism_constantCoeff
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.constantCoeff
        (padicCompletedMultiplicativeScalarEndomorphism p a) = 0

theorem padicCompletedMultiplicativeScalarEndomorphism_coeff_one
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.coeff 1
        (padicCompletedMultiplicativeScalarEndomorphism p a) =
      padicValuationSubringToCompletedUnramifiedWittRing p a

theorem
    padicCompletedChangedStandardScalarEndomorphism_constantCoeff
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.constantCoeff
        (padicCompletedChangedStandardScalarEndomorphism p u a) = 0

theorem
    padicCompletedChangedStandardScalarEndomorphism_coeff_one
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.coeff 1
        (padicCompletedChangedStandardScalarEndomorphism p u a) =
      padicValuationSubringToCompletedUnramifiedWittRing p a

theorem padicMultiplicativeScalarEndomorphism_commutes
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.subst
        (recursiveIntertwiner
          (padicMultiplicativeLubinTateSeries_isUniformizer p)
          (padicMultiplicativeLubinTateSeries p)
          (padicMultiplicativeLubinTateSeries p)
          (fun _ : Unit => a))
        (padicMultiplicativeLubinTateSeries p).toPowerSeries =
      PowerSeries.subst
        (padicMultiplicativeLubinTateSeries p).toPowerSeries
        (recursiveIntertwiner
          (padicMultiplicativeLubinTateSeries_isUniformizer p)
          (padicMultiplicativeLubinTateSeries p)
          (padicMultiplicativeLubinTateSeries p)
          (fun _ : Unit => a)) := by
  have h :=
    recursiveIntertwiner_intertwines
      (padicMultiplicativeLubinTateSeries_isUniformizer p)
      (padicMultiplicativeLubinTateSeries p)
      (padicMultiplicativeLubinTateSeries p)
      (fun _ : Unit => a)
  calc
    _ =
        MvPowerSeries.subst
          (fun i : Unit =>
            inVariable (padicMultiplicativeLubinTateSeries p) i)
          (recursiveIntertwiner
            (padicMultiplicativeLubinTateSeries_isUniformizer p)
            (padicMultiplicativeLubinTateSeries p)
            (padicMultiplicativeLubinTateSeries p)
            (fun _ : Unit => a)) :=
      h
    _ = _ := by
      rw [PowerSeries.subst_def]
      congr 1
      funext i
      cases i
      exact
        PowerSeries.X_subst
          (padicMultiplicativeLubinTateSeries p).toPowerSeries

theorem padicChangedStandardScalarEndomorphism_commutes
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.subst
        (standardLubinTateEndomorphism
          (standardLubinTateChangedUniformizer_isUniformizer
            (padicMultiplicativeLubinTateSeries_isUniformizer p) u)
          a)
        (standardLubinTateSeries
          (standardLubinTateChangedUniformizer_isUniformizer
            (padicMultiplicativeLubinTateSeries_isUniformizer p) u)).toPowerSeries =
      PowerSeries.subst
        (standardLubinTateSeries
          (standardLubinTateChangedUniformizer_isUniformizer
            (padicMultiplicativeLubinTateSeries_isUniformizer p) u)).toPowerSeries
        (standardLubinTateEndomorphism
          (standardLubinTateChangedUniformizer_isUniformizer
            (padicMultiplicativeLubinTateSeries_isUniformizer p) u)
          a)

theorem padicCompletedMultiplicativeScalarEndomorphism_commutes
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.subst
        (padicCompletedMultiplicativeScalarEndomorphism p a)
        (padicCompletedMultiplicativeSeries p) =
      PowerSeries.subst
        (padicCompletedMultiplicativeSeries p)
        (padicCompletedMultiplicativeScalarEndomorphism p a)

theorem padicCompletedChangedStandardScalarEndomorphism_commutes
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.subst
        (padicCompletedChangedStandardScalarEndomorphism p u a)
        (padicCompletedChangedStandardSeries p u) =
      PowerSeries.subst
        (padicCompletedChangedStandardSeries p u)
        (padicCompletedChangedStandardScalarEndomorphism p u a)

theorem padicCompletedMultiplicativeScalarEndomorphism_frobenius
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.map WittVector.frobenius
        (padicCompletedMultiplicativeScalarEndomorphism p a) =
      padicCompletedMultiplicativeScalarEndomorphism p a

theorem padicCompletedChangedStandardScalarEndomorphism_frobenius
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.map WittVector.frobenius
        (padicCompletedChangedStandardScalarEndomorphism p u a) =
      padicCompletedChangedStandardScalarEndomorphism p u a

theorem padicCompletedMultiplicativeSeries_frobenius
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.map WittVector.frobenius
        (padicCompletedMultiplicativeSeries p) =
      padicCompletedMultiplicativeSeries p

theorem padicCompletedChangedStandardSeries_frobenius
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.map WittVector.frobenius
        (padicCompletedChangedStandardSeries p u) =
      padicCompletedChangedStandardSeries p u

theorem
    padicCompletedMultiplicativeScalarEndomorphism_hasLinearTerm
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    HasLinearTerm
        (padicCompletedMultiplicativeScalarEndomorphism p a)
        (fun _ : Unit =>
          padicValuationSubringToCompletedUnramifiedWittRing p a) :=
  powerSeries_hasLinearTerm_of_constantCoeff_coeff_one
    (padicCompletedMultiplicativeScalarEndomorphism p a)
    (padicValuationSubringToCompletedUnramifiedWittRing p a)
    (padicCompletedMultiplicativeScalarEndomorphism_constantCoeff p a)
    (padicCompletedMultiplicativeScalarEndomorphism_coeff_one p a)

theorem padicCompletedMultiplicativeScalarEndomorphism_hasSubst
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.HasSubst
      (padicCompletedMultiplicativeScalarEndomorphism p a)

theorem padicCompletedMultiplicativeScalarEndomorphism_mul
    (p : ℕ) [Fact p.Prime]
    (a b : (padicLocalField p).valuationSubring) :
    padicCompletedMultiplicativeScalarEndomorphism p (a * b) =
      PowerSeries.subst
        (padicCompletedMultiplicativeScalarEndomorphism p b)
        (padicCompletedMultiplicativeScalarEndomorphism p a)

theorem
    padicCompletedChangedStandardScalarEndomorphism_hasLinearTerm
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a : (padicLocalField p).valuationSubring) :
    HasLinearTerm
        (padicCompletedChangedStandardScalarEndomorphism p u a)
        (fun _ : Unit =>
          padicValuationSubringToCompletedUnramifiedWittRing p a) :=
  powerSeries_hasLinearTerm_of_constantCoeff_coeff_one
    (padicCompletedChangedStandardScalarEndomorphism p u a)
    (padicValuationSubringToCompletedUnramifiedWittRing p a)
    (padicCompletedChangedStandardScalarEndomorphism_constantCoeff p u a)
    (padicCompletedChangedStandardScalarEndomorphism_coeff_one p u a)

theorem padicCompletedChangedStandardScalarEndomorphism_hasSubst
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.HasSubst
      (padicCompletedChangedStandardScalarEndomorphism p u a)

theorem padicCompletedChangedStandardScalarEndomorphism_uniformizer
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedChangedStandardScalarEndomorphism p u
        (standardLubinTateChangedUniformizer
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) u) =
      padicCompletedChangedStandardSeries p u

theorem padicCompletedChangedStandardScalarEndomorphism_mul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a b : (padicLocalField p).valuationSubring) :
    padicCompletedChangedStandardScalarEndomorphism p u (a * b) =
      PowerSeries.subst
        (padicCompletedChangedStandardScalarEndomorphism p u b)
        (padicCompletedChangedStandardScalarEndomorphism p u a)

theorem padicCompletedChangedStandardScalarEndomorphism_one
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedChangedStandardScalarEndomorphism p u 1 =
      PowerSeries.X