CharacterPairing108.lean

1 import PaperXI.HeisenbergTrace108
2 
3 /-! Exact character pairing on a finite intersection. The index equality used
4 for dimension one is an explicit, separate arithmetic obligation. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.CharacterPairing108
8 open Representation
9 variable {L W U : Type*} [Group L] [Fintype L]
10   [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
11   [AddCommGroup U] [Module ℂ U] [FiniteDimensional ℂ U]
12   (ρ : Representation ℂ L W) (σ : Representation ℂ L U)
13   (H₁ H₂ : Subgroup L) (θ₁ : H₁ →* ℂˣ) (θ₂ : H₂ →* ℂˣ)
14   (h₁ : ∀ h : H₁, ρ h = (θ₁ h : ℂ) • LinearMap.id)
15   (h₂ : ∀ h : H₂, σ h = (θ₂ h : ℂ) • LinearMap.id)
16   (hz₁ : ∀ x : L, x ∉ H₁ → ρ.character x = 0)
17   (hz₂ : ∀ x : L, x ∉ H₂ → σ.character x = 0)
18   (hc : ∀ x : L, ∀ h₁ : x ∈ H₁, ∀ h₂ : x ∈ H₂, θ₁ ⟨x, h₁⟩ = θ₂ ⟨x, h₂⟩)
19 
20 include h₁ h₂ hz₁ hz₂ hc in
21 /-- The formula computes the dimension of the actual Hom space. -/
22 theorem dimension_formula :
23     Nat.card L * Module.finrank ℂ (IntertwiningMap ρ σ) =
24       Module.finrank ℂ W * Module.finrank ℂ U * Nat.card (H₁ ⊓ H₂ : Subgroup L) := by
25   classical
26   have hcard : (Nat.card L : ℂ) ≠ 0 := by exact_mod_cast (Nat.card_pos (α := L)).ne'
27   let : Invertible (Nat.card L : ℂ) := invertibleOfNonzero hcard
28   have hp (x : L) (hx : x ∈ (H₁ ⊓ H₂ : Subgroup L)) :
29       σ.character x * ρ.character x⁻¹ =
30         (Module.finrank ℂ W : ℂ) * (Module.finrank ℂ U : ℂ) := by
31     have hxi : x⁻¹ ∈ H₁ := H₁.inv_mem hx.1
32     rw [HeisenbergTrace108.character_on_subgroup H₂ θ₂ σ h₂ ⟨x, hx.2⟩,
33       HeisenbergTrace108.character_on_subgroup H₁ θ₁ ρ h₁ ⟨x⁻¹, hxi⟩]
34     have hi : θ₁ ⟨x⁻¹, hxi⟩ = (θ₁ ⟨x, hx.1⟩)⁻¹ := map_inv θ₁ ⟨x, hx.1⟩
35     rw [hi, hc x hx.1 hx.2]
36     have hu : (θ₂ ⟨x, hx.2⟩ : ℂ) ≠ 0 := Units.ne_zero _
37     simp only [Units.val_inv_eq_inv_val]
38     field_simp
39   have hz (x : L) (hx : x ∉ (H₁ ⊓ H₂ : Subgroup L)) :
40       σ.character x * ρ.character x⁻¹ = 0 := by
41     by_cases ha : x ∈ H₁
42     · have hb : x ∉ H₂ := fun hb => hx ⟨ha, hb⟩
43       rw [hz₂ x hb, zero_mul]
44     · have hb : x⁻¹ ∉ H₁ := fun hb => ha (by simpa using H₁.inv_mem hb)
45       rw [hz₁ x⁻¹ hb, mul_zero]
46   have hs : ∑ x : L, σ.character x * ρ.character x⁻¹ =
47       (Module.finrank ℂ W : ℂ) * (Module.finrank ℂ U : ℂ) *
48         (Nat.card (H₁ ⊓ H₂ : Subgroup L) : ℂ) := by
49     rw [Finset.sum_congr_set ((H₁ ⊓ H₂ : Subgroup L) : Set L)
50       (fun x => σ.character x * ρ.character x⁻¹)
51       (fun _ => (Module.finrank ℂ W : ℂ) * (Module.finrank ℂ U : ℂ)) hp hz]
52     simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
53     rw [Fintype.card_eq_nat_card]
54     change (Nat.card (H₁ ⊓ H₂ : Subgroup L) : ℂ) *
55       ((Module.finrank ℂ W : ℂ) * (Module.finrank ℂ U : ℂ)) = _
56     ring
57   have he := ρ.card_inv_mul_sum_char_mul_char_eq_finrank σ
58   rw [hs] at he
59   have hm := congrArg (fun z : ℂ => (Nat.card L : ℂ) * z) he
60   simp only [← mul_assoc, mul_inv_cancel₀ hcard, one_mul] at hm
61   exact_mod_cast hm.symm
62 
63 include h₁ h₂ hz₁ hz₂ hc in
64 /-- Dimension one is equivalent to the precise finite index identity. -/
65 theorem dimension_one_iff :
66     Module.finrank ℂ (IntertwiningMap ρ σ) = 1 ↔
67       Module.finrank ℂ W * Module.finrank ℂ U * Nat.card (H₁ ⊓ H₂ : Subgroup L) =
68         Nat.card L := by
69   have he := dimension_formula ρ σ H₁ H₂ θ₁ θ₂ h₁ h₂ hz₁ hz₂ hc
70   constructor
71   · intro h; simpa [h] using he.symm
72   · intro h
73     have hp := Nat.card_pos (α := L)
74     have : Nat.card L * Module.finrank ℂ (IntertwiningMap ρ σ) = Nat.card L * 1 := by
75       exact he.trans (h.trans (Nat.mul_one _).symm)
76     exact Nat.eq_of_mul_eq_mul_left hp this
77 
78 end PaperXI.CharacterPairing108

Back to source controls