The coefficient recursion of the contracting Frobenius equation produces a sequence b_j in the completed maximal-unramified integer ring. The series used in the completed theta-intertwining theorem is the genuine sparse power series
theta(Y) = sum_j b_j Y^(q^j).
This file packages that outer series as an actual PowerSeries; no convergence or evaluation hypothesis is inserted into its definition.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristicinstance (p : Prop) : Decidable pThe predicate saying that a degree is one of the additive exponents q^j, where q = #k.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]def IsEqualCharacteristicAdditiveExponent (n : ℕ) : PropThe unique index of an additive exponent. It is only used under a proof that the degree really has the required form.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]def equalCharacteristicAdditiveExponentIndex
(n : ℕ) (hn : IsEqualCharacteristicAdditiveExponent k n) : ℕThe chosen additive exponent index realizes n as a power of q.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
omit [Field k] [Finite k] intheorem equalCharacteristicAdditiveExponentIndex_spec
(n : ℕ) (hn : IsEqualCharacteristicAdditiveExponent k n) :
Nat.card k ^ equalCharacteristicAdditiveExponentIndex k n hn = nThe selected additive-exponent index is no larger than any index realizing the same exponent.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
omit [Field k] [Finite k] intheorem equalCharacteristicAdditiveExponentIndex_min
(n : ℕ) (hn : IsEqualCharacteristicAdditiveExponent k n)
(j : ℕ) (hj : Nat.card k ^ j = n) :
equalCharacteristicAdditiveExponentIndex k n hn ≤ jThe selected additive-exponent index equals every index representing the same power. In particular it is independent of the existence proof used to define it.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]theorem equalCharacteristicAdditiveExponentIndex_eq_of_pow_eq
(n : ℕ) (hn : IsEqualCharacteristicAdditiveExponent k n)
(j : ℕ) (hj : Nat.card k ^ j = n) :
equalCharacteristicAdditiveExponentIndex k n hn = jThe chosen index of q ^ j is j.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]theorem equalCharacteristicAdditiveExponentIndex_pow (j : ℕ) :
equalCharacteristicAdditiveExponentIndex k (Nat.card k ^ j) ⟨j, rfl⟩ = jPowers of the cardinality of a nontrivial finite field have unique exponents.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]theorem natCard_pow_injective : Function.Injective (Nat.card k ^ ·)A power of the nontrivial finite-field cardinality is one only at exponent zero.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]theorem natCard_pow_eq_one_iff (j : ℕ) : Nat.card k ^ j = 1 ↔ j = 0The q-additive sparse power series attached to a coefficient sequence b: its coefficient at q^j is b_j, and every other coefficient is zero.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]def equalCharacteristicQAdditiveSeries (b : ℕ → R) : R⟦X⟧The nth coefficient of a q-additive series is selected by its power index.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
omit [Field k] [Finite k] intheorem equalCharacteristicQAdditiveSeries_coeff
(b : ℕ → R) (n : ℕ) :
PowerSeries.coeff n (equalCharacteristicQAdditiveSeries k b) =
if hn : IsEqualCharacteristicAdditiveExponent k n then
b (equalCharacteristicAdditiveExponentIndex k n hn)
else 0 := by
simp [equalCharacteristicQAdditiveSeries]The coefficient at exponent q ^ j is the prescribed coefficient b j.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]theorem equalCharacteristicQAdditiveSeries_coeff_pow
(b : ℕ → R) (j : ℕ) :
PowerSeries.coeff (Nat.card k ^ j)
(equalCharacteristicQAdditiveSeries k b) = b jCoefficients away from powers of q vanish in a q-additive series.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
omit [Field k] [Finite k] intheorem equalCharacteristicQAdditiveSeries_coeff_eq_zero
(b : ℕ → R) (n : ℕ)
(hn : ¬ IsEqualCharacteristicAdditiveExponent k n) :
PowerSeries.coeff n (equalCharacteristicQAdditiveSeries k b) = 0Every q-additive series has zero constant coefficient.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]theorem equalCharacteristicQAdditiveSeries_constantCoeff
(b : ℕ → R) :
PowerSeries.constantCoeff (equalCharacteristicQAdditiveSeries k b) = 0The linear coefficient of a q-additive series is its zeroth parameter.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]theorem equalCharacteristicQAdditiveSeries_coeff_one
(b : ℕ → R) :
PowerSeries.coeff 1 (equalCharacteristicQAdditiveSeries k b) = b 0Mapping the coefficient ring maps a q-additive series coefficientwise.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
omit [Field k] [Finite k] intheorem equalCharacteristicQAdditiveSeries_map
(f : R →+* S) (b : ℕ → R) :
PowerSeries.map f (equalCharacteristicQAdditiveSeries k b) =
equalCharacteristicQAdditiveSeries k (fun j ↦ f (b j)) := by
apply PowerSeries.ext
intro n
rw [PowerSeries.coeff_map,
equalCharacteristicQAdditiveSeries_coeff,
equalCharacteristicQAdditiveSeries_coeff]
split_ifs <;> simpMultiplication by a constant acts coefficientwise on a q-additive series.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
omit [Field k] [Finite k] intheorem equalCharacteristicQAdditiveSeries_C_mul
(a : R) (b : ℕ → R) :
PowerSeries.C a * equalCharacteristicQAdditiveSeries k b =
equalCharacteristicQAdditiveSeries k (fun j ↦ a * b j) := by
apply PowerSeries.ext
intro n
rw [PowerSeries.coeff_C_mul,
equalCharacteristicQAdditiveSeries_coeff,
equalCharacteristicQAdditiveSeries_coeff]
split_ifs <;> simpAddition of q-additive series is coefficientwise.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
omit [Field k] [Finite k] intheorem equalCharacteristicQAdditiveSeries_add
(a b : ℕ → R) :
equalCharacteristicQAdditiveSeries k a +
equalCharacteristicQAdditiveSeries k b =
equalCharacteristicQAdditiveSeries k (fun j ↦ a j + b j) := by
apply PowerSeries.ext
intro n
rw [map_add, equalCharacteristicQAdditiveSeries_coeff,
equalCharacteristicQAdditiveSeries_coeff,
equalCharacteristicQAdditiveSeries_coeff]
split_ifs <;> simpIn every algebra over the finite field k, raising to a q^j-th power is additive. This is the characteristic-p calculation used when composing additive power series.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
section FrobeniusPowers
variable {A : Type w} [CommRing A] [Algebra k A]theorem add_pow_natCard_pow (a b : A) (j : ℕ) :
(a + b) ^ (Nat.card k ^ j) =
a ^ (Nat.card k ^ j) + b ^ (Nat.card k ^ j)The q-power Frobenius on an algebra over the finite field k. Unlike the completed-unramified Frobenius used above, this raises the whole algebra element to its q-th power.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
section FrobeniusPowers
variable {A : Type w} [CommRing A] [Algebra k A]def equalCharacteristicCardFrobenius
{B : Type w} [CommRing B] [Algebra k B] : B →+* BCardinal Frobenius raises an element to the finite-field cardinality.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
section FrobeniusPowers
variable {A : Type w} [CommRing A] [Algebra k A]theorem equalCharacteristicCardFrobenius_apply
{B : Type w} [CommRing B] [Algebra k B] (x : B) :
equalCharacteristicCardFrobenius k x = x ^ Nat.card kFrobenius on a power-series algebra is coefficient Frobenius followed by the exponent expansion Y ↦ Y^q.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
section FrobeniusPowers
variable {A : Type w} [CommRing A] [Algebra k A]theorem powerSeries_pow_natCard_eq_expand_map_cardFrobenius
{B : Type w} [CommRing B] [Nontrivial B] [Algebra k B]
(f : B⟦X⟧) :
f ^ Nat.card k =
PowerSeries.expand (Nat.card k) Nat.card_pos.ne'
(PowerSeries.map (equalCharacteristicCardFrobenius k) f)Shift of a coefficient sequence induced by Y ↦ Y^q.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]def equalCharacteristicQAdditiveShift (b : ℕ → R) : ℕ → R
| 0 => 0
| j + 1 => b jExpanding exponents by q shifts a q-additive coefficient sequence by one place.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]theorem equalCharacteristicQAdditiveSeries_expand
(b : ℕ → R) :
PowerSeries.expand (Nat.card k) Nat.card_pos.ne'
(equalCharacteristicQAdditiveSeries k b) =
equalCharacteristicQAdditiveSeries k
(equalCharacteristicQAdditiveShift b)Taking a q-th power shifts the additive series and raises every coefficient to its q-th power.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]theorem equalCharacteristicQAdditiveSeries_pow_card
[Nontrivial R] [Algebra k R] (b : ℕ → R) :
equalCharacteristicQAdditiveSeries k b ^ Nat.card k =
equalCharacteristicQAdditiveSeries k
(equalCharacteristicQAdditiveShift
(fun j ↦ b j ^ Nat.card k)) := by
rw [powerSeries_pow_natCard_eq_expand_map_cardFrobenius k,
equalCharacteristicQAdditiveSeries_map,
equalCharacteristicQAdditiveSeries_expand]
congr 2
funext j
exact equalCharacteristicCardFrobenius_apply k (b j)The actual outer theta series from the completed theta-intertwining theorem.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}def equalCharacteristicThetaSeries
(u : k⟦X⟧ˣ) : ((AlgebraicClosure k)⟦X⟧)⟦X⟧The theta series coefficient at q ^ j is the jth theta coefficient.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicThetaSeries_coeff_pow
(u : k⟦X⟧ˣ) (j : ℕ) :
PowerSeries.coeff (Nat.card k ^ j)
(equalCharacteristicThetaSeries u) =
equalCharacteristicThetaCoefficient u jThe equal-characteristic theta series has zero constant coefficient.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicThetaSeries_constantCoeff
(u : k⟦X⟧ˣ) :
PowerSeries.constantCoeff (equalCharacteristicThetaSeries u) = 0The zero constant coefficient makes theta a valid formal substitution.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicThetaSeries_hasSubst
(u : k⟦X⟧ˣ) :
PowerSeries.HasSubst (equalCharacteristicThetaSeries u)Frobenius acts on the completed-unramified coefficients of theta.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}def equalCharacteristicThetaSeriesFrobenius
(u : k⟦X⟧ˣ) : ((AlgebraicClosure k)⟦X⟧)⟦X⟧Coefficientwise Frobenius of theta is the q-additive series of Frobenius coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicThetaSeriesFrobenius_eq_qAdditiveSeries
(u : k⟦X⟧ˣ) :
equalCharacteristicThetaSeriesFrobenius u =
equalCharacteristicQAdditiveSeries k
(fun j ↦ equalCharacteristicPowerSeriesFrobenius k
(equalCharacteristicThetaCoefficient u j)) := by
exact equalCharacteristicQAdditiveSeries_map k
(equalCharacteristicPowerSeriesFrobenius k)
(equalCharacteristicThetaCoefficient u)The Frobenius theta coefficient at q ^ j is Frobenius of the jth coefficient.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicThetaSeriesFrobenius_coeff_pow
(u : k⟦X⟧ˣ) (j : ℕ) :
PowerSeries.coeff (Nat.card k ^ j)
(equalCharacteristicThetaSeriesFrobenius u) =
equalCharacteristicPowerSeriesFrobenius k
(equalCharacteristicThetaCoefficient u j)The additive Lubin--Tate series Y^q + pi Y, now with coefficients in the completed maximal-unramified integer ring.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}def equalCharacteristicCompletedLubinTateSeries
(pi : (AlgebraicClosure k)⟦X⟧) :
((AlgebraicClosure k)⟦X⟧)⟦X⟧The completed Lubin–Tate series has zero constant coefficient.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicCompletedLubinTateSeries_constantCoeff
(pi : (AlgebraicClosure k)⟦X⟧) :
PowerSeries.constantCoeff
(equalCharacteristicCompletedLubinTateSeries (k := k) pi) = 0A Lubin--Tate series has zero constant coefficient and can therefore be substituted into theta.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicCompletedLubinTateSeries_hasSubst
(pi : (AlgebraicClosure k)⟦X⟧) :
PowerSeries.HasSubst
(equalCharacteristicCompletedLubinTateSeries (k := k) pi)A q^j-th power of Y^q + pi Y has exactly the two expected additive monomials.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicCompletedLubinTateSeries_pow_card_pow
(pi : (AlgebraicClosure k)⟦X⟧) (j : ℕ) :
equalCharacteristicCompletedLubinTateSeries (k := k) pi ^
(Nat.card k ^ j) =
PowerSeries.X ^ (Nat.card k ^ (j + 1)) +
PowerSeries.C (pi ^ (Nat.card k ^ j)) *
PowerSeries.X ^ (Nat.card k ^ j)Coefficient form of the preceding two-monomial calculation.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicCompletedLubinTateSeries_pow_card_pow_coeff
(pi : (AlgebraicClosure k)⟦X⟧) (j n : ℕ) :
PowerSeries.coeff n
(equalCharacteristicCompletedLubinTateSeries (k := k) pi ^
(Nat.card k ^ j)) =
(if n = Nat.card k ^ (j + 1) then 1 else 0) +
(if n = Nat.card k ^ j then pi ^ (Nat.card k ^ j) else 0) := by
rw [equalCharacteristicCompletedLubinTateSeries_pow_card_pow]
simp only [map_add, PowerSeries.coeff_X_pow, PowerSeries.coeff_C_mul]
split_ifs <;> simp_allCoefficients obtained by substituting Y^q + pi Y into a q-additive series.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}def equalCharacteristicLubinTateSubstitutionCoefficient
(pi : (AlgebraicClosure k)⟦X⟧)
(b : ℕ → (AlgebraicClosure k)⟦X⟧) :
ℕ → (AlgebraicClosure k)⟦X⟧
| 0 => b 0 * pi
| j + 1 => b j + b (j + 1) * pi ^ (Nat.card k ^ (j + 1))Substitution into an additive series cannot create a non-additive exponent.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicQAdditiveSeries_subst_coeff_eq_zero
(pi : (AlgebraicClosure k)⟦X⟧)
(b : ℕ → (AlgebraicClosure k)⟦X⟧)
(n : ℕ) (hn : ¬ IsEqualCharacteristicAdditiveExponent k n) :
PowerSeries.coeff n
(PowerSeries.subst
(equalCharacteristicCompletedLubinTateSeries (k := k) pi)
(equalCharacteristicQAdditiveSeries k b)) = 0The linear coefficient after substitution is b_0 pi.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicQAdditiveSeries_subst_coeff_one
(pi : (AlgebraicClosure k)⟦X⟧)
(b : ℕ → (AlgebraicClosure k)⟦X⟧) :
PowerSeries.coeff 1
(PowerSeries.subst
(equalCharacteristicCompletedLubinTateSeries (k := k) pi)
(equalCharacteristicQAdditiveSeries k b)) = b 0 * piAt the next additive exponent, substitution receives one contribution from the preceding q-power term and one from the linear term.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicQAdditiveSeries_subst_coeff_pow_succ
(pi : (AlgebraicClosure k)⟦X⟧)
(b : ℕ → (AlgebraicClosure k)⟦X⟧) (r : ℕ) :
PowerSeries.coeff (Nat.card k ^ (r + 1))
(PowerSeries.subst
(equalCharacteristicCompletedLubinTateSeries (k := k) pi)
(equalCharacteristicQAdditiveSeries k b)) =
b r + b (r + 1) * pi ^ (Nat.card k ^ (r + 1))Formal substitution formula for a q-additive series.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicQAdditiveSeries_subst_completedLubinTateSeries
(pi : (AlgebraicClosure k)⟦X⟧)
(b : ℕ → (AlgebraicClosure k)⟦X⟧) :
PowerSeries.subst
(equalCharacteristicCompletedLubinTateSeries (k := k) pi)
(equalCharacteristicQAdditiveSeries k b) =
equalCharacteristicQAdditiveSeries k
(equalCharacteristicLubinTateSubstitutionCoefficient pi b)Coefficients obtained by applying Y^q + pi Y after a q-additive series.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}def equalCharacteristicLubinTatePostcompositionCoefficient
(pi : (AlgebraicClosure k)⟦X⟧)
(b : ℕ → (AlgebraicClosure k)⟦X⟧) :
ℕ → (AlgebraicClosure k)⟦X⟧
| 0 => pi * b 0
| j + 1 => b j ^ Nat.card k + pi * b (j + 1)Formal postcomposition formula (Y^q + pi Y) ∘ (Σ b_j Y^(q^j)).
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicCompletedLubinTateSeries_subst_qAdditiveSeries
(pi : (AlgebraicClosure k)⟦X⟧)
(b : ℕ → (AlgebraicClosure k)⟦X⟧) :
PowerSeries.subst (equalCharacteristicQAdditiveSeries k b)
(equalCharacteristicCompletedLubinTateSeries (k := k) pi) =
equalCharacteristicQAdditiveSeries k
(equalCharacteristicLubinTatePostcompositionCoefficient pi b)The completed theta-intertwining theorem, the second theta identity theta^phi o e_bar_pi = e_T o theta.
Both sides are genuine formal substitutions. At the linear coefficient the claim is the semilinear unit equation phi(b_0) = u b_0; at every higher q-power coefficient it is exactly the contracting recursion defining b_(j+1).
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicThetaSeries_intertwines
(u : k⟦X⟧ˣ) :
PowerSeries.subst
(equalCharacteristicCompletedLubinTateSeries (k := k)
(equalCharacteristicCompletedSourceUniformizer u))
(equalCharacteristicThetaSeriesFrobenius u) =
PowerSeries.subst (equalCharacteristicThetaSeries u)
(equalCharacteristicCompletedLubinTateSeries (k := k) PowerSeries.X)The linear coefficient of theta is the semilinear unit constructed from phi(epsilon) = u * epsilon.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
local instance (p : Prop) : Decidable p := Classical.propDecidable p
variable (k : Type u) [Field k] [Finite k]
variable {R : Type v} [CommRing R]
variable {S : Type w} [CommRing S]
variable {k}theorem equalCharacteristicThetaSeries_coeff_one
(u : k⟦X⟧ˣ) :
PowerSeries.coeff 1 (equalCharacteristicThetaSeries u) =
equalCharacteristicSemilinearUnit (u : k⟦X⟧)
(by
intro hzero
have hunit := PowerSeries.isUnit_constantCoeff (u : k⟦X⟧) u.isUnit
apply hunit.ne_zero
simpa [PowerSeries.coeff_zero_eq_constantCoeff_apply] using hzero) := by
calc
PowerSeries.coeff 1 (equalCharacteristicThetaSeries u) =
equalCharacteristicThetaCoefficient u 0 := by
simpa only [pow_zero] using equalCharacteristicThetaSeries_coeff_pow u 0
_ = _ := equalCharacteristicThetaCoefficient_zero u