BreakBridge.lean

1 import PaperXI.BreakTensorMap
2 import PaperXI.HeisenbergTensor
3 import PaperXI.CharacterGenerators
4 
5 /-! Finite break tensor bridges on the actual central quotient. The total
6 stabilizer phase is the product of the actual factor discrepancies. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.BreakBridge
10 
11 variable {ι Z : Type*} [Fintype ι] [CommGroup Z]
12 variable {H A V W : ι → Type*} [∀ i, Group (H i)] [∀ i, CommGroup (A i)]
13 variable [∀ i, AddCommGroup (V i)] [∀ i, Module ℂ (V i)]
14 variable [∀ i, AddCommGroup (W i)] [∀ i, Module ℂ (W i)]
15 
16 omit [Fintype ι] in
17 /-- The tensor map intertwines the retained center and all original factors. -/
18 theorem ambient_intertwines (ζ : Z →* ℂˣ)
19     (ρ : ∀ i, Representation ℂ (H i) (V i))
20     (σ : ∀ i, Representation ℂ (H i) (W i)) (U : ∀ i, V i ≃ₗ[ℂ] W i)
21     (hU : ∀ i h x, U i (ρ i h x) = σ i h (U i x))
22     (h : Z × (∀ i, H i)) (x : PiTensorProduct ℂ V) :
23     BreakTensorMap.tensor U (HeisenbergTensor.ambient ζ ρ h x) =
24       HeisenbergTensor.ambient ζ σ h (BreakTensorMap.tensor U x) := by
25   rcases h with ⟨z, h⟩
26   simp only [HeisenbergTensor.ambient_apply, map_smul]
27   rw [BreakTensorMap.intertwines ρ σ U hU]
28 
29 /-- The actual quotient descent, with no assumed quotient intertwining conclusion. -/
30 theorem quotient_intertwines (D : ∀ i, CentralExtension.Datum Z (H i) (A i))
31     (ζ : Z →* ℂˣ) (ρ : ∀ i, Representation ℂ (H i) (V i))
32     (σ : ∀ i, Representation ℂ (H i) (W i))
33     (hρ : ∀ i z, ρ i ((D i).i z) = (ζ z : ℂ) • LinearMap.id)
34     (hσ : ∀ i z, σ i ((D i).i z) = (ζ z : ℂ) • LinearMap.id)
35     (U : ∀ i, V i ≃ₗ[ℂ] W i)
36     (hU : ∀ i h x, U i (ρ i h x) = σ i h (U i x)) :
37     ∀ h x, BreakTensorMap.tensor U (HeisenbergTensor.descend D ζ ρ hρ h x) =
38       HeisenbergTensor.descend D ζ σ hσ h (BreakTensorMap.tensor U x) := by
39   apply BreakTensorMap.descends (CentralProduct.mk D) (CentralProduct.mk_surjective D)
40   intro h x
41   simpa only [HeisenbergTensor.descend_mk] using ambient_intertwines ζ ρ σ U hU h x
42 
43 variable {C : Type*} [Group C]
44 
45 /-- Agreement of the total phase on generators closes the tensor stabilizer action.
46 Individual factor phases may be nontrivial and cancel in their product. -/
47 theorem stabilizer_intertwines
48     (R : ∀ i, Representation ℂ C (V i)) (T : ∀ i, Representation ℂ C (W i))
49     (U : ∀ i, V i ≃ₗ[ℂ] W i) (δ : ι → C →* ℂˣ)
50     (hδ : ∀ i g x, U i (R i g x) = (δ i g : ℂ) • T i g (U i x))
51     (S : Set C) (hgen : Subgroup.closure S = ⊤)
52     (hphase : ∀ g ∈ S, ∏ i, δ i g = 1) :
53     ∀ g x, BreakTensorMap.tensor U (BreakTensorMap.stabilizer R g x) =
54       BreakTensorMap.stabilizer T g (BreakTensorMap.tensor U x) := by
55   have hone := CharacterGenerators.trivial (BreakTensorMap.productCharacter δ) S hgen hphase
56   intro g x
57   simpa only [hone g, Units.val_one, one_smul] using
58     BreakTensorMap.scalar_intertwines R T U δ hδ g x
59 
60 /-- Factorwise phase equality is a sufficient special case of total phase equality. -/
61 theorem stabilizer_intertwines_of_factor_phases
62     (R : ∀ i, Representation ℂ C (V i)) (T : ∀ i, Representation ℂ C (W i))
63     (U : ∀ i, V i ≃ₗ[ℂ] W i) (δ : ι → C →* ℂˣ)
64     (hδ : ∀ i g x, U i (R i g x) = (δ i g : ℂ) • T i g (U i x))
65     (S : Set C) (hgen : Subgroup.closure S = ⊤)
66     (hphase : ∀ i g, g ∈ S → δ i g = 1) :
67     ∀ g x, BreakTensorMap.tensor U (BreakTensorMap.stabilizer R g x) =
68       BreakTensorMap.stabilizer T g (BreakTensorMap.tensor U x) := by
69   apply stabilizer_intertwines R T U δ hδ S hgen
70   intro g hg
71   simp [hphase, hg]
72 
73 /-- Full finite-envelope endpoint once the honest actions implement the declared
74 actual automorphisms of the central quotient. These are lift-covariance hypotheses. -/
75 theorem semidirect_intertwines
76     (D : ∀ i, CentralExtension.Datum Z (H i) (A i))
77     (ζ : Z →* ℂˣ) (ρ : ∀ i, Representation ℂ (H i) (V i))
78     (σ : ∀ i, Representation ℂ (H i) (W i))
79     (hρ : ∀ i z, ρ i ((D i).i z) = (ζ z : ℂ) • LinearMap.id)
80     (hσ : ∀ i z, σ i ((D i).i z) = (ζ z : ℂ) • LinearMap.id)
81     (U : ∀ i, V i ≃ₗ[ℂ] W i)
82     (hU : ∀ i h x, U i (ρ i h x) = σ i h (U i x))
83     (α : C →* MulAut (CentralProduct.Group D))
84     (R : ∀ i, Representation ℂ C (V i)) (T : ∀ i, Representation ℂ C (W i))
85     (hR : ∀ g h x, BreakTensorMap.stabilizer R g (HeisenbergTensor.descend D ζ ρ hρ h x) =
86       HeisenbergTensor.descend D ζ ρ hρ (α g h) (BreakTensorMap.stabilizer R g x))
87     (hT : ∀ g h x, BreakTensorMap.stabilizer T g (HeisenbergTensor.descend D ζ σ hσ h x) =
88       HeisenbergTensor.descend D ζ σ hσ (α g h) (BreakTensorMap.stabilizer T g x))
89     (δ : ι → C →* ℂˣ)
90     (hδ : ∀ i g x, U i (R i g x) = (δ i g : ℂ) • T i g (U i x))
91     (S : Set C) (hgen : Subgroup.closure S = ⊤)
92     (hphase : ∀ g ∈ S, ∏ i, δ i g = 1) :
93     ∀ a x, BreakTensorMap.tensor U
94         (CyclicBridge.semidirectRepresentation α (HeisenbergTensor.descend D ζ ρ hρ)
95           (BreakTensorMap.stabilizer R) hR a x) =
96       CyclicBridge.semidirectRepresentation α (HeisenbergTensor.descend D ζ σ hσ)
97         (BreakTensorMap.stabilizer T) hT a (BreakTensorMap.tensor U x) := by
98   apply CyclicBridge.semidirect_intertwining α _ _ (BreakTensorMap.tensor U)
99   · simpa only [CyclicBridge.semidirectRepresentation_inl] using
100       quotient_intertwines D ζ ρ σ hρ hσ U hU
101   · simpa only [CyclicBridge.semidirectRepresentation_inr] using
102       stabilizer_intertwines R T U δ hδ S hgen hphase
103 
104 end PaperXI.BreakBridge

Back to source controls