CyclicProjection.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Quotients of actual cyclic group rings

For m ∣ n, reduction of indices defines the quotient map from the cyclic group ring of order n to that of order m. In particular it sends the distinguished generator to the distinguished generator and fixes scalars. The definition is the convolution ring homomorphism induced by ZMod.castHom.

def OAI.CirculantHadamard.cyclicProjection line 25
Source documentation
The quotient of cyclic group rings induced by reduction of indices.
```
def cyclicProjection (h : m ∣ n) : Elem R n →+* Elem R m :=
…
```
theorem OAI.CirculantHadamard.cyclicProjection_apply line 30
theorem OAI.CirculantHadamard.cyclicProjection_single line 33
theorem OAI.CirculantHadamard.cyclicProjection_single_zero line 38
theorem OAI.CirculantHadamard.cyclicProjection_scalar line 42
theorem OAI.CirculantHadamard.cyclicProjection_generator line 46
theorem OAI.CirculantHadamard.cyclicProjection_single_natCast line 50
theorem OAI.CirculantHadamard.cyclicProjection_self line 55
theorem OAI.CirculantHadamard.cyclicProjection_comp line 61

theorem OAI.CirculantHadamard.sum_cyclicProjection line 78

Source documentation

Any additive coefficient evaluation factors through the quotient exactly when its index function is pulled back along reduction.

theorem sum_cyclicProjection {S : Type uS} [AddCommMonoid S]
    (h : m ∣ n) (F : Elem R n) (v : ZMod m → R →+ S) :
    (cyclicProjection R h F).coeff.sum (fun a r => v a r) =
      F.coeff.sum (fun a r => v (ZMod.castHom h (ZMod m) a) r) :=
…

Mentions: OAI.CirculantHadamard.cyclicProjection

theorem OAI.CirculantHadamard.augmentation_cyclicProjection line 85
Source documentation
Evaluation at the trivial character is unchanged by the cyclic quotient.
```
@[simp] theorem augmentation_cyclicProjection (h : m ∣ n) (F : Elem R n) :
    augmentation m (cyclicProjection R h F) = augmentation n F := by
…
```
Mentions: OAI.CirculantHadamard.cyclicProjection
theorem OAI.CirculantHadamard.cyclicProjection_ringStar line 97
Source documentation
Quotienting the indices commutes with conjugation and index reversal.
```
@[simp] theorem cyclicProjection_ringStar (h : m ∣ n) (F : Elem R n) :
    cyclicProjection R h (ringStar F) = ringStar (cyclicProjection R h F) := by
…
```
Mentions: OAI.CirculantHadamard.cyclicProjection

theorem OAI.CirculantHadamard.cyclicProjection_norm line 118

Source documentation

A scalar convolution norm descends to the quotient cyclic group.

theorem cyclicProjection_norm (h : m ∣ n) {F : Elem R n} {r : R}
    (hnorm : F * ringStar F = scalar n r) :
    cyclicProjection R h F * ringStar (cyclicProjection R h F) = scalar m r := by
…