MonomialAction.lean

1 import Mathlib.RepresentationTheory.Basic
2 import Mathlib.LinearAlgebra.Basis.Defs
3 import Mathlib.LinearAlgebra.TensorProduct.Basis
4 import Mathlib.Analysis.Complex.Basic
5 
6 /-! Actual monomial actions on a supplied basis. The scalar cocycle laws are
7 proved from an honest representation, then reused to construct orbit actions. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.MonomialAction
11 
12 variable {G X V : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
13 variable (b : Module.Basis X ℂ V) (p : G →* Equiv.Perm X) (c : G → X → ℂˣ)
14 
15 /-- The actual operator specified on the basis, extended linearly. -/
16 def operator (g : G) : Module.End ℂ V := b.constr ℂ (fun x => (c g x : ℂ) • b (p g x))
17 
18 @[simp] theorem operator_basis (g : G) (x : X) :
19     operator b p c g (b x) = (c g x : ℂ) • b (p g x) := b.constr_basis ℂ _ x
20 
21 /-- Honest multiplication on the basis gives an honest representation. -/
22 def representation (h1 : ∀ x, c 1 x = 1)
23     (hm : ∀ g h x, c (g*h) x = c g (p h x) * c h x) : Representation ℂ G V where
24   toFun := operator b p c
25   map_one' := by
26     apply b.ext
27     intro x
28     simp [h1]
29   map_mul' g h := by
30     apply b.ext
31     intro x
32     simp only [operator_basis, Module.End.mul_apply, map_smul, hm, Units.val_mul,
33       smul_smul, map_mul, Equiv.Perm.coe_mul]
34     rw [mul_comm (c g (p h x) : ℂ) (c h x : ℂ)]
35     rfl
36 
37 @[simp] theorem representation_basis (h1 : ∀ x, c 1 x = 1)
38     (hm : ∀ g h x, c (g*h) x = c g (p h x) * c h x) (g : G) (x : X) :
39     representation b p c h1 hm g (b x) = (c g x : ℂ) • b (p g x) := operator_basis b p c g x
40 
41 /-- Scalar cancellation on an actual nonzero basis vector. -/
42 theorem scalar_injective (x : X) {a d : ℂ} (h : a • b x = d • b x) : a = d := by
43   have hv := congrArg (fun v => b.repr v x) h
44   simpa using hv
45 
46 /-- The one law is derived from the supplied honest action. -/
47 theorem weight_one (ρ : Representation ℂ G V)
48     (hρ : ∀ g x, ρ g (b x) = (c g x : ℂ) • b (p g x)) (x : X) : c 1 x = 1 := by
49   apply Units.ext
50   apply scalar_injective b x
51   simpa using (hρ 1 x).symm
52 
53 /-- The cocycle law is derived from multiplication in the supplied action. -/
54 theorem weight_mul (ρ : Representation ℂ G V)
55     (hρ : ∀ g x, ρ g (b x) = (c g x : ℂ) • b (p g x)) (g h : G) (x : X) :
56     c (g*h) x = c g (p h x) * c h x := by
57   apply Units.ext
58   apply scalar_injective b (p (g*h) x)
59   rw [← hρ, map_mul, Module.End.mul_apply, hρ, map_smul, hρ]
60   simp [smul_smul, mul_comm]
61 
62 /-- The reconstructed action is the original action on every vector. -/
63 theorem representation_eq (ρ : Representation ℂ G V)
64     (hρ : ∀ g x, ρ g (b x) = (c g x : ℂ) • b (p g x)) :
65     representation b p c (weight_one b p c ρ hρ) (weight_mul b p c ρ hρ) = ρ := by
66   apply MonoidHom.ext
67   intro g
68   apply b.ext
69   intro x
70   rw [representation_basis]
71   exact (hρ g x).symm
72 
73 variable {Y W : Type*} [AddCommGroup W] [Module ℂ W]
74 
75 /-- The actual tensor basis carries the product permutation. -/
76 def tensorPermutation (q : G →* Equiv.Perm Y) : G →* Equiv.Perm (X × Y) where
77   toFun g := (p g).prodCongr (q g)
78   map_one' := by ext x <;> simp
79   map_mul' g h := by ext x <;> simp
80 
81 /-- The tensor coefficient is a product of the actual factor coefficients. -/
82 theorem tensor_basis (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
83     (d : Module.Basis Y ℂ W) (q : G →* Equiv.Perm Y) (w : G → Y → ℂˣ)
84     (hρ : ∀ g x, ρ g (b x) = (c g x : ℂ) • b (p g x))
85     (hσ : ∀ g y, σ g (d y) = (w g y : ℂ) • d (q g y)) (g : G) (x : X × Y) :
86     (ρ.tprod σ) g ((b.tensorProduct d) x) =
87       ((c g x.1 * w g x.2 : ℂˣ) : ℂ) •
88         (b.tensorProduct d) (tensorPermutation p q g x) := by
89   simp [Representation.tprod, Module.Basis.tensorProduct_apply', hρ, hσ,
90     tensorPermutation, TensorProduct.smul_tmul', TensorProduct.tmul_smul, smul_smul, mul_comm]
91 
92 end PaperXI.MonomialAction

Back to source controls