InducedTypeSpace68.lean

1 import PaperXI.InductionIrreducibility
2 import Mathlib.Algebra.Algebra.Equiv
3 
4 /-!
5 # The canonical inducing-type subspace of actual induction
6 
7 The full off-H Mackey condition gives factorization of every H-map through the
8 literal identity-coset inclusion.  No topological or semisimplicity hypothesis
9 is needed for this factorization.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.InducedTypeSpace68
14 
15 open Representation PaperXI.InductionIrreducibility
16 
17 variable {k G V : Type*} [Field k] [Group G] [AddCommGroup V] [Module k V]
18 variable (H : Subgroup G) (σ : Representation k H V)
19 
20 /-- Every type map factors through its identity coefficient. -/
21 theorem factorization
22     (hM : ∀ g : G, g ∉ H →
23       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
24         (σ.comp (intersectionConjugation H g)), A = 0)
25     (f : IntertwiningMap σ ((ind H.subtype σ).comp H.subtype)) :
26     f = (identityInclusion H σ).comp ((identityEvaluation H σ).comp f) := by
27   apply sub_eq_zero.mp
28   apply intertwiner_eq_zero_of_mackey H σ hM
29   intro v
30   change identityEvaluation H σ
31     (f v - identityInclusion H σ (identityEvaluation H σ (f v))) = 0
32   rw [map_sub, identityEvaluation_inclusion, sub_self]
33 
34 /-- The pointwise form is useful when comparing actual type images. -/
35 theorem factorization_apply
36     (hM : ∀ g : G, g ∉ H →
37       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
38         (σ.comp (intersectionConjugation H g)), A = 0)
39     (f : IntertwiningMap σ ((ind H.subtype σ).comp H.subtype)) (v : V) :
40     f v = identityInclusion H σ (identityEvaluation H σ (f v)) :=
41   congrArg (fun t => t v) (factorization H σ hM f)
42 
43 /-- Evaluation and identity-coset inclusion identify the actual Hom space with
44 the endomorphism space of the inducing representation. -/
45 def homEquiv
46     (hM : ∀ g : G, g ∉ H →
47       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
48         (σ.comp (intersectionConjugation H g)), A = 0) :
49     IntertwiningMap σ ((ind H.subtype σ).comp H.subtype) ≃ₗ[k]
50       IntertwiningMap σ σ where
51   toFun f := (identityEvaluation H σ).comp f
52   invFun b := (identityInclusion H σ).comp b
53   left_inv f := (factorization H σ hM f).symm
54   right_inv b := by ext v; simp
55   map_add' f g := by ext v; simp
56   map_smul' c f := by ext v; simp
57 
58 /-- Every nonzero type map has exactly the same image as the identity copy.
59 Irreducibility suffices, without any scalar-endomorphism assumption. -/
60 theorem range_eq_identity [IsIrreducible σ]
61     (hM : ∀ g : G, g ∉ H →
62       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
63         (σ.comp (intersectionConjugation H g)), A = 0)
64     (f : IntertwiningMap σ ((ind H.subtype σ).comp H.subtype)) (hf : f ≠ 0) :
65     LinearMap.range f.toLinearMap = LinearMap.range (identityInclusion H σ).toLinearMap := by
66   have hb : (identityEvaluation H σ).comp f ≠ 0 := by
67     intro hz
68     apply hf
69     rw [factorization H σ hM f, hz]
70     ext v
71     simp
72   have hsurj := (IsIrreducible.surjective_or_eq_zero
73     ((identityEvaluation H σ).comp f)).resolve_right hb
74   ext w
75   constructor
76   · rintro ⟨v, rfl⟩
77     exact ⟨identityEvaluation H σ (f v), (factorization_apply H σ hM f v).symm⟩
78   · rintro ⟨v, rfl⟩
79     obtain ⟨u, hu⟩ := hsurj v
80     exact ⟨u, (factorization_apply H σ hM f u).trans
81       (congrArg (identityInclusion H σ) hu)⟩
82 
83 /-- The distinguished type space is a literal submodule of the infinite
84 induced carrier, not an identification of that carrier with a finite diagram. -/
85 def typeSpace : Submodule k (IndV H.subtype σ) :=
86   LinearMap.range (identityInclusion H σ).toLinearMap
87 
88 /-- The actual inducing representation is linearly equivalent to its image. -/
89 def typeEquiv : V ≃ₗ[k] typeSpace H σ :=
90   LinearEquiv.ofInjective (identityInclusion H σ).toLinearMap (by
91     intro v w h
92     simpa using congrArg (identityEvaluation H σ) h)
93 
94 /-- Conjugation transports all operators faithfully into the canonical type
95 space. It preserves the full algebra, not merely its scalar invariants. -/
96 def typeOperators : Module.End k V ≃ₐ[k] Module.End k (typeSpace H σ) :=
97   (typeEquiv H σ).conjAlgEquiv k
98 
99 @[simp] theorem typeOperators_mul (A B : Module.End k V) :
100     typeOperators H σ (A * B) = typeOperators H σ A * typeOperators H σ B :=
101   map_mul (typeOperators H σ) A B
102 
103 @[simp] theorem typeOperators_add (A B : Module.End k V) :
104     typeOperators H σ (A + B) = typeOperators H σ A + typeOperators H σ B :=
105   map_add (typeOperators H σ) A B
106 
107 @[simp] theorem typeOperators_eq_zero_iff (A : Module.End k V) :
108     typeOperators H σ A = 0 ↔ A = 0 :=
109   (typeOperators H σ).map_eq_zero_iff
110 
111 /-- In particular, projector idempotence is preserved and reflected. -/
112 theorem typeOperators_idempotent_iff (A : Module.End k V) :
113     typeOperators H σ A * typeOperators H σ A = typeOperators H σ A ↔ A * A = A := by
114   rw [← map_mul]
115   exact (typeOperators H σ).injective.eq_iff
116 
117 /-- Over an algebraically closed field, every type map is a scalar multiple
118 of the canonical inclusion. -/
119 theorem type_map_scalar [FiniteDimensional k V] [IsAlgClosed k] [IsIrreducible σ]
120     (hM : ∀ g : G, g ∉ H →
121       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
122         (σ.comp (intersectionConjugation H g)), A = 0)
123     (f : IntertwiningMap σ ((ind H.subtype σ).comp H.subtype)) :
124     ∃ c : k, f = c • identityInclusion H σ := by
125   obtain ⟨c, hc⟩ := IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed
126     (ρ := σ) |>.surjective ((identityEvaluation H σ).comp f)
127   refine ⟨c, ?_⟩
128   rw [factorization H σ hM f, ← hc]
129   ext v
130   simp
131 
132 /-- Conjugating an operator is unchanged when the identifying equivalence is
133 rescaled. This is the operator-level consequence of scalar uniqueness. -/
134 theorem conjugation_eq_of_scalar {W : Type*} [AddCommGroup W] [Module k W]
135     (e₁ e₂ : V ≃ₗ[k] W) (c : k) (h : ∀ v, e₂ v = c • e₁ v)
136     (A : Module.End k V) : e₂.conjAlgEquiv k A = e₁.conjAlgEquiv k A := by
137   ext w
138   obtain ⟨v, rfl⟩ := e₂.surjective w
139   change e₂ (A (e₂.symm (e₂ v))) = e₁ (A (e₁.symm (e₂ v)))
140   rw [e₂.symm_apply_apply, h v, map_smul, e₁.symm_apply_apply, map_smul, map_smul, h]
141 
142 end PaperXI.InducedTypeSpace68

Back to source controls