TwistedRegular.lean

1 import PaperXI.CocycleCommutator
2 import Mathlib.Analysis.Complex.Basic
3 import Mathlib.LinearAlgebra.StdBasis
4 import Mathlib.LinearAlgebra.Basis.Basic
5 import Mathlib.Algebra.Algebra.Subalgebra.Basic
6 import Mathlib.LinearAlgebra.Dimension.Finite
7 
8 /-! The faithful twisted left regular operators for an arbitrary normalized
9 complex unit-valued cocycle. No finite-image hypothesis is used. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.TwistedRegular
13 
14 open CocycleCommutator
15 variable {A : Type*} [CommGroup A]
16 
17 /-- Twisted left translation on the space of complex functions. -/
18 def regular (c : Cocycle A ℂˣ) (a : A) : Module.End ℂ (A → ℂ) where
19   toFun f t := (c.coeff a (a⁻¹ * t) : ℂ) * f (a⁻¹ * t)
20   map_add' f g := by ext t; simp [mul_add]
21   map_smul' z f := by ext t; simp [mul_left_comm]
22 
23 @[simp] theorem regular_apply (c : Cocycle A ℂˣ) (a : A) (f : A → ℂ) (t : A) :
24     regular c a f t = (c.coeff a (a⁻¹ * t) : ℂ) * f (a⁻¹ * t) := rfl
25 
26 @[simp] theorem regular_one (c : Cocycle A ℂˣ) (hc : Normalized c) :
27     regular c 1 = 1 := by
28   ext f t
29   simp [hc.1]
30 
31 theorem regular_mul (c : Cocycle A ℂˣ) (a b : A) :
32     regular c a * regular c b = (c.coeff a b : ℂ) • regular c (a * b) := by
33   ext f t
34   have h := congrArg (fun z : ℂˣ => (z : ℂ)) (c.assoc a b ((a * b)⁻¹ * t))
35   simp only [Units.val_mul] at h
36   have hab : b * ((a * b)⁻¹ * t) = a⁻¹ * t := by simp [mul_assoc]
37   have harg : b⁻¹ * (a⁻¹ * t) = (a * b)⁻¹ * t := by simp [mul_assoc]
38   simp only [Module.End.mul_apply, regular_apply, LinearMap.smul_apply, Pi.smul_apply,
39     smul_eq_mul]
40   rw [hab] at h
41   rw [harg]
42   simpa [mul_assoc, mul_left_comm] using
43     congrArg (fun z : ℂ => z * f ((a * b)⁻¹ * t)) h.symm
44 
45 /-- The identity point mass. -/
46 def deltaOne : A → ℂ := by
47   classical
48   exact fun t => if t = 1 then 1 else 0
49 
50 @[simp] theorem regular_deltaOne [DecidableEq A] (c : Cocycle A ℂˣ) (hc : Normalized c) (a : A) :
51     regular c a deltaOne = Pi.single a 1 := by
52   classical
53   ext t
54   by_cases ht : t = a
55   · subst t
56     simp [deltaOne, hc.2]
57   · have hne : a⁻¹ * t ≠ 1 := by
58       intro h
59       apply ht
60       calc
61         t = a * (a⁻¹ * t) := by simp
62         _ = a := by rw [h, mul_one]
63     simp [deltaOne, hne, ht]
64 
65 /-- Evaluation on the identity point mass recovers all regular basis vectors. -/
66 def evaluateOne : Module.End ℂ (A → ℂ) →ₗ[ℂ] (A → ℂ) where
67   toFun T := T deltaOne
68   map_add' _ _ := rfl
69   map_smul' _ _ := rfl
70 
71 theorem regular_linearIndependent [Fintype A] (c : Cocycle A ℂˣ)
72     (hc : Normalized c) : LinearIndependent ℂ (regular c) := by
73   classical
74   apply LinearIndependent.of_comp (evaluateOne (A := A))
75   have heq : evaluateOne (A := A) ∘ regular c = ⇑(Pi.basisFun ℂ A) := by
76     funext a
77     exact (regular_deltaOne c hc a).trans (Pi.basisFun_apply ℂ A a).symm
78   rw [heq]
79   exact (Pi.basisFun ℂ A).linearIndependent
80 
81 end PaperXI.TwistedRegular

Back to source controls