CyclicBridge.lean

1 import PaperXI.DiscrepancyCharacter
2 import Mathlib.GroupTheory.SemidirectProduct
3 
4 /-! A trivial scalar discrepancy on one cyclic generator closes an actual
5 semidirect-product bridge. Phase means the scalar discrepancy, not trace. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CyclicBridge
9 variable {H C V W : Type*} [Group H] [Group C]
10 variable [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
11 
12 theorem character_trivial (δ : C →* ℂˣ) (c : C)
13     (hgen : ∀ g : C, ∃ n : ℤ, g = c ^ n) (hc : δ c = 1) : ∀ g, δ g = 1 := by
14   intro g
15   obtain ⟨n, rfl⟩ := hgen g
16   simp [map_zpow, hc]
17 
18 theorem semidirect_intertwining (α : C →* MulAut H)
19     (π : Representation ℂ (H ⋊[α] C) V) (σ : Representation ℂ (H ⋊[α] C) W)
20     (U : V ≃ₗ[ℂ] W)
21     (hH : ∀ h x, U (π (SemidirectProduct.inl h) x) = σ (SemidirectProduct.inl h) (U x))
22     (hC : ∀ g x, U (π (SemidirectProduct.inr g) x) = σ (SemidirectProduct.inr g) (U x)) :
23     ∀ a x, U (π a x) = σ a (U x) := by
24   intro a x
25   rw [← SemidirectProduct.inl_left_mul_inr_right a]
26   simp only [map_mul, Module.End.mul_apply, hH, hC]
27 
28 theorem stabilizer_covariance (α : C →* MulAut H)
29     (π : Representation ℂ (H ⋊[α] C) V) (g : C) (h : H) (x : V) :
30     π (SemidirectProduct.inr g) (π (SemidirectProduct.inl h) x) =
31       π (SemidirectProduct.inl (α g h)) (π (SemidirectProduct.inr g) x) := by
32   have he : (SemidirectProduct.inr g : H ⋊[α] C) * SemidirectProduct.inl h =
33       SemidirectProduct.inl (α g h) * SemidirectProduct.inr g := by
34     rw [SemidirectProduct.inl_aut]
35     simp [mul_assoc]
36   have hr := congrArg (fun a => π a x) he
37   simpa [map_mul, Module.End.mul_apply] using hr
38 
39 /-- The character is produced from the actual actions. Its generator value
40 being one is sufficient to intertwine every semidirect-product element. -/
41 theorem one_phase_bridge [FiniteDimensional ℂ V] (α : C →* MulAut H)
42     (π : Representation ℂ (H ⋊[α] C) V) (σ : Representation ℂ (H ⋊[α] C) W)
43     [Representation.IsIrreducible (π.comp SemidirectProduct.inl)]
44     (U : V ≃ₗ[ℂ] W)
45     (hH : ∀ h x, U (π (SemidirectProduct.inl h) x) = σ (SemidirectProduct.inl h) (U x))
46     (c : C) (hgen : ∀ g : C, ∃ n : ℤ, g = c ^ n) :
47     ∃ δ : C →* ℂˣ,
48       (∀ g x, U (π (SemidirectProduct.inr g) x) =
49         (δ g : ℂ) • σ (SemidirectProduct.inr g) (U x)) ∧
50       (δ c = 1 → ∀ a x, U (π a x) = σ a (U x)) := by
51   obtain ⟨δ, hδ⟩ := PaperXI.DiscrepancyCharacter.exists_character
52     (π.comp SemidirectProduct.inl) (σ.comp SemidirectProduct.inl) U hH α
53     (π.comp SemidirectProduct.inr) (σ.comp SemidirectProduct.inr)
54     (stabilizer_covariance α π) (stabilizer_covariance α σ)
55   refine ⟨δ, hδ, ?_⟩
56   intro hc
57   apply semidirect_intertwining α π σ U hH
58   intro g x
59   simpa [character_trivial δ c hgen hc g] using hδ g x
60 
61 
62 /-- Assemble compatible honest actions into the actual semidirect representation. -/
63 def semidirectRepresentation (α : C →* MulAut H)
64     (ρ : Representation ℂ H V) (R : Representation ℂ C V)
65     (hR : ∀ g h x, R g (ρ h x) = ρ (α g h) (R g x)) :
66     Representation ℂ (H ⋊[α] C) V where
67   toFun a := ρ a.left * R a.right
68   map_one' := by simp
69   map_mul' a b := by
70     apply LinearMap.ext
71     intro x
72     simp [map_mul, Module.End.mul_apply, hR]
73 
74 @[simp] theorem semidirectRepresentation_inl (α : C →* MulAut H)
75     (ρ : Representation ℂ H V) (R : Representation ℂ C V)
76     (hR : ∀ g h x, R g (ρ h x) = ρ (α g h) (R g x)) (h : H) :
77     semidirectRepresentation α ρ R hR (SemidirectProduct.inl h) = ρ h := by
78   simp [semidirectRepresentation]
79 
80 @[simp] theorem semidirectRepresentation_inr (α : C →* MulAut H)
81     (ρ : Representation ℂ H V) (R : Representation ℂ C V)
82     (hR : ∀ g h x, R g (ρ h x) = ρ (α g h) (R g x)) (g : C) :
83     semidirectRepresentation α ρ R hR (SemidirectProduct.inr g) = R g := by
84   simp [semidirectRepresentation]
85 
86 /-- The manuscript's input form: compatible normal-subgroup and cyclic
87 stabilizer actions are assembled here rather than assumed preassembled. -/
88 theorem one_phase_bridge_from_actions [FiniteDimensional ℂ V]
89     (ρ : Representation ℂ H V) [Representation.IsIrreducible ρ]
90     (σ : Representation ℂ H W) (U : V ≃ₗ[ℂ] W)
91     (hU : ∀ h x, U (ρ h x) = σ h (U x))
92     (α : C →* MulAut H) (R : Representation ℂ C V) (S : Representation ℂ C W)
93     (hR : ∀ g h x, R g (ρ h x) = ρ (α g h) (R g x))
94     (hS : ∀ g h x, S g (σ h x) = σ (α g h) (S g x))
95     (c : C) (hgen : ∀ g : C, ∃ n : ℤ, g = c ^ n) :
96     ∃ δ : C →* ℂˣ,
97       (∀ g x, U (R g x) = (δ g : ℂ) • S g (U x)) ∧
98       (δ c = 1 → ∀ a x,
99         U (semidirectRepresentation α ρ R hR a x) =
100           semidirectRepresentation α σ S hS a (U x)) := by
101   obtain ⟨δ, hδ⟩ := PaperXI.DiscrepancyCharacter.exists_character ρ σ U hU α R S hR hS
102   refine ⟨δ, hδ, ?_⟩
103   intro hc
104   apply semidirect_intertwining α (semidirectRepresentation α ρ R hR)
105     (semidirectRepresentation α σ S hS) U
106   · simpa only [semidirectRepresentation_inl] using hU
107   · intro g x
108     simpa only [semidirectRepresentation_inr, character_trivial δ c hgen hc g,
109       Units.val_one, one_smul] using hδ g x
110 
111 end PaperXI.CyclicBridge

Back to source controls