LubinTate.padicMultiplicativeLubinTateSeries
The multiplicative Lubin--Tate series (1 + X) ^ p - 1 over ℚ_p, represented by mathlib's binomial series.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.QpLean source · full declaration
def padicMultiplicativeLubinTateSeries
(p : ℕ) [Fact p.Prime] :
LubinTateSeries (padicLocalField p)
(padicIntEquivValuationSubring p (p : ℤ_[p])) where
toPowerSeries :=
PowerSeries.binomialSeries
(padicLocalField p).valuationSubring (p : ℤ) -
1
constantCoeff_eq_zero := by
simp
coeff_one_eq_uniformizer := by
have hcoeff : PowerSeries.coeff 1
(PowerSeries.binomialSeries
(padicLocalField p).valuationSubring (p : ℤ) - 1) =
(p : (padicLocalField p).valuationSubring) := by
simp only [PowerSeries.binomialSeries_nat, map_sub,
PowerSeries.coeff_one]
rw [PowerSeries.coeff_one_pow]
simp
exact hcoeff.trans (map_natCast (padicIntEquivValuationSubring p) p).symm
map_residue_eq_frobenius := by
let eO : ℤ_[p] ≃+*
(padicDVRValuation p).valuationSubring :=
padicIntEquivValuationSubring p
let eRes :
(padicLocalField p).residueField ≃+* ZMod p := by
change
IsLocalRing.ResidueField
(padicDVRValuation p).valuationSubring ≃+*
ZMod p
exact
(IsLocalRing.ResidueField.mapEquiv eO).symm.trans
(padicIntResidueFieldEquivZMod p)
let : CharP (padicLocalField p).residueField p :=
charP_of_injective_ringHom
(f := eRes.symm.toRingHom) eRes.symm.injective p
let : CharP (PowerSeries (padicLocalField p).residueField) p :=
CharP.of_ringHom_of_ne_zero
PowerSeries.C p ((Fact.out : p.Prime).ne_zero)
have hcard :
Nat.card (padicLocalField p).residueField = p := by
simpa [padicLocalField] using
padicCompleteDVF_residueField_card p
rw [hcard, PowerSeries.binomialSeries_nat (R := ℤ)]
simp only [map_sub, map_pow, map_add, map_one, PowerSeries.map_X]
rw [add_pow_char]
simp