RegularRepresentation.lean`

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The regular representation on square-summable functions.

abbrev OAI.TorsionFreeBass.Regular.Hilbert line 12
Source documentation
Square-summable functions on the discrete group.
```
abbrev Hilbert (G : Type*) := lp (fun _ : G => ℂ) 2
```
def OAI.TorsionFreeBass.Regular.permute line 15
Source documentation
Permuting coordinates is unitary on ℓ², including for arbitrary index sets.
```
def permute {X : Type*} (s : Equiv.Perm X) : Hilbert X ≃ₗᵢ[ℂ] Hilbert X where
…
```
Mentions: OAI.TorsionFreeBass.Regular.Hilbert
lemma OAI.TorsionFreeBass.Regular.permute_apply line 29
def OAI.TorsionFreeBass.Regular.leftShift line 34
def OAI.TorsionFreeBass.Regular.rightShift line 35
lemma OAI.TorsionFreeBass.Regular.leftShift_apply line 37
lemma OAI.TorsionFreeBass.Regular.rightShift_apply line 39
lemma OAI.TorsionFreeBass.Regular.left_right_commute line 42
lemma OAI.TorsionFreeBass.Regular.rightShift_inv line 47
def OAI.TorsionFreeBass.Regular.leftRegular line 53
Source documentation
The left regular representation by bounded operators.
```
def leftRegular : G →* (Hilbert G →L[ℂ] Hilbert G) where
…
```
Mentions: OAI.TorsionFreeBass.Regular.Hilbert
lemma OAI.TorsionFreeBass.Regular.leftRegular_apply line 58
def OAI.TorsionFreeBass.Regular.convolution line 62
Source documentation
Convolution is the algebra homomorphism extending the left regular representation.
```
def convolution : MonoidAlgebra ℂ G →ₐ[ℂ] (Hilbert G →L[ℂ] Hilbert G) :=
…
```
Mentions: OAI.TorsionFreeBass.Regular.Hilbert
lemma OAI.TorsionFreeBass.Regular.convolution_apply line 65
lemma OAI.TorsionFreeBass.Regular.convolution_rightShift line 69
def OAI.TorsionFreeBass.Regular.delta line 74
Source documentation
The usual delta functions.
```
def delta (g : G) : Hilbert G := lp.single 2 g 1
…
```
Mentions: OAI.TorsionFreeBass.Regular.Hilbert
lemma OAI.TorsionFreeBass.Regular.delta_apply line 77
lemma OAI.TorsionFreeBass.Regular.leftShift_delta line 80
lemma OAI.TorsionFreeBass.Regular.rightShift_delta line 84
lemma OAI.TorsionFreeBass.Regular.convolution_delta line 88
lemma OAI.TorsionFreeBass.Regular.inner_delta line 99
lemma OAI.TorsionFreeBass.Regular.trace_commute line 103
Source documentation
Traciality against a finite convolution operator follows just from right invariance.
```
lemma trace_commute (a : MonoidAlgebra ℂ G) (T : Hilbert G →L[ℂ] Hilbert G)
    (hT : ∀ g x, T (rightShift g x) = rightShift g (T x)) :
    T (convolution a (delta 1)) 1 = convolution a (T (delta 1)) 1 := by
…
```
Mentions: OAI.TorsionFreeBass.Regular.Hilbert, OAI.TorsionFreeBass.Regular.rightShift, OAI.TorsionFreeBass.Regular.convolution, OAI.TorsionFreeBass.Regular.delta
lemma OAI.TorsionFreeBass.Regular.projection_rightShift line 129
Source documentation
A right-translation-invariant closed subspace has a right-invariant orthogonal projection.
```
lemma projection_rightShift (M : Submodule ℂ (Hilbert G)) [M.HasOrthogonalProjection]
    (hM : ∀ g x, x ∈ M → rightShift g x ∈ M) (g : G) (x : Hilbert G) :
    M.starProjection (rightShift g x) = rightShift g (M.starProjection x) := by
…
```
Mentions: OAI.TorsionFreeBass.Regular.Hilbert, OAI.TorsionFreeBass.Regular.rightShift
theorem OAI.TorsionFreeBass.Regular.idempotent_eq_zero_of_coeff_one_eq_zero line 146
Source documentation
The coefficient trace detects zero idempotents in the complex group ring. We project onto the closed range of left convolution. This projection has the same coefficient trace as the idempotent, and its trace is faithful.
```
theorem idempotent_eq_zero_of_coeff_one_eq_zero (a : MonoidAlgebra ℂ G)
    (ha : a * a = a) (hzero : a.coeff 1 = 0) : a = 0 := by
…
```