CyclicEvaluationAt.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Evaluation at an actual root of unity

The algebra map factors through the proved polynomial presentation of the cyclic group ring and the universal property of AdjoinRoot (X ^ n - 1).

def OAI.CirculantHadamard.CyclicRing.evaluateAt line 26
Source documentation
Evaluate the polynomial quotient at a proved nth root of unity.
```
def evaluateAt (n : ℕ) [NeZero n] (x : S) (hx : x ^ n = 1) : Elem A n →ₐ[A] S :=
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem
theorem OAI.CirculantHadamard.CyclicRing.evaluateAt_single line 31
theorem OAI.CirculantHadamard.CyclicRing.evaluateAt_scalar line 41
theorem OAI.CirculantHadamard.CyclicRing.evaluateAt_generator line 45
theorem OAI.CirculantHadamard.CyclicRing.evaluateAt_aeval line 55
Source documentation
Evaluation agrees with evaluation of every polynomial in the cyclic generator.
```
@[simp] theorem evaluateAt_aeval (n : ℕ) [NeZero n] (x : S) (hx : x ^ n = 1)
    (p : A[X]) :
    evaluateAt n x hx (aeval (CyclicPolynomial.generator A n) p) = aeval x p := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.evaluateAt, OAI.CirculantHadamard.CyclicPolynomial.generator
theorem OAI.CirculantHadamard.CyclicRing.evaluateAt_eq_evaluate line 67
Source documentation
The quotient construction and the finite-character construction are the same ring homomorphism.
```
theorem evaluateAt_eq_evaluate (n : ℕ) [NeZero n] (x : S) (hx : x ^ n = 1) :
    (evaluateAt (A := A) n x hx).toRingHom =
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.evaluateAt
theorem OAI.CirculantHadamard.CyclicRing.evaluateAt_apply line 76
theorem OAI.CirculantHadamard.CyclicRing.evaluateAt_one line 84
Source documentation
Evaluation at one is the actual augmentation followed by the coefficient map.
```
@[simp] theorem evaluateAt_one (n : ℕ) [NeZero n] (f : Elem A n) :
    evaluateAt n (1 : S) (one_pow n) f = algebraMap A S (augmentation n f) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.evaluateAt, OAI.CirculantHadamard.CyclicRing.augmentation
theorem OAI.CirculantHadamard.CyclicRing.map_evaluateAt_hom line 90
Source documentation
Naturality under an algebra homomorphism that sends the chosen root to the chosen target root. Both root equations remain explicit proved hypotheses.
```
theorem map_evaluateAt_hom (n : ℕ) [NeZero n]
    (x : S) (hx : x ^ n = 1) (y : T) (hy : y ^ n = 1)
    (ψ : S →ₐ[A] T) (hxy : ψ x = y) :
    ψ.comp (evaluateAt n x hx) = evaluateAt n y hy := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.evaluateAt
theorem OAI.CirculantHadamard.CyclicRing.map_evaluateAt line 99
theorem OAI.CirculantHadamard.CyclicRing.map_evaluateAt_of_map_eq_one line 107
Source documentation
In particular, a residue map sending the root to one sends evaluation to the residue of augmentation.
```
theorem map_evaluateAt_of_map_eq_one (n : ℕ) [NeZero n]
    (x : S) (hx : x ^ n = 1) (ψ : S →ₐ[A] T) (hx1 : ψ x = 1) (f : Elem A n) :
    ψ (evaluateAt n x hx f) = algebraMap A T (augmentation n f) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.evaluateAt, OAI.CirculantHadamard.CyclicRing.augmentation