CharacterTwist.lean

1 import PaperXI.CyclicInducedCoordinates
2 
3 /-! Scalar twisting and its literal tensor comparison. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.CharacterTwist
7 open scoped TensorProduct
8 variable {G V W : Type*} [Group G]
9 variable [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
10 
11 def twist (ν : G →* ℂˣ) (ρ : Representation ℂ G V) : Representation ℂ G V where
12   toFun g := (ν g : ℂ) • ρ g
13   map_one' := by simp
14   map_mul' g h := by ext x; simp [smul_smul, mul_comm]
15 
16 @[simp] theorem twist_apply (ν : G →* ℂˣ) (ρ : Representation ℂ G V) (g : G) (v : V) :
17     twist ν ρ g v = (ν g : ℂ) • ρ g v := rfl
18 
19 /-- An actual tensor with a one-dimensional representation is the scalar twist. -/
20 def tensorEquiv (ν : G →* ℂˣ) (ρ : Representation ℂ G V) :
21     Representation.Equiv (ρ.tprod (CyclicInduced.scalar ν)) (twist ν ρ) :=
22   Representation.Equiv.mk (TensorProduct.rid ℂ V) (fun g => by
23     ext v
24     simp [CyclicInduced.scalar_apply, twist, mul_comm])
25 
26 /-- Scalar twisting preserves intertwining equivalences. -/
27 def mapEquiv (ν : G →* ℂˣ) {ρ : Representation ℂ G V} {σ : Representation ℂ G W}
28     (e : Representation.Equiv ρ σ) : Representation.Equiv (twist ν ρ) (twist ν σ) :=
29   Representation.Equiv.mk e.toLinearEquiv (fun g => by
30     ext v
31     change e ((ν g : ℂ) • ρ g v) = (ν g : ℂ) • σ g (e v)
32     rw [map_smul]
33     congr 1
34     exact LinearMap.congr_fun (e.isIntertwining' g) v)
35 
36 /-- A character trivial on a subgroup leaves its restricted action unchanged. -/
37 theorem restrict_eq (ν : G →* ℂˣ) (ρ : Representation ℂ G V) (I : Subgroup G)
38     (hν : ∀ i : I, ν i = 1) : (twist ν ρ).comp I.subtype = ρ.comp I.subtype := by
39   ext i v
40   simp [twist_apply, hν]
41 
42 theorem power_action (ν : G →* ℂˣ) (ρ : Representation ℂ G V) (g : G) (n : ℕ) (v : V) :
43     twist ν ρ (g ^ n) v = (ν g : ℂ) ^ n • ρ (g ^ n) v := by
44   change (ν (g ^ n) : ℂ) • ρ (g ^ n) v = _
45   simp only [map_pow, Units.val_pow_eq_pow_val]
46 
47 /-- The closed-cycle multiplier follows from the character power law. -/
48 theorem closing_scalar (ν : G →* ℂˣ) (ρ : Representation ℂ G V)
49     (φ : G) (n : ℕ) (v : V) (a : ℂ)
50     (hreturn : ρ (φ ^ n) v = a • v) :
51     twist ν ρ (φ ^ n) v = (a * (ν φ : ℂ) ^ n) • v := by
52   rw [power_action, hreturn, smul_smul, mul_comm]
53 
54 end PaperXI.CharacterTwist

Back to source controls