TensorTypeOperators70.lean

1 import PaperXI.InducedTypeSpace68
2 import Mathlib.RingTheory.TensorProduct.Maps
3 import Mathlib.LinearAlgebra.Dual.Lemmas
4 
5 /-! Faithful first-factor operator realization in the literal inducing-type image.
6 The multiplicity space must be nonzero. Neither tensor amplification nor the
7 ambient induced space is silently identified with the first-factor carrier. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.TensorTypeOperators70
11 open Representation
12 open scoped TensorProduct
13 variable {k W U G : Type*} [Field k] [AddCommGroup W] [Module k W]
14   [AddCommGroup U] [Module k U] [Group G]
15 
16 /-- First-factor amplification is an actual unital algebra homomorphism. -/
17 def amplify : Module.End k W →ₐ[k] Module.End k (W ⊗[k] U) :=
18   Module.End.rTensorAlgHom k W U
19 
20 @[simp] theorem amplify_tmul (B : Module.End k W) (w : W) (u : U) :
21     amplify (U := U) B (w ⊗ₜ[k] u) = B w ⊗ₜ[k] u := rfl
22 
23 /-- A nonzero multiplicity factor prevents loss of first-factor operators. -/
24 theorem amplify_injective [Nontrivial U] :
25     Function.Injective (amplify (k := k) (W := W) (U := U)) := by
26   obtain ⟨u, hu⟩ := exists_ne (0 : U)
27   obtain ⟨φ, hφ⟩ := Module.Projective.exists_dual_eq_one k hu
28   intro A B h
29   ext w
30   have he := congrArg (fun T : Module.End k (W ⊗[k] U) =>
31     (TensorProduct.rid k W) (TensorProduct.map LinearMap.id φ (T (w ⊗ₜ[k] u)))) h
32   simpa [hφ] using he
33 
34 variable (H : Subgroup G) (Λ : Representation k H (W ⊗[k] U))
35 
36 /-- The prescribed first-factor algebra inside the actual canonical type image. -/
37 def realize : Module.End k W →ₐ[k]
38     Module.End k (InducedTypeSpace68.typeSpace H Λ) :=
39   (InducedTypeSpace68.typeOperators H Λ).toAlgHom.comp amplify
40 
41 @[simp] theorem realize_tmul (B : Module.End k W) (w : W) (u : U) :
42     realize H Λ B (InducedTypeSpace68.typeEquiv H Λ (w ⊗ₜ[k] u)) =
43       InducedTypeSpace68.typeEquiv H Λ (B w ⊗ₜ[k] u) := by
44   change (InducedTypeSpace68.typeEquiv H Λ)
45     (amplify B ((InducedTypeSpace68.typeEquiv H Λ).symm
46       (InducedTypeSpace68.typeEquiv H Λ (w ⊗ₜ[k] u)))) = _
47   rw [LinearEquiv.symm_apply_apply, amplify_tmul]
48 
49 /-- The complete first-factor operator, not just its trace, is retained. -/
50 theorem realize_injective [Nontrivial U] : Function.Injective (realize H Λ) :=
51   (InducedTypeSpace68.typeOperators H Λ).injective.comp amplify_injective
52 
53 @[simp] theorem realize_eq_iff [Nontrivial U] (A B : Module.End k W) :
54     realize H Λ A = realize H Λ B ↔ A = B := (realize_injective H Λ).eq_iff
55 
56 @[simp] theorem realize_zero_iff [Nontrivial U] (A : Module.End k W) :
57     realize H Λ A = 0 ↔ A = 0 := by
58   rw [← map_zero (realize H Λ), realize_eq_iff]
59 
60 /-- Full operator residuals are preserved and reflected. -/
61 theorem residual_zero_iff [Nontrivial U] (A B : Module.End k W) :
62     realize H Λ A - realize H Λ B = 0 ↔ A - B = 0 := by
63   rw [sub_eq_zero, sub_eq_zero, realize_eq_iff]
64 
65 /-- Idempotence is not weakened to a scalar or character condition. -/
66 theorem projector_iff [Nontrivial U] (P : Module.End k W) :
67     realize H Λ P * realize H Λ P = realize H Λ P ↔ P * P = P := by
68   rw [← map_mul, realize_eq_iff]
69 
70 /-- Both orders of composition are transported literally. -/
71 theorem intertwining_iff [Nontrivial U] (A B T : Module.End k W) :
72     realize H Λ T * realize H Λ A = realize H Λ B * realize H Λ T ↔
73       T * A = B * T := by
74   rw [← map_mul, ← map_mul, realize_eq_iff]
75 
76 /-- Any finite word of full packet operators has the same realized product. -/
77 theorem word_product (xs : List (Module.End k W)) :
78     (xs.map (realize H Λ)).prod = realize H Λ xs.prod := by
79   induction xs with
80   | nil => simp
81   | cons A xs ih => simp [ih]
82 
83 /-- Zero holonomy is reflected as well as preserved, including the empty word. -/
84 theorem holonomy_iff [Nontrivial U] (xs : List (Module.End k W)) :
85     (xs.map (realize H Λ)).prod = 1 ↔ xs.prod = 1 := by
86   rw [word_product, ← map_one (realize H Λ), realize_eq_iff]
87 
88 /-- Finite weighted projectors commute with the realization map. -/
89 theorem weighted_sum {I : Type*} (s : Finset I) (c : I → k)
90     (A : I → Module.End k W) :
91     realize H Λ (∑ i ∈ s, c i • A i) = ∑ i ∈ s, c i • realize H Λ (A i) := by
92   simp only [map_sum, map_smul]
93 
94 end PaperXI.TensorTypeOperators70

Back to source controls