TensorSlices107.lean

1 import Mathlib.LinearAlgebra.TensorProduct.Basis
2 import Mathlib.LinearAlgebra.Dual.Lemmas
3 
4 /-! Slice an actual tensor operator and reconstruct it when all its first-factor
5 slices belong to one nonzero line. No invertibility of that line's generator,
6 and no finite-dimensionality of either carrier, is assumed. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.TensorSlices107
10 open scoped TensorProduct
11 variable {k W U : Type*} [Field k] [AddCommGroup W] [Module k W]
12   [AddCommGroup U] [Module k U]
13 
14 def right (φ : Module.Dual k U) : W ⊗[k] U →ₗ[k] W :=
15   (TensorProduct.rid k W).toLinearMap.comp (TensorProduct.map LinearMap.id φ)
16 
17 def left (ℓ : Module.Dual k W) : W ⊗[k] U →ₗ[k] U :=
18   (TensorProduct.lid k U).toLinearMap.comp (TensorProduct.map ℓ LinearMap.id)
19 
20 @[simp] theorem right_tmul (φ : Module.Dual k U) (w : W) (u : U) :
21     right φ (w ⊗ₜ[k] u) = φ u • w := by simp [right]
22 
23 @[simp] theorem left_tmul (ℓ : Module.Dual k W) (w : W) (u : U) :
24     left ℓ (w ⊗ₜ[k] u) = ℓ w • u := by simp [left]
25 
26 theorem right_ext {s t : W ⊗[k] U}
27     (h : ∀ φ : Module.Dual k U, right φ s = right φ t) : s = t := by
28   classical
29   let b := Module.Free.chooseBasis k U
30   apply (TensorProduct.equivFinsuppOfBasisRight b).injective
31   ext i
32   simpa only [TensorProduct.equivFinsuppOfBasisRight_apply,
33     LinearMap.lTensor_def, right, LinearMap.comp_apply, LinearEquiv.coe_coe] using h (b.coord i)
34 
35 theorem contractions_commute (ℓ : Module.Dual k W) (φ : Module.Dual k U)
36     (t : W ⊗[k] U) : φ (left ℓ t) = ℓ (right φ t) := by
37   induction t using TensorProduct.induction_on with
38   | zero => simp
39   | add x y hx hy => simp [hx, hy]
40   | tmul w u => simp [mul_comm]
41 
42 theorem right_map (φ : Module.Dual k U) (A : W →ₗ[k] W) (t : W ⊗[k] U) :
43     right φ (TensorProduct.map A LinearMap.id t) = A (right φ t) := by
44   induction t using TensorProduct.induction_on with
45   | zero => simp
46   | add x y hx hy => simp [hx, hy]
47   | tmul w u => simp
48 
49 def slice (T : W ⊗[k] U →ₗ[k] W ⊗[k] U) (u : U) (φ : Module.Dual k U) :
50     W →ₗ[k] W :=
51   (right φ).comp (T.comp ((TensorProduct.mk k W U).flip u))
52 
53 @[simp] theorem slice_apply (T : W ⊗[k] U →ₗ[k] W ⊗[k] U)
54     (u : U) (φ : Module.Dual k U) (w : W) :
55     slice T u φ w = right φ (T (w ⊗ₜ[k] u)) := rfl
56 
57 theorem exists_nonzero_slice (T : W ⊗[k] U →ₗ[k] W ⊗[k] U) (hT : T ≠ 0) :
58     ∃ u φ, slice T u φ ≠ 0 := by
59   classical
60   by_contra h
61   push Not at h
62   apply hT
63   ext w u
64   apply right_ext
65   intro φ
66   have hs := LinearMap.congr_fun (h u φ) w
67   simpa using hs
68 
69 /-- A nonzero first-factor map need not be invertible: one separating functional
70 on one nonzero value suffices to recover the entire second-factor operator. -/
71 theorem factor_of_slice_line (T : W ⊗[k] U →ₗ[k] W ⊗[k] U)
72     (S : W →ₗ[k] W) (hS : S ≠ 0)
73     (hline : ∀ u φ, ∃ c : k, slice T u φ = c • S) :
74     ∃ R : U →ₗ[k] U, T = TensorProduct.map S R := by
75   classical
76   obtain ⟨w₀, hw₀⟩ : ∃ w₀, S w₀ ≠ 0 := by
77     by_contra h
78     push Not at h
79     exact hS (LinearMap.ext h)
80   obtain ⟨ℓ, hℓ⟩ := Module.Projective.exists_dual_eq_one k hw₀
81   let R := (left ℓ).comp (T.comp (TensorProduct.mk k W U w₀))
82   refine ⟨R, ?_⟩
83   ext w u
84   apply right_ext
85   intro φ
86   obtain ⟨c, hc⟩ := hline u φ
87   have hcw := LinearMap.congr_fun hc w
88   have hc₀ := LinearMap.congr_fun hc w₀
89   have hR : φ (R u) = c := by
90     change φ (left ℓ (T (w₀ ⊗ₜ[k] u))) = c
91     rw [contractions_commute]
92     change ℓ (slice T u φ w₀) = c
93     rw [hc]
94     simp [hℓ]
95   simpa [hR] using hcw
96 
97 theorem tmul_left_injective (w : W) (hw : w ≠ 0) :
98     Function.Injective (fun u : U => w ⊗ₜ[k] u) := by
99   obtain ⟨ℓ, hℓ⟩ := Module.Projective.exists_dual_eq_one k hw
100   intro u v h
101   have he := congrArg (left ℓ) h
102   simpa [hℓ] using he
103 
104 theorem map_left_injective (S : W →ₗ[k] W) (hS : S ≠ 0) :
105     Function.Injective (fun R : U →ₗ[k] U => TensorProduct.map S R) := by
106   obtain ⟨w, hw⟩ : ∃ w, S w ≠ 0 := by
107     by_contra h
108     push Not at h
109     exact hS (LinearMap.ext h)
110   intro R R' h
111   ext u
112   apply tmul_left_injective (k := k) (S w) hw
113   simpa using LinearMap.congr_fun h (w ⊗ₜ[k] u)
114 
115 end PaperXI.TensorSlices107

Back to source controls