FoxDifferential/Common/FiniteFamilyLinearMap.lean
1import Mathlib.Algebra.Exact
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Common/FiniteFamilyLinearMap.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite-family linear maps
16coordinate functions, and its range is the span of the family.
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/-- Evaluate a finite-family linear map as the corresponding finite sum. -/
42theorem finiteFamilyLinearMap_apply (generators : X → M) (x : X → R) :
43 finiteFamilyLinearMap (R := R) generators x = ∑ i, x i • generators i := rfl
45/-- A finite-family linear map sends a coordinate basis vector to the corresponding generator. -/
46@[simp 900]
47theorem finiteFamilyLinearMap_single (generators : X → M) (i : X) :
48 finiteFamilyLinearMap (R := R) generators (Pi.single i 1) = generators i := by
50 rw [Finset.sum_eq_single i]
51 · simp only [Pi.single_eq_same, one_smul]
52 · intro j _ hji
53 simp only [ne_eq, hji, not_false_eq_true, Pi.single_eq_of_ne, zero_smul]
54 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
56section Reindex
58variable {Y : Type*} [Fintype Y] [DecidableEq Y]
60/-- Reindex finite coordinate functions by an equivalence of index types. -/
61def piReindexLinearEquiv (e : X ≃ Y) :
62 (X → R) ≃ₗ[R] (Y → R) where
63 toFun f := fun y => f (e.symm y)
64 invFun f := fun x => f (e x)
65 left_inv := by
66 intro f
67 funext x
68 simp only [Equiv.symm_apply_apply]
69 right_inv := by
70 intro f
71 funext y
72 simp only [Equiv.apply_symm_apply]
73 map_add' := by
74 intro f g
75 funext y
76 simp only [Pi.add_apply]
77 map_smul' := by
78 intro a f
79 funext y
80 simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
82omit [DecidableEq X] [DecidableEq Y] in
83/-- Finite-family linear maps are invariant under reindexing of their finite coordinate type. -/
84theorem finiteFamilyLinearMap_reindex
85 (e : X ≃ Y) (generators : Y → M) :
86 finiteFamilyLinearMap (R := R) (fun x : X => generators (e x)) =
87 (finiteFamilyLinearMap (R := R) generators).comp
88 (piReindexLinearEquiv (R := R) e).toLinearMap := by
89 apply LinearMap.ext
90 intro f
91 rw [finiteFamilyLinearMap_apply, LinearMap.comp_apply, finiteFamilyLinearMap_apply]
92 exact
93 Fintype.sum_equiv e
94 (fun x : X => f x • generators (e x))
95 (fun y : Y => f (e.symm y) • generators y)
96 (by intro x; simp only [Equiv.symm_apply_apply])
98end Reindex
100/-- A coordinate map sending a finite generating family to the standard basis is a left inverse to
103 (generators : X → M) (coordinateMap : M →ₗ[R] (X → R))
104 (hcoord : ∀ i : X, coordinateMap (generators i) = Pi.single i 1) :
105 coordinateMap.comp (finiteFamilyLinearMap (R := R) generators) = LinearMap.id := by
106 classical
107 apply LinearMap.ext
108 intro x
109 funext k
110 rw [LinearMap.comp_apply, finiteFamilyLinearMap_apply, LinearMap.id_apply]
111 calc
112 coordinateMap (∑ i, x i • generators i) k =
113 (∑ i, x i • coordinateMap (generators i)) k := by
114 rw [map_sum, Finset.sum_apply, Finset.sum_apply]
115 apply Finset.sum_congr rfl
116 intro i hi
118 _ = (∑ i, x i • (Pi.single i (1 : R) : X → R)) k := by
119 rw [Finset.sum_apply, Finset.sum_apply]
120 apply Finset.sum_congr rfl
121 intro i hi
122 rw [hcoord i]
123 _ = x k := by
124 rw [Finset.sum_apply, Finset.sum_eq_single k]
125 · simp only [Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one]
126 · intro i _ hik
127 simp only [Pi.smul_apply, Pi.single_eq_of_ne (Ne.symm hik), smul_eq_mul, mul_zero]
128 · simp only [Finset.mem_univ, not_true_eq_false, Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one,
129 IsEmpty.forall_iff]
131/-- The image of a finite-family linear map is exactly the submodule spanned by its target
132family. -/
133theorem finiteFamilyLinearMap_range_eq_span (generators : X → M) :
134 LinearMap.range (finiteFamilyLinearMap (R := R) generators) =
135 Submodule.span R (Set.range generators) := by
136 classical
137 apply le_antisymm
138 · intro y hy
139 rcases hy with ⟨x, rfl⟩
141 exact Submodule.sum_mem _ fun i _ =>
142 (Submodule.span R (Set.range generators)).smul_mem (x i)
143 (Submodule.subset_span ⟨i, rfl⟩)
144 · refine Submodule.span_le.2 ?_
145 rintro y ⟨i, rfl⟩
146 exact ⟨Pi.single i 1, finiteFamilyLinearMap_single (R := R) generators i⟩
148/-- A finite-family linear map is surjective when its target family spans the codomain. -/
150 (generators : X → M)
151 (hspan : Submodule.span R (Set.range generators) = ⊤) :
152 Function.Surjective (finiteFamilyLinearMap (R := R) generators) := by
153 apply (LinearMap.range_eq_top).1
154 rw [finiteFamilyLinearMap_range_eq_span, hspan]
156/-- Surjectivity of a finite-family map is exactly the statement that the target family spans. -/
158 (generators : X → M) :
159 Function.Surjective (finiteFamilyLinearMap (R := R) generators) ↔
160 Submodule.span R (Set.range generators) = ⊤ := by
161 rw [← LinearMap.range_eq_top, finiteFamilyLinearMap_range_eq_span]
163end FiniteFamilyLinearMap
165end
167end FoxDifferential