GrammarPaths.lean

1 import PaperIRelease.GrammarEquivalence
2 import Mathlib.Data.Finsupp.Basic
3 
4 set_option autoImplicit false
5 set_option maxHeartbeats 2000000
6 set_option linter.unusedVariables false
7 set_option linter.unnecessarySimpa false
8 set_option linter.unusedSimpArgs false
9 set_option linter.unusedSectionVars false
10 
11 noncomputable section
12 
13 namespace Komorebi.PaperIRelease.GrammarAlgebra
14 
15 open CategoryTheory
16 open scoped BigOperators
17 
18 universe u
19 variable {K V E : Type u} [Field K] [Fintype V]
20 attribute [local instance] Classical.propDecidable
21 
22 /-- A path retains its declared source and target in its type. -/
23 inductive TypedPath (s t : E → V) : V → V → Type u where
24   | nil (v : V) : TypedPath s t v v
25   | cons {v : V} (a : E) : TypedPath s t v (s a) → TypedPath s t v (t a)
26 
27 variable {s t : E → V}
28 
29 /-- Paths embed as vertex/arrow words; multiplication is composition from right to left. -/
30 def TypedPath.word : {v w : V} → TypedPath s t v w → Free K V E
31   | _, _, .nil v => vertexWord K V E v
32   | _, _, .cons a p => arrowWord K V E a * p.word
33 
34 /-- A homogeneous path relation is a finite K-linear combination at fixed endpoints. -/
35 abbrev PathCombination (s t : E → V) (v w : V) := TypedPath s t v w →₀ K
36 
37 def pathCombinationWord {v w : V} (p : PathCombination (K := K) s t v w) : Free K V E :=
38   p.sum (fun q c => c • q.word)
39 
40 variable {G : Grammar K V E}
41 
42 /-- The action of a typed path is the actual composition of its declared arrow maps. -/
43 def TypedData.pathMap (X : TypedData G) :
44     {v w : V} → TypedPath G.source G.target v w → (X.space v →ₗ[K] X.space w)
45   | _, _, .nil _ => LinearMap.id
46   | _, _, .cons a p => (X.arrow a).comp (X.pathMap p)
47 
48 /-- The constructed free-algebra action sends each path to its source-to-target block. -/
49 theorem TypedData.path_action (X : TypedData G) {v w : V}
50     (p : TypedPath G.source G.target v w) :
51     X.freeAction (p.word (K := K)) =
52       (LinearMap.single K X.space w).comp ((X.pathMap p).comp (LinearMap.proj v)) := by
53   classical
54   induction p with
55   | nil =>
56       apply LinearMap.ext
57       intro x
58       simp [TypedPath.word, freeAction, vertexWord, vertexOperator, pathMap]
59   | cons a p ih =>
60       apply LinearMap.ext
61       intro x
62       rw [TypedPath.word, map_mul, Module.End.mul_apply, ih]
63       simp [freeAction, arrowWord, arrowOperator, pathMap]
64 
65 /-- A finite homogeneous path relation acts by the same finite linear combination of path blocks. -/
66 theorem TypedData.pathCombination_action (X : TypedData G) {v w : V}
67     (p : PathCombination (K := K) G.source G.target v w) :
68     X.freeAction (pathCombinationWord p) =
69       p.sum (fun q c => c •
70         ((LinearMap.single K X.space w).comp ((X.pathMap q).comp (LinearMap.proj v)))) := by
71   classical
72   simp only [pathCombinationWord, Finsupp.sum, map_sum, map_smul, X.path_action]
73 
74 /-- The grammar obtained from exactly the manuscript's homogeneous path relations. -/
75 def grammarFromPathRelations (s t : E → V)
76     (relations : ∀ v w, Set (PathCombination (K := K) s t v w)) : Grammar K V E where
77   source := s
78   target := t
79   equations x y := ∃ v w, ∃ p ∈ relations v w, x = pathCombinationWord p ∧ y = 0
80 
81 /-- The equivalence applies to arbitrary sets of typed, homogeneous finite path relations. -/
82 def typedPathRelationModuleEquivalence (s t : E → V)
83     (relations : ∀ v w, Set (PathCombination (K := K) s t v w)) :
84     TypedRealization (G := grammarFromPathRelations s t relations) ≌
85       ModuleCat.{u} (Algebra (grammarFromPathRelations s t relations)) :=
86   typedModuleEquivalence
87 
88 end Komorebi.PaperIRelease.GrammarAlgebra

Back to source controls