BreakTensorMap.lean

1 import PaperXI.FiniteTensor
2 
3 /-! Actual finite tensor maps of the supplied break intertwiners. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.BreakTensorMap
7 
8 variable {ι K : Type*} [Field K] {H V W : ι → Type*}
9 variable [∀ i, Monoid (H i)]
10 variable [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
11 variable [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
12 
13 /-- The tensor bridge is an actual invertible map of multiple tensor products. -/
14 def tensor (U : ∀ i, V i ≃ₗ[K] W i) :
15     PiTensorProduct K V ≃ₗ[K] PiTensorProduct K W := PiTensorProduct.congr U
16 
17 @[simp] theorem tensor_tprod (U : ∀ i, V i ≃ₗ[K] W i) (v : ∀ i, V i) :
18     tensor U (PiTensorProduct.tprod K v) =
19       PiTensorProduct.tprod K (fun i => U i (v i)) :=
20   PiTensorProduct.congr_tprod U v
21 
22 @[simp] theorem tensor_symm_tprod (U : ∀ i, V i ≃ₗ[K] W i) (w : ∀ i, W i) :
23     (tensor U).symm (PiTensorProduct.tprod K w) =
24       PiTensorProduct.tprod K (fun i => (U i).symm (w i)) :=
25   PiTensorProduct.congr_symm_tprod U w
26 
27 theorem tensor_symm (U : ∀ i, V i ≃ₗ[K] W i) :
28     (tensor U).symm = tensor (fun i => (U i).symm) := by
29   apply LinearEquiv.toLinearMap_injective
30   apply PiTensorProduct.ext
31   ext v
32   simp
33 
34 /-- Actual factor covariance extends by the tensor universal property. -/
35 theorem intertwines (ρ : ∀ i, Representation K (H i) (V i))
36     (σ : ∀ i, Representation K (H i) (W i)) (U : ∀ i, V i ≃ₗ[K] W i)
37     (hU : ∀ i h x, U i (ρ i h x) = σ i h (U i x))
38     (h : ∀ i, H i) (x : PiTensorProduct K V) :
39     tensor U (FiniteTensor.representation ρ h x) =
40       FiniteTensor.representation σ h (tensor U x) := by
41   have he : (tensor U).toLinearMap.comp (FiniteTensor.representation ρ h) =
42       (FiniteTensor.representation σ h).comp (tensor U).toLinearMap := by
43     apply PiTensorProduct.ext
44     ext v
45     simp [hU]
46   exact DFunLike.congr_fun he x
47 
48 /-- Covariance passes through any actual surjective quotient map. -/
49 theorem descends {P Q X Y : Type*} [Monoid P] [Monoid Q]
50     [AddCommGroup X] [Module K X] [AddCommGroup Y] [Module K Y]
51     (q : P →* Q) (hq : Function.Surjective q)
52     (ρ : Representation K Q X) (σ : Representation K Q Y) (U : X ≃ₗ[K] Y)
53     (hU : ∀ p x, U (ρ (q p) x) = σ (q p) (U x)) :
54     ∀ g x, U (ρ g x) = σ g (U x) := by
55   intro g x
56   obtain ⟨p, rfl⟩ := hq g
57   exact hU p x
58 
59 variable {C : Type*} [Monoid C]
60 
61 /-- The common stabilizer acts on every break at once. -/
62 def stabilizer (R : ∀ i, Representation K C (V i)) :
63     Representation K C (PiTensorProduct K V) :=
64   (FiniteTensor.representation R).comp (MonoidHom.pi (fun _ => MonoidHom.id C))
65 
66 @[simp] theorem stabilizer_tprod (R : ∀ i, Representation K C (V i))
67     (g : C) (v : ∀ i, V i) :
68     stabilizer R g (PiTensorProduct.tprod K v) =
69       PiTensorProduct.tprod K (fun i => R i g (v i)) := by
70   exact FiniteTensor.representation_tprod R (fun _ => g) v
71 
72 /-- Factor discrepancies multiply to the actual total discrepancy. -/
73 def productCharacter [Fintype ι] (δ : ι → C →* Kˣ) : C →* Kˣ where
74   toFun g := ∏ i, δ i g
75   map_one' := by simp
76   map_mul' g h := by simp [Finset.prod_mul_distrib]
77 
78 @[simp] theorem productCharacter_apply [Fintype ι] (δ : ι → C →* Kˣ) (g : C) :
79     productCharacter δ g = ∏ i, δ i g := rfl
80 
81 /-- The total discrepancy permits nontrivial break characters to cancel. -/
82 theorem scalar_intertwines [Fintype ι]
83     (R : ∀ i, Representation K C (V i)) (T : ∀ i, Representation K C (W i))
84     (U : ∀ i, V i ≃ₗ[K] W i) (δ : ι → C →* Kˣ)
85     (hδ : ∀ i g x, U i (R i g x) = (δ i g : K) • T i g (U i x))
86     (g : C) (x : PiTensorProduct K V) :
87     tensor U (stabilizer R g x) =
88       (productCharacter δ g : K) • stabilizer T g (tensor U x) := by
89   have he : (tensor U).toLinearMap.comp (stabilizer R g) =
90       (productCharacter δ g : K) • ((stabilizer T g).comp (tensor U).toLinearMap) := by
91     apply PiTensorProduct.ext
92     ext v
93     simp only [LinearMap.compMultilinearMap_apply, LinearMap.comp_apply,
94       LinearEquiv.coe_coe, stabilizer_tprod, tensor_tprod, LinearMap.smul_apply, hδ]
95     simpa [productCharacter_apply] using
96       (PiTensorProduct.tprod K (s := W)).map_smul_univ (fun i => (δ i g : K))
97         (fun i => T i g (U i (v i)))
98   exact DFunLike.congr_fun he x
99 
100 end PaperXI.BreakTensorMap

Back to source controls