Source: ProCGroups.FoxDifferential.Common.FiniteFamilyLinearMap
1import Mathlib.Algebra.Exact.Basic
3/-!
4# Fox differential: common — finite family linear map
6The principal declarations in this module are:
8- `finiteFamilyLinearMap`
9 The linear map represented by a finite family of target vectors.
10- `piReindexLinearEquiv`
11 Reindex finite coordinate functions by an equivalence of index types.
12- `finiteFamilyLinearMap_apply`
13 The linear map represented by `generators` evaluates a coordinate vector as the finite sum `∑ i, x
14 i • generators i`.
15- `finiteFamilyLinearMap_single`
16 A finite-family linear map sends a coordinate basis vector to the corresponding generator.
17-/
19namespace FoxDifferential
21noncomputable section
23open scoped BigOperators
25section FiniteFamilyLinearMap
27variable {R : Type*} [Semiring R]
28variable {M : Type*} [AddCommMonoid M] [Module R M]
29variable {X : Type*} [Fintype X] [DecidableEq X]
31/-- The linear map represented by a finite family of target vectors. -/
32def finiteFamilyLinearMap (generators : X → M) :
33 (X → R) →ₗ[R] M where
34 toFun x := ∑ i, x i • generators i
35 map_add' x y := by
36 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
37 map_smul' a x := by
38 simp only [Pi.smul_apply, smul_eq_mul, mul_smul, RingHom.id_apply, Finset.smul_sum]
40omit [DecidableEq X] in
41/--
42The linear map represented by `generators` evaluates a coordinate vector as the finite sum `∑ i, x i
43• generators i`.
44-/
45theorem finiteFamilyLinearMap_apply (generators : X → M) (x : X → R) :
46 finiteFamilyLinearMap (R := R) generators x = ∑ i, x i • generators i := rfl
48/-- A finite-family linear map sends a coordinate basis vector to the corresponding generator. -/
49@[simp 900]
50theorem finiteFamilyLinearMap_single (generators : X → M) (i : X) :
51 finiteFamilyLinearMap (R := R) generators (Pi.single i 1) = generators i := by
52 rw [finiteFamilyLinearMap_apply]
53 rw [Finset.sum_eq_single i]
54 · simp only [Pi.single_eq_same, one_smul]
55 · intro j _ hji
56 simp only [ne_eq, hji, not_false_eq_true, Pi.single_eq_of_ne, zero_smul]
57 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
59section Reindex
61variable {Y : Type*} [Fintype Y] [DecidableEq Y]
63/-- Reindex finite coordinate functions by an equivalence of index types. -/
64def piReindexLinearEquiv (e : X ≃ Y) :
65 (X → R) ≃ₗ[R] (Y → R) where
66 toFun f := fun y => f (e.symm y)
67 invFun f := fun x => f (e x)
68 left_inv := by
69 intro f
70 funext x
71 simp only [Equiv.symm_apply_apply]
72 right_inv := by
73 intro f
74 funext y
75 simp only [Equiv.apply_symm_apply]
76 map_add' := by
77 intro f g
78 funext y
79 simp only [Pi.add_apply]
80 map_smul' := by
81 intro a f
82 funext y
83 simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
85omit [DecidableEq X] [DecidableEq Y] in
86/-- Finite-family linear maps are invariant under reindexing of their finite coordinate type. -/
87theorem finiteFamilyLinearMap_reindex
88 (e : X ≃ Y) (generators : Y → M) :
89 finiteFamilyLinearMap (R := R) (fun x : X => generators (e x)) =
90 (finiteFamilyLinearMap (R := R) generators).comp
91 (piReindexLinearEquiv (R := R) e).toLinearMap := by
92 apply LinearMap.ext
93 intro f
94 rw [finiteFamilyLinearMap_apply, LinearMap.comp_apply, finiteFamilyLinearMap_apply]
95 exact
96 Fintype.sum_equiv e
97 (fun x : X => f x • generators (e x))
98 (fun y : Y => f (e.symm y) • generators y)
99 (by intro x; simp only [Equiv.symm_apply_apply])
101end Reindex
103/--
104A coordinate map sending a finite generating family to the standard basis is a left inverse to
105the corresponding finite-family linear map.
106-/
107theorem finiteFamilyLinearMap_leftInverse_of_mapsToSingle
108 (generators : X → M) (coordinateMap : M →ₗ[R] (X → R))
109 (hcoord : ∀ i : X, coordinateMap (generators i) = Pi.single i 1) :
110 coordinateMap.comp (finiteFamilyLinearMap (R := R) generators) = LinearMap.id := by
111 classical
112 apply LinearMap.ext
113 intro x
114 funext k
115 rw [LinearMap.comp_apply, finiteFamilyLinearMap_apply, LinearMap.id_apply]
116 calc
117 coordinateMap (∑ i, x i • generators i) k =
118 (∑ i, x i • coordinateMap (generators i)) k := by
119 rw [map_sum, Finset.sum_apply, Finset.sum_apply]
120 apply Finset.sum_congr rfl
121 intro i hi
122 simp only [map_smul, Pi.smul_apply, smul_eq_mul]
123 _ = (∑ i, x i • (Pi.single i (1 : R) : X → R)) k := by
124 rw [Finset.sum_apply, Finset.sum_apply]
125 apply Finset.sum_congr rfl
126 intro i hi
127 rw [hcoord i]
128 _ = x k := by
129 rw [Finset.sum_apply, Finset.sum_eq_single k]
130 · simp only [Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one]
131 · intro i _ hik
132 simp only [Pi.smul_apply, Pi.single_eq_of_ne (Ne.symm hik), smul_eq_mul, mul_zero]
133 · simp only [Finset.mem_univ, not_true_eq_false, Pi.smul_apply, Pi.single_eq_same,
134 smul_eq_mul, mul_one,
135 IsEmpty.forall_iff]
137omit [DecidableEq X] in
138/--
139The image of a finite-family linear map is exactly the submodule spanned by its target family.
140-/
141theorem finiteFamilyLinearMap_range_eq_span (generators : X → M) :
142 LinearMap.range (finiteFamilyLinearMap (R := R) generators) =
143 Submodule.span R (Set.range generators) := by
144 classical
145 apply le_antisymm
146 · intro y hy
147 rcases hy with ⟨x, rfl⟩
148 rw [finiteFamilyLinearMap_apply]
149 exact Submodule.sum_mem _ fun i _ =>
150 (Submodule.span R (Set.range generators)).smul_mem (x i)
151 (Submodule.subset_span ⟨i, rfl⟩)
152 · refine Submodule.span_le.2 ?_
153 rintro y ⟨i, rfl⟩
154 exact ⟨Pi.single i 1, finiteFamilyLinearMap_single (R := R) generators i⟩
156omit [DecidableEq X] in
157/-- A finite-family linear map is surjective when its target family spans the codomain. -/
158theorem finiteFamilyLinearMap_surjective_of_span_eq_top
159 (generators : X → M)
160 (hspan : Submodule.span R (Set.range generators) = ⊤) :
161 Function.Surjective (finiteFamilyLinearMap (R := R) generators) := by
162 apply (LinearMap.range_eq_top).1
163 rw [finiteFamilyLinearMap_range_eq_span, hspan]
165omit [DecidableEq X] in
166/-- Surjectivity of a finite-family map is exactly the statement that the target family spans. -/
167theorem finiteFamilyLinearMap_surjective_iff_span_eq_top
168 {generators : X → M} :
169 Function.Surjective (finiteFamilyLinearMap (R := R) generators) ↔
170 Submodule.span R (Set.range generators) = ⊤ := by
171 rw [← LinearMap.range_eq_top, finiteFamilyLinearMap_range_eq_span]
173end FiniteFamilyLinearMap
175end
177end FoxDifferential