ProjectorSummands.lean

1 import Mathlib.RepresentationTheory.Subrepresentation
2 import Mathlib.LinearAlgebra.Projection
3 
4 /-! Actual equivariant image and complementary kernel of a commuting projector.
5 The carrier is arbitrary; no decomposition or basis for its summands is assumed. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.ProjectorSummands
9 
10 variable {R G V : Type*} [CommRing R] [Monoid G]
11   [AddCommGroup V] [Module R V]
12 
13 variable (ρ : Representation R G V) (E : Module.End R V)
14   (hE : IsIdempotentElem E) (hcomm : ∀ g, ρ g * E = E * ρ g)
15 
16 /-- The summand is the actual image, with its inherited carrier action. -/
17 def image : Subrepresentation ρ where
18   toSubmodule := LinearMap.range E
19   apply_mem_toSubmodule g := by
20     rintro v ⟨x, rfl⟩
21     exact ⟨ρ g x, (LinearMap.congr_fun (hcomm g) x).symm⟩
22 
23 /-- The complementary subrepresentation is the actual kernel. -/
24 def kernel : Subrepresentation ρ where
25   toSubmodule := LinearMap.ker E
26   apply_mem_toSubmodule g := by
27     intro v hv
28     change E (ρ g v) = 0
29     have H : ρ g (E v) = E (ρ g v) := LinearMap.congr_fun (hcomm g) v
30     rw [← H]
31     change E v = 0 at hv
32     rw [hv, map_zero]
33 
34 def inclusion : (image ρ E hcomm).toSubmodule →ₗ[R] V :=
35   (LinearMap.range E).subtype
36 
37 def retraction : V →ₗ[R] (image ρ E hcomm).toSubmodule := E.rangeRestrict
38 
39 include hE in
40 theorem image_iff (v : V) :
41     v ∈ (image ρ E hcomm).toSubmodule ↔ E v = v := (LinearMap.IsIdempotentElem.mem_range_iff hE)
42 
43 include hE in
44 theorem retraction_inclusion (v : (image ρ E hcomm).toSubmodule) :
45     retraction ρ E hcomm (inclusion ρ E hcomm v) = v := by
46   apply Subtype.ext
47   exact (LinearMap.IsIdempotentElem.mem_range_iff hE).mp v.property
48 
49 include hE in
50 theorem split_law :
51     (retraction ρ E hcomm).comp (inclusion ρ E hcomm) = LinearMap.id := by
52   ext v : 1
53   exact retraction_inclusion ρ E hE hcomm v
54 
55 theorem inclusion_retraction :
56     (inclusion ρ E hcomm).comp (retraction ρ E hcomm) = E := rfl
57 
58 theorem inclusion_injective : Function.Injective (inclusion ρ E hcomm) :=
59   Subtype.val_injective
60 
61 include hE in
62 theorem retraction_surjective : Function.Surjective (retraction ρ E hcomm) :=
63   Function.LeftInverse.surjective (retraction_inclusion ρ E hE hcomm)
64 
65 theorem range_inclusion :
66     LinearMap.range (inclusion ρ E hcomm) = LinearMap.range E :=
67   Submodule.range_subtype _
68 
69 theorem inclusion_equivariant (g : G) (v : (image ρ E hcomm).toSubmodule) :
70     inclusion ρ E hcomm ((image ρ E hcomm).toRepresentation g v) =
71       ρ g (inclusion ρ E hcomm v) := rfl
72 
73 theorem retraction_equivariant (g : G) (v : V) :
74     retraction ρ E hcomm (ρ g v) =
75       (image ρ E hcomm).toRepresentation g (retraction ρ E hcomm v) := by
76   apply Subtype.ext
77   exact (LinearMap.congr_fun (hcomm g) v).symm
78 
79 include hE in
80 theorem image_kernel_complementary :
81     IsCompl (image ρ E hcomm).toSubmodule (kernel ρ E hcomm).toSubmodule :=
82   LinearMap.IsIdempotentElem.isCompl hE
83 
84 /-- Addition gives an actual decomposition of the original carrier. -/
85 def decomposition :
86     ((image ρ E hcomm).toSubmodule × (kernel ρ E hcomm).toSubmodule) ≃ₗ[R] V :=
87   Submodule.prodEquivOfIsCompl _ _ (image_kernel_complementary ρ E hE hcomm)
88 
89 theorem decomposition_apply
90     (v : (image ρ E hcomm).toSubmodule × (kernel ρ E hcomm).toSubmodule) :
91     decomposition ρ E hE hcomm v = (v.1 : V) + (v.2 : V) := rfl
92 
93 theorem decomposition_equivariant (g : G)
94     (v : (image ρ E hcomm).toSubmodule × (kernel ρ E hcomm).toSubmodule) :
95     decomposition ρ E hE hcomm
96       ((image ρ E hcomm).toRepresentation g v.1,
97        (kernel ρ E hcomm).toRepresentation g v.2) =
98       ρ g (decomposition ρ E hE hcomm v) := by
99   change ρ g (v.1 : V) + ρ g (v.2 : V) = ρ g ((v.1 : V) + (v.2 : V))
100   exact (map_add (ρ g) _ _).symm
101 
102 theorem decomposition_inverse_first (v : V) :
103     ((decomposition ρ E hE hcomm).symm v).1 = retraction ρ E hcomm v := by
104   apply Subtype.ext
105   have hv := (decomposition ρ E hE hcomm).apply_symm_apply v
106   have hv' := congrArg E hv
107   rw [decomposition_apply, map_add] at hv'
108   rw [(LinearMap.IsIdempotentElem.mem_range_iff hE).mp (((decomposition ρ E hE hcomm).symm v).1.property),
109     show E (((decomposition ρ E hE hcomm).symm v).2 : V) = 0 from
110       ((decomposition ρ E hE hcomm).symm v).2.property, add_zero] at hv'
111   exact hv'
112 
113 include hE in
114 theorem unique_image_kernel_decomposition (v : V) :
115     ∃! w : (image ρ E hcomm).toSubmodule × (kernel ρ E hcomm).toSubmodule,
116       (w.1 : V) + (w.2 : V) = v :=
117   (decomposition ρ E hE hcomm).toEquiv.bijective.existsUnique v
118 
119 end PaperX.ProjectorSummands

Back to source controls