MatrixProjector.lean

1 import PaperX.ProjectorSummands
2 import PaperX.RepresentationLimits
3 
4 /-! Commuting matrix projectors as actual split subrepresentations, and the
5 precise image of their reduction through a surjective coefficient map. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.MatrixProjector
9 open PaperX.RepresentationLimits
10 
11 variable {R Γ ι : Type*} [CommRing R] [Group Γ] [Fintype ι] [DecidableEq ι]
12 
13 def carrier (ρ : MatrixRep R Γ ι) : Representation R Γ (ι → R) :=
14   Matrix.toLinAlgEquiv'.toAlgHom.toMonoidHom.comp ρ
15 
16 /-- Both equations are obligations on the actual integral matrix. -/
17 structure Projector (ρ : MatrixRep R Γ ι) where
18   matrix : Matrix ι ι R
19   idempotent : matrix * matrix = matrix
20   commutes : ∀ g, ρ g * matrix = matrix * ρ g
21 
22 namespace Projector
23 variable {ρ : MatrixRep R Γ ι} (P : Projector ρ)
24 
25 def linear : Module.End R (ι → R) := Matrix.toLinAlgEquiv' P.matrix
26 
27 theorem linear_idempotent : IsIdempotentElem P.linear := by
28   change Matrix.toLinAlgEquiv' P.matrix * Matrix.toLinAlgEquiv' P.matrix = _
29   rw [← map_mul, P.idempotent]
30   rfl
31 
32 theorem linear_commutes (g : Γ) : carrier ρ g * P.linear = P.linear * carrier ρ g := by
33   change Matrix.toLinAlgEquiv' (ρ g) * Matrix.toLinAlgEquiv' P.matrix =
34     Matrix.toLinAlgEquiv' P.matrix * Matrix.toLinAlgEquiv' (ρ g)
35   rw [← map_mul, ← map_mul, P.commutes]
36 
37 def image : Subrepresentation (carrier ρ) :=
38   ProjectorSummands.image (carrier ρ) P.linear P.linear_commutes
39 
40 def kernel : Subrepresentation (carrier ρ) :=
41   ProjectorSummands.kernel (carrier ρ) P.linear P.linear_commutes
42 
43 def inclusion : P.image.toSubmodule →ₗ[R] (ι → R) :=
44   ProjectorSummands.inclusion (carrier ρ) P.linear P.linear_commutes
45 
46 def retraction : (ι → R) →ₗ[R] P.image.toSubmodule :=
47   ProjectorSummands.retraction (carrier ρ) P.linear P.linear_commutes
48 
49 theorem split_law : P.retraction.comp P.inclusion = LinearMap.id :=
50   ProjectorSummands.split_law _ _ P.linear_idempotent P.linear_commutes
51 
52 theorem inclusion_retraction : P.inclusion.comp P.retraction = P.linear := rfl
53 
54 theorem inclusion_equivariant (g : Γ) (v : P.image.toSubmodule) :
55     P.inclusion (P.image.toRepresentation g v) = carrier ρ g (P.inclusion v) := rfl
56 
57 theorem retraction_equivariant (g : Γ) (v : ι → R) :
58     P.retraction (carrier ρ g v) = P.image.toRepresentation g (P.retraction v) :=
59   ProjectorSummands.retraction_equivariant _ _ P.linear_commutes g v
60 
61 theorem image_iff (v : ι → R) :
62     v ∈ P.image.toSubmodule ↔ P.matrix.mulVec v = v :=
63   ProjectorSummands.image_iff _ _ P.linear_idempotent P.linear_commutes v
64 
65 theorem range_inclusion : LinearMap.range P.inclusion = LinearMap.range P.linear :=
66   ProjectorSummands.range_inclusion _ _ P.linear_commutes
67 
68 def decomposition : (P.image.toSubmodule × P.kernel.toSubmodule) ≃ₗ[R] (ι → R) :=
69   ProjectorSummands.decomposition _ _ P.linear_idempotent P.linear_commutes
70 
71 theorem decomposition_equivariant (g : Γ)
72     (v : P.image.toSubmodule × P.kernel.toSubmodule) :
73     P.decomposition (P.image.toRepresentation g v.1, P.kernel.toRepresentation g v.2) =
74       carrier ρ g (P.decomposition v) :=
75   ProjectorSummands.decomposition_equivariant _ _ P.linear_idempotent P.linear_commutes g v
76 
77 variable {S : Type*} [CommRing S]
78 
79 def changeCoefficients (f : R →+* S) : Projector (RepresentationLimits.changeCoefficients f ρ) where
80   matrix := P.matrix.map f
81   idempotent := by rw [← Matrix.map_mul, P.idempotent]
82   commutes g := by
83     change (ρ g).map f * P.matrix.map f = P.matrix.map f * (ρ g).map f
84     rw [← Matrix.map_mul, ← Matrix.map_mul, P.commutes]
85 
86 theorem projection_reduces (f : R →+* S) (v : ι → R) :
87     f ∘ P.matrix.mulVec v = (P.changeCoefficients f).matrix.mulVec (f ∘ v) := by
88   funext i
89   exact f.map_mulVec _ _ i
90 
91 /-- The reduction of the actual image equals the image of the reduced projector.
92 This proves surjectivity onto that image, not only containment. -/
93 theorem image_reduction_iff (f : R →+* S) (hf : Function.Surjective f) (w : ι → S) :
94     (∃ v : P.image.toSubmodule, f ∘ (v : ι → R) = w) ↔
95       w ∈ (P.changeCoefficients f).image.toSubmodule := by
96   constructor
97   · rintro ⟨v, rfl⟩
98     rw [(P.changeCoefficients f).image_iff]
99     rw [← P.projection_reduces, (P.image_iff _).mp v.property]
100   · intro hw
101     choose v hv using fun i => hf (w i)
102     have hvec : f ∘ v = w := funext hv
103     refine ⟨⟨P.matrix.mulVec v, ?_⟩, ?_⟩
104     · exact ⟨v, rfl⟩
105     · rw [P.projection_reduces, hvec, ((P.changeCoefficients f).image_iff _).mp hw]
106 
107 /-- The complementary kernel also has exactly the expected reduced image. -/
108 theorem kernel_reduction_iff (f : R →+* S) (hf : Function.Surjective f) (w : ι → S) :
109     (∃ v : P.kernel.toSubmodule, f ∘ (v : ι → R) = w) ↔
110       w ∈ (P.changeCoefficients f).kernel.toSubmodule := by
111   constructor
112   · rintro ⟨v, rfl⟩
113     change (P.changeCoefficients f).matrix.mulVec (f ∘ (v : ι → R)) = 0
114     rw [← P.projection_reduces]
115     have hv : P.matrix.mulVec (v : ι → R) = 0 := v.property
116     rw [hv]
117     ext i
118     exact map_zero f
119   · intro hw
120     choose v hv using fun i => hf (w i)
121     have hvec : f ∘ v = w := funext hv
122     refine ⟨⟨v - P.linear v, ?_⟩, ?_⟩
123     · change P.linear (v - P.linear v) = 0
124       rw [map_sub]
125       have h : P.linear (P.linear v) = P.linear v :=
126         LinearMap.congr_fun P.linear_idempotent v
127       rw [h, sub_self]
128     · have hm : f ∘ P.matrix.mulVec v = 0 := by
129         rw [P.projection_reduces, hvec]
130         exact hw
131       ext i
132       have hm' := congrFun hm i
133       change f (v i - P.matrix.mulVec v i) = w i
134       rw [map_sub, show f (P.matrix.mulVec v i) = 0 from hm', sub_zero, hv]
135 
136 end Projector
137 end PaperX.MatrixProjector

Back to source controls