InertiaQuotient.lean

1 import PaperXI.InteractionPolynomial
2 
3 /-! Invariant-space and restricted-operator comparison for a supplied finite
4 inertia quotient. No finite quotient is embedded into the original group. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.InertiaQuotient
8 open Polynomial
9 open scoped Classical
10 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.InvariantPolynomial
11 variable {K V G H : Type*} [Field K] [AddCommGroup V] [Module K V] [Group G] [Group H]
12 
13 theorem invariants_comp_of_surjective (ρ : Representation K G V) (s : H →* G)
14     (hs : Function.Surjective s) : (Representation.invariants (ρ.comp s)) = ρ.invariants := by
15   ext v
16   constructor
17   · intro hv g
18     obtain ⟨x, rfl⟩ := hs g
19     exact hv x
20   · intro hv x
21     exact hv (s x)
22 
23 def invariantEquiv (ρ : Representation K G V) (s : H →* G) (hs : Function.Surjective s) :
24     (Representation.invariants (ρ.comp s)) ≃ₗ[K] ρ.invariants :=
25   LinearEquiv.ofEq _ _ (invariants_comp_of_surjective ρ s hs)
26 
27 theorem invariantEquiv_apply (ρ : Representation K G V) (s : H →* G)
28     (hs : Function.Surjective s) (v : (Representation.invariants (ρ.comp s))) :
29     (invariantEquiv ρ s hs v : V) = v := rfl
30 
31 variable {U I : Type*} [AddCommGroup U] [Module ℂ U] [Group I]
32 variable {M : ℕ} [NeZero M]
33 
34 def factoredFrobenius (ρ : Action (K := ℂ) (V := U) (M := M))
35     (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
36     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
37     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s) :
38     (Representation.invariants (ρ.comp s)) ≃ₗ[ℂ] (Representation.invariants (ρ.comp s)) :=
39   ((invariantEquiv ρ s hs).trans (fixedFrobenius ρ F q h)).trans (invariantEquiv ρ s hs).symm
40 
41 /-- The transported map is exactly F on the original inertia-fixed vectors. -/
42 theorem factoredFrobenius_apply (ρ : Action (K := ℂ) (V := U) (M := M))
43     (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
44     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
45     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s)
46     (v : (Representation.invariants (ρ.comp s))) : (factoredFrobenius ρ F q h s hs v : U) = F v := by
47   simp [factoredFrobenius, invariantEquiv, fixedFrobenius]
48 
49 theorem factored_polynomial_eq [FiniteDimensional ℂ U]
50     (ρ : Action (K := ℂ) (V := U) (M := M)) (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
51     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
52     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s) :
53     operatorPolynomial (factoredFrobenius ρ F q h s hs).toLinearMap = localPolynomial ρ F q h := by
54   change operatorPolynomial ((invariantEquiv ρ s hs).symm.conj
55     (fixedFrobenius ρ F q h).toLinearMap) = _
56   exact operatorPolynomial_conj _ _
57 
58 theorem factored_local_polynomial [FiniteDimensional ℂ U]
59     (ρ : Action (K := ℂ) (V := U) (M := M)) (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
60     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
61     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s)
62     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℂ U) (j : ZMod M) {v : U}
63     (hv : v ∈ packet ρ j) (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v)
64     (c : ℂ) (hclose : (F ^ n) v = c • v) :
65     operatorPolynomial (factoredFrobenius ρ F q h s hs).toLinearMap =
66       if j = 0 then 1 - C c * X ^ n else 1 := by
67   rw [factored_polynomial_eq]
68   exact PaperXI.InteractionPolynomial.local_polynomial ρ F q h hn b j hv hb c hclose
69 
70 theorem factored_character_trivial_iff
71     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s) (j : ZMod M) :
72     (∀ x : I, ZMod.stdAddChar (j * (s x).toAdd) = (1 : ℂ)) ↔ j = 0 := by
73   constructor
74   · intro h
75     apply (PaperXI.InteractionPolynomial.character_trivial_iff j).mp
76     intro a
77     obtain ⟨x, hx⟩ := hs (Multiplicative.ofAdd a)
78     simpa [hx] using h x
79   · rintro rfl
80     simp
81 
82 /-- The literal determinant on the original inertia-fixed space, in any basis. -/
83 theorem factored_determinant [FiniteDimensional ℂ U]
84     (ρ : Action (K := ℂ) (V := U) (M := M)) (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
85     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
86     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s)
87     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℂ U) (j : ZMod M) {v : U}
88     (hv : v ∈ packet ρ j) (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v)
89     (c : ℂ) (hclose : (F ^ n) v = c • v)
90     {κ : Type*} [Fintype κ] [DecidableEq κ] (B : Module.Basis κ ℂ (Representation.invariants (ρ.comp s))) :
91     Matrix.det (1 - (X : ℂ[X]) •
92       (LinearMap.toMatrix B B (factoredFrobenius ρ F q h s hs).toLinearMap).map C) =
93       if (∀ x : I, ZMod.stdAddChar (j * (s x).toAdd) = (1 : ℂ))
94       then 1 - C c * X ^ n else 1 := by
95   rw [← operatorPolynomial_eq_det _ B, factored_local_polynomial ρ F q h s hs hn b j hv hb c hclose]
96   simp only [factored_character_trivial_iff s hs]
97 
98 end PaperXI.InertiaQuotient

Back to source controls