CompactTypeTensor58.lean

1 import PaperXI.GallagherTensorIrreducibility58
2 import PaperXI.SmoothDegreeQuotient
3 import PaperXI.FiniteRepresentation
4 
5 /-!
6 # The prescribed compact factor with an actual finite quotient factor
7 
8 An irreducible quotient representation is tensored with the supplied extension
9 of an irreducible subgroup action. The resulting compact inducing action is
10 constructed on the literal tensor space, is irreducible and smooth, and retains
11 the supplied subgroup action on the first factor exactly. No type-theoretic
12 compact-induction theorem or arithmetic comparison is asserted.
13 -/
14 set_option autoImplicit false
15 noncomputable section
16 namespace PaperXI.CompactTypeTensor58
17 
18 open Representation
19 open scoped TensorProduct
20 
21 variable {J Q W U : Type*} [Group J] [Group Q]
22 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup U] [Module ℂ U]
23 variable (N : Subgroup J) (q : J →* Q) (hN : N ≤ q.ker)
24 variable (κ : Representation ℂ J W) (σ : Representation ℂ Q U)
25 
26 /-- The actual action obtained by adjoining the residue multiplicity factor. -/
27 abbrev action : Representation ℂ J (W ⊗[ℂ] U) := κ.tprod (σ.comp q)
28 
29 include hN in
30 /-- Restriction retains the prescribed subgroup action, with the second factor
31 acting trivially; it does not identify the whole tensor space with W. -/
32 theorem restriction : (action q κ σ).comp N.subtype = Representation.tprod (κ.comp N.subtype) (1 : Representation ℂ N U) := by
33   ext n w u
34   have hn : q n = 1 := hN n.property
35   simp [action, hn]
36 
37 include hN in
38 /-- Literal subgroup action on every pure tensor. -/
39 theorem subgroup_action (n : N) (w : W) (u : U) :
40     action q κ σ n (w ⊗ₜ[ℂ] u) = κ n w ⊗ₜ[ℂ] u := by
41   have hn : q n = 1 := hN n.property
42   simp [action, hn]
43 
44 variable [FiniteDimensional ℂ W]
45 
46 include hN in
47 /-- The completed compact action is irreducible, derived from the two factors. -/
48 theorem irreducible (hq : Function.Surjective q)
49     [IsIrreducible (κ.comp N.subtype)] [IsIrreducible σ] :
50     IsIrreducible (action q κ σ) :=
51   GallagherTensorIrreducibility58.tensor_irreducible N q hq hN κ σ
52 
53 /-- The residue factor, hence the whole tensor space, is finite-dimensional
54 when the actual quotient group is finite. -/
55 theorem finiteDimensional [Finite Q] [IsIrreducible σ] :
56     FiniteDimensional ℂ (W ⊗[ℂ] U) := by
57   let : FiniteDimensional ℂ U := FiniteRepresentation.finiteDimensional σ
58   infer_instance
59 
60 section Topology
61 variable [TopologicalSpace J] [IsTopologicalGroup J]
62 
63 include hN in
64 /-- An open subgroup on which the second factor is trivial gives smoothness
65 of the tensor action from smoothness of the prescribed first factor. -/
66 theorem smooth (hopen : IsOpen (N : Set J))
67     (hκ : SmoothDegreeQuotient.IsSmooth κ) :
68     SmoothDegreeQuotient.IsSmooth (action q κ σ) := by
69   intro x
70   apply Subgroup.isOpen_mono (H₁ := κ.ker ⊓ N) ?_
71     ((SmoothDegreeQuotient.isOpen_kernel_of_smooth κ hκ).inter hopen)
72   intro g hg
73   have hk : κ g = 1 := hg.1
74   have hq : q g = 1 := hN hg.2
75   change TensorProduct.map (κ g) (σ (q g)) x = x
76   rw [hk, hq, map_one, TensorProduct.map_one]
77   rfl
78 
79 include hN in
80 /-- Same-candidate compact completion: all conclusions refer to the displayed
81 tensor action and its exact prescribed first factor. -/
82 theorem completed [Finite Q] (hq : Function.Surjective q)
83     [IsIrreducible (κ.comp N.subtype)] [IsIrreducible σ]
84     (hopen : IsOpen (N : Set J)) (hκ : SmoothDegreeQuotient.IsSmooth κ) :
85     IsIrreducible (action q κ σ) ∧
86     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
87     SmoothDegreeQuotient.IsSmooth (action q κ σ) ∧
88     (action q κ σ).comp N.subtype = Representation.tprod (κ.comp N.subtype) (1 : Representation ℂ N U) :=
89   ⟨irreducible N q hN κ σ hq, finiteDimensional (W := W) σ,
90     smooth N q hN κ σ hopen hκ, restriction N q hN κ σ⟩
91 
92 end Topology
93 end PaperXI.CompactTypeTensor58

Back to source controls