CarrierSummands.lean

1 import Mathlib.RepresentationTheory.Basic
2 import Mathlib.LinearAlgebra.Pi
3 
4 /-! Explicit summands of a supplied constituent-copy carrier. No arithmetic
5 compatibility or decomposition of an unknown carrier is assumed implicitly. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.CarrierSummands
9 
10 variable {R G I : Type*} [CommRing R] [Monoid G]
11 variable {V : I → Type*} [∀ i, AddCommGroup (V i)] [∀ i, Module R (V i)]
12 
13 abbrev Copies (V : I → Type*) (m : I → ℕ) := (i : I) → Fin (m i) → V i
14 
15 /-- The actual componentwise representation on the selected copies. -/
16 def copiesRep (ρ : ∀ i, Representation R G (V i)) (m : I → ℕ) :
17     Representation R G (Copies V m) where
18   toFun g :=
19     { toFun := fun x i k => ρ i g (x i k)
20       map_add' := by intros; ext i k; simp
21       map_smul' := by intros; ext i k; simp }
22   map_one' := by ext x i k; simp
23   map_mul' g h := by ext x i k; simp
24 
25 @[simp] theorem copiesRep_apply (ρ : ∀ i, Representation R G (V i))
26     (m : I → ℕ) (g : G) (x : Copies V m) (i : I) (k : Fin (m i)) :
27     copiesRep ρ m g x i k = ρ i g (x i k) := rfl
28 
29 /-- Extend by zero in the remaining copies. -/
30 def inclusion {m c : I → ℕ} (_h : ∀ i, m i ≤ c i) :
31     Copies V m →ₗ[R] Copies V c where
32   toFun x i k := if hk : k.val < m i then x i ⟨k.val, hk⟩ else 0
33   map_add' := by intros; ext i k; dsimp; split <;> simp
34   map_smul' := by intros; ext i k; dsimp; split <;> simp
35 
36 /-- Restrict to the first selected copies. -/
37 def retraction {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
38     Copies V c →ₗ[R] Copies V m where
39   toFun x i k := x i ⟨k.val, lt_of_lt_of_le k.isLt (h i)⟩
40   map_add' := by intros; rfl
41   map_smul' := by intros; rfl
42 
43 @[simp] theorem retraction_inclusion {m c : I → ℕ} (h : ∀ i, m i ≤ c i)
44     (x : Copies V m) : retraction (R := R) h (inclusion (R := R) h x) = x := by
45   ext i k
46   simp [retraction, inclusion, k.isLt]
47 
48 theorem split_law {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
49     (retraction (R := R) h (V := V)).comp (inclusion (R := R) h) = LinearMap.id := by
50   ext x : 1
51   exact retraction_inclusion (R := R) h x
52 
53 theorem inclusion_injective {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
54     Function.Injective (inclusion (R := R) h (V := V)) := by
55   exact Function.LeftInverse.injective (retraction_inclusion (R := R) h)
56 
57 theorem retraction_surjective {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
58     Function.Surjective (retraction (R := R) h (V := V)) := by
59   intro x
60   exact ⟨inclusion (R := R) h x, retraction_inclusion (R := R) h x⟩
61 
62 theorem inclusion_equivariant (ρ : ∀ i, Representation R G (V i))
63     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (g : G) (x : Copies V m) :
64     inclusion (R := R) h (copiesRep ρ m g x) = copiesRep ρ c g (inclusion (R := R) h x) := by
65   ext i k
66   dsimp [inclusion]
67   split <;> simp
68 
69 theorem retraction_equivariant (ρ : ∀ i, Representation R G (V i))
70     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (g : G) (x : Copies V c) :
71     retraction (R := R) h (copiesRep ρ c g x) = copiesRep ρ m g (retraction (R := R) h x) := rfl
72 
73 /-- The image is characterized by its unused coordinates, independently of maps. -/
74 def Supported (m c : I → ℕ) (x : Copies V c) : Prop :=
75   ∀ i (k : Fin (c i)), m i ≤ k.val → x i k = 0
76 
77 theorem range_inclusion_iff {m c : I → ℕ} (h : ∀ i, m i ≤ c i)
78     (x : Copies V c) :
79     x ∈ LinearMap.range (inclusion (R := R) h) ↔ Supported m c x := by
80   constructor
81   · rintro ⟨y, rfl⟩ i k hk
82     simp [inclusion, not_lt.mpr hk]
83   · intro hx
84     refine ⟨retraction (R := R) h x, ?_⟩
85     ext i k
86     dsimp [inclusion, retraction]
87     split
88     · rfl
89     · rename_i hk
90       exact (hx i k (le_of_not_gt hk)).symm
91 
92 def projector {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
93     Module.End R (Copies V c) := (inclusion (R := R) h).comp (retraction (R := R) h)
94 
95 theorem projector_idempotent {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
96     (projector (R := R) h (V := V)).comp (projector (R := R) h) = projector (R := R) h := by
97   ext x : 1
98   exact congrArg (inclusion (R := R) h) (retraction_inclusion (R := R) h (retraction (R := R) h x))
99 
100 theorem projector_equivariant (ρ : ∀ i, Representation R G (V i))
101     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (g : G) :
102     (projector (R := R) h).comp (copiesRep ρ c g) = (copiesRep ρ c g).comp (projector (R := R) h) := by
103   ext x : 1
104   exact inclusion_equivariant ρ h g (retraction (R := R) h x)
105 
106 theorem projector_fixed_iff {m c : I → ℕ} (h : ∀ i, m i ≤ c i)
107     (x : Copies V c) : projector (R := R) h x = x ↔ Supported m c x := by
108   rw [← range_inclusion_iff (R := R) h x]
109   constructor
110   · intro hx; exact ⟨retraction (R := R) h x, hx⟩
111   · rintro ⟨y, rfl⟩
112     exact congrArg (inclusion (R := R) h) (retraction_inclusion (R := R) h y)
113 
114 variable {W : Type*} [AddCommGroup W] [Module R W]
115 
116 /-- Transport into an original carrier using a supplied decomposition. -/
117 def transportedInclusion {m c : I → ℕ} (h : ∀ i, m i ≤ c i)
118     (D : W ≃ₗ[R] Copies V c) : Copies V m →ₗ[R] W :=
119   D.symm.toLinearMap.comp (inclusion (R := R) h)
120 
121 def transportedRetraction {m c : I → ℕ} (h : ∀ i, m i ≤ c i)
122     (D : W ≃ₗ[R] Copies V c) : W →ₗ[R] Copies V m :=
123   (retraction (R := R) h).comp D.toLinearMap
124 
125 theorem transported_split {m c : I → ℕ} (h : ∀ i, m i ≤ c i)
126     (D : W ≃ₗ[R] Copies V c) (x : Copies V m) :
127     transportedRetraction h D (transportedInclusion h D x) = x := by
128   simp [transportedRetraction, transportedInclusion]
129 
130 theorem transported_inclusion_equivariant (ρ : ∀ i, Representation R G (V i))
131     (σ : Representation R G W) {m c : I → ℕ} (h : ∀ i, m i ≤ c i)
132     (D : W ≃ₗ[R] Copies V c)
133     (hD : ∀ g x, D (σ g x) = copiesRep ρ c g (D x)) (g : G) (x : Copies V m) :
134     transportedInclusion h D (copiesRep ρ m g x) = σ g (transportedInclusion h D x) := by
135   apply D.injective
136   simp only [transportedInclusion, LinearMap.comp_apply, LinearEquiv.coe_coe,
137     LinearEquiv.apply_symm_apply, hD]
138   exact inclusion_equivariant ρ h g x
139 
140 theorem transported_retraction_equivariant (ρ : ∀ i, Representation R G (V i))
141     (σ : Representation R G W) {m c : I → ℕ} (h : ∀ i, m i ≤ c i)
142     (D : W ≃ₗ[R] Copies V c)
143     (hD : ∀ g x, D (σ g x) = copiesRep ρ c g (D x)) (g : G) (x : W) :
144     transportedRetraction h D (σ g x) = copiesRep ρ m g (transportedRetraction h D x) := by
145   change retraction (R := R) h (D (σ g x)) = _
146   rw [hD]
147   exact retraction_equivariant ρ h g (D x)
148 
149 end PaperX.CarrierSummands

Back to source controls