source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIII.PacketCoordinates
6 import Mathlib.Algebra.DirectSum.Module
7 
8 /-! # Literal finite direct-sum form of the constructed packet coordinates -/
9 set_option autoImplicit false
10 noncomputable section
11 open scoped BigOperators
12 namespace Komorebi.PaperIII.PacketCoordinates.System
13 universe u v w
14 variable {R : Type u} {M : Type v} {I : Type w}
15 variable [Semiring R] [AddCommMonoid M] [Module R M]
16 variable [Fintype I]
17 variable (P : Komorebi.PaperIII.PacketCoordinates.System R M I)
18 
19 /-- The literal algebraic direct sum printed in Paper III, Section 16. -/
20 abbrev DirectCoordinates := DirectSum I (fun i => LinearMap.range (P.projector i))
21 
22 /-- The pinned finite direct-sum/product equivalence, on the actual packet ranges. -/
23 def directSumToCoordinates : P.DirectCoordinates ≃ₗ[R] P.Coordinates :=
24   DirectSum.linearEquivFunOnFintype R I (fun i => LinearMap.range (P.projector i))
25 
26 /-- Analysis as an equivalence to the literal direct sum, without a supplied coordinate certificate. -/
27 def directSumEquiv : M ≃ₗ[R] P.DirectCoordinates :=
28   P.coordinateEquiv.trans P.directSumToCoordinates.symm
29 
30 /-- The finite product bridge takes literal direct-sum analysis to the same actual tuple. -/
31 @[simp] theorem directSumToCoordinates_analysis (x : M) :
32     P.directSumToCoordinates (P.directSumEquiv x) = P.analysis x := by
33   change P.directSumToCoordinates (P.directSumToCoordinates.symm (P.analysis x)) = P.analysis x
34   exact P.directSumToCoordinates.apply_symm_apply (P.analysis x)
35 
36 /-- Every direct-sum component is the original projected ambient vector. -/
37 @[simp] theorem directSumEquiv_component (x : M) (i : I) :
38     (P.directSumEquiv x i : M) = P.projector i x := by
39   exact congrArg (fun y : P.Coordinates => (y i : M)) (P.directSumToCoordinates_analysis x)
40 
41 /-- The inverse of literal direct-sum analysis is the finite ambient sum. -/
42 @[simp] theorem directSumEquiv_symm_apply (x : P.DirectCoordinates) :
43     P.directSumEquiv.symm x = ∑ i, (x i : M) := rfl
44 
45 end Komorebi.PaperIII.PacketCoordinates.System

Back to source controls