TwistedRescaling.lean

1 import PaperXI.TwistedAction
2 import PaperXI.CocycleBasis
3 
4 /-! Actual algebra equivalences under normalized scalar changes of basis.
5 The equivalence is constructed from the canonical bases of the two concrete
6 twisted algebras; its multiplicativity follows from their proved tables. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.TwistedRescaling
10 
11 open CocycleCommutator Module
12 variable {A : Type*} [CommGroup A] [Fintype A]
13 
14 /-- Equality of cocycles transports the actual algebras and their bases. -/
15 def congrEquiv (c d : Cocycle A ℂˣ) (hc : Normalized c) (hd : Normalized d)
16     (h : c = d) : TwistedAlgebra.Algebra c hc ≃ₐ[ℂ] TwistedAlgebra.Algebra d hd := by
17   cases h
18   exact AlgEquiv.refl
19 
20 @[simp] theorem congrEquiv_basis (c d : Cocycle A ℂˣ)
21     (hc : Normalized c) (hd : Normalized d) (h : c = d) (a : A) :
22     congrEquiv c d hc hd h (TwistedAlgebra.basis c hc a) =
23       TwistedAlgebra.basis d hd a := by
24   cases h
25   rfl
26 
27 /-- The constructed linear equivalence sends each rescaled algebra basis
28 element to the corresponding scalar multiple in the original algebra. -/
29 def linearEquiv (c : Cocycle A ℂˣ) (hc : Normalized c)
30     (s : A → ℂˣ) (hs : s 1 = 1) :
31     TwistedAlgebra.Algebra (rescale c s) (normalized_rescale c hc s hs) ≃ₗ[ℂ]
32       TwistedAlgebra.Algebra c hc :=
33   (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs)).equiv
34     ((TwistedAlgebra.basis c hc).unitsSMul s) (Equiv.refl A)
35 
36 @[simp] theorem linearEquiv_basis (c : Cocycle A ℂˣ) (hc : Normalized c)
37     (s : A → ℂˣ) (hs : s 1 = 1) (a : A) :
38     linearEquiv c hc s hs
39       (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs) a) =
40         (s a : ℂ) • TwistedAlgebra.basis c hc a := by
41   simp only [linearEquiv, Basis.equiv_apply, Equiv.refl_apply,
42     Basis.unitsSMul_apply, Units.smul_def]
43 
44 set_option backward.isDefEq.respectTransparency false in
45 /-- The rescaled basis obeys the rescaled cocycle's multiplication table. -/
46 theorem scaled_basis_mul (c : Cocycle A ℂˣ) (hc : Normalized c)
47     (s : A → ℂˣ) (a b : A) :
48     ((s a : ℂ) • TwistedAlgebra.basis c hc a) *
49       ((s b : ℂ) • TwistedAlgebra.basis c hc b) =
50         ((rescale c s).coeff a b : ℂ) •
51           ((s (a * b) : ℂ) • TwistedAlgebra.basis c hc (a * b)) := by
52   have h := rescaled_basis_mul (B := TwistedAlgebra.Algebra c hc) c
53     (TwistedAlgebra.basis c hc) (TwistedAlgebra.basis_mul c hc) s a b
54   simpa only [Basis.unitsSMul_apply, Units.smul_def] using h
55 
56 theorem linearEquiv_one (c : Cocycle A ℂˣ) (hc : Normalized c)
57     (s : A → ℂˣ) (hs : s 1 = 1) : linearEquiv c hc s hs 1 = 1 := by
58   rw [← TwistedAlgebra.basis_one (rescale c s) (normalized_rescale c hc s hs),
59     linearEquiv_basis, hs, Units.val_one, one_smul, TwistedAlgebra.basis_one]
60 
61 theorem linearEquiv_mul (c : Cocycle A ℂˣ) (hc : Normalized c)
62     (s : A → ℂˣ) (hs : s 1 = 1)
63     (x y : TwistedAlgebra.Algebra (rescale c s) (normalized_rescale c hc s hs)) :
64     linearEquiv c hc s hs (x * y) =
65       linearEquiv c hc s hs x * linearEquiv c hc s hs y := by
66   classical
67   have hBasis (a b : A) :
68       linearEquiv c hc s hs
69         (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs) a *
70           TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs) b) =
71         linearEquiv c hc s hs
72           (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs) a) *
73         linearEquiv c hc s hs
74           (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs) b) := by
75     rw [TwistedAlgebra.basis_mul, map_smul, linearEquiv_basis,
76       linearEquiv_basis, linearEquiv_basis, scaled_basis_mul]
77   conv_lhs => rw [← (TwistedAlgebra.basis (rescale c s)
78       (normalized_rescale c hc s hs)).sum_repr x,
79     ← (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs)).sum_repr y]
80   conv_rhs => rw [← (TwistedAlgebra.basis (rescale c s)
81       (normalized_rescale c hc s hs)).sum_repr x,
82     ← (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs)).sum_repr y]
83   simp only [Finset.sum_mul, Finset.mul_sum, map_sum, map_smul,
84     smul_mul_assoc, mul_smul_comm, hBasis]
85 
86 /-- The actual twisted algebras of cohomologous normalized cocycles are
87 isomorphic, with the source-to-target direction matching basis rescaling. -/
88 def rescaleEquiv (c : Cocycle A ℂˣ) (hc : Normalized c)
89     (s : A → ℂˣ) (hs : s 1 = 1) :
90     TwistedAlgebra.Algebra (rescale c s) (normalized_rescale c hc s hs) ≃ₐ[ℂ]
91       TwistedAlgebra.Algebra c hc :=
92   AlgEquiv.ofLinearEquiv (linearEquiv c hc s hs)
93     (linearEquiv_one c hc s hs) (linearEquiv_mul c hc s hs)
94 
95 @[simp] theorem rescaleEquiv_basis (c : Cocycle A ℂˣ) (hc : Normalized c)
96     (s : A → ℂˣ) (hs : s 1 = 1) (a : A) :
97     rescaleEquiv c hc s hs
98       (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs) a) =
99         (s a : ℂ) • TwistedAlgebra.basis c hc a :=
100   linearEquiv_basis c hc s hs a
101 
102 /-- The inverse sends an original basis vector to its inverse scalar multiple. -/
103 @[simp] theorem rescaleEquiv_symm_basis (c : Cocycle A ℂˣ) (hc : Normalized c)
104     (s : A → ℂˣ) (hs : s 1 = 1) (a : A) :
105     (rescaleEquiv c hc s hs).symm (TwistedAlgebra.basis c hc a) =
106       ((s a)⁻¹ : ℂˣ) •
107         TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs) a := by
108   apply (rescaleEquiv c hc s hs).injective
109   simp only [AlgEquiv.apply_symm_apply, Units.smul_def, map_smul,
110     rescaleEquiv_basis, smul_smul]
111   simp
112 
113 variable {B : Type*} [Semiring B] [Algebra ℂ B]
114 
115 /-- Transport any algebra action through the constructed rescaling map. -/
116 def transport (c : Cocycle A ℂˣ) (hc : Normalized c)
117     (s : A → ℂˣ) (hs : s 1 = 1)
118     (F : TwistedAlgebra.Algebra c hc →ₐ[ℂ] B) :
119     TwistedAlgebra.Algebra (rescale c s) (normalized_rescale c hc s hs) →ₐ[ℂ] B :=
120   F.comp (rescaleEquiv c hc s hs).toAlgHom
121 
122 @[simp] theorem transport_basis (c : Cocycle A ℂˣ) (hc : Normalized c)
123     (s : A → ℂˣ) (hs : s 1 = 1)
124     (F : TwistedAlgebra.Algebra c hc →ₐ[ℂ] B) (a : A) :
125     transport c hc s hs F
126       (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs) a) =
127         (s a : ℂ) • F (TwistedAlgebra.basis c hc a) := by
128   simp only [transport, AlgHom.comp_apply, AlgEquiv.coe_toAlgHom, rescaleEquiv_basis, map_smul]
129 
130 /-- A transported action is determined by the rescaled basis operators. -/
131 theorem transport_unique (c : Cocycle A ℂˣ) (hc : Normalized c)
132     (s : A → ℂˣ) (hs : s 1 = 1)
133     (F : TwistedAlgebra.Algebra c hc →ₐ[ℂ] B)
134     (G : TwistedAlgebra.Algebra (rescale c s) (normalized_rescale c hc s hs) →ₐ[ℂ] B)
135     (hG : ∀ a, G (TwistedAlgebra.basis (rescale c s)
136       (normalized_rescale c hc s hs) a) =
137         (s a : ℂ) • F (TwistedAlgebra.basis c hc a)) :
138     G = transport c hc s hs F := by
139   apply AlgHom.toLinearMap_injective
140   apply (TwistedAlgebra.basis (rescale c s) (normalized_rescale c hc s hs)).ext
141   intro a
142   exact (hG a).trans (transport_basis c hc s hs F a).symm
143 
144 /-- Rescaling induces an equivalence on actual algebra actions. -/
145 def actionEquiv (c : Cocycle A ℂˣ) (hc : Normalized c)
146     (s : A → ℂˣ) (hs : s 1 = 1) :
147     (TwistedAlgebra.Algebra c hc →ₐ[ℂ] B) ≃
148       (TwistedAlgebra.Algebra (rescale c s) (normalized_rescale c hc s hs) →ₐ[ℂ] B) where
149   toFun := transport c hc s hs
150   invFun F := F.comp (rescaleEquiv c hc s hs).symm.toAlgHom
151   left_inv F := by
152     ext x
153     exact congrArg F ((rescaleEquiv c hc s hs).apply_symm_apply x)
154   right_inv F := by
155     ext x
156     exact congrArg F ((rescaleEquiv c hc s hs).symm_apply_apply x)
157 
158 end PaperXI.TwistedRescaling

Back to source controls