Skip to content

Commit 0f1a598

Browse files
sinhpsinhp
committed
blueprint update
1 parent 4719333 commit 0f1a598

5 files changed

Lines changed: 270 additions & 8 deletions

File tree

‎blueprint/src/chapter/lccc.tex‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
1-
\begin{definition}[exponentiable morphism]\label{defn:exponentiable-morphism}
2-
\lean{CategoryTheory.ExponentiableMorphism} \leanok
1+
\begin{definition}[exponentiable morphism]
2+
\label{defn:exponentiable-morphism}
3+
\lean{CategoryTheory.ExponentiableMorphism}
4+
\leanok
35
Suppose $\catC$ is a category with pullbacks.
46
A morphism $f \colon A \to B$ in $\catC$ is \textbf{exponentiable} if the pullback functor
57
$f^* \colon \catC / B \to \catC / A$ has a right adjoint $f_*$.
@@ -17,8 +19,10 @@
1719
\end{tikzcd}\end{center}
1820
\end{definition}
1921

20-
\begin{definition}[pushforward functor]\label{rmk:pushforward}
21-
\lean{CategoryTheory.ExponentiableMorphism.pushforward} \leanok
22+
\begin{definition}[pushforward functor]
23+
\label{rmk:pushforward}
24+
\lean{CategoryTheory.ExponentiableMorphism.pushforward}
25+
\leanok
2226
Let $f \colon A \to B$ be an exponentiable morphism in a category $\catC$ with pullbacks.
2327
We call the right adjoint $f_*$ of the pullback functor $f^*$ the \textbf{pushforward} functor
2428
along $f$.

‎blueprint/src/chapter/mvpoly.tex‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,17 @@
77
$$\polyspan IEBJipo.$$
88
The object $I$ is the object of input variables and the object $O$ is the object of output
99
variables. The morphism $p$ encodes the arities/exponents.
10-
\end{definition}
10+
\end{definition}
11+
12+
13+
1114

1215

1316
\begin{definition}[extension of polynomial functors]
1417
\label{defn:extension}
1518
\lean{CategoryTheory.MvPoly.functor} \leanok
1619
The \textbf{extension} of a polynomial $\polyspan IBAJipo$ is the functor
1720
$\upP = o_! \, f_* \, i^* \colon \catC / I \to \catC/ O$. Internally, we can define $\upP$ by
18-
$$\upP \seqbn{X_i}{i \in I} = \seqbn{\sum_{a \in A_j} \prod_{b \in B_a} X_{s(b)}}{j \in J}$$
21+
$$\upP \seqbn{X_i}{i \in I} = \seqbn{\sum_{b \in B_j} \prod_{e \in E_b} X_{s(b)}}{j \in J}$$
1922
A \textbf{polynomial functor} is a functor that is naturally isomorphic to the extension of a polynomial.
2023
\end{definition}

‎blueprint/src/print.pdf‎

37.3 KB
Binary file not shown.

‎blueprint/src/web.pdf‎

17.2 KB
Binary file not shown.

‎blueprint/web/dep_graph_document.html‎

Lines changed: 257 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,262 @@ <h1 id="doc_title">Dependencies</h1>
5858
</dl>
5959
</div>
6060
<div id="graph"></div>
61-
<div id="statements"></div>
61+
<div id="statements">
62+
63+
64+
<div class="dep-modal-container" id="defn:exponentiable-morphism_modal">
65+
<div class="dep-modal-content">
66+
<button class="dep-closebtn">
67+
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
68+
</button>
69+
70+
<div class="thm" id="defn:exponentiable-morphism" style="display: none">
71+
<div class="thm_thmheading">
72+
<span class="definition_thmcaption">
73+
Definition
74+
</span>
75+
<span class="definition_thmlabel">1.0.1</span><span class="definition_thmtitle">exponentiable morphism</span></div>
76+
<div class="thm_thmcontent"><p> Suppose \(\mathbb {C}\) is a category with pullbacks. A morphism \(f \colon A \to B\) in \(\mathbb {C}\) is <b class="bfseries">exponentiable</b> if the pullback functor \(f^* \colon \mathbb {C}/ B \to \mathbb {C}/ A\) has a right adjoint \(f_*\). Since \(f^*\) always has a left adjoint \(f_!\), given by post-composition with \(f\), an exponentiable morphism \(f\) gives rise to an adjoint triple </p>
77+
<div class="centered"><div class="tikzcd" id="a0000000005">
78+
<img src="images/img-0001.svg" class="tikzcd-vector" alt="\begin{tikzcd}
79+
&amp; {\catC / B} \\
80+
\\
81+
{} &amp; {\catC / A}
82+
\arrow[&#34;&#34;{name=0, anchor=center, inner sep=0}, &#34;{f_*}&#34;, bend left, shift left=5, from=1-2, to=3-2]
83+
\arrow[&#34;&#34;{name=1, anchor=center, inner sep=0}, &#34;{f_!}&#34;&#39;, bend right, shift right=5, from=1-2, to=3-2]
84+
\arrow[&#34;&#34;{name=2, anchor=center, inner sep=0}, &#34;{f^*}&#34;{description}, from=3-2, to=1-2]
85+
\arrow[&#34;\dashv&#34;{anchor=center}, draw=none, from=1, to=2]
86+
\arrow[&#34;\dashv&#34;{anchor=center}, draw=none, from=2, to=0]
87+
\end{tikzcd}" />
88+
</div></div>
89+
</div>
90+
91+
<a class="latex_link" href="sect0001.html#defn:exponentiable-morphism">LaTeX</a>
92+
93+
94+
<a class="lean_link lean_decl" href="https://sinhp.github.io/Poly/docs/find/#doc/CategoryTheory.ExponentiableMorphism">Lean</a>
95+
96+
97+
98+
99+
</div>
100+
101+
</div>
102+
</div>
103+
104+
105+
106+
<div class="dep-modal-container" id="defn:extension_modal">
107+
<div class="dep-modal-content">
108+
<button class="dep-closebtn">
109+
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
110+
</button>
111+
112+
<div class="thm" id="defn:extension" style="display: none">
113+
<div class="thm_thmheading">
114+
<span class="definition_thmcaption">
115+
Definition
116+
</span>
117+
<span class="definition_thmlabel">3.0.2</span><span class="definition_thmtitle">extension of polynomial functors</span></div>
118+
<div class="thm_thmcontent"><p> The <b class="bfseries">extension</b> of a polynomial \(I \xleftarrow {i} B \xrightarrow {p} A \xrightarrow {o} J\) is the functor \(\mathrm{P}= o_! \, f_* \, i^* \colon \mathbb {C}/ I \to \mathbb {C}/ O\). Internally, we can define \(\mathrm{P}\) by </p>
119+
<div class="displaymath" id="a0000000010">
120+
\[ \mathrm{P}\left(\left. X_i \ \middle \rvert \ i \in I \right.\right) = \left(\left. \sum _{b \in B_j} \prod _{e \in E_b} X_{s(b)} \ \middle \rvert \ j \in J \right.\right) \]
121+
</div>
122+
<p> A <b class="bfseries">polynomial functor</b> is a functor that is naturally isomorphic to the extension of a polynomial. </p>
123+
</div>
124+
125+
<a class="latex_link" href="sect0003.html#defn:extension">LaTeX</a>
126+
127+
128+
<a class="lean_link lean_decl" href="https://sinhp.github.io/Poly/docs/find/#doc/CategoryTheory.MvPoly.functor">Lean</a>
129+
130+
131+
132+
133+
</div>
134+
135+
</div>
136+
</div>
137+
138+
139+
140+
<div class="dep-modal-container" id="defn:LCCC_modal">
141+
<div class="dep-modal-content">
142+
<button class="dep-closebtn">
143+
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
144+
</button>
145+
146+
<div class="thm" id="defn:LCCC" style="display: none">
147+
<div class="thm_thmheading">
148+
<span class="definition_thmcaption">
149+
Definition
150+
</span>
151+
<span class="definition_thmlabel">1.0.4</span><span class="definition_thmtitle">Locally cartesian closed categories</span></div>
152+
<div class="thm_thmcontent"><p> A category with pullbacks is <b class="bfseries">locally cartesian closed</b> if is a category \(\mathbb {C}\) with a terminal object \(1\) and with all slices \(\mathbb {C}/ A\) cartesian closed. </p>
153+
</div>
154+
155+
<a class="latex_link" href="sect0001.html#defn:LCCC">LaTeX</a>
156+
157+
158+
<a class="lean_link lean_decl" href="https://sinhp.github.io/Poly/docs/find/#doc/CategoryTheory.LocallyCartesianClosed">Lean</a>
159+
160+
161+
162+
163+
</div>
164+
165+
</div>
166+
</div>
167+
168+
169+
170+
<div class="dep-modal-container" id="defn:Polynomial_modal">
171+
<div class="dep-modal-content">
172+
<button class="dep-closebtn">
173+
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
174+
</button>
175+
176+
<div class="thm" id="defn:Polynomial" style="display: none">
177+
<div class="thm_thmheading">
178+
<span class="definition_thmcaption">
179+
Definition
180+
</span>
181+
<span class="definition_thmlabel">3.0.1</span><span class="definition_thmtitle">multivariable polynomial functor</span></div>
182+
<div class="thm_thmcontent"><p> A <b class="bfseries">polynomial</b> in \(\mathbb {C}\) from \(I\) to \(O\) is a triple \((i,p,o)\) where \(i\), \(p\) and \(o\) are morphisms in \(\mathbb {C}\) forming the diagram </p>
183+
<div class="displaymath" id="a0000000009">
184+
\[ I \xleftarrow {i} E \xrightarrow {p} B \xrightarrow {o} J. \]
185+
</div>
186+
<p> The object \(I\) is the object of input variables and the object \(O\) is the object of output variables. The morphism \(p\) encodes the arities/exponents. </p>
187+
</div>
188+
189+
<a class="latex_link" href="sect0003.html#defn:Polynomial">LaTeX</a>
190+
191+
192+
<a class="lean_link lean_decl" href="https://sinhp.github.io/Poly/docs/find/#doc/CategoryTheory.MvPoly">Lean</a>
193+
194+
195+
196+
197+
</div>
198+
199+
</div>
200+
</div>
201+
202+
203+
204+
<div class="dep-modal-container" id="defn:UvPoly_modal">
205+
<div class="dep-modal-content">
206+
<button class="dep-closebtn">
207+
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
208+
</button>
209+
210+
<div class="thm" id="defn:UvPoly" style="display: none">
211+
<div class="thm_thmheading">
212+
<span class="definition_thmcaption">
213+
Definition
214+
</span>
215+
<span class="definition_thmlabel">2.0.1</span><span class="definition_thmtitle">Polynomial endofunctor</span></div>
216+
<div class="thm_thmcontent"><p> Let \(\mathbb {C}\) be a locally Cartesian closed category (in our case, presheaves on the category of contexts). This means for each morphism \(t : B \to A\) we have an adjoint triple </p>
217+
<div class="centered"><div class="tikzcd" id="a0000000006">
218+
<img src="images/img-0002.svg" class="tikzcd-vector" alt="\begin{tikzcd}
219+
&amp; {\catC / B} \\
220+
\\
221+
{} &amp; {\catC / A}
222+
\arrow[&#34;&#34;{name=0, anchor=center, inner sep=0}, &#34;{t_*}&#34;, bend left, shift left=5, from=1-2, to=3-2]
223+
\arrow[&#34;&#34;{name=1, anchor=center, inner sep=0}, &#34;{t_!}&#34;&#39;, bend right, shift right=5, from=1-2, to=3-2]
224+
\arrow[&#34;&#34;{name=2, anchor=center, inner sep=0}, &#34;{t^*}&#34;{description}, from=3-2, to=1-2]
225+
\arrow[&#34;\dashv&#34;{anchor=center}, draw=none, from=1, to=2]
226+
\arrow[&#34;\dashv&#34;{anchor=center}, draw=none, from=2, to=0]
227+
\end{tikzcd}" />
228+
</div></div>
229+
<p> where \(t^{*}\) is pullback, and \(t_{!}\) is composition with \(t\). </p>
230+
<p>Let \(t : B \to A\) be a morphism in \(\mathbb {C}\). Then define \(P_{t} : \mathbb {C}\to \mathbb {C}\) be the composition </p>
231+
<div class="displaymath" id="a0000000007">
232+
\[ P_{t} := A_{!} \circ t_{*} \circ B^{*} \quad \quad \quad \]
233+
</div>
234+
<div class="centered"><div class="tikzcd" id="a0000000008">
235+
<img src="images/img-0003.svg" class="tikzcd-vector" alt="\begin{tikzcd}
236+
\catC &amp; {\catC / B} &amp; {\catC / A} &amp; \catC
237+
\arrow[&#34;{B^*}&#34;, from=1-1, to=1-2]
238+
\arrow[&#34;{t_*}&#34;, from=1-2, to=1-3]
239+
\arrow[&#34;{A_!}&#34;, from=1-3, to=1-4]
240+
\end{tikzcd}" />
241+
</div></div>
242+
</div>
243+
244+
<a class="latex_link" href="sect0002.html#defn:UvPoly">LaTeX</a>
245+
246+
247+
<a class="lean_link lean_decl" href="https://sinhp.github.io/Poly/docs/find/#doc/CategoryTheory.UvPoly">Lean</a>
248+
249+
250+
251+
252+
</div>
253+
254+
</div>
255+
</div>
256+
257+
258+
259+
<div class="dep-modal-container" id="rmk:pushforward_modal">
260+
<div class="dep-modal-content">
261+
<button class="dep-closebtn">
262+
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
263+
</button>
264+
265+
<div class="thm" id="rmk:pushforward" style="display: none">
266+
<div class="thm_thmheading">
267+
<span class="definition_thmcaption">
268+
Definition
269+
</span>
270+
<span class="definition_thmlabel">1.0.2</span><span class="definition_thmtitle">pushforward functor</span></div>
271+
<div class="thm_thmcontent"><p> Let \(f \colon A \to B\) be an exponentiable morphism in a category \(\mathbb {C}\) with pullbacks. We call the right adjoint \(f_*\) of the pullback functor \(f^*\) the <b class="bfseries">pushforward</b> functor along \(f\). </p>
272+
</div>
273+
274+
<a class="latex_link" href="sect0001.html#rmk:pushforward">LaTeX</a>
275+
276+
277+
<a class="lean_link lean_decl" href="https://sinhp.github.io/Poly/docs/find/#doc/CategoryTheory.ExponentiableMorphism.pushforward">Lean</a>
278+
279+
280+
281+
282+
</div>
283+
284+
</div>
285+
</div>
286+
287+
288+
289+
<div class="dep-modal-container" id="thm:exponentiable-mor-exponentiable-obj_modal">
290+
<div class="dep-modal-content">
291+
<button class="dep-closebtn">
292+
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
293+
</button>
294+
295+
<div class="thm" id="thm:exponentiable-mor-exponentiable-obj" style="display: none">
296+
<div class="thm_thmheading">
297+
<span class="theorem_thmcaption">
298+
Theorem
299+
</span>
300+
<span class="theorem_thmlabel">1.0.3</span><span class="theorem_thmtitle">exponentiable morphisms are exponentiable objects of the slices</span></div>
301+
<div class="thm_thmcontent"><p> A morphism \(f \colon A \to B\) in a category \(\mathbb {C}\) with pullbacks is exponentiable if and only if it is an exponentiable object, regarded as an object of the slice \(\mathbb {C}/ B\). </p>
302+
</div>
303+
304+
<a class="latex_link" href="sect0001.html#thm:exponentiable-mor-exponentiable-obj">LaTeX</a>
305+
306+
307+
<a class="lean_link lean_decl" href="https://sinhp.github.io/Poly/docs/find/#doc/CategoryTheory.ExponentiableMorphism.OverMkHom">Lean</a>
308+
309+
310+
311+
312+
</div>
313+
314+
</div>
315+
</div>
316+
</div>
62317
</div> <!-- content -->
63318
</div> <!-- wrapper -->
64319
<script src="js/jquery.min.js" type="text/javascript"></script>
@@ -77,7 +332,7 @@ <h1 id="doc_title">Dependencies</h1>
77332
.width(width)
78333
.height(height)
79334
.fit(true)
80-
.renderDot(`strict digraph "" { graph [bgcolor=transparent]; node [penwidth=1.8]; edge [arrowhead=vee];}`)
335+
.renderDot(`strict digraph "" { graph [bgcolor=transparent]; node [label="\N", penwidth=1.8 ]; edge [arrowhead=vee]; "defn:exponentiable-morphism" [color=green, fillcolor="#B0ECA3", label="exponentiable-morphism", shape=box, style=filled]; "thm:exponentiable-mor-exponentiable-obj" [color=green, label="exponentiable-mor-exponentiable-obj", shape=ellipse]; "defn:exponentiable-morphism" -> "thm:exponentiable-mor-exponentiable-obj" [style=dashed]; "defn:UvPoly" [color=green, fillcolor="#B0ECA3", label=UvPoly, shape=box, style=filled]; "defn:Polynomial" [color=green, fillcolor="#B0ECA3", label=Polynomial, shape=box, style=filled]; "defn:LCCC" [color=green, fillcolor="#B0ECA3", label=LCCC, shape=box, style=filled]; "rmk:pushforward" [color=green, fillcolor="#B0ECA3", label=pushforward, shape=box, style=filled]; "defn:extension" [color=green, fillcolor="#B0ECA3", label=extension, shape=box, style=filled];}`)
81336
.on("end", interactive);
82337

83338
latexLabelEscaper = function(label) {

0 commit comments

Comments
 (0)