avewright/proofwiki-math huggingface dataset:
Theorem: Morphism of Unit of Adjunction is Universal

Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let  $\tuple {F, G, \alpha}$ be an adjunction between $\mathbf C$ and $\mathbf D$.
Let $\eta: \operatorname {id}_{\mathbf D} \to GF$ be the unit of adjunction $\tuple {F, G, \alpha}$
Then:
:for each object $D$ in $\mathbf D$ the morphism $\eta_D$ is a universal morphism from $FD$ to $G$

Proof:
By definition of unit of adjunction:
:* for each $D$ of $\mathbf D: \eta_{_D} = \map {\alpha_{\tuple{D, F D}}} {\operatorname {id}_{FD}}$ where
::* $\alpha_{\tuple{D, F D}} : \map {\operatorname{Hom}_{\mathbf C} } {F D, F D} \to \map {\operatorname{Hom}_{\mathbf D} } {D, GF D}$ is the bijection from the adjunction $\tuple {F, G, \alpha}$
::* $\operatorname {id}_{F D}$ is the identity morphism of $F D$.
:* $\operatorname {id}_{\mathbf D}$ is the identity functor on $\mathbf D$
:* $GF$ is the composite functor of $G$ with $F$
By definition of universal morphism, it is to be shown:
:for each morphism $m: D \to GC \in \mathbf D$ there exists a unique morphism $m': FD \to C \in \mathbf C$:
::$Gm' \circ \eta_D = m$
Let $D \in \mathbf D$ and $C \in \mathbf C$ be objects.
Let $m: D \to GC \in \mathbf D$ be a morphism.
From Characterization of Adjunction Using Right Adjuncts of Morphisms:
:$\alpha$ associates a bijection with each object $\tuple{D, C} \in \mathbf D \times \mathbf C$ :
::$\alpha_{\tuple{D, C} } : \map {\operatorname{Hom}_{\mathbf C} } {FD, C} \to \map {\operatorname{Hom}_{\mathbf D} } {D, GC}$
:such that:
::$(1)\quad$ for every $g:FD \to C \in \mathbf C$:
:::$\qquad\qquad\map {\alpha_{\tuple{D, C} } } {g} = Gg \circ \map {\alpha_{\tuple{D, FD} } } {\operatorname{id}_{FD}}$
::$(2)\quad$ for every $f:D_2 \to D_1 \in \mathbf D$:
:::$\qquad\qquad\map {\alpha_{\tuple{D_2, FD_1} } } {Ff} = \map {\alpha_{\tuple{D_1, FD_1} } } {\operatorname{id}_{FD_1}} \circ f$
Let $m' = \map {\alpha_{\tuple{D, C} }^{-1} } m$.
We have:
{{begin-eqn}}
{{eqn | l = m
      | r = \map {\alpha_{\tuple{D, C} } } {m'}
      | c = As $m' = \map {\alpha_{\tuple{D, C} }^{-1} } m$
}}
{{eqn | r = Gm' \circ \map {\alpha_{\tuple{D, C} } } {\operatorname{id}_{FD} }
      | c = By $(1)$
}}
{{eqn | r = Gm' \circ \eta_D
      | c = {{Defof|Unit of Adjunction}}
}}
{{end-eqn}}
It remains to show that $m'$ is unique.
Let $m' ': FD \to C \in \mathbf C$ be a morphism such that:
:$Gm' ' \circ \eta_D = m$
We have:
{{begin-eqn}}
{{eqn | l = \map {\alpha_{\tuple{D, C} } } {m' '}
      | r = Gm' ' \circ \map {\alpha_{\tuple{D, C} } } {\operatorname{id}_{FD} }
      | c = By $(1)$
}}
{{eqn | r = Gm' ' \circ \eta_D
      | c = {{Defof|Unit of Adjunction}}
}}
{{eqn | r = m
      | c = {{Hypothesis}}
}}
{{eqn | r = \map {\alpha_{\tuple{D, C} } } {m'}
      | c = As $m' = \map {\alpha_{\tuple{D, C} }^{-1} } m$
}}
{{eqn | ll = \leadsto
      | l = m' '
      | r = m'
      | c = {{Defof|Bijection}}
}}
{{end-eqn}}
It follows that $\eta_D: D \to GFD$ is universal from $FD$ to $G$
{{qed}}
Theorem: Equivalence of Definitions of Universal Morphism from Functor to Object

Let $\mathbf C$ and $\mathbf D$ be metacategories.
Let $C$ be an object of $\mathbf C$.
Let $F: \mathbf D \to \mathbf C$ be a covariant functor.
Let the pair $\tuple{R, v}$ consist of an object $R$ of $\mathbf D$ and a morphism $v: FR \to C$ in $C$.
{{TFAE|def=Universal Morphism from Functor to Object|context=Category Theory}}
=== Definition 1 ===
{{:Definition:Universal Morphism from Functor to Object/Definition 1}}
=== Definition 2 ===
{{:Definition:Universal Morphism from Functor to Object/Definition 2}}

Proof:
The result follows immediately from:
* Definition:Terminal Object
* Definition:Functor Over Object Comma Category
{{qed}}
Theorem: Morphism of Counit of Adjunction is Universal

Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let  $\tuple {F, G, \alpha}$ be an adjunction between $\mathbf C$ and $\mathbf D$.
Let $\xi: FG \to \operatorname {id}_{\mathbf C}$ be the counit of adjunction $\tuple {F, G, \alpha}$
Then:
:for each object $C$ in $\mathbf C$ the morphism $\xi_C$ is a universal morphism from $F$ to $GC$

Proof:
Let $\beta$ be the inverse of the natural isomorphism $\alpha$.
By definition of counit of adjunction:
:* for each $C$ of $\mathbf C: \xi_{C} = \map {\beta_{\tuple{GC, C}}} {\operatorname {id}_{GC}}$ where
::* $\beta_{\tuple{GC, C} }: \map {\operatorname{Hom}_{\mathbf C} } {F G C, C} \to \map {\operatorname{Hom}_{\mathbf D} } {G C, G C}$ is the bijection of the inverse natural isomorphism $\beta$.
::* $\operatorname {id}_{G C}$ is the identity morphism of $G C$.
:* $\operatorname {id}_{\mathbf C}$ is the identity functor on $\mathbf C$
:* $FG$ is the composite functor of $F$ with $G$
By definition of universal morphism, it is to be shown:
:for each morphism $m: FD \to C \in \mathbf C$ there exists a unique morphism $m': D \to GC \in \mathbf D$:
::$\xi_C \circ Fm' = m$
Let $D \in \mathbf D$ and $C \in \mathbf C$ be objects.
Let $m: D \to GC \in \mathbf D$ be a morphism.
From Characterization of Adjunction Using Left Adjuncts of Morphisms, we have:
:$(1):\quad$ for every $g:C_1 \to C_2 \in \mathbf C$:
::$\qquad\qquad\map {\beta_{\tuple{GC_1, C_2} } } {G g} = g \circ \map {\beta_{\tuple{GC_1, C_1} } } {\operatorname{id}_{GC_1}}$
:$(2):\quad$ for every $f:D \to GC \in \mathbf D$:
::$\qquad\qquad\map {\beta_{\tuple{D, C} } } f = \map {\beta_{\tuple{GC, C} } } {\operatorname{id}_{GC} } \circ F f$
Let $m' = \map {\alpha_{\tuple{D, C} } } m$.
We have:
{{begin-eqn}}
{{eqn | l = m
      | r = \map {\alpha_{\tuple{D, C} }^{-1} } {m'}
      | c = As $m' = \map {\alpha_{\tuple{D, C} }^{-1} } m$
}}
{{eqn | r = \map {\beta_{\tuple{D, C} } } {m'}
      | c = By definition of $\beta: \beta_{\tuple{D, C} } = \alpha_{\tuple{D, C} }^{-1}$
}}
{{eqn | r = \map {\beta_{\tuple{GC, C} } } {\operatorname{id}_{GC} } \circ F m'
      | c = By $(2)$
}}
{{eqn | r = \xi_C \circ Fm'
      | c = {{Defof|Counit of Adjunction}}
}}
{{end-eqn}}
It remains to show that $m'$ is unique.
Let $m' ': D \to GC \in \mathbf D$ be a morphism such that:
:$\xi_C \circ Fm' ' = m$
We have:
{{begin-eqn}}
{{eqn | l = \map {\beta_{\tuple{D, C} } } {m' '}
      | r = \map {\beta_{\tuple{GC, C} } } {\operatorname{id}_{GC} } \circ F m' '
      | c = By $(2)$
}}
{{eqn | r = \xi_C \circ Fm' '
      | c = {{Defof|Counit of Adjunction}}
}}
{{eqn | r = m
      | c = {{Hypothesis}}
}}
{{eqn | r = \map {\beta_{\tuple{D, C} } } {m'}
      | c = As $m' = \map {\alpha_{\tuple{D, C} } } m$
}}
{{eqn | ll = \leadsto
      | l = m' '
      | r = m'
      | c = {{Defof|Bijection}}
}}
{{end-eqn}}
It follows that $\xi_C: FGC \to C$ is universal from $F$ to $GC$
{{qed}}
Theorem: Unit of Adjunction Induces Adjunction

Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let  $F: \mathbf D \to \mathbf C$ and $G:\mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: \operatorname {id}_{\mathbf D} \to GF$ be a natural transformation such that:
:for each object $D$ in $\mathbf D$ the morphism $\eta_D$ is a universal morphism from object $FD$ to functor $G$
For each $D$ in $\mathbf D$ and $C$ in $\mathbf C$ let:
:$\alpha_{\tuple{D, C}}: \map {\mathrm {Hom}_{\mathbf C} } {FD, C} \to \map {\mathrm {Hom}_{\mathbf D} } {D, GC}$
be the mapping defined by:
:$\forall g \in \map {\mathrm {Hom}_{\mathbf C} } {FD, C}: \map {\alpha_{\tuple{D, C}}} g = Gg \circ \eta_D$
Then:
:$\tuple{F, G, \alpha}$ is an an adjunction between $\mathbf C$ and $\mathbf D$ such that $\eta$ is the unit of adjunction $\tuple{F, G, \alpha}$.

Proof:
From Characterization of Adjunction Using Right Adjuncts of Morphisms:
::the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(1)\quad$ For each $D$ in $\mathbf D$ and $C$ in $\mathbf C : \alpha_{\tuple{D, C}}: \map {\mathrm {Hom}_{\mathbf C} } {FD, C} \to \map {\mathrm {Hom}_{\mathbf D} } {D, GC}$ is a bijection
:$(2)\quad$ for every $g:FD \to C \in \mathbf C$:
::$\qquad\qquad\map {\alpha_{\tuple{D, C} } } {g} = Gg \circ \map {\alpha_{\tuple{D, FD} } } {\operatorname{id}_{FD}}$
:$(3)\quad$ for every $f:D_2 \to D_1 \in \mathbf D$:
::$\qquad\qquad\map {\alpha_{\tuple{D_2, FD_1} } } {Ff} = \map {\alpha_{\tuple{D_1, FD_1} } } {\operatorname{id}_{FD_1}} \circ f$
Theorem: Counit of Adjunction Induces Adjunction

Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let  $F: \mathbf D \to \mathbf C$ and $G:\mathbf C \to \mathbf D$ be functors.
Let $\xi: FG \to \operatorname {id}_{\mathbf C}$ be a natural transformation such that:
:for each object $C$ in $\mathbf C$ the morphism $\xi_C$ is a universal morphism from $F$ to $GC$
For objects $D$ in $\mathbf D$ and $C$ in $\mathbf C$ let:
:$\alpha_{\tuple{D, C}}: \map {\mathrm {Hom}_{\mathbf C} } {FD, C} \to \map {\mathrm {Hom}_{\mathbf D} } {D, GC}$
be the mapping with inverse defined by:
:$\forall f \in \map {\mathrm {Hom}_{\mathbf D} } {D, GC}: \map {\beta_{\tuple{D, C}}} f = \xi_C \circ Ff$
Then:
:$\tuple{F, G, \alpha}$ is an an adjunction between $\mathbf C$ and $\mathbf D$.

Proof:
From Characterization of Adjunction Using Left Adjuncts of Morphisms, we have:
:$(1)\quad$For each $D$ in $\mathbf D$ and $C$ in $\mathbf C : \beta_{\tuple{D, C}}: \map {\mathrm {Hom}_{\mathbf D} } {D, GC} \to \map {\mathrm {Hom}_{\mathbf C} } {FD, C}$ is a bijection
:$(2):\quad$ for every $g:C_1 \to C_2 \in \mathbf C$:
::$\qquad\qquad\map {\beta_{\tuple{GC_1, C_2} } } {G g} = g \circ \map {\beta_{\tuple{GC_1, C_1} } } {\operatorname{id}_{GC_1}}$
:$(3):\quad$ for every $f:D \to GC \in \mathbf D$:
::$\qquad\qquad\map {\beta_{\tuple{D, C} } } f = \map {\beta_{\tuple{GC, C} } } {\operatorname{id}_{GC} } \circ F f$
Theorem: Characterization of Convergence of Net in Initial Topology

Let $X$ be a set.
Let $\FF$ be a set of functions $f : X \to Y_f$. 
For each $f \in \FF$, let $\tau_f$ be a topology on $Y_f$. 
Let $\tau$ be the initial topology on $X$ induced by $\FF$ with $f \in \FF$ given the topology $\tau_f$. 
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a net in $X$.
Let $x \in X$. 
Then $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$ in $\struct {X, \tau}$ {{iff}}:
:$\map f {x_\lambda} \to \map f x$ in $\struct {Y_f, \tau_f}$
for each $f \in \FF$.

Proof:
=== Necessary Condition ===
Suppose that $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$.
Let $f \in \FF$.
From the definition of the initial topology, $f$ is continuous. 
From Characterization of Continuity in terms of Nets, we have:
:$\map f {x_\lambda} \to \map f x$ in $\struct {Y_f, \tau_f}$. 
{{qed|lemma}}
Theorem: Characterization of Convergence of Net in Product Topology

Let $I$ be a set. 
Let $\family {\tuple {X_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$ be an $I$-indexed family of sets.
Let:
:$\ds X = \prod_{\alpha \mathop \in I} X_\alpha$ 
Let $\family {\pi_\alpha}_{\alpha \mathop \in I}$ be the coordinate projections $X \to X_\alpha$. 
Let $\tau$ be the product topology on $X$. 
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a net in $X$.
Let $x \in X$. 
Then $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$ {{iff}}:
:$\map {\pi_\alpha} {x_\lambda} \to \map {\pi_\alpha} x$
for each $\alpha \in I$.

Proof:
Note that $\tau$ is the initial topology on $X$ induced by $\FF = \family {\pi_\alpha}_{\alpha \mathop \in I}$.
The result then follows from Characterization of Convergence of Net in Initial Topology.
{{qed}}
Category:Product Topology
Category:Nets (Set Theory)
fkznrsyme589w5l9sr43d7ui72mhayq
Theorem: Closed Graph Theorem/Compact Hausdorff Codomain

Let $\struct {X, \tau_X}$ be a topological space.
Let $\struct {Y, \tau_Y}$ be a compact $T_2$ (Hausdorff) space.
Equip $X \times Y$ with the product topology $\tau_{X \times Y}$. 
Let $f : X \to Y$ be a mapping.
Let $G_f$ be the graph of $f$.
Then $f$ is continuous {{iff}} $G_f$ is closed in $\struct {X \times Y, \tau_{X \times Y} }$.

Proof:
=== Necessary Condition ===
Suppose that $f$ is continuous.
From Characterization of Closedness in terms of Nets, it is enough to show that:
:every convergent net in $G_f$ has its limit in $G_f$.
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {\tuple {x_\lambda, y_\lambda} }_{\lambda \mathop \in \Lambda}$ be a convergent net in $G_f$ with limit $\tuple {u, v}$.
We aim to show that $u = x$ and $v = \map f x$.
From Characterization of Convergence of Net in Product Topology, we have:
:$x_\lambda \to x$
and:
:$y_\lambda \to v$ 
Hence we have $u = x$. 
We have $y_\lambda = \map f {x_\lambda}$ for each $\lambda \in \Lambda$.
Since $f$ is continuous, we have $y_\lambda = \map f {x_\lambda} \to \map f x$ from Characterization of Continuity in terms of Nets.
Since $Y$ is $T_2$ (Hausdorff) and $y_\lambda \to v$, we obtain $v = \map f x$ from Characterization of Hausdorff Property in terms of Nets.
Hence $\tuple {u, v} \in G_f$.
Hence every convergent net in $G_f$ has its limit in $G_f$.
Hence from Characterization of Closedness in terms of Nets, $G_f$ is closed in $\struct {X \times Y, \tau_{X \times Y} }$.
{{qed|lemma}}
Theorem: Vector Space with Subspace of Algebraic Dual Separating Points is Dual System

Let $K$ be a field.
Let $E$ be a vector space over $K$.
Let $E^\#$ be the algebraic dual of $E$.
Let $F \subseteq E^\#$ be a vector subspace of $E^\#$ that separates points.
Define $\innerprod \cdot \cdot : E \times F \to K$ by:
:$\innerprod x f = \map f x$ for each $\tuple {x, f} \in E \times F$. 
Then $\tuple {E, F, \innerprod \cdot \cdot}$ is a dual system.

Proof:
We first show that $\innerprod \cdot \cdot$ is a bilinear mapping.
Let $x_1, x_2, x \in E$ and $f_1, f_2, f \in F$ and $\lambda \in K$.
We have:
{{begin-eqn}}
{{eqn	| l = \innerprod {x_1 + \lambda x_2} f
		| r = \map f {x_1 + \lambda x_2} 
}}
{{eqn	| r = \map f {x_1} + \lambda \map f {x_2}
		| c = {{Defof|Linear Functional}}
}}
{{eqn	| r = \innerprod {x_1} f + \lambda \innerprod {x_2} f
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn	| l = \innerprod x {f_1 + \lambda f_2}
		| r = \map {\paren {f_1 + \lambda f_2} } x
}}
{{eqn	| r = \map {f_1} x + \lambda \map {f_2} x
}}
{{eqn	| r = \innerprod x {f_1} + \lambda \innerprod x {f_2} 
}}
{{end-eqn}}
Hence $\innerprod \cdot \cdot$ is a bilinear mapping.
We now show that if $x \in E$ and $\innerprod x f = {\mathbf 0}_K$ for all $f \in F$, then $x = {\mathbf 0}_E$.
Since $f$ separates points, if $x \ne {\mathbf 0}_E$ then there exists $f \in F$ such that $\map f x = \innerprod x f \ne {\mathbf 0}_K = \map f { {\mathbf 0}_E}$.
Hence if $x \in E$ and $\innerprod x f = {\mathbf 0}_K$ for all $f \in F$, then $x = {\mathbf 0}_E$.
We now show that if $f \in F$ and $\innerprod x f = {\mathbf 0}_K$ for all $x \in E$, then $f = {\mathbf 0}_F$.
Since $\innerprod x f = \map f x$, we have that $\map f x = {\mathbf 0}_K$ for all $x \in E$.
Hence $f = {\mathbf 0}_F$.
{{qed}}
Category:Dual Systems
Category:Vector Space with Subspace of Algebraic Dual Separating Points is Dual System
Category:Algebraic Duals
llhzd488z3qyj04izra447x9ketiu1d
Theorem: Algebraic Dual Separates Points of Vector Space

Let $K$ be a field.
Let $E$ be a vector space over $K$.
Let $E^\#$ be the algebraic dual of $E$. 
Then $E^\#$ separates points.

Proof:
We have that $E^\#$ separates points {{iff}}:
:for all $x, y \in E$ with $x \ne y$, there exists $f \in E^\#$ with $\map f x \ne \map f y$. 
If $E = \set { {\mathbf 0}_E}$ (that is, $\dim E = 0$), then there are no $x, y \in E$ with $x \ne y$, hence this holds trivially.
Now suppose that $\dim E \ge 1$.
Since each $f \in E^\#$ is a linear functional, the claim is equivalent to:
:for all $x, y \in E$ with $x - y \ne {\mathbf 0}_E$, there exists $f \in E^\#$ with $\map f x \ne {\mathbf 0}_K$
In other words:
:for all $x \in E \setminus \set { {\mathbf 0}_E}$, there exists $f \in E^\#$ with $\map f x \ne {\mathbf 0}_K$.
Let $x \in E \setminus \set { {\mathbf 0}_E}$.
From Linearly Independent Set is Contained in some Basis, there exists a basis $\BB$ for $E$ containing $x$.
From Linear Transformation Defined from Basis, it is enough to specify an $f \in E^\#$ on $\BB$. 
We do this by taking $\map f x = {\mathbf 1}_K$ and $\map f y = {\mathbf 0}_K$ for $y \in \BB \setminus \set x$. 
Then $f \in E^\#$ and $\map f x \ne {\mathbf 0}_K$.
Hence $E^\#$ separates points.
{{qed}}
Category:Algebraic Duals
7ojm5us5m9aoshh8768nr3sbhxfteyp
Theorem: Linear Transformation Defined from Basis

Let $K$ be a field.
Let $X$ and $Y$ be vector spaces over $K$.
Let $\BB = \set {e_\alpha : \alpha \in I}$ be a basis for $X$. 
For each $\alpha \in I$, let $c_\alpha \in Y$.
Then there exists a linear transformation $T : X \to Y$ with $T e_\alpha = c_\alpha$ for each $\alpha \in I$.
This allows us to define a linear transformation $T$ by specifying its action on a basis and then "extending linearly".

Proof:
Define a mapping $T : X \to Y$ by:
:$\map T { {\mathbf 0}_X} = {\mathbf 0}_Y$
and:
:$\ds \map T {\sum_{\alpha \mathop \in F} \lambda_\alpha e_\alpha} = \sum_{\alpha \mathop \in F} \lambda_\alpha c_\alpha$ for every non-empty finite set $F \subseteq I$ and $\set {\lambda_\alpha : \alpha \in F} \subseteq K$. 
Note that the presence of $\lambda_\alpha$ with $\lambda_\alpha = {\mathbf 0}_K$ does not effect the value of $T$, so we will omit consideration of this.
Since $\BB$ is a basis for $X$:
:for each $x \in X$ there exists a unique finite set $F \subseteq I$ and unique $\set {\lambda_\alpha : \alpha \in F} \subseteq K \setminus \set { {\mathbf 0}_K}$ such that:
::$\ds x = \sum_{\alpha \mathop \in F} \lambda_\alpha e_\alpha$
Hence we are assured that $T$ is well-defined.
From this definition, we have $T e_\alpha = c_\alpha$ for each $\alpha \in I$.
We aim to show that $T$ is linear.
Let $x, y \in X$ and $t \in K$.
Let $F_1 \subseteq I$, $F_2 \subseteq I$, $\set {\lambda_\alpha : \alpha \in F_1} \subseteq K$ and $\set {\lambda_\alpha : \alpha \in F_2} \subseteq K$ be such that:
:$\ds x = \sum_{\alpha \mathop \in F_1} \lambda_\alpha e_\alpha$
and:
:$\ds y = \sum_{\alpha \mathop \in F_2} \mu_\alpha e_\alpha$
Then we have:
:$\ds x + t y = \sum_{\alpha \mathop \in F_1 \cup F_2} \paren {\lambda_\alpha + t \mu_\alpha} e_\alpha$
Hence by the definition of $T$, we have:
:$\ds \map T {x + t y} = \sum_{\alpha \mathop \in F_1 \cup F_2} \paren {\lambda_\alpha + t \mu_\alpha} c_\alpha$
We then have:
:$\ds \sum_{\alpha \mathop \in F_1 \cup F_2} \paren {\lambda_\alpha + t \mu_\alpha} c_\alpha = \sum_{\alpha \mathop \in F_1} \lambda_\alpha c_\alpha + t \sum_{\alpha \mathop \in F_2} \mu_\alpha c_\alpha = T x + t T y$
Hence we have:
:$\map T {x + t y} = T x + t T y$ for each $x, y \in X$ and $t \in K$.
Hence $T$ is linear.
We have already established that $T e_\alpha = c_\alpha$ for each $\alpha \in I$, so we are done.
{{qed}}
Category:Linear Algebra
tdozssl6lzddhkqztbfsacb5ek3ljnm
Theorem: Absolute Polar Reverses Subset Relation

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $A \subseteq B \subseteq E$ be non-empty.
Let $A^\circ$ and $B^\circ$ denote the absolute polars of $A$ and $B$ in $\innerprod E F$.
Then $B^\circ \subseteq A^\circ$.

Proof:
Suppose that $f \in B^\circ$.
Then $\cmod {\innerprod x f} \le 1$ for all $x \in B$.
Since $A \subseteq B$, we in particular have $\cmod {\innerprod x f} \le 1$ for all $x \in A$.
Hence $f \in A^\circ$.
We have shown that if $f \in B^\circ$, then $f \in A^\circ$, so $B^\circ \subseteq A^\circ$.
{{qed}}
Theorem: Absolute Polar of Dilation

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $A \subseteq E$ be non-empty.
Let $\lambda > 0$. 
Let $A^\circ$ and $\paren {\lambda A}^\circ$ be the absolute polar of $A$ and $\lambda A$ respectively.
Then:
:$\paren {\lambda A}^\circ = \dfrac 1 \lambda A^\circ$

Proof:
Let $f \in \dfrac 1 \lambda A^\circ$. 
This is the case {{iff}} $\lambda f \in A^\circ$.
This is equivalent to $\cmod {\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 $\cmod {\innerprod x {\lambda f} } \le 1$ for each $x \in A$ is equivalent to $\cmod {\innerprod {\lambda x} f} \le 1$ for each $x \in A$.
This is equivalent to $\cmod {\innerprod z f} \le 1$ for each $z \in \lambda A$.
This is equivalent to $f \in \paren {\lambda A}^\circ$.
Hence:
:$\paren {\lambda A}^\circ = \dfrac 1 \lambda A^\circ$ 
{{qed}}
Theorem: Intersection of Absolute Polars is Absolute Polar of Union

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

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

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $A \subseteq E$ be non-empty. 
Let $A^\circ$ be the absolute polar of $A$.
Then $A^\circ \ne \O$.

Proof:
Since $\innerprod \cdot \cdot$ is bilinear, we have $\innerprod x { {\mathbf 0}_F} = 0$ for each $x \in E$.
In particular, we have $\innerprod x { {\mathbf 0}_F} = 0$ for each $x \in A$.
Hence ${\mathbf 0}_F \in A^\circ$, and $A^\circ \ne \O$.
{{qed}}
Theorem: Absolute Polar is Convex

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

Proof:
Let $f, g \in A^\circ$ and $t \in \closedint 0 1$.
Then, for all $x \in A$ we have:
:$\cmod {\innerprod x f} \le 1$
and:
:$\cmod {\innerprod x g} \le 1$
Then we have:
{{begin-eqn}}
{{eqn	| l = \cmod {\innerprod x {t f + \paren {1 - t} g} }
		| r = \cmod {t \innerprod x f + \paren {1 - t} \innerprod x g}
		| c = $\innerprod \cdot \cdot$ is bilinear
}}
{{eqn	| o = \le
		| r = t \cmod {\innerprod x f} + \paren {1 - t} \cmod {\innerprod x g}
}}
{{eqn	| o = \le
		| r = t + \paren {1 - t}
		| c = since $f, g \in A^\circ$ and $x \in A$ 
}}
{{eqn	| r = 1
}}
{{end-eqn}}
Hence $t f + \paren {1 - t} g \in A^\circ$ for all $f, g \in A^\circ$ and $t \in \closedint 0 1$.
Hence $A^\circ$ is convex.
{{qed}}
Theorem: Absolute Polar is Balanced

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

Proof:
Let $s \in \GF$ be such that $\cmod s \le 1$. 
Let $f \in A^\circ$.
Then $\cmod {\innerprod x f} \le 1$ for each $x \in A$.
Then:
{{begin-eqn}}
{{eqn	| l = \cmod {\innerprod x {s f} }
		| r = \cmod {s \innerprod x f}
		| c = $\innerprod \cdot \cdot$ is bilinear
}}
{{eqn	| r = \cmod s \cmod {\innerprod x f}
}}
{{eqn	| o = \le
		| r = \cmod {\innerprod x f}
}}
{{eqn	| o = \le
		| r = 1
}}
{{end-eqn}}
{{qed}}