avewright/proofwiki-math huggingface dataset:
Theorem: Square Pyramidal and Triangular Numbers

The only positive integers which are simultaneously square pyramidal and triangular are:
:$1, 55, 91, 208 \, 335$
{{OEIS|A039596}}

Proof:
{{begin-eqn}}
{{eqn | l = 1
      | r = \dfrac {1 \paren {1 + 1} \paren {2 \times 1 + 1} } 6
      | c = Closed Form for Square Pyramidal Numbers
}}
{{eqn | r = \dfrac {1 \times \paren {1 + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 55
      | r = \dfrac {5 \paren {5 + 1} \paren {2 \times 5 + 1} } 6
      | c = Closed Form for Square Pyramidal Numbers
}}
{{eqn | r = \dfrac {10 \times \paren {10 + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 91
      | r = \dfrac {6 \paren {6 + 1} \paren {2 \times 6 + 1} } 6
      | c = Closed Form for Square Pyramidal Numbers
}}
{{eqn | r = \dfrac {13 \times \paren {13 + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 208 \, 335
      | r = \dfrac {85 \paren {85 + 1} \paren {2 \times 85 + 1} } 6
      | c = Closed Form for Square Pyramidal Numbers
}}
{{eqn | r = \dfrac {645 \times \paren {645 + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{end-eqn}}
{{ProofWanted|It remains to be shown that these are the only such instances.}}
Theorem: Palindromes Formed by Multiplying by 55

$55$ multiplied by any of the odd integers between $91$ and $109$ inclusive produces a palindromic number.

Proof:
We have that:
:$55 \times 91 = 5005$
Then we have that:
:$55 \times 2 = 110$
Thus:
:$\forall k: 1 \le k \le 9: 55 \times 2 k = 110k = 110, 220, 330, \ldots, 990$
Thus for $1 \le k \le 9$:
:$55 \times \paren {91 + 2 k} = \sqbrk {5kk5}_{10}$
That is:
{{begin-eqn}}
{{eqn | l = 55 \times 91
      | r = 5005
}}
{{eqn | l = 55 \times 93
      | r = 5115
}}
{{eqn | l = 55 \times 95
      | r = 5225
}}
{{eqn | l = 55 \times 97
      | r = 5335
}}
{{eqn | l = 55 \times 99
      | r = 5445
}}
{{eqn | l = 55 \times 101
      | r = 5555
}}
{{eqn | l = 55 \times 103
      | r = 5665
}}
{{eqn | l = 55 \times 105
      | r = 5775
}}
{{eqn | l = 55 \times 107
      | r = 5885
}}
{{eqn | l = 55 \times 109
      | r = 5995
}}
{{end-eqn}}
{{qed}}
Theorem: Dirichlet Convolution is Commutative

:$f * g = g * f$

Proof:
From the definition of the Dirichlet convolution:
:$\ds \map {\paren {f * g} } n = \sum_{a b \mathop = n} \map f a \map g b$
By definition, arithmetic functions are mappings from the natural numbers $\N$ to the complex numbers $\C$.
Thus $\map f a, \map g b \in \C$ and commutativity follows from Complex Multiplication is Commutative.
{{qed}}
Theorem: Dirichlet Convolution is Associative

: $\paren {f * g} * h = f * \paren {g * h}$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map {\paren {\paren {f * g} * h} } n
      | r = \sum_{a b \mathop = n} \map {\paren {f * g} } a \map h b
}}
{{eqn | r = \sum_{a b \mathop = n} \ \sum_{c d \mathop = a} \map f c \map g d \map h b
}}
{{eqn | r = \sum_{b c d \mathop = n} \map f c \map g d \map h b
}}
{{end-eqn}}
and
{{begin-eqn}}
{{eqn | l = \map {\paren {f * \paren {g * h} } } n
      | r = \sum_{a b \mathop = n} \map f a \map {\paren {g * h} } b
}}
{{eqn | r = \sum_{a b \mathop = n} \map f a \sum_{c d \mathop = b} \map g c \map h d
}}
{{eqn | r = \sum_{a c d \mathop = n} \map f a \map g c \map h d
}}
{{end-eqn}}
and associativity follows.
{{qed}}
Theorem: Identity Element for Dirichlet Convolution

:$\iota * f = f$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map {\paren {\iota * f} } n
      | r = \sum_{d \mathop \divides n} \delta_{d 1} \map f {\frac n d}
}}
{{eqn | r = \map f n
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Upper Adjoint of Galois Connection is Surjection implies Lower Adjoint at Element is Minimum of Preimage of Singleton of Element

Let $L = \struct {S, \preceq}, R = \paren {T, \precsim}$ be ordered sets.
Let $g: S \to T, d:T \to S$ be mappings such that:
:$\tuple {g, d}$ is a Galois connection
and
:$g$ is a surjection.
Then
:$\forall t \in T: \map d t = \min \set {g^{-1} \sqbrk {\set t} }$

Proof:
By definition of Galois connection:
:$g$ is an increasing mapping.
Let $t \in T$.
By definition of surjection:
:$\Img g = T$
By {{Corollary|Image of Preimage under Mapping}}:
:$g \sqbrk {g^{-1} \sqbrk {t^\succeq} } = t^\succeq$
By Galois Connection is Expressed by Minimum:
:$\map d t = \min \set {g^{-1} \sqbrk {t^\succeq} }$
By definition of min operation:
:$\map d t = \inf \set {g^{-1} \sqbrk {t^\succeq} }$ and $\map d t \in g^{-1} \sqbrk {t^\succeq}$
By definition of image of set:
:$\map g {\map d t} \in g \sqbrk {g^{-1} \sqbrk {t^\succeq} }$
By definition of upper closure of element:
:$t \precsim \map g {\map d t}$
By definition of minimum element:
:$g^{-1} \sqbrk {t^\succeq}$ admits an infimum.
By definition of infimum:
:$\map d t$ is lower bound for $g^{-1} \sqbrk {t^\succeq}$
By definition of surjection:
:$\exists s \in S: t = \map g s$
By definition of singleton:
:$t \in \set t$
By Set is Subset of Upper Closure
:$\set t \subseteq \set t^\succeq$
By Upper Closure of Singleton:
:$\set t^\succeq = t^\succeq$
By definition of image of set:
:$s \in g^{-1} \sqbrk {t^\succeq}$
By definition of lower bound:
:$\map d t \preceq s$
By definition of increasing mapping:
:$\map g {\map d t} \precsim t$
By definition of antisymmetry:
:$\map g {\map d t} = t$
By definition of preimage of set:
:$\map d t \in g^{-1} \sqbrk {\set t}$
By Preimage of Subset is Subset of Preimage:
:$g^{-1} \sqbrk {\set t} \subseteq g^{-1} \sqbrk {t^\succeq}$
We will prove that
:$\map d t$ is an infimum of $g^{-1} \sqbrk {\set t}$
Thus by Lower Bound is Lower Bound for Subset:
:$\map d t$ is lower bound for $g^{-1} \sqbrk {\set t}$
Thus by definition:
:$\forall s \in S: s$ is lower bound for $g^{-1} \sqbrk {\set t} \implies s \preceq \map d t$
{{qed|lemma}}
Thus by definition of min operation:
:$\map d t = \min \set {g^{-1} \sqbrk {\set t} }$
{{qed}}
Theorem: Dirichlet Convolution Preserves Multiplicativity

Let $f, g: \N \to \C$ be multiplicative arithmetic functions.
Then their Dirichlet convolution $f * g$ is again multiplicative.

Proof:
Let $m, n$ be coprime integers.
By definition of multiplicative functions, we have:
:$(1): \quad \map f {m n} = \map f m \map f n$
:$(2): \quad \map g {m n} = \map g m \map g n$
{{begin-eqn}}
{{eqn | l = \map {\paren {f * g} } {m n}
      | r = \sum_{d \mathop \divides m n} \map f d \map g {\frac {m n} d}
      | c = {{Defof|Dirichlet Convolution}}
}}
{{eqn | r = \sum_{\substack {r \mathop \divides m \\ s \mathop \divides n} } \map f {r s} \map g {\frac m r \frac n s}
      | c = Divisors of Product of Coprime Integers
}}
{{eqn | r = \sum_{\substack {r \mathop \divides m \\ s \mathop \divides n} } \map f r \map f s \map g {\frac m r} \map g {\frac n s}
      | c = $f, g$ are multiplicative
}}
{{eqn | r = \paren {\sum_{r \mathop \divides m} \map f r \map g {\frac m r} } \paren {\sum_{s \mathop \divides n} \map f s \map g {\frac n s} }
      | c = 
}}
{{eqn | r = \map {\paren {f * g} } m \times \map {\paren {f * g} } n
      | c = {{Defof|Dirichlet Convolution}}
}}
{{end-eqn}}
{{qed}}
Theorem: Dirichlet Convolution Preserves Multiplicativity/General Result

Let $S \subset \N$ be a set of natural numbers with the property:
:$m n \in S, \map \gcd {m, n} = 1 \implies m, n \in S$
Define:
:$\map {\paren {f*_S g} } n = \ds \sum_{\substack {d \mathop \divides n \\ d \mathop \in S} } \map f d \map g {n / d}$
Then $f*_S g$ is multiplicative.

Proof:
{{ProofWanted}}
Category:Dirichlet Convolution
Category:Multiplicative Functions
6pxmrgwltwzdbylg0m216tm3dnlo927
Theorem: Even Integer with Abundancy Index greater than 9

Let $n \in \Z_{>0}$ have an abundancy index greater than $9$.
Then $n$ has at least $35$ distinct prime factors.

Proof:
As Divisor Sum Function is Multiplicative, it follows easily that abundancy index is multiplicative as well.
We have for any prime $p$ and positive integer $k$:
{{begin-eqn}}
{{eqn | l = \frac {\map {\sigma_1} {p^k} } {p^k}
      | r = \frac {p^{k + 1} - 1} {p^k \paren {p - 1} }
      | c = Divisor Sum of Power of Prime
}}
{{eqn | r = \frac {p - p^{-k} } {p - 1}
}}
{{eqn | o = <
      | r = \frac p {p - 1}
      | c = as $p^{-k} > 0$
}}
{{eqn | r = 1 + \frac 1 {p - 1}
}}
{{end-eqn}}
In fact this is the limit of the abundancy index of a prime power.
The greater the prime, the smaller this value is.
Therefore finding the least number of prime factors a number needs to have its abundancy index exceed $9$ is to find the least $m$ such that:
:$\ds \prod_{i \mathop = 1}^m \frac {p_i} {p_i - 1} > 9$
where $p_i$ is the $i$th prime ordered by size.
The result can be verified by direct computation.
{{qed}}
Theorem: Closed Form for Pentatope Numbers

The closed-form expression for the $n$th pentatope number is:
:$P_n = \dfrac {n \paren {n + 1} \paren {n + 2} \paren {n + 3} } {24}$

Proof:
{{begin-eqn}}
{{eqn | l = P_n
      | r = \sum_{k \mathop = 1}^n T_k
      | c = {{Defof|Pentatope Number}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n \frac {n \paren {n + 1} \paren {n + 2} } 6
      | c = Closed Form for Tetrahedral Numbers
}}
{{eqn | r = \sum_{k \mathop = 1}^n \frac {\paren {n^3 + 3 n^2 + 2 n} } 6
      | c = 
}}
{{eqn | r = \frac 1 6 \sum_{k \mathop = 1}^n n^3 + \frac 1 2 \sum_{k \mathop = 1}^n n^2 + \frac 1 3 \sum_{k \mathop = 1}^n n
      | c = Summation is Linear
}}
{{eqn | r = \frac 1 6 \sum_{k \mathop = 1}^n n^3 + \frac 1 2 \sum_{k \mathop = 1}^n n^2 + \frac 1 3 \frac {n \paren {n + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \frac 1 6 \sum_{k \mathop = 1}^n n^3 + \frac 1 2 \frac {n \paren {n + 1} \paren {2 n + 1} } 6 + \frac 1 3 \frac {n \paren {n + 1} } 2
      | c = Sum of Sequence of Squares
}}
{{eqn | r = \frac 1 6 \dfrac {n^2 \paren {n + 1}^2} 4 + \frac 1 2 \frac {n \paren {n + 1} \paren {2 n + 1} } 6 + \frac 1 3 \frac {n \paren {n + 1} } 2
      | c = Sum of Sequence of Cubes
}}
{{eqn | r = \dfrac {n^2 \paren {n + 1}^2 + 2 n \paren {n + 1} \paren {2 n + 1} + 4 n \paren {n + 1} } {24}
      | c = putting over a common denominator
}}
{{eqn | r = \dfrac {n \paren {n + 1} \paren {n \paren {n + 1} + 2 \paren {2 n + 1} + 4} } {24}
      | c = extracting $n \paren {n + 1}$ as a factor
}}
{{eqn | r = \dfrac {n \paren {n + 1} \paren {n^2 + 5 n + 6} } {24}
      | c = simplifying
}}
{{eqn | r = \dfrac {n \paren {n + 1} \paren {n + 2} \paren {n + 3} } {24}
      | c = factorising
}}
{{end-eqn}}
{{qed}}
Theorem: Relation Between Rank and Exponent of Convergence

Let $f: \C \to \C$ be an entire function.
Let $k$ be its rank and $\tau$ be its exponent of convergence.
Then:
* $k=\tau=0$ if $f$ has finitely many zeroes.
* $k<\tau\leq k+1$ otherwise.

Proof:
{{ProofWanted}}
Category:Entire Functions
epim9a757ti02kdsc835c98mkdrn4my
Theorem: Necessary and Sufficient Condition for First Order System to be Field for Second Order System

Let $\mathbf y$, $\mathbf f$, $\boldsymbol \psi$ be N-dimensional vectors.
Let $\boldsymbol\psi$ be continuously differentiable.
Then $\forall x \in \closedint a b$ the first-order system of differential equations:
:$\mathbf y' = \map {\boldsymbol \psi} {x, \mathbf y}$
is a field for the second-order system
:$\mathbf y'' = \map {\mathbf f} {x, \mathbf y, \mathbf y'}$
{{iff}} $\boldsymbol \psi$ satisfies:
:$\ds \frac {\partial \boldsymbol \psi} {\partial x} + \sum_{i \mathop = 1}^N \frac {\partial \boldsymbol \psi} {\partial y_i} \psi_i = \map {\mathbf f} {x, \mathbf y, \boldsymbol \psi}$
That is, every solution to Hamilton-Jacobi system is a field for the original system.

Proof:
=== Necessary condition ===
Differentiate the first-order system {{WRT|Differentiation}} $x$:
{{begin-eqn}}
{{eqn | l = \mathbf y''
      | r = \frac {\d \boldsymbol \psi} {\d x}
}}
{{eqn | r = \frac {\partial \boldsymbol \psi} {\partial x} + \sum_{i \mathop = 1}^N \frac {\partial \boldsymbol \psi} {\partial y_i} \frac {\d y_i} {\d x}
}}
{{eqn | r = \frac {\partial \boldsymbol \psi} {\partial x} + \sum_{i \mathop = 1}^N \frac {\partial \boldsymbol \psi} {\partial y_i} \psi_i
}}
{{end-eqn}}
This can be rewritten as the following system of equations:
:$\mathbf y'' = \map {\mathbf f} {x, \mathbf y, \mathbf y'}$
:$\ds \frac {\partial \boldsymbol \psi} {\partial x} + \sum_{i \mathop = 1}^N \frac {\partial \boldsymbol \psi} {\partial y_i} \psi_i = \map {\mathbf f} {x, \mathbf y, \mathbf y'}$
By assumption, the first-order system is valid in $\closedint a b$.
For the second-order system to be valid in the same interval, the corresponding Hamilton-Jacobi equation has to hold as well.
{{qed|lemma}}
Theorem: Tetrahedral Number as Sum of Squares

:$H_n = \ds \sum_{k \mathop = 0}^{n / 2} \paren {n - 2 k}^2$
where $H_n$ denotes the $n$th tetrahedral number.

Proof:
Let $n$ be even such that $n = 2 m$.
We have:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{n / 2} \paren {n - 2 k}^2
      | r = \sum_{k \mathop = 0}^m \paren {2 m - 2 k}^2
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^m \paren {2 k}^2
      | c = Permutation of Indices of Summation
}}
{{eqn | r = \frac {2 m \paren {m + 1} \paren {2 m + 1} } 3
      | c = Sum of Sequence of Even Squares
}}
{{eqn | r = \frac {2 m \paren {2 m + 1} \paren {2 m + 2} } 6
      | c = 
}}
{{eqn | r = H_{2 m}
      | c = Closed Form for Tetrahedral Numbers
}}
{{end-eqn}}
Let $n$ be odd such that $n = 2 m + 1$.
We have:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{n / 2} \paren {n - 2 k}^2
      | r = \sum_{k \mathop = 0}^m \paren {2 m + 1 - 2 k}^2
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^m \paren {2 k + 1}^2
      | c = Permutation of Indices of Summation
}}
{{eqn | r = \frac {\paren {m + 1} \paren {2 m + 1} \paren {2 m + 3} } 3
      | c = {{Corollary|Sum of Sequence of Odd Squares}}
}}
{{eqn | r = \frac {\paren {2 m + 1} \paren {2 m + 2} \paren {2 m + 3} } 6
      | c = 
}}
{{eqn | r = H_{2 m + 1}
      | c = Closed Form for Tetrahedral Numbers
}}
{{end-eqn}}
{{qed}}
Category:Tetrahedral Number as Sum of Squares
Category:Tetrahedral Numbers
Category:Square Numbers
r2onjs36asjghpiqif8qm9s8qhdnz7z
Theorem: Sum of Sequence of Odd Squares/Corollary

:$\ds \forall n \in \N: \sum_{r \mathop = 0}^n \paren {2 r + 1}^2 = \frac {\paren {n + 1} \paren {2 n + 1} \paren {2 n + 3} } 3$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 0}^n \paren {2 n + 1}^2
      | r = \sum_{r \mathop = 0}^{n - 1} \paren {2 r + 1}^2 + \paren {2 n + 1}^2
      | c = 
}}
{{eqn | r = \sum_{r \mathop = 1}^n \paren {2 \paren {r - 1} + 1}^2 + \paren {2 n + 1}^2
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \sum_{r \mathop = 1}^n \paren {2 r - 1}^2 + \paren {2 n + 1}^2
      | c = simplifying
}}
{{eqn | r = \frac {n \paren {4 n^2 - 1} } 3 + \paren {2 n + 1}^2
      | c = Sum of Sequence of Odd Squares
}}
{{eqn | r = \frac {n \paren {2 n + 1} \paren {2 n - 1} + 3 \paren {2 n + 1}^2} 3
      | c = Difference of Two Squares
}}
{{eqn | r = \frac {\paren {2 n + 1} \paren {n \paren {2 n - 1} + 3 \paren {2 n + 1} } } 3
      | c = factoring
}}
{{eqn | r = \frac {\paren {2 n + 1} \paren {2 n^2 - n + 6 n + 3} } 3
      | c = multiplying out
}}
{{eqn | r = \frac {\paren {2 n + 1} \paren {2 n^2 + 5 n + 3} } 3
      | c = 
}}
{{eqn | r = \frac {\paren {n + 1} \paren {2 n + 1} \paren {2 n + 3} } 3
      | c = factoring
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence of Odd Squares/Corollary

:$\ds \forall n \in \N: \sum_{r \mathop = 0}^n \paren {2 r + 1}^2 = \frac {\paren {n + 1} \paren {2 n + 1} \paren {2 n + 3} } 3$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 0}^n \paren {2 r + 1}^2
      | r = \sum_{r \mathop = 0}^n \paren {2 r}^2 + \sum_{r \mathop = 0}^n 4 i + \sum_{r \mathop = 0}^n 1
      | c = 
}}
{{eqn | r = \frac {2 n \paren {n + 1} \paren {2 n + 1} } 3 + 4 \sum_{r \mathop = 0}^n r + \sum_{r \mathop = 0}^n 1
      | c = Sum of Sequence of Even Squares
}}
{{eqn | r = \frac {2 n \paren {n + 1} \paren {2 n + 1} } 3 + 4 \sum_{r \mathop = 1}^n r + \sum_{r \mathop = 0}^n 1
      | c = adjustment of indices: $4 r = 0$ when $r = 0$
}}
{{eqn | r = \frac {2 n \paren {n + 1} \paren {2 n + 1} } 3 + 4 \frac {n \paren {n + 1} } 2 + \sum_{r \mathop = 0}^n 1
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \frac {2 n \paren {n + 1} \paren {2 n + 1} } 3 + 2 n \paren {n + 1} + \paren {n + 1}
      | c = further simplification
}}
{{eqn | r = \frac {\paren {n + 1} \paren {2 n \paren {2 n + 1} + 6 n + 3} } 3
      | c = factorising
}}
{{eqn | r = \frac {\paren {n + 1} \paren {4 n^2 + 8 n + 3} } 3
      | c = multiplying out
}}
{{eqn | r = \frac {\paren {n + 1} \paren {2 n + 1} \paren {2 n + 3} } 3
      | c = factorising
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence of Even Squares

:$\ds \forall n \in \N: \sum_{i \mathop = 0}^n \paren {2 i}^2 = \frac {2 n \paren {n + 1} \paren {2 n + 1} } 3$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 0}^n \paren {2 i}^2
      | r = 4 \sum_{i \mathop = 1}^n i^2
      | c = adjustment of indices: $4 i^2 = 0$ when $i = 0$
}}
{{eqn | r = 4 \frac {n \paren {n + 1} \paren {2 n + 1} } 6
      | c = Sum of Sequence of Squares
}}
{{eqn | r = \frac {2 n \paren {n + 1} \paren {2 n + 1} } 3
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Category:Square Numbers
Category:Sums of Sequences
5smeev4yhmidppseh1h2dzz5riecxlp
Theorem: Killing Form of Orthogonal Lie Algebra

Let $\mathbb K \in \set {\C, \R}$.
Let $n$ be a positive integer.
Let $\map {\mathfrak {so}_n} {\mathbb K}$ be the Lie algebra of the special orthogonal group $\map {\operatorname {SO_n} } {\mathbb K}$.
Then its Killing form is $B: \tuple {X, Y} \mapsto \paren {n - 2} \map \tr {X Y}$.

Proof:
=== Lemma ===
Let $R$ be a ring with unity.
Let $n$ be a positive integer.
Let $E_{ij}$ denote the matrix with only zeroes except a $1$ at the $\tuple {i, j}$th position.
Then for all $X, Y \in R^{n \times n}$:
:$\ds \sum_{1 \mathop \le i \mathop < j \le n} \map \tr {\paren {\map X {E_{ij} - E_{ji} } Y}^t \paren {E_{ij} - E_{ji} } } = \map \tr Y \map \tr X - \map \tr {Y^t X}$
{{qed|lemma}}
{{ProofWanted|Use Trace of Alternating Product of Matrices and Almost Zero Matrices. Use Definition:Frobenius Inner Product and Trace in Terms of Orthonormal Basis and the fact that the $\paren {E_{ij} - E_{ji} } / \sqrt 2$ are an orthonormal basis of $\mathfrak {so}_n$.}}
Theorem: Killing Form of Symplectic Lie Algebra

Let $\mathbb K \in \set {\C, \R}$.
Let $n$ be a positive integer.
Let $\map {\mathfrak {sp}_{2 n} } {\mathbb K}$ be the Lie algebra of the symplectic group $\map {\operatorname {Sp} } {2 n, \mathbb K}$.
Then its Killing form is $B: \tuple {X, Y} \mapsto \paren {2 n + 2} \map \tr {X Y}$.

Proof:
=== Lemma ===
Let $R$ be a ring with unity.
Let $n$ be a positive integer.
Let $E_{ij}$ denote the matrix with only zeroes except a $1$ at the $\tuple {i, j}$th position.
Let $X, Y \in R^{2 n \times 2 n}$.
Let $X = \begin {pmatrix} X_{11} & X_{12} \\ X_{21} & X_{22} \end{pmatrix}$ and $Y = \begin{pmatrix} Y_{11} & Y_{12} \\ Y_{21} & Y_{22}\end{pmatrix}$
Then:
:$\ds \sum_{i, j \mathop = 1}^{2 n} \map \tr {\paren {X E_{i j} Y}^t E_{i j} } = \map \tr Y \map \tr X$
:$\ds \sum_{i, j \mathop = 1}^n \map \tr {\paren {X E_{ij} Y}^t E_{j + n, i + n} } = \map \tr {Y_{1 2}^t X_{2 1} }$
Theorem: Trace of Alternating Product of Matrices and Almost Zero Matrices

Let $R$ be a ring with unity.
Let $n, m$ be positive integers.
Let $E_{ij}$ denote the $n \times n$ matrix with only zeroes except a $1$ at the $\tuple {i, j}$th element.
Let $A_1, \ldots, A_m \in R^{n \times n}$.
Let $i_k, j_k \in \set {1, \ldots, n}$ for $k \in \set {1, \ldots, m}$.
Let $i_0 = i_m$ and $j_0 = j_m$.
Then:
:$\map \tr {A_1 E_{i_1, j_1} A_2 E_{i_2, j_2} \cdots A_m E_{i_m, j_m} } = \ds \prod_{k \mathop = 1}^m \sqbrk {A_k}_{j_{k - 1} i_k}$

Proof:
Use induction and the facts $E_{i j} A E_{k l} = A_{j k} E_{i l}$ and $\map \tr {A E_{i j} } = A_{j i}$ (induction basis).
{{ProofWanted}}
Category:Matrix Theory
90xzg6kakcyz1uk8egkxzr0imns4wuo
Theorem: Trace in Terms of Orthonormal Basis

Let $\mathbb K \subset \C$ be a field.
{{explain|Can the field be more general than just being a subfield of $\C$? Can it not in fact be an arbitrary Definition:Valued Field?}}
Let $\struct {V, \innerprod {\, \cdot \,} {\, \cdot \,} }$ be an inner product space over $\mathbb K$ of dimension $n$.
Let $\tuple {e_1, \ldots, e_n}$ be an orthonormal basis of $V$.
Let $f: V \to V$ be a linear operator.
Then its trace equals:
:$\map \tr f = \ds \sum_{i \mathop = 1}^n \innerprod {\map f {e_i} } {e_i}$

Proof:
Let $\ds \map f {e_i} = \sum_{j \mathop = 1}^n c_{ij} e_j$
Let $A$ be the matrix relative to the basis $\tuple {e_1, \ldots, e_n}$.
Then by the above assumption, $A_{ij} = c_{ij}$.
Then:
{{begin-eqn}}
{{eqn | l = \map \tr f
      | r = \map \tr A
      | c = {{Defof|Trace of Linear Operator}}
}}
{{eqn | r = \sum_{i \mathop = 1}^n A_{ii}
      | c = {{Defof|Trace of Matrix}}
}}
{{eqn | r = \sum_{i \mathop = 1}^n c_{ii}
      | c = From above
}}
{{end-eqn}}
Now it remains to show that $c_{ii} = \innerprod {\map f {e_i} } {e_i}$:
{{begin-eqn}}
{{eqn | l = \innerprod {\map f {e_i} } {e_i}
      | r = \innerprod {\sum_{j \mathop = 1}^n c_{ij} e_j} {e_i}
      | c = From above assumption
}}
{{eqn | r = \sum_{j \mathop = 1}^n c_{ij} \innerprod {e_j} {e_i}
      | c = Axiom $(2)$ of Inner Product: Bilinearity
}}
{{eqn | r = c_{ii} (1)
      | c = {{Defof|Orthonormal Subset}}: other terms vanish
}}
{{eqn | r = c_{ii}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Galois Connection with Upper Adjoint Surjective implies Scond Ordered Set and Image of Lower Adjoint are Isomorphic

Let $L = \left({S, \preceq}\right), R = \left({T, \precsim}\right)$ be ordered sets.
Ley $g:S \to T, d:T \to S$ be mappings such that
:$\left({g, d}\right)$ is Galois connection
and
:$g$ is a surjection/
Let $N = \left({d\left[{T}\right], \preceq'}\right)$ be an ordered subset of $L$.
Then $R$ and $N$ are order isomorphic.

Proof:
By Galois Connection implies Upper Adjoint is Surjection iff Lower Adjoint is Injection:
:$d$ is an injection.
Define $d' = d:T \to g\left[{T}\right]$
By definition:
:$d'$ is an injection.
By definition of Galois connection:
:$d$ is an increasing mapping.
We will prove that
:$d$ is order embedding.
Let $x, y \in T$.
By definition of increasing mapping:
:$x \precsim y \implies d\left({x}\right) \preceq d\left({y}\right)$
Thus by definition of $d'$ and ordered subset:
:$x \precsim y \implies d'\left({x}\right) \preceq' d'\left({y}\right)$
Assume that
:$d'\left({x}\right) \preceq' d'\left({y}\right)$
By Upper Adjoint of Galois Connection is Surjection implies Lower Adjoint at Element is Minimum of Preimage of Singleton of Element
:$\forall t \in T: d\left({t}\right) = \min\left({g^{-1}\left[{\left\{ {t}\right\} }\right]}\right)$
By Lower Adjoint at Element is Minimum of Preimage of Singleton of Element implies Composition is Identity:
:$g \circ d = I_T$
By definition of Galois connection:
:$g$ is an increasing mapping.
Thus by definition of $d'$ and ordered subset:
:$d\left({x}\right) \preceq d\left({y}\right)$
By definition of increasing mapping:
:$g\left({d\left({x}\right)}\right) \precsim g\left({d\left({y}\right)}\right)$
Thus by definitions of composition of mappings and identity mapping:
:$x \precsim y$
{{qed|lemma}}
By definition:
:$d'$ is a surjection.
Hence $d'$ is order isomorphism between $R$ and $N$.
{{qed}}