CyclicEvaluation.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of the finite cyclic group ring

Evaluation is a ring homomorphism obtained from a coefficient homomorphism and an actual character of the cyclic group. Its compatibility with the group-ring involution is proved from the coefficient and character identities.

def OAI.CirculantHadamard.CyclicRing.evaluate line 25
Source documentation
Evaluation at a multiplicative character of the additive cyclic group.
```
def evaluate (φ : R →+* S) (χ : Multiplicative (ZMod n) →* S) : Elem R n →+* S :=
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem
theorem OAI.CirculantHadamard.CyclicRing.evaluate_single line 28
theorem OAI.CirculantHadamard.CyclicRing.evaluate_scalar line 33
theorem OAI.CirculantHadamard.CyclicRing.evaluate_apply line 41
Source documentation
The full finite sum, rather than a sum over an unspecified support.
```
theorem evaluate_apply [NeZero n] (φ : R →+* S)
    (χ : Multiplicative (ZMod n) →* S) (f : Elem R n) :
    evaluate φ χ f = ∑ a : ZMod n, φ (f.coeff a) * χ (Multiplicative.ofAdd a) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.evaluate
theorem OAI.CirculantHadamard.CyclicRing.evaluate_ofCoeffs line 47
theorem OAI.CirculantHadamard.CyclicRing.evaluate_trivial_eq_augmentation line 53
Source documentation
The trivial character recovers augmentation followed by the coefficient map.
```
theorem evaluate_trivial_eq_augmentation [NeZero n] (φ : R →+* S)
    (f : Elem R n) :
    evaluate φ (1 : Multiplicative (ZMod n) →* S) f = φ (augmentation n f) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.evaluate, OAI.CirculantHadamard.CyclicRing.augmentation
theorem OAI.CirculantHadamard.CyclicRing.map_evaluate line 59
Source documentation
Evaluation commutes with a change of target coefficient ring.
```
theorem map_evaluate [NeZero n] (φ : R →+* S)
    (χ : Multiplicative (ZMod n) →* S) (ψ : S →+* T) (f : Elem R n) :
    ψ (evaluate φ χ f) = evaluate (ψ.comp φ) (ψ.toMonoidHom.comp χ) f := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.evaluate

theorem OAI.CirculantHadamard.CyclicRing.map_evaluate_hom line 68

Source documentation

Bundled naturality of character evaluation.

theorem map_evaluate_hom [NeZero n] (φ : R →+* S)
    (χ : Multiplicative (ZMod n) →* S) (ψ : S →+* T) :
    ψ.comp (evaluate φ χ) = evaluate (ψ.comp φ) (ψ.toMonoidHom.comp χ) := by
…

Mentions: OAI.CirculantHadamard.CyclicRing.evaluate

theorem OAI.CirculantHadamard.CyclicRing.evaluate_ringStar_intertwining line 77
Source documentation
A target endomorphism intertwines evaluation and the full group-ring star when it intertwines the coefficient involution and character inversion.
```
theorem evaluate_ringStar_intertwining [StarRing R] [NeZero n]
    (φ : R →+* S) (χ : Multiplicative (ZMod n) →* S) (τ : S →+* S)
    (hφ : ∀ r, φ (star r) = τ (φ r))
    (hχ : ∀ a : ZMod n,
      χ (Multiplicative.ofAdd (-a)) = τ (χ (Multiplicative.ofAdd a)))
    (f : Elem R n) :
    evaluate φ χ (ringStar f) = τ (evaluate φ χ f) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.evaluate, OAI.CirculantHadamard.CyclicRing.ringStar

theorem OAI.CirculantHadamard.CyclicRing.evaluate_ringStar line 92

Source documentation

Character evaluation carries the full group-ring involution to target star.

theorem evaluate_ringStar [StarRing R] [StarRing S] [NeZero n]
    (φ : R →+* S) (χ : Multiplicative (ZMod n) →* S)
    (hφ : ∀ r, φ (star r) = star (φ r))
    (hχ : ∀ a : ZMod n,
      χ (Multiplicative.ofAdd (-a)) = star (χ (Multiplicative.ofAdd a)))
    (f : Elem R n) :
    evaluate φ χ (ringStar f) = star (evaluate φ χ f) :=
…

Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.evaluate, OAI.CirculantHadamard.CyclicRing.ringStar

theorem OAI.CirculantHadamard.CyclicRing.evaluate_mul_ringStar line 102

Source documentation

The group-ring norm product becomes the usual star norm product.

theorem evaluate_mul_ringStar [StarRing R] [StarRing S] [NeZero n]
    (φ : R →+* S) (χ : Multiplicative (ZMod n) →* S)
    (hφ : ∀ r, φ (star r) = star (φ r))
    (hχ : ∀ a : ZMod n,
      χ (Multiplicative.ofAdd (-a)) = star (χ (Multiplicative.ofAdd a)))
    (f : Elem R n) :
    evaluate φ χ (f * ringStar f) = evaluate φ χ f * star (evaluate φ χ f) := by
…

Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.evaluate, OAI.CirculantHadamard.CyclicRing.ringStar

theorem OAI.CirculantHadamard.CyclicRing.evaluate_norm_eq line 113
Source documentation
A proved scalar group-ring norm equation transfers to every compatible character; the norm equation is not built into the evaluation definition.
```
theorem evaluate_norm_eq [StarRing R] [StarRing S] [NeZero n]
    (φ : R →+* S) (χ : Multiplicative (ZMod n) →* S)
    (hφ : ∀ r, φ (star r) = star (φ r))
    (hχ : ∀ a : ZMod n,
      χ (Multiplicative.ofAdd (-a)) = star (χ (Multiplicative.ofAdd a)))
    (f : Elem R n) (r : R) (hf : f * ringStar f = scalar n r) :
    evaluate φ χ f * star (evaluate φ χ f) = φ r := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar, OAI.CirculantHadamard.CyclicRing.evaluate

theorem OAI.CirculantHadamard.CyclicRing.evaluate_int_ringStar line 123

Source documentation

For integer coefficients, coefficient-star compatibility is automatic.

theorem evaluate_int_ringStar {A : Type uA} [CommRing A] [StarRing A] [NeZero n]
    (χ : Multiplicative (ZMod n) →* A)
    (hχ : ∀ a : ZMod n,
      χ (Multiplicative.ofAdd (-a)) = star (χ (Multiplicative.ofAdd a)))
    (f : Elem ℤ n) :
    evaluate (Int.castRingHom A) χ (ringStar f) =
      star (evaluate (Int.castRingHom A) χ f) := by
…

Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.evaluate, OAI.CirculantHadamard.CyclicRing.ringStar