CategoryExport.lean

1 import Mathlib.CategoryTheory.Linear.LinearFunctor
2 import Mathlib.CategoryTheory.Limits.Preserves.Basic
3 
4 /-!
5 Paper I: typed equational realization.  The source expression is syntax, not
6 an assumed preservation theorem.  Evaluation commutes with a linear additive
7 functor by structural induction.  Universal constructions are transported only
8 under the corresponding mathlib preservation instance.
9 -/
10 
11 set_option autoImplicit false
12 
13 namespace Komorebi.PaperIRelease.CategoryExport
14 
15 open CategoryTheory
16 
17 universe u v w u' v' r
18 
19 variable (R : Type r) (C : Type u) [Category.{v} C]
20 
21 /-- Well-typed finite expressions over a declared family of generators. -/
22 inductive Expression (G : C → C → Type w) : C → C → Type (max u v w r) where
23   | generator {X Y : C} : G X Y → Expression G X Y
24   | identity (X : C) : Expression G X X
25   | zero (X Y : C) : Expression G X Y
26   | add {X Y : C} : Expression G X Y → Expression G X Y → Expression G X Y
27   | neg {X Y : C} : Expression G X Y → Expression G X Y
28   | scalar {X Y : C} : R → Expression G X Y → Expression G X Y
29   | comp {X Y Z : C} : Expression G X Y → Expression G Y Z → Expression G X Z
30 
31 variable {R C} [Semiring R] [Preadditive C] [CategoryTheory.Linear R C]
32 variable {G : C → C → Type w}
33 
34 /-- Interpret source syntax using the specified primitive morphisms. -/
35 def evaluate (g : ∀ {X Y : C}, G X Y → (X ⟶ Y)) :
36     {X Y : C} → Expression R C G X Y → (X ⟶ Y)
37   | _, _, .generator a => g a
38   | _, _, .identity X => 𝟙 X
39   | _, _, .zero _ _ => 0
40   | _, _, .add a b => evaluate g a + evaluate g b
41   | _, _, .neg a => -evaluate g a
42   | _, _, .scalar c a => c • evaluate g a
43   | _, _, .comp a b => evaluate g a ≫ evaluate g b
44 
45 variable {D : Type u'} [Category.{v'} D] [Preadditive D]
46 variable [CategoryTheory.Linear R D]
47 
48 /-- Interpret the same source syntax after transporting its primitives. -/
49 def evaluateTransported (F : C ⥤ D)
50     (g : ∀ {X Y : C}, G X Y → (X ⟶ Y)) :
51     {X Y : C} → Expression R C G X Y → (F.obj X ⟶ F.obj Y)
52   | _, _, .generator a => F.map (g a)
53   | _, _, .identity X => 𝟙 (F.obj X)
54   | _, _, .zero _ _ => 0
55   | _, _, .add a b => evaluateTransported F g a + evaluateTransported F g b
56   | _, _, .neg a => -evaluateTransported F g a
57   | _, _, .scalar c a => c • evaluateTransported F g a
58   | _, _, .comp a b => evaluateTransported F g a ≫ evaluateTransported F g b
59 
60 /-- Every operation allowed by the declared syntax is transported. -/
61 theorem evaluate_transport (F : C ⥤ D) [F.Additive] [F.Linear R]
62     (g : ∀ {X Y : C}, G X Y → (X ⟶ Y))
63     {X Y : C} (e : Expression R C G X Y) :
64     F.map (evaluate g e) = evaluateTransported F g e := by
65   induction e with
66   | generator => rfl
67   | identity => simp [evaluate, evaluateTransported]
68   | zero => simp [evaluate, evaluateTransported]
69   | add a b ha hb => simp [evaluate, evaluateTransported, ha, hb]
70   | neg a ha => simp [evaluate, evaluateTransported, ha]
71   | scalar c a ha => simp [evaluate, evaluateTransported, ha]
72   | comp a b ha hb => simp [evaluate, evaluateTransported, ha, hb]
73 
74 /-- PSC-I-T-REALIZATION-EXPORT: a proved source equation gives its target equation. -/
75 theorem equation_transport (F : C ⥤ D) [F.Additive] [F.Linear R]
76     (g : ∀ {X Y : C}, G X Y → (X ⟶ Y))
77     {X Y : C} (a b : Expression R C G X Y)
78     (h : evaluate g a = evaluate g b) :
79     evaluateTransported F g a = evaluateTransported F g b := by
80   rw [← evaluate_transport F g a, ← evaluate_transport F g b, h]
81 
82 /-- Additive-only profiles obtain the same result using the canonical integer enrichment. -/
83 theorem additive_equation_transport
84     {C₀ : Type u} {D₀ : Type u'} [Category.{v} C₀] [Category.{v'} D₀]
85     [Preadditive C₀] [Preadditive D₀]
86     (F : C₀ ⥤ D₀) [F.Additive] {G₀ : C₀ → C₀ → Type w}
87     (g : ∀ {X Y : C₀}, G₀ X Y → (X ⟶ Y))
88     {X Y : C₀} (a b : Expression ℤ C₀ G₀ X Y)
89     (h : evaluate g a = evaluate g b) :
90     evaluateTransported F g a = evaluateTransported F g b :=
91   equation_transport F g a b h
92 
93 open CategoryTheory.Limits
94 
95 /-- Kernel, product and other limit diagrams pass under their declared preservation hypothesis. -/
96 noncomputable def transportLimit
97     {J : Type*} [Category J] (K : J ⥤ C) (F : C ⥤ D)
98     [PreservesLimit K F] (c : Cone K) (h : IsLimit c) :
99     IsLimit (F.mapCone c) := isLimitOfPreserves F h
100 
101 /-- Cokernel, quotient and other colimit diagrams use a separate preservation hypothesis. -/
102 noncomputable def transportColimit
103     {J : Type*} [Category J] (K : J ⥤ C) (F : C ⥤ D)
104     [PreservesColimit K F] (c : Cocone K) (h : IsColimit c) :
105     IsColimit (F.mapCocone c) := isColimitOfPreserves F h
106 
107 end Komorebi.PaperIRelease.CategoryExport

Back to source controls