RamifiedEisenstein.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Eisenstein polynomials for the ramified cyclotomic extension

The maximal ideal is generated by the actual natural prime p. We transport the integer coefficient divisibilities and prove separately that the constant term p is outside the square of the maximal ideal. This yields irreducibility over the local base, and hence the minimal polynomial of an actual primitive root in any faithful domain extension.

def OAI.CirculantHadamard.RamifiedEisenstein.shifted line 27
Source documentation
The prime-power cyclotomic polynomial translated to put the root at ξ - 1.
```
def shifted (A : Type uA) [CommRing A] (p k : ℕ) : A[X] :=
…
```
theorem OAI.CirculantHadamard.RamifiedEisenstein.shifted_monic line 30
theorem OAI.CirculantHadamard.RamifiedEisenstein.shifted_natDegree line 35
theorem OAI.CirculantHadamard.RamifiedEisenstein.cyclotomic_natDegree line 42
theorem OAI.CirculantHadamard.RamifiedEisenstein.shifted_coeff_zero line 47
theorem OAI.CirculantHadamard.RamifiedEisenstein.shifted_isWeaklyEisensteinAt line 56
theorem OAI.CirculantHadamard.RamifiedEisenstein.shifted_isEisensteinAt line 72
theorem OAI.CirculantHadamard.RamifiedEisenstein.shifted_irreducible line 88
theorem OAI.CirculantHadamard.RamifiedEisenstein.cyclotomic_irreducible line 94
theorem OAI.CirculantHadamard.RamifiedEisenstein.mod_maximal_shifted line 100
Source documentation
Modulo the maximal ideal, the translated polynomial is exactly a pure power.
```
theorem mod_maximal_shifted :
    (shifted A p k).map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) =
      (X : (A ⧸ IsLocalRing.maximalIdeal A)[X]) ^ ((p - 1) * p ^ k) := by
…
```
Mentions: OAI.CirculantHadamard.RamifiedEisenstein.shifted
theorem OAI.CirculantHadamard.RamifiedEisenstein.cyclotomic_prime line 124
theorem OAI.CirculantHadamard.RamifiedEisenstein.cyclotomic_adjoinRoot_isDomain line 127
theorem OAI.CirculantHadamard.RamifiedEisenstein.cyclotomic_eq_minpoly line 133
Source documentation
The minimal polynomial equality is for the actual primitive root in a faithful domain extension, not merely for the formal quotient root.
```
theorem cyclotomic_eq_minpoly {B : Type uB} [CommRing B] [IsDomain B]
    [Algebra A B] [NoZeroSMulDivisors A B] {ξ : B}
    (hξ : IsPrimitiveRoot ξ (p ^ (k + 1))) :
    cyclotomic (p ^ (k + 1)) A = minpoly A ξ := by
…
```