avewright/proofwiki-math huggingface dataset:
Theorem: Expected Number of Cards Drawn Before First Ace

Consider a standard deck of $52$ cards.
We draw cards from the deck at uniform random without replacement.
The expected number of cards drawn ''before'' the first ace is $9.6$.
Hence the expected number of cards drawn before and including the first ace is $10.6$.

Proof:
Note that there are $4$ aces in the deck.
We number the $48$ other cards $1, 2, \ldots, 48$.
Label the aces by $A_1, A_2, A_3, A_4$. 
Define the indicator random variable $I_i$ by:
:$\ds I_i = \begin{cases}1 & \text {card } i \text { is drawn before the first ace} \\ 0 & \text{otherwise}\end{cases}$
The number of cards drawn before the first ace is:
:$\ds \sum_{i \mathop = 1}^{48} I_i$
The desired expected value is therefore:
:$\ds \sum_{i \mathop = 1}^{48} \expect {I_i}$
by Expectation is Linear.
We have:
:$\ds \expect {I_i} = \map \Pr {\text {card } i \text { is drawn before the first ace} }$
Since the $48$ non-ace cards are indistinguishable, we have:
:$\ds \expect {I_i} = \expect {I_1}$ for $1 \le i \le 48$. 
We therefore aim to compute $48 \map \Pr {\text {card } 1 \text { is drawn before the first ace} }$.
Consider the events:
:$\tuple {C_1, C_2, C_3, C_4, C_5}$
where: 
:$C_i$ are all distinct and equal to either $1$ or one of the aces $A_j$
:$C_i$ is the card that is drawn $i$th out of the cards in $\set {A_1, A_2, A_3, A_4, 1}$.
There are $5!$ ways to permute $\set {A_1, A_2, A_3, A_4, 1}$.
Since all cards remaining in the deck are equally likely to be drawn at any point, all such permutations are equally likely.
We aim to count the permutations with $C_1 = 1$. 
This corresponds to realizations where card $1$ is drawn before any ace.
Fixing $C_1 = 1$, there are $4!$ ways to permute the remaining cards $\set {A_1, A_2, A_3, A_4}$.
For every draw of $52$ cards without replacement, precisely one event $\tuple {C_1, C_2, C_3, C_4, C_5}$ will occur.
The probability that $C_1 = 1$ is:
:$\ds \frac {4!} {5!} = \frac 1 5$ 
Hence expected value of cards drawn ''before'' the first ace is:
:$\ds 48 \expect {I_1} = \frac {48} 5 = 9.6$
Including the first ace, the expected value is $10.6$ by Expectation is Linear.
{{qed}}
Category:Combinatorics
Category:Cards
eg49hfckw2u0lqv752d7k9js22s9xl4
Theorem: Fredholm Alternative/Simple Form

Let $\mathbf A$ be a square matrix.
Then either:
:$(1): \quad \mathbf v = \mathbf A \mathbf v + \mathbf b$ has a solution $\mathbf v$ for all $\mathbf b$
or:
:$(2): \quad \mathbf v = \mathbf A \mathbf v$ has a non-zero solution.
$(1)$ holds when $\mathbf A - \mathbf I$ is invertible
$(2)$ holds when $\mathbf A - \mathbf I$ is singular.

Proof:
{{ProofWanted}}
{{Namedfor|Erik Ivar Fredholm}}
Theorem: Fredholm Alternative/General Form

Let $\mathbf A$ be a self-adjoint compact operator over an infinite-dimensional Hilbert space.
{{help|The source work I am using does not go into detail of exactly what it is}}

Proof:
{{ProofWanted}}
{{Namedfor|Erik Ivar Fredholm}}
Theorem: Characterization of Adjunction Using Counit of 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.
Then:
:there exists an adjunction $\tuple{F, G, \alpha}$ between $\mathbf C$ and $\mathbf D$
{{iff}}:
:there exists a natural transformation $\xi: FG \to \operatorname {id}_{\mathbf C}$ such that:
::for each object $C$ in $\mathbf C$ the morphism $\xi_C$ is a universal morphism from functor $F$ to object $GC$.
Moreover:
:$\forall C \in \mathbf C: \map {\beta_{\tuple{GC, C}}} {\operatorname{id}_{GC}} = \xi_C$
and:
:$\forall f:D \to GC \in \mathbf D: \map {\beta_{\tuple{D, C}}} f = \xi_C \circ Ff$
where $\beta$ is the inverse of the natural isomorphism $\alpha$

Proof:
=== Necessary Condition ===
Let $\tuple{F, G, \alpha}$ be an adjunction between $\mathbf C$ and $\mathbf D$.
Let $\beta$ denote the inverse of the natural isomorphism $\alpha$
From Adjunction Induces Counit of Adjunction:
:the counit of adjunction $\eta$ is a natural transformation $\xi: FG \to \operatorname {id}_{\mathbf C}$ such that:
::for each object $C$ of $\mathbf C: \xi_{C} = \map {\beta_{\tuple{GC, C}}} {\operatorname {id}_{GC}}$
From Morphism of Counit of Adjunction is Universal:
:for each object $C$ in $\mathbf C$ the morphism $\xi_C$ is a universal morphism from functor $F$ to object $GC$
From Characterization of Adjunction Using Left Adjuncts of Morphisms:
:$\forall f:D \to GC \in \mathbf D: \map {\beta_{\tuple{D, C}}} f = \xi_C \circ Ff$
{{qed|lemma}}
Theorem: Universal Morphism from Object to Functor is Unique up to Isomorphism

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 $\tuple{R_1, u_1}$ and $\tuple{R_2, u_2}$ be a universal morphisms from $C$ to $F$.
Then:
:there exists an isomorphism $i: R_1 \to R_2$ such that $u_2 = Fi \circ u_1$

Proof:
By definition of universal morphisms from object to functor:
:$\tuple{R_1, u_1}$ and $\tuple{R_2, u_2}$ are initial objects of the functor under object comma category $\paren{C \downarrow F}$
From Initial Object is Unique:
:$\tuple{R_1, u_1}$ and $\tuple{R_2, u_2}$ are isomorphic in the functor under object comma category $\paren{C \downarrow F}$
From Isomorphism of Functor Under Object Comma Category:
:there exists an isomorphism $i: R_1 \to R_2$ such that $u_2 = Fi \circ u_1$
{{qed}}
Theorem: Universal Morphism from Functor to Object is Unique up to Isomorphism

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 $\tuple{R_1, u_1}$ and $\tuple{R_2, u_2}$ be a universal morphisms from $F$ to $C$.
Then:
:there exists an isomorphism $i: R_2 \to R_1$ such that $u_2 = u_1 \circ Fi$

Proof:
By definition of universal morphisms from functor to object:
:$\tuple{R_1, u_1}$ and $\tuple{R_2, u_2}$ are terminal objects of the functor over object comma category $\paren{F \downarrow C}$
From Terminal Object is Unique:
:$\tuple{R_1, u_1}$ and $\tuple{R_2, u_2}$ are isomorphic in the functor over object comma category $\paren{F \downarrow C}$
From Isomorphism of Functor Over Object Comma Category:
:there exists an isomorphism $i: R_2 \to R_1$ such that $u_2 = u_1 \circ Fi$
{{qed}}
Theorem: Isomorphism of Functor Under Object Comma Category

Let $\mathbf C$, $\mathbf D$ be categories.
Let $C$ be an object of $\mathbf C$.
Let $F : \mathbf D \to \mathbf C$ be a covariant functor.
Let $\paren{C \downarrow F}$ denote the comma category $F$ under $C$.
Let $h : \tuple{D_1, f_1} \to \tuple{D_2, f_2}$ be a morphism in $\paren{C \downarrow F}$.
Then:
:$h$ is an isomorphism in $\paren{C \downarrow F}$
{{iff}}
:$h: D_1 \to D_2 \in \mathbf D$ is an isomorphism such that $f_2 = F h \circ f_1$

Proof:
By definition of morphisms in $\paren{C \downarrow F}$:
:$h:D_1 \to D_2 \in \mathbf D$ is a morphism:
::$(1):\quad f_2 = F h \circ f_1$
By definition of isomorphism:
:$h$ is an isomorphism in $\paren{C \downarrow F}$
{{iff}}
:$(2): \quad \exists g : \tuple{D_2, f_2} \to \tuple{D_1, f_1} \in \paren{C \downarrow F}: g \circ h = \operatorname{id}_{\tuple{D_1,f_1}}$ and $h \circ g = \operatorname{id}_{\tuple{D_2,f_2} }$
By definition of identity morphisms in $\paren{C \downarrow F}$:
:$(2)$ holds
{{iff}}
:$(3): \quad \exists g : \tuple{D_2, f_2} \to \tuple{D_1, f_1} \in \paren{C \downarrow F}: g \circ h = \operatorname{id}_{D_1}$ and $h \circ g = \operatorname{id}_{D_2}$
By definition of morphisms in $\paren{C \downarrow F}$:
:$(3)$ holds
{{iff}}
:$(4): \quad \exists g : D_2 \to D_1 \in \mathbf D:$
::$f_1 = F g \circ f_2$
::$g \circ h = \operatorname{id}_{D_1}$
::$h \circ g = \operatorname{id}_{D_2}$
By definition of isomorphism:
:$h$ is an isomorphism in $\mathbf D$
{{iff}}
:$(5): \quad \exists g : D_2 \to D_1 \in \mathbf D:$
::$g \circ h = \operatorname{id}_{D_1}$
::$h \circ g = \operatorname{id}_{D_2}$
It follows that if $(4)$ holds then $(5)$ holds.
To complete the proof it needs to be shown that if $(5)$ holds then $(4)$ holds.
Let $(5)$ hold, that is let $g:D_2 \to D_1 \in \mathbf D$ be a morphism:
:$g \circ h = \operatorname{id}_{D_1}$
:$h \circ g = \operatorname{id}_{D_2}$
We have:
{{begin-eqn}}
{{eqn | l = F g \circ f_2 
      | r = F g \circ \paren{F h \circ f_1}
      | c = By $(1)$
}}
{{eqn | r = \paren{F g \circ F h} \circ f_1
      | c = {{Defof|Metacategory|Associativity of Composition}}
}}
{{eqn | r = \map F {g \circ h} \circ f_1
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r = \map F {\operatorname{id}_{D_1} } \circ f_1
      | c = {{Defof|Isomorphism (Category Theory)|Isomorphism}}
}}
{{eqn | r = \operatorname{id}_{FD_1} \circ f_1
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r = f_1
      | c = {{Defof|Identity Morphism}}
}}
{{end-eqn}}
It follows that $(4)$ holds.
The result follows.
{{qed}}
Category:Isomorphisms
Category:Comma Categories
qyjc864bd1wopgcc7tp9to6us86cbpr
Theorem: Isomorphism of Functor Over Object Comma Category

Let $\mathbf C$, $\mathbf D$ be categories.
Let $C$ be an object of $\mathbf C$.
Let $G : \mathbf E \to \mathbf C$ be a covariant functor.
Let $\paren{G \downarrow C}$ denote the comma category $G$ over $C$.
Let $k : \tuple{E_1, g_1} \to \tuple{E_2, g_2}$ be a morphism in $\paren{G \downarrow C}$.
Then:
:$k$ is an isomorphism in $\paren{G \downarrow C}$
{{iff}}
:$k: E_1 \to E_2 \in \mathbf E$ is an isomorphism such that $g_1 = g_2 \circ G k$

Proof:
By definition of morphisms in $\paren{G \downarrow C}$:
:$k:E_1 \to E_2 \in \mathbf E$ is a morphism:
::$(1):\quad g_1 = g_2 \circ G k$
By definition of isomorphism:
:$h$ is an isomorphism in $\paren{G \downarrow C}$
{{iff}}
:$(2): \quad \exists l : \tuple{E_2, g_2} \to \tuple{E_1, g_1} \in \paren{G \downarrow C}: l \circ k = \operatorname{id}_{\tuple{E_1,g_1}}$ and $k \circ l = \operatorname{id}_{\tuple{E_2,g_2} }$
By definition of identity morphisms in $\paren{G \downarrow C}$:
:$(2)$ holds
{{iff}}
:$(3): \quad \exists l : \tuple{E_2, g_2} \to \tuple{E_1, g_1} \in \paren{G \downarrow C}: l \circ k = \operatorname{id}_{E_1}$ and $k \circ l = \operatorname{id}_{E_2}$
By definition of morphisms in $\paren{G \downarrow C}$:
:$(3)$ holds
{{iff}}
:$(4): \quad \exists l : E_2 \to E_1 \in \mathbf E:$
::$g_2 = g_1 \circ G l$
::$l \circ k = \operatorname{id}_{E_1}$
::$k \circ l = \operatorname{id}_{E_2}$
By definition of isomorphism:
:$k$ is an isomorphism in $\mathbf D$
{{iff}}
:$(5): \quad \exists l : E_2 \to E_1 \in \mathbf E:$
::$l \circ k = \operatorname{id}_{E_1}$
::$k \circ l = \operatorname{id}_{E_2}$
It follows that if $(4)$ holds then $(5)$ holds.
To complete the proof it needs to be shown that if $(5)$ holds then $(4)$ holds.
Let $(5)$ hold, that is, let $l:E_2 \to E_1 \in \mathbf E$ be a morphism:
:$l \circ k = \operatorname{id}_{E_1}$
:$k \circ l = \operatorname{id}_{E_2}$
We have:
{{begin-eqn}}
{{eqn | l = g_1 \circ G l 
      | r = \paren{g_2 \circ G k} \circ G l
      | c = By $(1)$
}}
{{eqn | r = g_2 \circ \paren{G k \circ G l}
      | c = {{Defof|Metacategory|Associativity of Composition}}
}}
{{eqn | r = g_2 \circ \map G {k \circ l}
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r = g_2 \circ G \operatorname{id}_{E_2}
      | c = {{Defof|Isomorphism (Category Theory)|Isomorphism}}
}}
{{eqn | r = g_2 \circ \operatorname{id}_{G E_2}
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r = g_2
      | c = {{Defof|Identity Morphism}}
}}
{{end-eqn}}
It follows that $(4)$ holds.
The result follows.
{{qed}}
Category:Isomorphisms
Category:Comma Categories
5wiyk9hfi3lldqujyam9cuwaphfd1bu
Theorem: Characterization of Adjunction Using Right Adjuncts of Commutative Squares

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let $F : \mathbf D \to \mathbf C$,  $G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\mathbf D \times \mathbf C$ denote the product category of $\mathbf D$ with $\mathbf C$.
For each object $\tuple{D, C} \in \mathbf D \times \mathbf C$ let $\alpha$ associate $\tuple{D, C}$ with a bijection:
:$\alpha_{\tuple{D, C} } : \map {\operatorname{Hom}_{\mathbf C} } {FD, C} \to \map {\operatorname{Hom}_{\mathbf D} } {D, GC}$
Then:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(1):\quad$for every:
::$f:D_1 \to D_2 \in \mathbf D$
::$g:C_1 \to C_2 \in \mathbf C$
::$h:FD_1 \to C_1 \in \mathbf C$
::$k:FD_2 \to C_2 \in \mathbf C$
:we have:
::$k \circ Ff = g \circ h \quad \leadstoandfrom \quad \map {\alpha_{\tuple{D_2, C_2} } } k \circ f = Gg \circ \map {\alpha_{\tuple{D_1, C_1} } } h$
:That is, the left-hand square commutes in $\mathbf C$ {{iff}} the right-hand square commutes in $\mathbf D$:
::<nowiki>$\begin{xy}
<0em,5em>*+{FD_1} = "TL",
<9em,5em>*+{FD_2} = "TR",
<0em,0em>*+{C_1} = "BL",
<9em,0em>*+{C_2} = "BR",
"TL";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{F f},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{h},
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{k},
<13em,2.5em>*+{\leadstoandfrom} = "C",
<21em,5em>*+{D_1} = "TL",
<30em,5em>*+{D_2} = "TR",
<21em,0em>*+{G C_1} = "BL",
<30em,0em>*+{G C_2} = "BR",
"TL";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{Gg},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^3.0em/{\map {\alpha_{\tuple{D_1, C_1} } } h},
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_3.0em/{\map {\alpha_{\tuple{D_2, C_2} } } k},
\end{xy}$</nowiki>

Proof:
From Characterization of Adjunction Using Right Adjuncts of Compositions:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(2)\quad$ for every $h:FD \to C_1 \in \mathbf C$ and $g:C_1 \to C_2 \in \mathbf C$
::$\qquad\qquad\map {\alpha_{\tuple{D, C_2} } } {g \circ h} = Gg \circ \map {\alpha_{\tuple{D, C_1} } } h$
:$(3)\quad$ for every $f:D_1 \to D_2 \in \mathbf D$ and $k:FD_1 \to C \in \mathbf C$:
::$\qquad\qquad\map {\alpha_{\tuple{D_1, C} } } {k \circ Ff} = \map {\alpha_{\tuple{D_2, C} } } k \circ f$
We show that $(2)$ and $(3)$ hold {{iff}} $(1)$ hollds.
Theorem: Characterization of Adjunction Using Left Adjuncts of Commutative Squares

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let $F : \mathbf D \to \mathbf C$,  $G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\mathbf D \times \mathbf C$ denote the product category of $\mathbf D$ with $\mathbf C$.
For each object $\tuple{D, C} \in \mathbf D \times \mathbf C$ let $\beta$ associate $\tuple{D, C}$ with a bijection:
:$\beta_{\tuple{D, C} } : \map {\operatorname{Hom}_{\mathbf D} } {D, GC} \to \map {\operatorname{Hom}_{\mathbf C} } {FD, C}$
For each object $\tuple{D, C} \in \mathbf D \times \mathbf C$ let $\alpha_{\tuple{D, C} }$ denote the inverse of $\beta_{\tuple{D, C} }$:
:$\alpha_{\tuple{D, C} } = \beta_{\tuple{D, C} }^{-1} : \map {\operatorname{Hom}_{\mathbf C} } {FD, C} \to \map {\operatorname{Hom}_{\mathbf D} } {D, GC}$
Then:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(1)$ for every:
::$f:D_1 \to D_2 \in \mathbf D$
::$g:C_1 \to C_2 \in \mathbf C$
::$h:D_1 \to G C_1 \in \mathbf C$
::$k:D_2 \to G C_2 \in \mathbf C$
:we have:
::$k \circ f = G g \circ h \quad \leadstoandfrom \quad \map {\beta_{\tuple{D_2, C_2} } } k \circ Ff = g \circ \map {\beta_{\tuple{D_1, C_1} } } h$
:That is, the left-hand square commutes in $\mathbf D$ {{iff}} the right-hand square commutes in $\mathbf C$:
::<nowiki>$\begin{xy}
<0em,5em>*+{D_1} = "TL",
<9em,5em>*+{D_2} = "TR",
<0em,0em>*+{GC_1} = "BL",
<9em,0em>*+{GC_2} = "BR",
"TL";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{G g},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{h},
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{k},
<13em,2.5em>*+{\leadstoandfrom} = "C",
<21em,5em>*+{F D_1} = "TL",
<30em,5em>*+{F D_2} = "TR",
<21em,0em>*+{C_1} = "BL",
<30em,0em>*+{C_2} = "BR",
"TL";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{F f},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^3.0em/{\map {\beta_{\tuple{D_1, C_1} } } h},
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_3.0em/{\map {\beta_{\tuple{D_2, C_2} } } k},
\end{xy}$</nowiki>

Proof:
From Characterization of Adjunction Using Right Adjuncts of Commutative Squares:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(2):\quad$for every:
::$f:D_1 \to D_2 \in \mathbf D$
::$g:C_1 \to C_2 \in \mathbf C$
::$h:FD_1 \to C_1 \in \mathbf C$
::$k:FD_2 \to C_2 \in \mathbf C$
:we have:
::$k \circ Ff = g \circ h \quad \leadstoandfrom \quad \map {\alpha_{\tuple{D_2, C_2} } } k \circ f = Gg \circ \map {\alpha_{\tuple{D_1, C_1} } } h$
It is to be shown that $(1)$ holds {{iff}} $(2)$ holds.
Theorem: Left Whiskered Composite of Natural Transformation is Natural Transformation

Let $\mathbf C$, $\mathbf D$ and $\mathbf B$ be categories.
Let $F, G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: F \to G$ be a natural transformation.
Let $H : \mathbf B \to \mathbf C$ be a covariant functor.
Let $\eta H: F \circ H \to G \circ H$ denote the left whiskered composite of $\eta$ by $H$.
Then:
:$\eta H$ is a natural transformation.

Proof:
Let $\operatorname{id}_{\mathbf D}$ denote the identity functor of $\mathbf D$
Let $\operatorname{id}_{\mathbf D} \eta H : \operatorname{id}_{\mathbf D} \mathop \circ F \circ H \to \operatorname{id}_{\mathbf D} \mathop \circ G \circ H$ denote the double-sided whiskered composite of $\eta$ by $\operatorname{id}_{\mathbf D}$ and $H$.
From Double-sided Whiskered Composite of Natural Transformation is Natural Transformation:
:$\operatorname{id}_{\mathbf D} \eta H$ is a natural transformation.
From Left Whiskered Composite of Natural Transformation is Double-sided Whiskered Composite:
:$\eta H = \operatorname{id}_{\mathbf D} \eta H$
The result follows.
{{qed}}
Theorem: Square Matrix has Full Rank iff Nonsingular

Let $\mathbf A$ be an $n \times n$ square matrix.
Then:
:$\mathbf A$ is of full rank
{{iff}}:
:$\mathbf A$ is nonsingular.

Proof:
By the definition of full rank:
:$\mathbf A$ is of full rank {{iff}} $\map \rho {\mathbf A} = n$
where $\map \rho {\mathbf A}$ denotes the rank of $\mathbf A$.
By the definition of rank:
:$\map \rho {\mathbf A} = n$ {{iff}} the rows of $\mathbf A$ are linearly independent
By Square Matrix has Linearly Dependent Rows iff Determinant is Zero:
:the rows of $\mathbf A$ are linearly independent {{iff}} $\map \det {\mathbf A} \ne 0$
By the definition of nonsingular matrix:
:$\map \det {\mathbf A} \ne 0$ {{iff}} $\mathbf A$ is nonsingular
{{qed}}
Theorem: Right Whiskered Composite of Natural Transformation is Natural Transformation

Let $\mathbf C$, $\mathbf D$ and $\mathbf E$ be categories.
Let $F, G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: F \to G$ be a natural transformation.
Let $K : \mathbf D \to \mathbf E$ be a covariant functor.
Let $K \eta : K \circ F \to K \circ G$ denote the right whiskered composite of $\eta$ by $K$.
Then:
:$K \eta$ is a natural transformation.

Proof:
Let $\operatorname{id}_{\mathbf C}$ denote the identity functor of $\mathbf C$
Let $K \eta \operatorname{id}_{\mathbf C}: K \circ F \circ \operatorname{id}_{\mathbf C} \to K \circ G \circ \operatorname{id}_{\mathbf C}$ denote the double-sided whiskered composite of $\eta$ by $K$ and $\operatorname{id}_{\mathbf C}$.
From Double-sided Whiskered Composite of Natural Transformation is Natural Transformation:
:$K \eta \operatorname{id}_{\mathbf C}$ is a natural transformation.
From Right Whiskered Composite of Natural Transformation is Double-sided Whiskered Composite:
:$K \eta = K \eta \operatorname{id}_{\mathbf C}$
The result follows.
{{qed}}
Theorem: Double-sided Whiskered Composite of Natural Transformation is Natural Transformation

Let $\mathbf C$, $\mathbf D$, $\mathbf E$ and $\mathbf B$ be categories.
Let $F, G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: F \to G$ be a natural transformation.
Let $H : \mathbf B \to \mathbf C$ and $K : \mathbf D \to \mathbf E$ be a covariant functors.
Let $K \eta H: K \circ F \circ H \to K \circ G \circ H$ denote the double-sided whiskered composite of $\eta$ by $K$ and $H$.
Then:
:$K \eta H$ is a natural transformation

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall f: X \to Y \in \mathbf B
      | l = \paren{K \eta H}_Y \circ \paren{K \circ F \circ H} f
      | r = K \eta_{HY} \circ \paren{K \circ F \circ H} f
      | c = {{Defof|Double-sided Whiskered Composite of Natural Transformation|Double-sided Whiskered Composite}}
}}
{{eqn | r = K \eta_{HY} \circ \map K {\map F {H f} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = \map K {\eta_{HY} \circ \map F {H f} }
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r = \map K {\map G {H f} \circ \eta_{HX} }
      | c = {{Defof|Natural Transformation}}
}}
{{eqn | r = \map K {\map G {H f} } \circ K \eta_{HX}
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r = \paren{K \circ G \circ H} f \circ K \eta_{HX}
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = \paren{K \circ G \circ H} f \circ \paren{K \eta H}_X
      | c = {{Defof|Double-sided Whiskered Composite of Natural Transformation|Double-sided Whiskered Composite}}
}}
{{end-eqn}}
It follows that $K \eta H: K \circ F \circ H \to K \circ G \circ H$ is a natural transformation by definition.
{{qed}}
Theorem: Left Whiskered Composite of Natural Transformation is Double-sided Whiskered Composite

Let $\mathbf C$, $\mathbf D$ and $\mathbf B$ be categories.
Let $F, G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: F \to G$ be a natural transformation.
Let $H : \mathbf B \to \mathbf C$ be a covariant functor.
Let $\eta H: F \circ H \to G \circ H$ denote the left whiskered composite of $\eta$ by $H$.
Let $\operatorname{id}_{\mathbf D}$ denote the identity functor of $\mathbf D$
Let $\operatorname{id}_{\mathbf D} \eta H : \operatorname{id}_{\mathbf D} \mathop \circ F \circ H \to \operatorname{id}_{\mathbf D} \mathop \circ G \circ H$ denote the double-sided whiskered composite of $\eta$ by $\operatorname{id}_{\mathbf D}$ and $H$.
Then:
:$\eta H = \operatorname{id}_{\mathbf D} \eta H$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall B \in \mathbf B
      | l = \paren{\operatorname{id}_{\mathbf D} \eta H}_B
      | r = \operatorname{id}_{\mathbf D} \eta_{HB}
      | c = {{Defof|Double-sided Whiskered Composite of Natural Transformation|Double-sided Whiskered Composite}}
}}
{{eqn | r = \eta_{HB}
      | c = {{Defof|Identity Functor}}
}}
{{eqn | r = \paren{\eta H}_B
      | c = {{Defof|Left Whiskered Composite of Natural Transformation|Left Whiskered Composite}}
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Whiskered Composites
f88jygtc3wten4gc4rn5e1bmi7urwa2
Theorem: Right Whiskered Composite of Natural Transformation is Double-sided Whiskered Composite

Let $\mathbf C$, $\mathbf D$ and $\mathbf E$ be categories.
Let $F, G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: F \to G$ be a natural transformation.
Let $K : \mathbf D \to \mathbf E$ be a covariant functor.
Let $K \eta: K \circ F \to K \circ G$ denote the right whiskered composite of $\eta$ by $K$.
Let $\operatorname{id}_{\mathbf C}$ denote the identity functor of $\mathbf C$
Let $K \eta \operatorname{id}_{\mathbf C}: K \circ F \circ \operatorname{id}_{\mathbf C} \to K \circ G \circ \operatorname{id}_{\mathbf C}$ denote the double-sided whiskered composite of $\eta$ by $K$ and $\operatorname{id}_{\mathbf C}$.
Then:
:$K \eta = K \eta \operatorname{id}_{\mathbf C}$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall C \in \mathbf C
      | l = \paren{K \eta \operatorname{id}_{\mathbf C} }_C
      | r = K \eta_{\operatorname{id}_{\mathbf C} C}
      | c = {{Defof|Double-sided Whiskered Composite of Natural Transformation|Double-sided Whiskered Composite}}
}}
{{eqn | r = K \eta_C
      | c = {{Defof|Identity Functor}}
}}
{{eqn | r = \paren{K \eta}_C
      | c = {{Defof|Right Whiskered Composite of Natural Transformation|Right Whiskered Composite}}
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Whiskered Composites
i4npl9r5yygwnu88v3w6xy2mlldwjpx