BreakTensorFactorization.lean

1 import PaperXI.CentralProductComparison
2 import PaperXI.HeisenbergTensorComparison
3 import PaperXI.BreakHeisenbergSum
4 import PaperXI.AbstractHeisenbergExtension
5 
6 /-! Source 15.2: actual tensor factorization on the declared full group.
7 Compatible factor embeddings construct the group comparison. In the odd
8 symplectic branch both this comparison and scalar nondegeneracy are derived. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.BreakTensorFactorization
12 open CentralExtension CocycleCommutator
13 open scoped Classical
14 
15 section SuppliedExtensions
16 variable {S Z G : Type*} [Fintype S] [CommGroup Z] [Group G]
17 variable {H A V : S → Type*} [∀ s, Group (H s)] [∀ s, CommGroup (A s)]
18 variable [∀ s, Fintype (A s)] [∀ s, AddCommGroup (V s)] [∀ s, Module ℂ (V s)]
19 variable {W : Type*} [AddCommGroup W] [Module ℂ W]
20 
21 /-- The full tensor representation and its equivalence to the given irreducible
22 representation are constructed from the actual commuting factor embeddings. -/
23 def source
24     (D : ∀ s, Datum Z (H s) (A s)) (E : Datum Z G (∀ s, A s))
25     (j : ∀ s, H s →* G)
26     (hc : Pairwise fun s t => ∀ h k, Commute (j s h) (j t k))
27     (hi : ∀ s z, j s ((D s).i z) = E.i z)
28     (hq : ∀ s h, E.q (j s h) = Pi.mulSingle s ((D s).q h))
29     (ζ : Z →* ℂˣ) (hnd : ∀ s, radical (scalarCocycle (D s) ζ) = ⊥)
30     (σ : ∀ s, Representation ℂ (H s) (V s)) [∀ s, Representation.IsIrreducible (σ s)]
31     (hσ : ∀ s z, σ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id)
32     (τ : Representation ℂ G W) [Representation.IsIrreducible τ]
33     (hτ : ∀ z, τ (E.i z) = (ζ z : ℂ) • LinearMap.id) :
34     Representation.Equiv
35       (HeisenbergTensor.onFullEnvelope D ζ σ hσ
36         (CentralProductComparison.equiv D E j hc hi hq)) τ := by
37   apply HeisenbergTensor.fullEnvelopeFactorization D ζ hnd σ hσ
38   intro z
39   simpa only [CentralProduct.datum_i, CentralProductComparison.equiv_center] using hτ z
40 end SuppliedExtensions
41 
42 section Odd
43 variable {S K T : Type*} [Fintype S] [Field K] [Finite K]
44 variable {B V : S → Type*} [∀ s, AddCommGroup (B s)] [∀ s, Module K (B s)]
45 variable [∀ s, FiniteDimensional K (B s)]
46 variable [∀ s, AddCommGroup (V s)] [∀ s, Module ℂ (V s)]
47 variable [AddCommGroup T] [Module K T]
48 variable {W : Type*} [AddCommGroup W] [Module ℂ W]
49 
50 /-- Odd symplectic source endpoint. Neither the full group comparison nor
51 scalar-cocycle nondegeneracy is assumed; both are constructed from the actual
52 orthogonal decomposition and the nontrivial additive central character. -/
53 theorem odd_source
54     (b : ∀ s, LinearMap.BilinForm K (B s))
55     (hb : ∀ s, (b s).IsAlt) (hbn : ∀ s, (b s).Nondegenerate) (h2 : (2 : K) ≠ 0)
56     (c : LinearMap.BilinForm K T) (e : (∀ s, B s) ≃ₗ[K] T)
57     (he : ∀ v w, c (e v) (e w) = BreakHeisenbergSum.form b v w)
58     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1)
59     (σ : ∀ s, Representation ℂ (AbstractHeisenberg.Element (b s)) (V s))
60     [∀ s, Representation.IsIrreducible (σ s)]
61     (hσ : ∀ s z, σ s (AbstractHeisenberg.centralElement (b s) z) = ψ z • LinearMap.id)
62     (τ : Representation ℂ (AbstractHeisenberg.Element c) W) [Representation.IsIrreducible τ]
63     (hτ : ∀ z, τ (AbstractHeisenberg.centralElement c z) = ψ z • LinearMap.id) :
64     Nonempty (Representation.Equiv
65       (HeisenbergTensor.onFullEnvelope (fun s => AbstractHeisenberg.datum (b s))
66         (SymplecticCentralExtension.scalarCharacter ψ) σ (fun s z => hσ s z.toAdd)
67         (BreakHeisenbergSum.decompositionEquiv b c e he)) τ) := by
68   let : ∀ s, Finite (B s) := fun s => Module.finite_of_finite K
69   let : ∀ s, Fintype (Multiplicative (B s)) := fun s => Fintype.ofFinite _
70   refine ⟨HeisenbergTensor.fullEnvelopeFactorization _ _ (fun s =>
71     AbstractHeisenberg.scalar_radical_eq_bot_scalarCharacter (b s) (hb s) h2 (hbn s).1 ψ hψ)
72     σ (fun s z => hσ s z.toAdd) (BreakHeisenbergSum.decompositionEquiv b c e he) τ ?_⟩
73   intro z
74   rw [CentralProduct.datum_i, BreakHeisenbergSum.decompositionEquiv_center]
75   exact hτ z.toAdd
76 end Odd
77 end PaperXI.BreakTensorFactorization

Back to source controls