CategoryUniversal.lean

1 import PaperIRelease.CategoryExport
2 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
3 
4 /-!
5 Universal-construction part of the realization profile.
6 
7 A tensor product can be represented as an initial object of its category of
8 bilinear maps; a completion as an initial complete target of the specified
9 continuous/uniform map. To use either construction, the declared profile must
10 supply the appropriate structured categories, an induced functor on them,
11 its compatibility with the underlying realization functor, and actual
12 preservation evidence. No tensor or completion preservation is inferred from
13 additivity alone. The theorems below transport the universal object and its
14 uniquely induced morphisms from exactly those conditional inputs.
15 -/
16 
17 set_option autoImplicit false
18 
19 noncomputable section
20 
21 namespace Komorebi.PaperIRelease.CategoryExport
22 
23 open CategoryTheory CategoryTheory.Limits
24 
25 universe u v u' v' uS vS uT vT
26 variable {C : Type u} [Category.{v} C]
27 variable {D : Type u'} [Category.{v'} D]
28 
29 /-- Preserve an initial universal object under the declared preservation instance. -/
30 def transportInitial (F : C ⥤ D) [PreservesColimit (Functor.empty.{0} C) F]
31     {X : C} (hX : IsInitial X) : IsInitial (F.obj X) :=
32   hX.isInitialObj F X
33 
34 /-- The uniquely induced arrow is transported, rather than supplied as an assumption. -/
35 theorem transportInitial_map (F : C ⥤ D) [PreservesColimit (Functor.empty.{0} C) F]
36     {X : C} (hX : IsInitial X) (Y : C) :
37     F.map (hX.to Y) = (transportInitial F hX).to (F.obj Y) :=
38   (transportInitial F hX).hom_ext _ _
39 
40 /-- Preserve a terminal universal object under the declared preservation instance. -/
41 def transportTerminal (F : C ⥤ D) [PreservesLimit (Functor.empty.{0} C) F]
42     {X : C} (hX : IsTerminal X) : IsTerminal (F.obj X) :=
43   hX.isTerminalObj F X
44 
45 /-- The uniquely induced arrow into a terminal universal object is transported. -/
46 theorem transportTerminal_map (F : C ⥤ D) [PreservesLimit (Functor.empty.{0} C) F]
47     {X : C} (hX : IsTerminal X) (Y : C) :
48     F.map (hX.from Y) = (transportTerminal F hX).from (F.obj Y) :=
49   (transportTerminal F hX).hom_ext _ _
50 
51 variable {S : Type uS} [Category.{vS} S]
52 variable {T : Type uT} [Category.{vT} T]
53 
54 /-- A profile's induced structured functor and underlying compatibility isomorphism
55 carry the actual initial-object arrow diagram to the realized category. -/
56 theorem transportInitial_underlying
57     (F : C ⥤ D) (US : S ⥤ C) (UT : T ⥤ D) (G : S ⥤ T)
58     [PreservesColimit (Functor.empty.{0} S) G]
59     (comparison : G ⋙ UT ≅ US ⋙ F) {X : S} (hX : IsInitial X) (Y : S) :
60     UT.map ((transportInitial G hX).to (G.obj Y)) ≫ comparison.hom.app Y =
61       comparison.hom.app X ≫ F.map (US.map (hX.to Y)) := by
62   rw [← transportInitial_map G hX Y]
63   exact comparison.hom.naturality (hX.to Y)
64 
65 /-- The dual terminal-object comparison diagram, with the same explicit profile data. -/
66 theorem transportTerminal_underlying
67     (F : C ⥤ D) (US : S ⥤ C) (UT : T ⥤ D) (G : S ⥤ T)
68     [PreservesLimit (Functor.empty.{0} S) G]
69     (comparison : G ⋙ UT ≅ US ⋙ F) {X : S} (hX : IsTerminal X) (Y : S) :
70     UT.map ((transportTerminal G hX).from (G.obj Y)) ≫ comparison.hom.app X =
71       comparison.hom.app Y ≫ F.map (US.map (hX.from Y)) := by
72   rw [← transportTerminal_map G hX Y]
73   exact comparison.hom.naturality (hX.from Y)
74 
75 end Komorebi.PaperIRelease.CategoryExport

Back to source controls