PacketTypeAttachment70.lean

1 import PaperXI.TensorTypeOperators70
2 
3 /-! The finite packet action is the restriction of the SAME actual induced
4 representation on its literal type image. Full operator relations and graph
5 edge residuals are preserved and reflected. No arithmetic factor theory is used. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.PacketTypeAttachment70
9 open Representation
10 open scoped TensorProduct
11 open PaperXI.InductionIrreducibility PaperXI.InducedTypeSpace68
12 variable {k G W U : Type*} [Field k] [Group G]
13   [AddCommGroup W] [Module k W] [AddCommGroup U] [Module k U]
14 variable (H : Subgroup G) (Λ : Representation k H (W ⊗[k] U))
15 
16 /-- The conjugated action on the literal identity-coset type image. -/
17 def typeAction : Representation k H (typeSpace H Λ) :=
18   (typeOperators H Λ).toAlgHom.toMonoidHom.comp Λ
19 
20 /-- The conjugated action really is the restriction of the ambient induction. -/
21 theorem ambient_action (h : H) (x : typeSpace H Λ) :
22     ((typeAction H Λ h x : typeSpace H Λ) : IndV H.subtype Λ) =
23       ind H.subtype Λ (h : G) (x : IndV H.subtype Λ) := by
24   obtain ⟨v, rfl⟩ := (typeEquiv H Λ).surjective x
25   change ((typeEquiv H Λ)
26     (Λ h ((typeEquiv H Λ).symm ((typeEquiv H Λ) v))) : IndV H.subtype Λ) = _
27   rw [LinearEquiv.symm_apply_apply]
28   exact LinearMap.congr_fun ((identityInclusion H Λ).isIntertwining' h) v
29 
30 /-- On a subgroup where the quotient factor is trivial, the actual induced
31 restriction is exactly the faithful realization of the prescribed first factor. -/
32 theorem first_factor_action {J Q : Type*} [Group J] [Group Q]
33     (i : J →* H) (q : J →* Q)
34     (κ : Representation k J W) (σ : Representation k Q U)
35     (hr : ∀ j, Λ (i j) = κ.tprod (σ.comp q) j)
36     (j : J) (hj : q j = 1) :
37     typeAction H Λ (i j) = TensorTypeOperators70.realize H Λ (κ j) := by
38   change typeOperators H Λ (Λ (i j)) =
39     typeOperators H Λ (TensorTypeOperators70.amplify (κ j))
40   apply congrArg (typeOperators H Λ)
41   rw [hr]
42   ext w u
43   simp [hj]
44 
45 /-- Weighted finite packet projectors agree with averages of the actual
46 restricted inducing-type action, not merely with a relabeled operator. -/
47 theorem first_factor_average {J Q I : Type*} [Group J] [Group Q]
48     (i : J →* H) (q : J →* Q)
49     (κ : Representation k J W) (σ : Representation k Q U)
50     (hr : ∀ j, Λ (i j) = κ.tprod (σ.comp q) j)
51     (s : Finset I) (g : I → J) (c : I → k) (hg : ∀ a ∈ s, q (g a) = 1) :
52     (∑ a ∈ s, c a • typeAction H Λ (i (g a))) =
53       TensorTypeOperators70.realize H Λ (∑ a ∈ s, c a • κ (g a)) := by
54   rw [TensorTypeOperators70.weighted_sum]
55   apply Finset.sum_congr rfl
56   intro a ha
57   rw [first_factor_action H Λ i q κ σ hr (g a) (hg a ha)]
58 
59 /-- The supplied first-factor uniformizer operator becomes the exact generator
60 operator on the type image after the tensor extension. -/
61 theorem generator_action (t : H) (A : Module.End k W)
62     (hg : ∀ w u, Λ t (w ⊗ₜ[k] u) = A w ⊗ₜ[k] u) :
63     typeAction H Λ t = TensorTypeOperators70.realize H Λ A := by
64   change typeOperators H Λ (Λ t) =
65     typeOperators H Λ (TensorTypeOperators70.amplify A)
66   apply congrArg (typeOperators H Λ)
67   ext w u
68   exact hg w u
69 
70 /-- Actual edgewise intertwining is neither lost nor spuriously created. -/
71 theorem edge_compatibility_iff [Nontrivial U] {X E : Type*}
72     (s t : E → X) (F : X → Module.End k W) (A B : E → Module.End k W) :
73     (∀ e, TensorTypeOperators70.realize H Λ (F (t e)) * TensorTypeOperators70.realize H Λ (A e) =
74       TensorTypeOperators70.realize H Λ (B e) * TensorTypeOperators70.realize H Λ (F (s e))) ↔
75     (∀ e, F (t e) * A e = B e * F (s e)) := by
76   simp only [← map_mul, TensorTypeOperators70.realize_eq_iff]
77 
78 /-- A literal graph edge defect has the same zero set after realization. -/
79 theorem edge_residual_iff [Nontrivial U] (Fₜ Fₛ A B : Module.End k W) :
80     TensorTypeOperators70.realize H Λ Fₜ * TensorTypeOperators70.realize H Λ A -
81       TensorTypeOperators70.realize H Λ B * TensorTypeOperators70.realize H Λ Fₛ = 0 ↔
82       Fₜ * A - B * Fₛ = 0 := by
83   rw [← map_mul, ← map_mul, TensorTypeOperators70.residual_zero_iff]
84 
85 end PaperXI.PacketTypeAttachment70

Back to source controls