source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import Mathlib.LinearAlgebra.Pi
6 
7 /-!
8 # Actual coordinates of a finite orthogonal projector family
9 
10 The coordinate type is the dependent product of the actual projector ranges.
11 Analysis and synthesis are constructed from the projectors, not supplied as an
12 invertibility certificate. Finiteness identifies this product with the finite
13 algebraic direct sum used in Paper III, Section 16. Zero projectors and the empty
14 index type are allowed; completeness then imposes the appropriate degeneracy.
15 -/
16 set_option autoImplicit false
17 noncomputable section
18 open scoped BigOperators
19 
20 namespace Komorebi.PaperIII.PacketCoordinates
21 universe u v w
22 
23 /-- A complete, pairwise orthogonal family of idempotent linear endomorphisms. -/
24 structure System (R : Type u) (M : Type v) (I : Type w)
25     [Semiring R] [AddCommMonoid M] [Module R M] [Fintype I] where
26   projector : I → M →ₗ[R] M
27   complete : ∑ i, projector i = LinearMap.id
28   idempotent : ∀ i, (projector i).comp (projector i) = projector i
29   orthogonal : ∀ i j, i ≠ j → (projector i).comp (projector j) = 0
30 
31 namespace System
32 variable {R : Type u} {M : Type v} {I : Type w}
33 variable [Semiring R] [AddCommMonoid M] [Module R M] [Fintype I]
34 variable (P : System R M I)
35 
36 /-- The coordinate in slot `i` belongs to the actual range of projector `i`. -/
37 abbrev Coordinates := (i : I) → LinearMap.range (P.projector i)
38 
39 /-- A vector in a projector range is fixed by that projector. -/
40 theorem projector_range_self (i : I) (x : LinearMap.range (P.projector i)) :
41     P.projector i (x : M) = (x : M) := by
42   rcases x.property with ⟨y, hy⟩
43   rw [← hy]
44   exact LinearMap.congr_fun (P.idempotent i) y
45 
46 /-- Distinct projectors annihilate vectors in each other's ranges. -/
47 theorem projector_range_other (i j : I) (h : i ≠ j)
48     (x : LinearMap.range (P.projector j)) : P.projector i (x : M) = 0 := by
49   rcases x.property with ⟨y, hy⟩
50   rw [← hy]
51   exact LinearMap.congr_fun (P.orthogonal i j h) y
52 
53 /-- Split an ambient vector into its projected components. -/
54 def analysis : M →ₗ[R] P.Coordinates where
55   toFun x i := ⟨P.projector i x, ⟨x, rfl⟩⟩
56   map_add' x y := by
57     funext i
58     apply Subtype.ext
59     exact (P.projector i).map_add x y
60   map_smul' r x := by
61     funext i
62     apply Subtype.ext
63     exact (P.projector i).map_smul r x
64 
65 /-- Reconstruct an ambient vector by summing the complete packet tuple. -/
66 def synthesis : P.Coordinates →ₗ[R] M where
67   toFun x := ∑ i, (x i : M)
68   map_add' x y := by
69     change (∑ i, ((x i : M) + (y i : M))) = _
70     exact Finset.sum_add_distrib
71   map_smul' r x := by
72     change (∑ i, r • (x i : M)) = r • (∑ i, (x i : M))
73     exact Finset.smul_sum.symm
74 
75 @[simp] theorem analysis_apply (x : M) (i : I) :
76     (P.analysis x i : M) = P.projector i x := rfl
77 
78 @[simp] theorem synthesis_apply (x : P.Coordinates) :
79     P.synthesis x = ∑ i, (x i : M) := rfl
80 
81 /-- Completeness proves synthesis after analysis is the ambient identity. -/
82 @[simp] theorem synthesis_analysis (x : M) : P.synthesis (P.analysis x) = x := by
83   change (∑ i, P.projector i x) = x
84   simpa only [LinearMap.sum_apply, LinearMap.id_apply] using
85     LinearMap.congr_fun P.complete x
86 
87 /-- Idempotence and orthogonality prove analysis after synthesis is the tuple identity. -/
88 @[simp] theorem analysis_synthesis (x : P.Coordinates) : P.analysis (P.synthesis x) = x := by
89   classical
90   funext i
91   apply Subtype.ext
92   change P.projector i (∑ j, (x j : M)) = (x i : M)
93   rw [map_sum]
94   rw [Finset.sum_eq_single i]
95   · exact P.projector_range_self i (x i)
96   · intro j _ hji
97     exact P.projector_range_other i j hji.symm (x j)
98   · simp
99 
100 /-- The coordinate linear equivalence is constructed from the projector axioms. -/
101 def coordinateEquiv : M ≃ₗ[R] P.Coordinates :=
102   { P.analysis with
103     invFun := P.synthesis
104     left_inv := P.synthesis_analysis
105     right_inv := P.analysis_synthesis }
106 
107 @[simp] theorem coordinateEquiv_apply (x : M) : P.coordinateEquiv x = P.analysis x := rfl
108 @[simp] theorem coordinateEquiv_symm_apply (x : P.Coordinates) :
109     P.coordinateEquiv.symm x = P.synthesis x := rfl
110 
111 /-- Range membership and being fixed are literally the same packet condition. -/
112 theorem mem_range_iff_fixed (i : I) (x : M) :
113     x ∈ LinearMap.range (P.projector i) ↔ P.projector i x = x := by
114   constructor
115   · intro hx
116     exact P.projector_range_self i ⟨x, hx⟩
117   · intro hx
118     exact ⟨x, hx⟩
119 
120 /-- Complete projected data distinguish ambient vectors. -/
121 theorem analysis_injective : Function.Injective P.analysis := by
122   intro x y h
123   have hh := congrArg P.synthesis h
124   simpa only [P.synthesis_analysis] using hh
125 
126 /-- Every legal packet tuple is realized by its actual finite sum. -/
127 theorem analysis_surjective : Function.Surjective P.analysis := by
128   intro x
129   exact ⟨P.synthesis x, P.analysis_synthesis x⟩
130 
131 end System
132 end Komorebi.PaperIII.PacketCoordinates

Back to source controls