FamilySummands.lean

1 import PaperX.OrthogonalProjectors
2 
3 /-! A complete orthogonal family gives the full equivariant decomposition into
4 its actual images. No bases or freeness of those images are assumed. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.OrthogonalProjectors
8 namespace Family
9 open PaperX.RepresentationLimits PaperX.MatrixProjector
10 open PaperX.OrthogonalProjectors
11 open scoped BigOperators
12 
13 variable {R Γ ι J : Type*} [CommRing R] [Group Γ]
14   [Fintype ι] [DecidableEq ι] [Fintype J]
15   {ρ : MatrixRep R Γ ι} (E : Family ρ J)
16 
17 theorem linear_total : ∑ j, (E.projector j).linear = LinearMap.id := by
18   change ∑ j, Matrix.toLinAlgEquiv' (E.projector j).matrix = _
19   rw [← map_sum, E.total, map_one]
20   rfl
21 
22 theorem linear_orthogonal (i j : J) (hij : i ≠ j) :
23     (E.projector i).linear * (E.projector j).linear = 0 := by
24   change Matrix.toLinAlgEquiv' (E.projector i).matrix *
25     Matrix.toLinAlgEquiv' (E.projector j).matrix = 0
26   rw [← map_mul, E.orthogonal i j hij, map_zero]
27 
28 /-- Every component is the actual image of the corresponding projector. -/
29 abbrev Components := ∀ j, (E.projector j).image.toSubmodule
30 
31 def assemble : E.Components →ₗ[R] (ι → R) where
32   toFun v := ∑ j, ((v j : (E.projector j).image.toSubmodule) : ι → R)
33   map_add' v w := by simp [Finset.sum_add_distrib]
34   map_smul' a v := by simp [Finset.smul_sum]
35 
36 def components : (ι → R) →ₗ[R] E.Components :=
37   LinearMap.pi fun j => (E.projector j).retraction
38 
39 theorem linear_image (j : J) (v : (E.projector j).image.toSubmodule) :
40     (E.projector j).linear (v : ι → R) = v := by
41   exact ((E.projector j).image_iff _).mp v.property
42 
43 theorem linear_other_image (i j : J) (hij : i ≠ j)
44     (v : (E.projector j).image.toSubmodule) :
45     (E.projector i).linear (v : ι → R) = 0 := by
46   rw [← E.linear_image j v]
47   exact LinearMap.congr_fun (E.linear_orthogonal i j hij) (v : ι → R)
48 
49 theorem assemble_components (v : ι → R) : E.assemble (E.components v) = v := by
50   change (∑ j, (E.projector j).linear v) = v
51   have h := LinearMap.congr_fun E.linear_total v
52   simpa using h
53 
54 theorem components_assemble (v : E.Components) : E.components (E.assemble v) = v := by
55   classical
56   funext i
57   apply Subtype.ext
58   change (E.projector i).linear (∑ j, (v j : ι → R)) = (v i : ι → R)
59   rw [map_sum, Finset.sum_eq_single i]
60   · exact E.linear_image i (v i)
61   · intro j _ hji
62     exact E.linear_other_image i j (Ne.symm hji) (v j)
63   · simp
64 
65 /-- The full decomposition, with summation as its forward map. -/
66 def decomposition : E.Components ≃ₗ[R] (ι → R) :=
67   LinearEquiv.ofLinearMap E.assemble E.components
68     (LinearMap.ext E.assemble_components) (LinearMap.ext E.components_assemble)
69 
70 theorem decomposition_apply (v : E.Components) :
71     E.decomposition v = ∑ j, (v j : ι → R) := rfl
72 
73 theorem decomposition_symm_apply (v : ι → R) (j : J) :
74     E.decomposition.symm v j = (E.projector j).retraction v := rfl
75 
76 theorem decomposition_equivariant (g : Γ) (v : E.Components) :
77     E.decomposition (fun j => (E.projector j).image.toRepresentation g (v j)) =
78       carrier ρ g (E.decomposition v) := by
79   change (∑ j, carrier ρ g (v j : ι → R)) = carrier ρ g (∑ j, (v j : ι → R))
80   rw [map_sum]
81 
82 theorem inverse_equivariant (g : Γ) (v : ι → R) (j : J) :
83     E.decomposition.symm (carrier ρ g v) j =
84       (E.projector j).image.toRepresentation g (E.decomposition.symm v j) :=
85   (E.projector j).retraction_equivariant g v
86 
87 end Family
88 end PaperX.OrthogonalProjectors

Back to source controls