BreakBridgeAlong.lean

1 import PaperXI.BreakBridge
2 import PaperXI.CentralProductMap
3 import PaperXI.HeisenbergTensorFactorization
4 
5 /-! Tensor bridges between different actual break extensions, with discrepancy
6 characters derived from the chosen honest stabilizer actions. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.BreakBridgeAlong
10 
11 variable {S Z C : Type*} [Fintype S] [CommGroup Z] [Group C]
12 variable {H A H' A' V W : S → Type*}
13 variable [∀ s, Group (H s)] [∀ s, CommGroup (A s)]
14 variable [∀ s, Group (H' s)] [∀ s, CommGroup (A' s)]
15 variable [∀ s, AddCommGroup (V s)] [∀ s, Module ℂ (V s)]
16 variable [∀ s, AddCommGroup (W s)] [∀ s, Module ℂ (W s)]
17 
18 /-- Actual group isomorphisms of the factors induce the tensor quotient bridge. -/
19 theorem quotient_intertwines
20     (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
21     (E : ∀ s, CentralExtension.Datum Z (H' s) (A' s))
22     (f : ∀ s, H s ≃* H' s) (hf : ∀ s z, f s ((D s).i z) = (E s).i z)
23     (ζ : Z →* ℂˣ) (ρ : ∀ s, Representation ℂ (H s) (V s))
24     (σ : ∀ s, Representation ℂ (H' s) (W s))
25     (hρ : ∀ s z, ρ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id)
26     (hσ : ∀ s z, σ s ((E s).i z) = (ζ z : ℂ) • LinearMap.id)
27     (U : ∀ s, V s ≃ₗ[ℂ] W s)
28     (hU : ∀ s h x, U s (ρ s h x) = σ s (f s h) (U s x))
29     (h : CentralProduct.Group D) (x : PiTensorProduct ℂ V) :
30     BreakTensorMap.tensor U (HeisenbergTensor.descend D ζ ρ hρ h x) =
31       HeisenbergTensor.descend E ζ σ hσ (CentralProduct.congr D E f hf h)
32         (BreakTensorMap.tensor U x) := by
33   obtain ⟨⟨z,h⟩, rfl⟩ := CentralProduct.mk_surjective D h
34   have he : (BreakTensorMap.tensor U).toLinearMap.comp (HeisenbergTensor.ambient ζ ρ (z,h)) =
35       (HeisenbergTensor.ambient ζ σ (z, fun s => f s (h s))).comp
36         (BreakTensorMap.tensor U).toLinearMap := by
37     apply PiTensorProduct.ext
38     ext v
39     simp [hU]
40   exact DFunLike.congr_fun he x
41 
42 /-- The factor discrepancies are produced by Schur from the actual lift
43 covariance. Only their product must vanish on generators. Finite dimensionality
44 is derived from the original Heisenberg representations. -/
45 theorem source [∀ s, Fintype (A s)]
46     (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
47     (E : ∀ s, CentralExtension.Datum Z (H' s) (A' s))
48     (f : ∀ s, H s ≃* H' s) (hf : ∀ s z, f s ((D s).i z) = (E s).i z)
49     (ζ : Z →* ℂˣ)
50     (hnd : ∀ s, CocycleCommutator.radical (CentralExtension.scalarCocycle (D s) ζ) = ⊥)
51     (ρ : ∀ s, Representation ℂ (H s) (V s)) [∀ s, Representation.IsIrreducible (ρ s)]
52     (σ : ∀ s, Representation ℂ (H' s) (W s))
53     (hρ : ∀ s z, ρ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id)
54     (hσ : ∀ s z, σ s ((E s).i z) = (ζ z : ℂ) • LinearMap.id)
55     (U : ∀ s, V s ≃ₗ[ℂ] W s)
56     (hU : ∀ s h x, U s (ρ s h x) = σ s (f s h) (U s x))
57     (α : ∀ s, C →* MulAut (H s))
58     (R : ∀ s, Representation ℂ C (V s)) (T : ∀ s, Representation ℂ C (W s))
59     (hR : ∀ s g h x, R s g (ρ s h x) = ρ s (α s g h) (R s g x))
60     (hT : ∀ s g h x, T s g (σ s (f s h) x) = σ s (f s (α s g h)) (T s g x))
61     (gens : Set C) (hgen : Subgroup.closure gens = ⊤) :
62     ∃ δ : S → C →* ℂˣ,
63       (∀ s g x, U s (R s g x) = (δ s g : ℂ) • T s g (U s x)) ∧
64       ((∀ g ∈ gens, ∏ s, δ s g = 1) →
65         (∀ h x, BreakTensorMap.tensor U (HeisenbergTensor.descend D ζ ρ hρ h x) =
66           HeisenbergTensor.descend E ζ σ hσ (CentralProduct.congr D E f hf h)
67             (BreakTensorMap.tensor U x)) ∧
68         (∀ g x, BreakTensorMap.tensor U (BreakTensorMap.stabilizer R g x) =
69           BreakTensorMap.stabilizer T g (BreakTensorMap.tensor U x))) := by
70   let : ∀ s, FiniteDimensional ℂ (V s) :=
71     HeisenbergTensor.factor_finiteDimensional D ζ hnd ρ hρ
72   have hd (s : S) : ∃ δ : C →* ℂˣ,
73       ∀ g x, U s (R s g x) = (δ g : ℂ) • T s g (U s x) :=
74     DiscrepancyCharacter.exists_character (ρ s) ((σ s).comp (f s).toMonoidHom)
75       (U s) (hU s) (α s) (R s) (T s) (hR s) (hT s)
76   choose δ hδ using hd
77   exact ⟨δ, hδ, fun hphase => ⟨quotient_intertwines D E f hf ζ ρ σ hρ hσ U hU,
78     BreakBridge.stabilizer_intertwines R T U δ hδ gens hgen hphase⟩⟩
79 
80 end PaperXI.BreakBridgeAlong

Back to source controls