LubinTate.EqualCharacteristic.equalCharacteristicThetaCoefficient_unique
A q-additive theta intertwiner is uniquely determined by its linear coefficient. This is the uniqueness part of the contracting Frobenius equation specialized to the coefficient recursion used in the completed theta-intertwining theorem.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type*} [Field k] [Finite k]Lean source · statement
theorem equalCharacteristicThetaCoefficient_unique
(u : k⟦X⟧ˣ)
(c : ℕ → (AlgebraicClosure k)⟦X⟧)
(hc0 : c 0 = equalCharacteristicThetaCoefficient u 0)
(hrec : ∀ j : ℕ,
PowerSeries.X * c (j + 1) -
equalCharacteristicCompletedSourceUniformizer u ^
(Nat.card k ^ (j + 1)) *
equalCharacteristicPowerSeriesFrobenius k (c (j + 1)) =
equalCharacteristicThetaBetaNumerator (c j)) :
c = equalCharacteristicThetaCoefficient u