FullBridgeTransport.lean

1 import PaperXI.CyclicBridge
2 
3 /-! Actual semidirect and carrier transport of a finite bridge. These endpoints
4 connect the tensor model's normal and stabilizer equations to full operators. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.FullBridgeTransport
8 
9 variable {H H' C V W : Type*} [Group H] [Group H'] [Group C]
10 variable [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
11 
12 /-- Matching actual group lifts and both generator actions give a bridge for
13 all elements of the two isomorphic semidirect products. -/
14 theorem semidirect_along (e : H ≃* H')
15     (α : C →* MulAut H) (β : C →* MulAut H')
16     (he : ∀ g, (α g).trans e = e.trans (β g))
17     (ρ : Representation ℂ H V) (σ : Representation ℂ H' W)
18     (R : Representation ℂ C V) (T : Representation ℂ C W)
19     (hR : ∀ g h x, R g (ρ h x) = ρ (α g h) (R g x))
20     (hT : ∀ g h x, T g (σ h x) = σ (β g h) (T g x))
21     (U : V ≃ₗ[ℂ] W)
22     (hU : ∀ h x, U (ρ h x) = σ (e h) (U x))
23     (hC : ∀ g x, U (R g x) = T g (U x)) :
24     ∀ a x, U (CyclicBridge.semidirectRepresentation α ρ R hR a x) =
25       CyclicBridge.semidirectRepresentation β σ T hT
26         (SemidirectProduct.congr e (MulEquiv.refl C) he a) (U x) := by
27   intro a x
28   change U (ρ a.left (R a.right x)) = σ (e a.left) (T a.right (U x))
29   rw [hU, hC]
30 
31 variable {V₀ W₀ : Type*} [AddCommGroup V₀] [Module ℂ V₀]
32 variable [AddCommGroup W₀] [Module ℂ W₀]
33 
34 /-- Conjugating a model bridge by actual intertwining factorizations produces
35 a bridge of the declared representations on their original carrier spaces. -/
36 theorem through_factorizations (e : H →* H')
37     (ρ₀ : Representation ℂ H V₀) (σ₀ : Representation ℂ H' W₀)
38     (ρ : Representation ℂ H V) (σ : Representation ℂ H' W)
39     (F : V₀ ≃ₗ[ℂ] V) (G : W₀ ≃ₗ[ℂ] W)
40     (hF : ∀ h x, F (ρ₀ h x) = ρ h (F x))
41     (hG : ∀ h x, G (σ₀ h x) = σ h (G x))
42     (U : V₀ ≃ₗ[ℂ] W₀) (hU : ∀ h x, U (ρ₀ h x) = σ₀ (e h) (U x)) :
43     ∀ h x, (F.symm.trans (U.trans G)) (ρ h x) =
44       σ (e h) ((F.symm.trans (U.trans G)) x) := by
45   intro h x
46   obtain ⟨y, rfl⟩ := F.surjective x
47   rw [← hF]
48   simp only [LinearEquiv.trans_apply, LinearEquiv.symm_apply_apply, hU, hG]
49 
50 end PaperXI.FullBridgeTransport

Back to source controls