AmbientBracketAction.lean

theorem ambientAddMonoidEnd_mul_apply
    {A : Type*} [AddCommMonoid A]
    (f g : AddMonoid.End A) (x : A) :
    (f * g) x = f (g x)

theorem ambientAddMonoidEnd_sum_apply
    {A I : Type*} [AddCommMonoid A]
    (s : Finset I) (f : I → AddMonoid.End A) (x : A) :
    (∑ i ∈ s, f i) x = ∑ i ∈ s, f i x

theorem ambientAddMonoidHom_map_finset_sum
    {A I : Type*} [AddCommMonoid A]
    (f : AddMonoid.End A) (s : Finset I) (g : I → A) :
    f (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i)

def equalCharacteristicLubinTateAmbientPiEnd
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) : AddMonoid.End A where
  toFun x :=
    iterateFrobenius A F.residueCharacteristic
        (CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueRank F) x +
      t * x
  map_zero' := by simp
  map_add' x y := by
    rw [(iterateFrobenius A F.residueCharacteristic
      (CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueRank F)).map_add,
      mul_add]
    abel

theorem equalCharacteristicLubinTateAmbientPiEnd_apply
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t x : A) :
    equalCharacteristicLubinTateAmbientPiEnd F t x =
      x ^ Nat.card F.residueField + t * x

def equalCharacteristicLubinTateAmbientCoefficientEnd
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A]
    (ι : F.residueField →+* A) (a : F.residueField) :
    AddMonoid.End A where
  toFun x := ι a * x
  map_zero' := mul_zero _
  map_add' := mul_add _

theorem equalCharacteristicLubinTateAmbientCoefficientEnd_apply
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A]
    (ι : F.residueField →+* A) (a : F.residueField) (x : A) :
    equalCharacteristicLubinTateAmbientCoefficientEnd F ι a x = ι a * x

theorem equalCharacteristicLubinTateAmbientPiEnd_coefficient_mul
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (a : F.residueField) (x : A) :
    equalCharacteristicLubinTateAmbientPiEnd F t (ι a * x) =
      ι a * equalCharacteristicLubinTateAmbientPiEnd F t x

def equalCharacteristicLubinTateAmbientPiIterate
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) (i : ℕ) : AddMonoid.End A

theorem equalCharacteristicLubinTateAmbientPiIterate_zero
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t x : A) :
    equalCharacteristicLubinTateAmbientPiIterate F t 0 x = x

theorem equalCharacteristicLubinTateAmbientPiIterate_succ
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) (i : ℕ) (x : A) :
    equalCharacteristicLubinTateAmbientPiIterate F t (i + 1) x =
      equalCharacteristicLubinTateAmbientPiIterate F t i
        (equalCharacteristicLubinTateAmbientPiEnd F t x)

theorem equalCharacteristicLubinTateAmbientPiIterate_coefficient_mul
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (i : ℕ) (a : F.residueField) (x : A) :
    equalCharacteristicLubinTateAmbientPiIterate F t i (ι a * x) =
      ι a * equalCharacteristicLubinTateAmbientPiIterate F t i x

def equalCharacteristicLubinTateAmbientBracket
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) : AddMonoid.End A

theorem equalCharacteristicLubinTateAmbientBracket_apply
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) (x : A) :
    equalCharacteristicLubinTateAmbientBracket F ι t n a x =
      ∑ i ∈ Finset.range n,
        ι (PowerSeries.coeff i a) *
          equalCharacteristicLubinTateAmbientPiIterate F t i x

theorem equalCharacteristicLubinTateAmbientBracket_zero
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A) (n : ℕ) :
    equalCharacteristicLubinTateAmbientBracket F ι t n 0 = 0

theorem equalCharacteristicLubinTateAmbientBracket_add
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a b : F.residueField⟦X⟧) :
    equalCharacteristicLubinTateAmbientBracket F ι t n (a + b) =
      equalCharacteristicLubinTateAmbientBracket F ι t n a +
        equalCharacteristicLubinTateAmbientBracket F ι t n b

theorem equalCharacteristicLubinTateAmbientBracket_C
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField) :
    equalCharacteristicLubinTateAmbientBracket F ι t (n + 1)
        (PowerSeries.C a) =
      equalCharacteristicLubinTateAmbientCoefficientEnd F ι a

theorem equalCharacteristicLubinTateAmbientPiIterate_add
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) (i j : ℕ) (x : A) :
    equalCharacteristicLubinTateAmbientPiIterate F t (i + j) x =
      equalCharacteristicLubinTateAmbientPiIterate F t i
        (equalCharacteristicLubinTateAmbientPiIterate F t j x)

def IsEqualCharacteristicLubinTateAmbientTorsion
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) (n : ℕ) (x : A) : Prop

theorem equalCharacteristicLubinTateAmbientPiIterate_eq_zero_of_le
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) {n m : ℕ} (hnm : n ≤ m) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t n x) :
    equalCharacteristicLubinTateAmbientPiIterate F t m x = 0

theorem equalCharacteristicLubinTateAmbientPiEnd_torsion_pred
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) (n : ℕ) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t (n + 1) x) :
    IsEqualCharacteristicLubinTateAmbientTorsion F t n
      (equalCharacteristicLubinTateAmbientPiEnd F t x)

theorem equalCharacteristicLubinTateAmbientBracket_succ_apply
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) (x : A) :
    equalCharacteristicLubinTateAmbientBracket F ι t (n + 1) a x =
      ι (PowerSeries.coeff 0 a) * x +
        equalCharacteristicLubinTateAmbientBracket F ι t n
          (equalCharacteristicPowerSeriesTail a)
          (equalCharacteristicLubinTateAmbientPiEnd F t x)

theorem equalCharacteristicLubinTateAmbientPiIterate_one
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t x : A) :
    equalCharacteristicLubinTateAmbientPiIterate F t 1 x =
      equalCharacteristicLubinTateAmbientPiEnd F t x

theorem equalCharacteristicLubinTateAmbientPiEnd_iterate
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) (i : ℕ) (x : A) :
    equalCharacteristicLubinTateAmbientPiEnd F t
        (equalCharacteristicLubinTateAmbientPiIterate F t i x) =
      equalCharacteristicLubinTateAmbientPiIterate F t i
        (equalCharacteristicLubinTateAmbientPiEnd F t x)

theorem equalCharacteristicLubinTateAmbientBracket_coefficient_mul_apply
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) (c : F.residueField) (x : A) :
    equalCharacteristicLubinTateAmbientBracket F ι t n a (ι c * x) =
      ι c * equalCharacteristicLubinTateAmbientBracket F ι t n a x

theorem equalCharacteristicLubinTateAmbientBracket_C_mul_apply
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (c : F.residueField) (a : F.residueField⟦X⟧) (x : A) :
    equalCharacteristicLubinTateAmbientBracket F ι t n
        (PowerSeries.C c * a) x =
      ι c * equalCharacteristicLubinTateAmbientBracket F ι t n a x

theorem equalCharacteristicLubinTateAmbientPiEnd_bracket
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) (x : A) :
    equalCharacteristicLubinTateAmbientPiEnd F t
        (equalCharacteristicLubinTateAmbientBracket F ι t n a x) =
      equalCharacteristicLubinTateAmbientBracket F ι t n a
        (equalCharacteristicLubinTateAmbientPiEnd F t x)

theorem equalCharacteristicLubinTateAmbientBracket_succ_eq_of_torsion
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t n x) :
    equalCharacteristicLubinTateAmbientBracket F ι t (n + 1) a x =
      equalCharacteristicLubinTateAmbientBracket F ι t n a x

theorem equalCharacteristicLubinTateAmbientPiEnd_bracket_succ_of_torsion
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t (n + 1) x) :
    equalCharacteristicLubinTateAmbientPiEnd F t
        (equalCharacteristicLubinTateAmbientBracket F ι t (n + 1) a x) =
      equalCharacteristicLubinTateAmbientBracket F ι t n a
        (equalCharacteristicLubinTateAmbientPiEnd F t x)

theorem equalCharacteristicLubinTateAmbientBracket_mul_apply_of_torsion
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a b : F.residueField⟦X⟧) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t n x) :
    equalCharacteristicLubinTateAmbientBracket F ι t n (a * b) x =
      equalCharacteristicLubinTateAmbientBracket F ι t n a
        (equalCharacteristicLubinTateAmbientBracket F ι t n b x)