FiniteOrbitAverage68.lean

1 import Mathlib.RepresentationTheory.Intertwining
2 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
3 import Mathlib.Algebra.BigOperators.Field
4 
5 /-! Finite-orbit averaging with preservation of a genuine affine constraint. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.FiniteOrbitAverage68
9 
10 open Representation
11 
12 variable {k G V W : Type*} [Field k] [CharZero k] [Group G]
13   [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W]
14 
15 /-- The actual orbit as a subtype, not a chosen collection of group elements. -/
16 abbrev Orbit (ρ : Representation k G V) (v : V) :=
17   {w : V // w ∈ Set.range fun g => ρ g v}
18 
19 /-- Translation permutes every orbit. -/
20 def orbitEquiv (ρ : Representation k G V) (v : V) (g : G) :
21     Orbit ρ v ≃ Orbit ρ v where
22   toFun w := ⟨ρ g w, by
23     obtain ⟨h, hh⟩ := w.property
24     exact ⟨g * h, by simp [hh, Module.End.mul_apply]⟩⟩
25   invFun w := ⟨ρ g⁻¹ w, by
26     obtain ⟨h, hh⟩ := w.property
27     exact ⟨g⁻¹ * h, by simp [hh, Module.End.mul_apply]⟩⟩
28   left_inv w := Subtype.ext (ρ.inv_self_apply g w)
29   right_inv w := Subtype.ext (ρ.self_inv_apply g w)
30 
31 /-- Average over distinct orbit points. -/
32 def average (ρ : Representation k G V) (v : V)
33     (h : Set.Finite (Set.range fun g => ρ g v)) : V :=
34   let : Fintype (Orbit ρ v) := h.fintype
35   (Fintype.card (Orbit ρ v) : k)⁻¹ • ∑ w : Orbit ρ v, (w : V)
36 
37 omit [CharZero k] in
38 /-- The mean is invariant because each group element permutes the same finite
39 set of actual orbit points. -/
40 theorem average_invariant (ρ : Representation k G V) (v : V)
41     (h : Set.Finite (Set.range fun g => ρ g v)) (g : G) :
42     ρ g (average ρ v h) = average ρ v h := by
43   let : Fintype (Orbit ρ v) := h.fintype
44   change ρ g ((Fintype.card (Orbit ρ v) : k)⁻¹ • ∑ w : Orbit ρ v, (w : V)) = _
45   rw [map_smul, map_sum]
46   congr 1
47   exact (orbitEquiv ρ v g).sum_comp (fun w : Orbit ρ v => (w : V))
48 
49 /-- Any affine linear constraint satisfied by every orbit point survives the
50 average.  In particular, an orbit of linear splittings averages to a splitting. -/
51 theorem average_constraint (ρ : Representation k G V) (v : V)
52     (h : Set.Finite (Set.range fun g => ρ g v))
53     (p : V →ₗ[k] W) (w : W) (hw : ∀ g, p (ρ g v) = w) :
54     p (average ρ v h) = w := by
55   let : Fintype (Orbit ρ v) := h.fintype
56   let : Nonempty (Orbit ρ v) := ⟨⟨v, ⟨1, by simp⟩⟩⟩
57   have hc : (Fintype.card (Orbit ρ v) : k) ≠ 0 :=
58     Nat.cast_ne_zero.mpr (Fintype.card_ne_zero)
59   have hall : ∀ x : Orbit ρ v, p (x : V) = w := by
60     rintro ⟨x, g, rfl⟩
61     exact hw g
62   change p ((Fintype.card (Orbit ρ v) : k)⁻¹ • ∑ x : Orbit ρ v, (x : V)) = w
63   rw [map_smul, map_sum]
64   simp only [hall, Finset.sum_const, Finset.card_univ]
65   rw [← Nat.cast_smul_eq_nsmul k, smul_smul, inv_mul_cancel₀ hc, one_smul]
66 
67 /-- An invariant vector in the actual Hom representation is an intertwiner. -/
68 def invariantHom (ρ : Representation k G V) (τ : Representation k G W)
69     (s : V →ₗ[k] W) (hs : ∀ g, linHom ρ τ g s = s) :
70     IntertwiningMap ρ τ where
71   toLinearMap := s
72   isIntertwining' g := by
73     ext v
74     have he := LinearMap.congr_fun (hs g) (ρ g v)
75     simpa only [linHom_apply, LinearMap.comp_apply, inv_self_apply] using he.symm
76 
77 /-- Finite-orbit averaging constructs an equivariant right inverse, without
78 assuming semisimplicity of the target representation. -/
79 theorem equivariant_section_of_finite_orbit
80     (ρ : Representation k G V) (τ : Representation k G W)
81     (p : IntertwiningMap τ ρ) (s : V →ₗ[k] W)
82     (hs : ∀ v, p (s v) = v)
83     (hfinite : Set.Finite (Set.range fun g => linHom ρ τ g s)) :
84     ∃ a : IntertwiningMap ρ τ, ∀ v, p (a v) = v := by
85   let m := average (linHom ρ τ) s hfinite
86   let a := invariantHom ρ τ m (average_invariant (linHom ρ τ) s hfinite)
87   refine ⟨a, ?_⟩
88   let post : (V →ₗ[k] W) →ₗ[k] (V →ₗ[k] V) :=
89     { toFun := fun f => p.toLinearMap.comp f
90       map_add' := fun f g => by ext v; simp
91       map_smul' := fun c f => by ext v; simp }
92   have hpost : ∀ g, post (linHom ρ τ g s) = LinearMap.id := by
93     intro g
94     ext v
95     change p (τ g (s (ρ g⁻¹ v))) = v
96     rw [p.isIntertwining, hs, self_inv_apply]
97   have hm := average_constraint (linHom ρ τ) s hfinite post LinearMap.id hpost
98   intro v
99   exact LinearMap.congr_fun hm v
100 
101 end PaperXI.FiniteOrbitAverage68

Back to source controls