CyclotomicProjection.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Integral division after projection to a smaller cyclic group

At an element of order dividing p ^ e, the prime-power cyclotomic polynomial cyclotomic (p ^ (e + 1)) R evaluates to the scalar p. Consequently, if all coefficients of a polynomial's monic remainder are divisible by p, its image in the group algebra of ZMod (p ^ e) is divisible by the same scalar.

All divisions are witnessed inside the coefficient ring or group algebra. No domain instance or cancellation assumption on a finite group algebra is used.

theorem OAI.CirculantHadamard.exists_cyclic_polynomial line 32
Source documentation
Every actual cyclic group-ring element has a polynomial representative.
```
theorem exists_cyclic_polynomial (n : ℕ) [NeZero n]
    (F : AddMonoidAlgebra R (ZMod n)) :
    ∃ P : R[X], aeval (CyclicPolynomial.generator R n) P = F := by
…
```
Mentions: OAI.CirculantHadamard.CyclicPolynomial.generator
theorem OAI.CirculantHadamard.cyclotomicAdjoinRoot_pow line 42
Source documentation
The actual root in the cyclotomic quotient satisfies its nth-power relation, directly because the cyclotomic polynomial divides X ^ n - 1.
```
theorem cyclotomicAdjoinRoot_pow (n : ℕ) :
    AdjoinRoot.root (cyclotomic n R) ^ n = 1 := by
…
```
def OAI.CirculantHadamard.cyclicCyclotomicEvaluation line 50
Source documentation
Evaluation of the actual cyclic group ring at the root in its cyclotomic quotient, using the root's proved power relation.
```
def cyclicCyclotomicEvaluation (R : Type uR) [CommRing R] (n : ℕ) [NeZero n] :
    AddMonoidAlgebra R (ZMod n) →ₐ[R] AdjoinRoot (cyclotomic n R) :=
…
```
theorem OAI.CirculantHadamard.cyclicCyclotomicEvaluation_aeval line 56
theorem OAI.CirculantHadamard.aeval_cyclotomic_prime_pow_of_pow_eq_one line 63
Source documentation
A prime-power cyclotomic polynomial becomes p at every element whose p ^ eth power is one.
```
theorem aeval_cyclotomic_prime_pow_of_pow_eq_one {p e : ℕ} (hp : p.Prime)
    (x : S) (hx : x ^ (p ^ e) = 1) :
    aeval x (cyclotomic (p ^ (e + 1)) R) = (p : S) := by
…
```
theorem OAI.CirculantHadamard.aeval_divisible_of_modByMonic_coeff line 71
Source documentation
Evaluating a monic division identity preserves integral divisibility if both the divisor's evaluation and the remainder have the stated scalar factor.
```
theorem aeval_divisible_of_modByMonic_coeff (x : S) (F Q : R[X]) (a : R)
    (_hQ : Q.Monic) (hQx : aeval x Q = algebraMap R S a)
    (hcoeff : ∀ i, a ∣ (F %ₘ Q).coeff i) :
    ∃ G : S, aeval x F = algebraMap R S a * G := by
…
```

theorem OAI.CirculantHadamard.aeval_divisible_of_cyclotomic_remainder_coeff line 85

Source documentation

Integral divisibility at a p ^ eth root follows from coefficientwise divisibility of the remainder modulo the next cyclotomic polynomial.

theorem aeval_divisible_of_cyclotomic_remainder_coeff {p e : ℕ} (hp : p.Prime)
    (x : S) (hx : x ^ (p ^ e) = 1) (F : R[X])
    (hcoeff : ∀ i, (p : R) ∣ (F %ₘ cyclotomic (p ^ (e + 1)) R).coeff i) :
    ∃ G : S, aeval x F = (p : S) * G := by
…

theorem OAI.CirculantHadamard.cyclicProjection_divisible_of_remainder_coeff line 97

Source documentation

The concrete p-division step in the cyclic group algebra: project from order p ^ (e + 1) to order p ^ e, then divide integrally by p.

theorem cyclicProjection_divisible_of_remainder_coeff {p e : ℕ} (hp : p.Prime)
    (F : R[X])
    (hcoeff : ∀ i, (p : R) ∣ (F %ₘ cyclotomic (p ^ (e + 1)) R).coeff i) :
    ∃ G : AddMonoidAlgebra R (ZMod (p ^ e)),
      cyclicProjection R (pow_dvd_pow p (Nat.le_succ e))
          (aeval (CyclicPolynomial.generator R (p ^ (e + 1))) F) =
        (p : AddMonoidAlgebra R (ZMod (p ^ e))) * G := by
…

Mentions: OAI.CirculantHadamard.cyclicProjection, OAI.CirculantHadamard.CyclicPolynomial.generator

theorem OAI.CirculantHadamard.cyclicProjection_divisible_of_cyclotomicEvaluation line 114
Source documentation
Divisibility at the actual primitive-root quotient forces integral divisibility after projecting the actual cyclic group-ring element.
The concrete monic quotient's linear remainder map supplies coefficientwise divisibility of the remainder.
```
theorem cyclicProjection_divisible_of_cyclotomicEvaluation {p e : ℕ}
    [NeZero p] (hp : p.Prime) (F : AddMonoidAlgebra R (ZMod (p ^ (e + 1))))
    (hdiv : (p : AdjoinRoot (cyclotomic (p ^ (e + 1)) R)) ∣
      cyclicCyclotomicEvaluation R (p ^ (e + 1)) F) :
    ∃ G : AddMonoidAlgebra R (ZMod (p ^ e)),
      cyclicProjection R (pow_dvd_pow p (Nat.le_succ e)) F =
        (p : AddMonoidAlgebra R (ZMod (p ^ e))) * G := by
…
```
Mentions: OAI.CirculantHadamard.cyclicCyclotomicEvaluation, OAI.CirculantHadamard.cyclicProjection