FiniteIntersectionCriterion108.lean

1 import PaperXI.CompactIntersection108
2 
3 /-! An exact criterion on a literal finite model. The scalar character profile,
4 compatibility and index identity must still be proved for the arithmetic data. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.FiniteIntersectionCriterion108
8 open Representation IntersectionModel108
9 variable {K G Q W : Type*} [Group K] [Group G] [Group Q] [Fintype Q]
10   [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
11 
12 /-- Dimension one of the original operator space is equivalent to the finite
13 index identity, once the two actual character profiles are established. -/
14 theorem dimension_one_iff (ι : K →* G) (ρ : Representation ℂ K W) (g : G)
15     (q : pairs ι g →* Q) (hq : Function.Surjective q)
16     (ρ₁ ρ₂ : Representation ℂ Q W)
17     (he₁ : ρ₁.comp q = ρ.comp (left ι g)) (he₂ : ρ₂.comp q = ρ.comp (right ι g))
18     (H₁ H₂ : Subgroup Q) (θ₁ : H₁ →* ℂˣ) (θ₂ : H₂ →* ℂˣ)
19     (h₁ : ∀ h : H₁, ρ₁ h = (θ₁ h : ℂ) • LinearMap.id)
20     (h₂ : ∀ h : H₂, ρ₂ h = (θ₂ h : ℂ) • LinearMap.id)
21     (hz₁ : ∀ x : Q, x ∉ H₁ → ρ₁.character x = 0)
22     (hz₂ : ∀ x : Q, x ∉ H₂ → ρ₂.character x = 0)
23     (hc : ∀ x : Q, ∀ h₁ : x ∈ H₁, ∀ h₂ : x ∈ H₂, θ₁ ⟨x, h₁⟩ = θ₂ ⟨x, h₂⟩) :
24     Module.finrank ℂ (IntertwiningSpace107.space ι ρ g) = 1 ↔
25       Module.finrank ℂ W * Module.finrank ℂ W * Nat.card (H₁ ⊓ H₂ : Subgroup Q) =
26         Nat.card Q := by
27   rw [finrank_model ι ρ g q hq ρ₁ ρ₂ he₁ he₂]
28   exact CharacterPairing108.dimension_one_iff ρ₁ ρ₂ H₁ H₂ θ₁ θ₂ h₁ h₂ hz₁ hz₂ hc
29 
30 end PaperXI.FiniteIntersectionCriterion108

Back to source controls