PolynomialAssembly.lean

1 import PaperXI.InvariantAssembly
2 import PaperXI.PiPolynomial
3 import Mathlib.FieldTheory.RatFunc.Basic
4 
5 /-! Restricted Frobenius and determinant products under equivariant decompositions. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.PolynomialAssembly
9 open scoped BigOperators Classical
10 open Polynomial PaperXI.InvariantPolynomial PaperXI.InvariantAssembly
11 variable {K G U : Type*} [Field K] [Group G] [AddCommGroup U] [Module K U]
12 variable {ι : Type*} {V : ι → Type*} [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
13 
14 def restricted (ρ : Representation K G U) (F : Module.End K U)
15     (hF : ∀ x ∈ ρ.invariants, F x ∈ ρ.invariants) : Module.End K ρ.invariants where
16   toFun x := ⟨F x, hF x x.property⟩
17   map_add' x y := by ext; simp
18   map_smul' c x := by ext; simp
19 
20 theorem restricted_apply (ρ : Representation K G U) (F : Module.End K U)
21     (hF : ∀ x ∈ ρ.invariants, F x ∈ ρ.invariants) (x : ρ.invariants) :
22     (restricted ρ F hF x : U) = F x := rfl
23 
24 theorem stable_of_decomposition
25     (ρ : Representation K G U) (τ : ∀ i, Representation K G (V i))
26     (e : U ≃ₗ[K] (∀ i, V i)) (he : ∀ g x i, e (ρ g x) i = τ i g (e x i))
27     (F : Module.End K U) (A : ∀ i, Module.End K (V i))
28     (hA : ∀ i x, x ∈ (τ i).invariants → A i x ∈ (τ i).invariants)
29     (hmap : ∀ x i, e (F x) i = A i (e x i)) :
30     ∀ x ∈ ρ.invariants, F x ∈ ρ.invariants := by
31   intro x hx g
32   apply e.injective
33   funext i
34   rw [he, hmap]
35   exact hA i (e x i) (fun g => by rw [← he, hx g]) g
36 
37 theorem restricted_conj
38     (ρ : Representation K G U) (τ : ∀ i, Representation K G (V i))
39     (e : U ≃ₗ[K] (∀ i, V i)) (he : ∀ g x i, e (ρ g x) i = τ i g (e x i))
40     (F : Module.End K U) (A : ∀ i, Module.End K (V i))
41     (hF : ∀ x ∈ ρ.invariants, F x ∈ ρ.invariants)
42     (hA : ∀ i x, x ∈ (τ i).invariants → A i x ∈ (τ i).invariants)
43     (hmap : ∀ x i, e (F x) i = A i (e x i)) :
44     (invariantsEquiv ρ τ e he).conj (restricted ρ F hF) =
45       LinearMap.piMap (fun i => restricted (τ i) (A i) (hA i)) := by
46   apply LinearMap.ext
47   intro x
48   funext i
49   apply Subtype.ext
50   change e (F (e.symm (fun i => (x i : V i)))) i = A i (x i : V i)
51   rw [hmap, e.apply_symm_apply]
52 
53 theorem polynomial_product [Fintype ι] [FiniteDimensional K U]
54     [∀ i, FiniteDimensional K (V i)]
55     (ρ : Representation K G U) (τ : ∀ i, Representation K G (V i))
56     (e : U ≃ₗ[K] (∀ i, V i)) (he : ∀ g x i, e (ρ g x) i = τ i g (e x i))
57     (F : Module.End K U) (A : ∀ i, Module.End K (V i))
58     (hF : ∀ x ∈ ρ.invariants, F x ∈ ρ.invariants)
59     (hA : ∀ i x, x ∈ (τ i).invariants → A i x ∈ (τ i).invariants)
60     (hmap : ∀ x i, e (F x) i = A i (e x i)) :
61     operatorPolynomial (restricted ρ F hF) =
62       ∏ i, operatorPolynomial (restricted (τ i) (A i) (hA i)) := by
63   rw [← operatorPolynomial_conj (invariantsEquiv ρ τ e he),
64     restricted_conj ρ τ e he F A hF hA hmap, PaperXI.PiPolynomial.operatorPolynomial_pi]
65 
66 /-- Rational local factors are reciprocals of actual restricted determinants. -/
67 def localFactor [FiniteDimensional K U] (ρ : Representation K G U) (F : Module.End K U)
68     (hF : ∀ x ∈ ρ.invariants, F x ∈ ρ.invariants) : RatFunc K :=
69   (algebraMap K[X] (RatFunc K) (operatorPolynomial (restricted ρ F hF)))⁻¹
70 
71 theorem localFactor_product [Fintype ι] [FiniteDimensional K U]
72     [∀ i, FiniteDimensional K (V i)]
73     (ρ : Representation K G U) (τ : ∀ i, Representation K G (V i))
74     (e : U ≃ₗ[K] (∀ i, V i)) (he : ∀ g x i, e (ρ g x) i = τ i g (e x i))
75     (F : Module.End K U) (A : ∀ i, Module.End K (V i))
76     (hF : ∀ x ∈ ρ.invariants, F x ∈ ρ.invariants)
77     (hA : ∀ i x, x ∈ (τ i).invariants → A i x ∈ (τ i).invariants)
78     (hmap : ∀ x i, e (F x) i = A i (e x i)) :
79     localFactor ρ F hF = ∏ i, localFactor (τ i) (A i) (hA i) := by
80   simp only [localFactor, polynomial_product ρ τ e he F A hF hA hmap, map_prod,
81     Finset.prod_inv_distrib]
82 
83 end PaperXI.PolynomialAssembly

Back to source controls