LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePredecessor_isRoot
The (n - m)-fold Lubin--Tate predecessor of a primitive level-n + 1 point is a root of the primitive level-m + 1 polynomial.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]Lean source · full declaration
theorem equalCharacteristicLubinTatePrimitivePredecessor_isRoot
(F : LocalField.{u, v} K)
[CharP K F.residueCharacteristic]
{m n : ℕ} (hmn : m ≤ n) :
let y :=
equalCharacteristicLubinTateAmbientPiIterate F
(equalCharacteristicSeparableUniformizer F) (n - m)
(chosenEqualCharacteristicLubinTatePrimitiveRoot F n)
((equalCharacteristicLubinTatePrimitivePolynomial F m).map
(equalCharacteristicSeparableBaseHom F)).IsRoot y := by
let y :=
equalCharacteristicLubinTateAmbientPiIterate F
(equalCharacteristicSeparableUniformizer F) (n - m)
(chosenEqualCharacteristicLubinTatePrimitiveRoot F n)
have hyEquation :
equalCharacteristicLubinTateAmbientPiIterate F
(equalCharacteristicSeparableUniformizer F) m y ^
(Nat.card F.residueField - 1) +
equalCharacteristicSeparableUniformizer F = 0 := by
rw [show
equalCharacteristicLubinTateAmbientPiIterate F
(equalCharacteristicSeparableUniformizer F) m y =
equalCharacteristicLubinTateAmbientPiIterate F
(equalCharacteristicSeparableUniformizer F) n
(chosenEqualCharacteristicLubinTatePrimitiveRoot F n) by
simp only [y]
rw [← equalCharacteristicLubinTateAmbientPiIterate_add,
Nat.add_sub_of_le hmn]]
exact chosenEqualCharacteristicLubinTatePrimitiveRoot_equation F n
change Polynomial.eval y
((equalCharacteristicLubinTatePrimitivePolynomial F m).map
(equalCharacteristicSeparableBaseHom F)) = 0
rw [Polynomial.eval_map,
equalCharacteristicLubinTatePrimitivePolynomial_eval₂]
exact hyEquation