NormalInertia.lean

1 import PaperXI.QuotientRepresentation
2 import Mathlib.RepresentationTheory.Invariants
3 import Mathlib.Analysis.Complex.Polynomial.Basic
4 
5 /-! Normal-inertia fixed spaces and abelian quotient descent.
6 No cyclic finite-inertia generator, Frobenius orbit basis, or tame hypothesis
7 is required for the fixed-space vanishing theorem. -/
8 set_option autoImplicit false
9 noncomputable section
10 open scoped Classical
11 namespace PaperXI.NormalInertia
12 
13 variable {G V : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
14 
15 /-- The fixed space of a normal subgroup is a genuine ambient subrepresentation. -/
16 def fixedSubrepresentation (ρ : Representation ℂ G V) (I : Subgroup G) [I.Normal] :
17     Subrepresentation ρ where
18   toSubmodule := Representation.invariants (ρ.comp I.subtype)
19   apply_mem_toSubmodule g := Representation.le_comap_invariants ρ I g
20 
21 /-- Irreducibility gives the normal-subgroup invariant dichotomy. -/
22 theorem fixed_eq_bot_or_top (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
23     (I : Subgroup G) [I.Normal] :
24     Representation.invariants (ρ.comp I.subtype) = ⊥ ∨ Representation.invariants (ρ.comp I.subtype) = ⊤ := by
25   rcases eq_bot_or_eq_top (fixedSubrepresentation ρ I) with h | h
26   · exact Or.inl (congrArg Subrepresentation.toSubmodule h)
27   · exact Or.inr (congrArg Subrepresentation.toSubmodule h)
28 
29 /-- Full inertia-fixed space is equivalent to the literal kernel containment. -/
30 theorem fixed_top_iff_le_kernel (ρ : Representation ℂ G V) (I : Subgroup G) :
31     Representation.invariants (ρ.comp I.subtype) = ⊤ ↔ I ≤ ρ.ker := by
32   constructor
33   · intro h g hg
34     apply LinearMap.ext
35     intro v
36     have hv : v ∈ Representation.invariants (ρ.comp I.subtype) := by rw [h]; trivial
37     exact hv ⟨g, hg⟩
38   · intro h
39     apply top_unique
40     intro v _ g
41     have hg := h g.property
42     exact LinearMap.congr_fun hg v
43 
44 /-- If the quotient by inertia is commutative, an irreducible representation
45 trivial on inertia is one-dimensional. -/
46 theorem dimension_one_of_inertia_trivial [FiniteDimensional ℂ V]
47     (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
48     (I : Subgroup G) [I.Normal] [IsMulCommutative (G ⧸ I)]
49     (hI : I ≤ ρ.ker) : Module.finrank ℂ V = 1 := by
50   let σ := PaperXI.QuotientRepresentation.descend I ρ hI
51   let : Representation.IsIrreducible σ :=
52     PaperXI.QuotientRepresentation.descend_irreducible I ρ hI
53   exact Representation.IsIrreducible.finrank_eq_one_of_isMulCommutative σ
54 
55 /-- The original invariant-space argument needs abelian residual quotient,
56 not finite cyclic inertia or the tame induction theorem. -/
57 theorem fixed_eq_bot_of_dimension_gt_one [FiniteDimensional ℂ V]
58     (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
59     (I : Subgroup G) [I.Normal] [IsMulCommutative (G ⧸ I)]
60     (hdim : 1 < Module.finrank ℂ V) : Representation.invariants (ρ.comp I.subtype) = ⊥ := by
61   rcases fixed_eq_bot_or_top ρ I with h | h
62   · exact h
63   · have hd := dimension_one_of_inertia_trivial ρ I ((fixed_top_iff_le_kernel ρ I).mp h)
64     omega
65 
66 /-- Nontrivial normal inertia acts without fixed vectors in an irreducible,
67 including one-dimensional ramified characters. -/
68 theorem fixed_eq_bot_of_not_le_kernel
69     (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
70     (I : Subgroup G) [I.Normal] (hI : ¬ I ≤ ρ.ker) :
71     Representation.invariants (ρ.comp I.subtype) = ⊥ :=
72   (fixed_eq_bot_or_top ρ I).resolve_right
73     (fun h => hI ((fixed_top_iff_le_kernel ρ I).mp h))
74 
75 /-- Exact codimension dichotomy, preserving the unramified one-dimensional case. -/
76 theorem fixed_codimension [FiniteDimensional ℂ V]
77     (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
78     (I : Subgroup G) [I.Normal] :
79     Module.finrank ℂ V - Module.finrank ℂ (Representation.invariants (ρ.comp I.subtype)) =
80       if I ≤ ρ.ker then 0 else Module.finrank ℂ V := by
81   split_ifs with hI
82   · rw [(fixed_top_iff_le_kernel ρ I).mpr hI]; simp
83   · rw [fixed_eq_bot_of_not_le_kernel ρ I hI]; simp
84 
85 end PaperXI.NormalInertia

Back to source controls