avewright/proofwiki-math huggingface dataset:
Theorem: Convex Real Function has Minimum at Point iff Zero is Subgradient at Point

Let $\innerprod X {X'}$ be a dual system over $\R$.
Let $C \subseteq X$ be a convex set.
Let $f : C \to \R$ be a convex function.
Let $x \in C$.
Then $f$ has a minimum at $x$ {{iff}} ${\mathbf 0}_{X'}$ is a subgradient at $x$ with respect to $\innerprod X {X'}$.

Proof:
We have that $f$ is a minimum at $x$ {{iff}}:
:$\map f y \ge \map f x$ for all $y \in C$.
That is:
:$\map f y - \map f x \ge 0$
We have:
:$\innerprod {y - x} { {\mathbf 0}_{X'} } = 0$
Hence:
:$\map f y - \map f x \ge \innerprod {y - x} { {\mathbf 0}_{X'} }$ for all $y \in C$.
Hence ${\mathbf 0}_{X'}$ is a subgradient at $x$.
{{qed}}
Theorem: Bipolar Set is Convex

vLet $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $A \subseteq E$ be non-empty. 
Let $\paren {A^\circ}_\circ$ be the bipolar set of $A$.
Then $\paren {A^\circ}_\circ$ is convex.

Proof:
Let $A^\circ$ be the absolute polar of $A$.
From Absolute Polar is Non-Empty, $A^\circ$ is non-empty.
From Absolute Prepolar is Convex Set, $\paren {A^\circ}_\circ$ is convex.
{{qed}}
Category:Bipolar Sets
5soc331wuibt5vnuqve15nrs970yy28
Theorem: Bipolar Set is Balanced

vLet $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $A \subseteq E$ be non-empty. 
Let $\paren {A^\circ}_\circ$ be the bipolar set of $A$.
Then $\paren {A^\circ}_\circ$ is balanced.

Proof:
Let $A^\circ$ be the absolute polar of $A$.
From Absolute Polar is Non-Empty, $A^\circ$ is non-empty.
From Absolute Prepolar is Balanced, $\paren {A^\circ}_\circ$ is balanced.
{{qed}}
Category:Bipolar Sets
Category:Balanced Sets
3n36esx3beyn7y6st7ce58giq3ll55o
Theorem: One-Sided Polar of Dilation

Let $\innerprod E F$ be a dual system over $\R$.
Let $A \subseteq E$ be non-empty.
Let $\lambda > 0$. 
Let $A^\odot$ and $\paren {\lambda A}^\odot$ be the one-sided polar of $A$ and $\lambda A$ respectively.
Then:
:$\paren {\lambda A}^\odot = \dfrac 1 \lambda A^\odot$

Proof:
Let $f \in \dfrac 1 \lambda A^\odot$. 
This is the case {{iff}} $\lambda f \in A^\odot$.
This is equivalent to $\innerprod x {\lambda f} \le 1$ for each $x \in A$.
Since $\innerprod \cdot \cdot$ is bilinear, we have $\innerprod x {\lambda f} = \innerprod {\lambda x} f$.
Hence $\innerprod x {\lambda f} \le 1$ for each $x \in A$ is equivalent to $\innerprod {\lambda x} f \le 1$ for each $x \in A$.
This is equivalent to $\innerprod z f \le 1$ for each $z \in \lambda A$.
This is equivalent to $f \in \paren {\lambda A}^\odot$.
Hence:
:$\paren {\lambda A}^\odot = \dfrac 1 \lambda A^\odot$ 
{{qed}}
Theorem: Intersection of One-Sided Polars is One-Sided Polar of Union

Let $\innerprod E F$ be a dual system over $\R$.
Let $\FF$ be a set of non-empty subsets of $E$. 
Then:
:$\ds \bigcap_{A \in \FF} A^\odot = \paren {\bigcup_{A \in \FF} A}^\odot$
where $\odot$ denotes one-sided polar.

Proof:
We have:
:$\ds f \in \paren {\bigcup_{A \in \FF} A}^\odot$
{{iff}}:
:$\innerprod x f \le 1$ for each $\ds x \in \bigcup_{A \in \FF} A$
This is equivalent to:
:$\innerprod x f \le 1$ for each $\ds x \in A$
for each $A \in \FF$.
This is equivalent to $f \in A^\odot$ for each $A \in \FF$.
This is equivalent to $\ds f \in \bigcap_{A \in \FF} A^\odot$.
Hence we have:
:$\ds \bigcap_{A \in \FF} A^\odot = \paren {\bigcup_{A \in \FF} A}^\odot$
{{qed}}
Theorem: One-Sided Polar is Non-Empty

Let $\innerprod E F$ be a dual system over $\R$.
Let $A \subseteq E$ be non-empty.
Let $A^\circ$ be the one-sided polar of $A$ in $\innerprod E F$.
Then $A^\circ \ne \O$.

Proof:
Note that we have:
:$\innerprod x { {\mathbf 0}_F} = 0$ for all $x \in E$.
In particular:
:$\innerprod x { {\mathbf 0}_F} \le 1$ for all $x \in A$.
Hence we have ${\mathbf 0}_F \in A^\circ$.
Hence $A^\circ \ne \O$.
{{qed}}
Category:One-Sided Polars
banrxb2c7tm0lg4a7kgrrg0vysbpysc
Theorem: One-Sided Polar is Convex

Let $\innerprod E F$ be a dual system over $\R$.
Let $A \subseteq E$ be non-empty.
Let $A^\odot$ be the one-sided polar of $A$ in $\innerprod E F$.
Then $A^\odot$ is convex.

Proof:
Let $f, g \in A^\odot$ and $t \in \closedint 0 1$.
Then for each $x \in A$, we have:
{{begin-eqn}}
{{eqn	| l = \innerprod x {t f + \paren {1 - t} g}
		| r = t \innerprod x f + \paren {1 - t} \innerprod x g
		| c = $\innerprod \cdot \cdot$ is bilinear
}}
{{eqn	| o = \le
		| r = t + \paren {1 - t}
}}
{{eqn	| r = 1
}}
{{end-eqn}}
Hence:
:$t f + \paren {1 - t} g \in A^\odot$
Hence $A^\odot$ is convex.
{{qed}}
Category:One-Sided Polars
epak65a51zi33i32uwcm16285no1dgx
Theorem: One-Sided Prepolar is Convex

Let $\innerprod E F$ be a dual system over $\R$.
Let $B \subseteq F$ be non-empty.
Let $B_\odot$ be the one-sided prepolar of $B$ in $\innerprod E F$.
Then $B_\odot$ is convex.

Proof:
Let $x, y \in B_\odot$ and $t \in \closedint 0 1$.
Then for each $f \in B$, we have:
{{begin-eqn}}
{{eqn	| l = \innerprod {t x + \paren {1 - t} y} f
		| r = t \innerprod x f + \paren {1 - t} \innerprod y f
		| c = $\innerprod \cdot \cdot$ is bilinear
}}
{{eqn	| o = \le
		| r = t + \paren {1 - t}
}}
{{eqn	| r = 1
}}
{{end-eqn}}
{{qed}}
Category:One-Sided Prepolars
iaw0e24bendsr444orxbq4y8vikmbrv
Theorem: One-Sided Prepolar is Closed in Weak Topology

Let $\innerprod E F$ be a dual system over $\R$.
Let $\map \sigma {E, F}$ be the weak topology on $E$ induced by $\innerprod E F$.
Let $B \subseteq F$ be non-empty.
Let $B_\odot$ be the one-sided prepolar of $B$ in $\innerprod E F$.
Then $B_\odot$ is $\map \sigma {E, F}$-closed.

Proof:
We use Characterization of Closedness in terms of Nets.
We show that every convergent net valued in $B_\odot$ has its limit in $B_\odot$.
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a convergent net valued in $B_\odot$ with limit $x \in E$.
Then for each $f \in B$ and $\lambda \in \Lambda$ we have:
:$\innerprod {x_\lambda} f \le 1$
From Characterization of Convergence of Net in Weak Topology Induced by Dual System, we have:
:$\innerprod {x_\lambda} f \to \innerprod x f$
Hence:
:$\innerprod x f \le 1$ for each $f \in B$.
We conclude that $x \in B_\odot$. 
Hence by Characterization of Closedness in terms of Nets, $B_\odot$ is $\map \sigma {E, F}$-closed.
{{qed}}
Category:One-Sided Prepolars
2edk5o494342nf7uu6y3qxm7wpnzg7s
Theorem: Bipolar Theorem/One-Sided Polar

Let $\GF \in \set {\R, \C}$.
Let $\innerprod X {X'}$ be a dual system over $\GF$.
Let $A \subseteq X$ be a non-empty set. 
Let $\paren {A^\odot}_\odot$ be the one-sided bipolar of $A$.
Let $\map \sigma {X, X'}$ be the weak topology on $X$ induced by $\innerprod X {X'}$. 
Let $\operatorname {conv}$ be the convex hull.
Let $\cl_\sigma$ denote closure taken in $\map \sigma {X, X'}$.
Then we have:
:$\paren {A^\odot}_\odot = \map {\cl_\sigma} {\map {\operatorname {conv} } {A \cup \set { {\mathbf 0}_X} } }$

Proof:
From One-Sided Bipolar is Convex, $\paren {A^\odot}_\odot$ is convex.
From One-Sided Bipolar is Closed in Weak Topology, $\paren {A^\odot}_\odot$ is $\map \sigma {E, F}$-closed.
Let:
:$C = \map {\cl_\sigma} {\map {\operatorname {conv} } {A \cup \set { {\mathbf 0}_X} } }$
From One-Sided Bipolar Set contains Original Set and Origin, we have:
:$A \cup \set { {\mathbf 0}_X} \subseteq \paren {A^\odot}_\odot$
Hence from Closure of Convex Hull is Smallest Closed Convex Set containing Set, we have:
:$C \subseteq \paren {A^\odot}_\odot$
{{AimForCont}} that $\paren {A^\odot}_\odot \not \subseteq C$. 
Let $x \in \paren {A^\odot}_\odot \setminus C$. 
Applying Hahn-Banach Separation Theorem: Hausdorff Locally Convex Space: Real Case: Compact Convex Set and Closed Convex Set to $\set x$ and $B$, there exists $\alpha \in \R$ and a $\map \sigma {E, F}$-continuous linear functional $\phi$ such that:
:$\ds \map \phi x < \alpha < \inf_{y \mathop \in C} \map \phi y$
Replacing $\phi$ with $-\phi$, we obtain:
:$\ds \sup_{y \mathop \in C} \map \phi y < -\alpha < \map \phi x$
From Continuity of Linear Functionals in Weak Topology Induced by Pair of Vector Spaces with Bilinear Mapping, there exists $x' \in X'$ such that:
:$\map \phi u = \innerprod u {x'}$ for each $u \in X$.
Hence we have:
:$\ds \sup_{y \mathop \in C} \innerprod y {x'} < -\alpha < \innerprod x {x'}$
Since ${\mathbf 0}_X \in C$, we have:
:$\ds \sup_{y \mathop \in C} \innerprod y {x'} \ge \innerprod { {\mathbf 0}_X} {x'} = 0$
Hence $\beta = -\alpha > 0$.
To recap, we have:
:$\innerprod y {x'} < \beta$ for each $y \in C$
and:
:$\innerprod x {x'} > \beta$
Setting:
:$\ds y = \frac {y'} \beta$
we have that:
:$\innerprod y {y'} < 1$ for each $y \in C$
and:
:$\innerprod x {y'} > 1$
by bilinearity. 
Since $\innerprod y {y'} < 1$ for each $y \in C$ and $A \subseteq C$, we have $y' \in A^\odot$. 
However, since $\innerprod x {y'} > 1$, we cannot have $\innerprod x {y'} \le 1$, and hence $x \not \in \paren {A^\odot}_\odot$. 
This is a contradiction.
Hence $\paren {A^\odot}_\odot \subseteq C$.
Hence $C = \paren {A^\odot}_\odot$.
{{qed}}
Theorem: One-Sided Bipolar is Convex

Let $\innerprod E F$ be a dual system over $\R$.
Let $A \subseteq E$ be non-empty.
Let $\paren {A^\odot}_\odot$ be the one-sided bipolar of $A$ in $\innerprod E F$.
Then $\paren {A^\odot}_\odot$ is convex.

Proof:
Let $A^\odot$ be the one-sided absolute polar of $A$.
From One-Sided Polar is Non-Empty, $A^\odot \ne \O$.
Hence from One-Sided Prepolar is Convex, $\paren {A^\odot}_\odot$ is convex.
{{qed}}
Category:One-Sided Bipolars
Category:Convex Sets (Vector Spaces)
rbxus0o8rcetxnt96jfp3z7zw2pfiui
Theorem: Functor Under Object Comma Category is Isomorphic to Comma Category/Lemma 1

:$I$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
Let $\tuple{D,f}$ be an object in $\paren{C \downarrow F}$.
By definition of functor under object comma category:
:$f$ is a morphism $f: C \to FD$ of $\mathbf C$
Hence:
:$f$ is a morphism $f: G* \to FD$ of $\mathbf C$
By definition of comma category:
:$\tuple{*, D, f}$ is an object in $\paren{G \downarrow F}$
It follows that $I$ is a well-defined object functor.
{{qed|lemma}}
Theorem: One-Sided Bipolar Set contains Original Set and Origin

Let $\innerprod X {X'}$ be a dual system over $\R$.
Let $A \subseteq X$ be a non-empty set.
Let $\paren {A^\odot}_\odot$ be the one-sided bipolar of $A$.
Then: 
:$A \cup \set { {\mathbf 0}_X} \subseteq \paren {A^\odot}_\odot$

Proof:
We have $x \in \paren {A^\odot}_\odot$ {{iff}}:
:$\innerprod x f \le 1$ for each $f \in A^\odot$.
We have that $f \in A^\odot$ {{iff}}:
:$\innerprod x f \le 1$ for each $x \in A$. 
Hence for $x \in A$, we have:
:$\innerprod x f \le 1$ for each $f \in A^\odot$.
Hence $x \in \paren {A^\odot}_\odot$.
Hence $A \subseteq \paren {A^\odot}_\odot$.
Further, it is shown in One-Sided Bipolar Set is Non-Empty that ${\mathbf 0}_X \in \paren {A^\odot}_\odot$. 
Hence:
:$A \cup \set { {\mathbf 0}_X} \subseteq \paren {A^\odot}_\odot$
{{qed}}
Category:One-Sided Bipolars
h6uslo6uea07ylstlup5c4trdf42nq0
Theorem: Closure of Convex Hull is Smallest Closed Convex Set containing Set

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Let $\cl$ be the closure taken in $\struct {X, \tau}$. 
Let $\operatorname {conv}$ denote convex hull.
Let $A \subseteq X$ be non-empty. 
Then $\map \cl {\map {\operatorname {conv} } A}$ is $\subseteq$-smallest closed convex set containing $A$.

Proof:
From Closed Convex Hull in Topological Vector Space is Closed and Convex, $\map \cl {\map {\operatorname {conv} } A}$ is a closed convex set containing $A$.
Let $C$ be a closed convex set containing $A$.
From Convex Hull is Smallest Convex Set containing Set, we have:
:$\map {\operatorname {conv} } A \subseteq C$
From Topological Closure of Subset is Subset of Topological Closure:
:$\map \cl {\map {\operatorname {conv} } A} \subseteq \map \cl C$
From Set is Closed iff Equals Topological Closure, we have:
:$\map \cl C = C$
That is:
:$\map \cl {\map {\operatorname {conv} } A} \subseteq C$
Hence:
:$\map \cl {\map {\operatorname {conv} } A}$ is $\subseteq$-smallest closed convex set containing $A$.
{{qed}}
Category:Closed Convex Hulls
8he7q430dw26qp9il6bsl52jieigcj6
Theorem: Functor Under Object Comma Category is Isomorphic to Comma Category/Lemma 2

:$J$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
By definition of category $\mathbf 1$:
:the only object in $\mathbf 1$ is $*$
By definition of comma category:
:every object in $\paren{G \downarrow F}$ is of the form $\tuple{*, D, f}$ where:
::$*$ is in $\mathbf 1$
::$D$ is an object of $\mathbf D$
::$f$ is a morphism $f:G* \to  FD$ of $\mathbf C$
By definition of $G$:
:given an object $\tuple{*, D, f}$ in $\paren{G \downarrow F}$:
::$f$ is a morphism $f:C \to  FD$ of $\mathbf C$
By definition of functor under object comma category:
:$\tuple{D, f}$ is an object in $\paren{C \downarrow F}$
It follows that $J$ is a well-defined object functor.
{{qed|lemma}}
Theorem: Functor Under Object Comma Category is Isomorphic to Comma Category/Lemma 3

:$J \circ I = \operatorname{id}_{\paren{C \downarrow F} }$
where:
:$\operatorname{id}_{\paren{C \downarrow F} }$ denotes the identity functor on $\paren{C \downarrow F}$

Proof:
For each object $\tuple{D,f}$ in $\paren{C \downarrow F}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} \tuple{D, f}
      | r = \map J {I \tuple{D, f} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{*, D, f}
      | c = Definition of $I$
}}
{{eqn | r = \tuple{D, f}
      | c = Definition of $J$
}}
{{eqn | r = \operatorname{id}_{\paren{C \downarrow F} } \tuple{D, f}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $h: \tuple{D,f} \to \tuple{D',f'}$ in $\paren{C \downarrow F}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} h
      | r = \map J {I h }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{\operatorname{id}_*, h}
      | c = Definition of $I$
}}
{{eqn | r = h
      | c = Definition of $J$
}}
{{eqn | r = \operatorname{id}_{\paren{C \downarrow F} } h
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$J \circ I = \operatorname{id}_{\paren{C \downarrow F} }$
{{qed}}
Category:Functor Under Object Comma Category is Isomorphic to Comma Category
ii3t5xgpcpczn4xe5y86mupeqkzmwuc
Theorem: Functor Under Object Comma Category is Isomorphic to Comma Category/Lemma 4

:$I \circ J = \operatorname{id}_{\paren{G \downarrow F} }$
where:
:$\operatorname{id}_{\paren{G \downarrow F} }$ denotes the identity functor on $\paren{G \downarrow F}$

Proof:
For each object $\tuple{*, D,f}$ in $\paren{G \downarrow F}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{*, D, f}
      | r = \map I {J \tuple{*, D, f} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = I \tuple{D, f}
      | c = Definition of $J$
}}
{{eqn | r = \tuple{*, D, f}
      | c = Definition of $I$
}}
{{eqn | r = \operatorname{id}_{\paren{G \downarrow F} } \tuple{*, D, f}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $\tuple{\operatorname{id}_*, h}: \tuple{*, D,f} \to \tuple{*, D',f'}$ in $\paren{G \downarrow F}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{\operatorname{id}_*, h}
      | r = \map I {J \tuple{\operatorname{id}_*, h} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = I h
      | c = Definition of $J$
}}
{{eqn | r = \tuple{\operatorname{id}_*, h}
      | c = Definition of $I$
}}
{{eqn | r = \operatorname{id}_{\paren{G \downarrow F} } \tuple{\operatorname{id}_*, h}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$I \circ J = \operatorname{id}_{\paren{G \downarrow F} }$
{{qed}}
Category:Functor Under Object Comma Category is Isomorphic to Comma Category
3ih6zch04jqgdtlrytm2664rdcgut5t
Theorem: Functor Over Object Comma Category is Isomorphic to Comma Category/Lemma 1

:$I$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
Let $\tuple{E,g}$ be an object in $\paren{G \downarrow C}$.
By definition of functor over object comma category:
:$g$ is a morphism $g: GE \to C$ of $\mathbf C$
Hence:
:$g$ is a morphism $g: GE \to F*$ of $\mathbf C$
By definition of comma category:
:$\tuple{E, *, g}$ is an object in $\paren{G \downarrow F}$
It follows that $I$ is a well-defined object functor.
{{qed|lemma}}
Theorem: Functor Over Object Comma Category is Isomorphic to Comma Category/Lemma 2

:$J$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
By definition of category $\mathbf 1$:
:the only object in $\mathbf 1$ is $*$
By definition of comma category:
:every object in $\paren{G \downarrow F}$ is of the form $\tuple{E, *, g}$ where:
::$E$ is an object of $\mathbf D$
::$*$ is in $\mathbf 1$
::$g$ is a morphism $f:GE \to  F*$ of $\mathbf C$
By definition of $G$:
:given an object $\tuple{E, *, g}$ in $\paren{G \downarrow F}$:
::$g$ is a morphism $g:GE \to  C$ of $\mathbf C$
By definition of functor over object comma category:
:$\tuple{E, g}$ is an object in $\paren{G \downarrow C}$
It follows that $J$ is a well-defined object functor.
{{qed|lemma}}
Theorem: Functor Over Object Comma Category is Isomorphic to Comma Category/Lemma 3

:$J \circ I = \operatorname{id}_{\paren{G \downarrow C}}$
where $\operatorname{id}_{\paren{G \downarrow C}}$ denotes the identity functor on $\paren{G \downarrow C}$

Proof:
For each object $\tuple{E,g}$ in $\paren{G \downarrow C}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} \tuple{E, g}
      | r = \map J {I \tuple{E, g} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{E, *, g}
      | c = Definition of $I$
}}
{{eqn | r = \tuple{E, g}
      | c = Definition of $J$
}}
{{eqn | r = \operatorname{id}_{\paren{G \downarrow C} } \tuple{E, g}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $k: \tuple{E,g} \to \tuple{E',g'}$ in $\paren{G \downarrow C}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} k
      | r = \map J {I k }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{k, \operatorname{id}_*}
      | c = Definition of $I$
}}
{{eqn | r = k
      | c = Definition of $J$
}}
{{eqn | r = \operatorname{id}_{\paren{G \downarrow C} } k
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$J \circ I = \operatorname{id}_{\paren{G \downarrow C} }$
{{qed}}
Category:Functor Over Object Comma Category is Isomorphic to Comma Category
svrs0fn2moz14iistnapjkcgyhrc6ob
Theorem: Functor Over Object Comma Category is Isomorphic to Comma Category/Lemma 4

:$I \circ J = \operatorname{id}_{\paren{G \downarrow F}}$
where $\operatorname{id}_{\paren{G \downarrow F}}$ denotes the identity functor on $\paren{G \downarrow F}$

Proof:
For each object $\tuple{E, *, g}$ in $\paren{G \downarrow F}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{E, *, g}
      | r = \map I {J \tuple{E, *, g} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = I \tuple{E, g}
      | c = Definition of $J$
}}
{{eqn | r = \tuple{E, *, g}
      | c = Definition of $I$
}}
{{eqn | r = \operatorname{id}_{\paren{G \downarrow F} } \tuple{E, *, g}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $\tuple{k, \operatorname{id}_*}: \tuple{E, *, g} \to \tuple{E', *,g'}$ in $\paren{G \downarrow F}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{k, \operatorname{id}_*}
      | r = \map I {J \tuple{k, \operatorname{id}_*} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = I k
      | c = Definition of $J$
}}
{{eqn | r = \tuple{k, \operatorname{id}_*}
      | c = Definition of $I$
}}
{{eqn | r = \operatorname{id}_{\paren{G \downarrow F} } \tuple{k, \operatorname{id}_*}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$I \circ J = \operatorname{id}_{\paren{G \downarrow F} }$
{{qed}}
Category:Functor Over Object Comma Category is Isomorphic to Comma Category
0wtnvmi9qoqeze02xzq10n75knl2t2o
Theorem: Slice Category is Isomorphic to Comma Category/Lemma 1

:$I$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
Let $g$ be an object in $\mathbf C / C$.
By definition of slice category:
:$g$ is a morphism $g: \operatorname{dom} g \to C$ of $\mathbf C$
By definition of identity functor:
:$\map {\operatorname{id}_{\mathbf C} } {\operatorname{dom} g} = \operatorname{dom} g$
Hence:
:$g$ is a morphism $g: \map {\operatorname{id}_{\mathbf C} } {\operatorname{dom} g} \to F*$ of $\mathbf C$
By definition of comma category:
:$\tuple{\operatorname{dom} g, *, g}$ is an object in $\paren{\operatorname{id}_{\mathbf C} \downarrow F}$
It follows that $I$ is a well-defined object functor.
{{qed|lemma}}
Theorem: Slice Category is Isomorphic to Comma Category/Lemma 2

:$J$ is a covariant functor

Proof:
=== Object Functor is Well-defined ===
By definition of category $\mathbf 1$:
:the only object in $\mathbf 1$ is $*$
By definition of comma category:
:every object in $\paren{\operatorname{id}_{\mathbf C} \downarrow F}$ is of the form $\tuple{E, *, g}$ where:
::$E$ is an object of $\mathbf D$
::$*$ is in $\mathbf 1$
::$g$ is a morphism $g:\operatorname{id}_{\mathbf C}E \to  F*$ of $\mathbf C$
By definition of $\operatorname{id}_{\mathbf C}$:
:given an object $\tuple{E, *, g}$ in $\paren{G \downarrow F}$:
::$g$ is a morphism $g:E \to  C$ of $\mathbf C$
By definition of slice category:
:$g$ is an object in $\mathbf C / C$
It follows that $J$ is a well-defined object functor.
{{qed|lemma}}
Theorem: Slice Category is Isomorphic to Comma Category/Lemma 3

:$J \circ I = \operatorname{id}_{\mathbf C / C}$
where $\operatorname{id}_{\mathbf C / C}$ is the identity functor on $\mathbf C / C$

Proof:
For each object $g$ in $\mathbf C / C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} g
      | r = \map J {I g }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{\operatorname {dom} g, *, g}
      | c = Definition of $I$
}}
{{eqn | r = g
      | c = Definition of $J$
}}
{{eqn | r = \map {\operatorname{id}_{\mathbf C / C } } g
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $k: g \to g'$ in $\mathbf C / C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J \circ I} k
      | r = \map J {I k }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J \tuple{k, \operatorname{id}_*}
      | c = Definition of $I$
}}
{{eqn | r = k
      | c = Definition of $J$
}}
{{eqn | r = \map {\operatorname{id}_{\mathbf C / C} } k
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$J \circ I = \operatorname{id}_{\mathbf C / C}$
{{qed}}
Category:Slice Category is Isomorphic to Comma Category
p95gvoak3ab550k2mvttdxm6n4wdi5f
Theorem: Slice Category is Isomorphic to Comma Category/Lemma 4

:$I \circ J = \operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow F }}$
where $\operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow F }}$ is the identity functor on $\paren{\operatorname{id}_{\mathbf C} \downarrow F }$

Proof:
By definition of comma category:
:For each object $\tuple{E, *, g}$ in $\paren{\operatorname{id}_{\mathbf C} \downarrow F}$:
::$\text{(1)} \quad \operatorname{dom} g = E$
For each object $\tuple{E, *, g}$ in $\paren{\operatorname{id}_{\mathbf C} \downarrow F}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{E, *, g}
      | r = \map I {J \tuple{E, *, g} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = g
      | c = Definition of $J$
}}
{{eqn | r = \tuple{\operatorname{dom} g, *, g}
      | c = Definition of $I$
}}
{{eqn | r = \tuple{E, *, g}
      | c = By $\text{(1)}$
}}
{{eqn | r = \operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow F} } \tuple{E, *, g}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
For each morphism $\tuple{k, \operatorname{id}_*}: \tuple{E, *, g} \to \tuple{E', *,g'}$ in $\paren{\operatorname{id}_{\mathbf C} \downarrow F}$ we have:
{{begin-eqn}}
{{eqn | l = \paren{I \circ J} \tuple{k, \operatorname{id}_*}
      | r = \map I {J \tuple{k, \operatorname{id}_*} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = I k
      | c = Definition of $J$
}}
{{eqn | r = \tuple{k, \operatorname{id}_*}
      | c = Definition of $J$
}}
{{eqn | r = \operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow F} } \tuple{k, \operatorname{id}_*}
      | c = {{Defof|Identity Functor}}
}}
{{end-eqn}}
It follows that:
:$I \circ J = \operatorname{id}_{\paren{\operatorname{id}_{\mathbf C} \downarrow F} }$
{{qed}}
Category:Slice Category is Isomorphic to Comma Category
7d748emgbvudi57tp4uacctgoal6u40