Toolkit for AL2

In the setting of Linear Algebra: Standing Notation: for classes $F$, $D$, $A$ and $B$, $F|_{D}$ is the restriction of $F$ to $D$, $A\times B$ the Cartesian product and $F^{-1}$ the inverse of $F$. Iterated operations over an interval, the empty one included, are as in Sums and Products over a Finite Set and over an Interval (iv) and Sums and Products over a Finite Set and over an Interval (ii). In the last clause, a condition on set variables $x_{0}$ and $x_{1}$ is expressed by a predicative formula as in Conditions Expressed by a Predicative Formula, and Guards (ii), with $x_{0},x_{1}$ in place of the variables $x_{1},\dots,x_{k}$ of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables.

(i) Negatives in a commutative ring. Let $r$, with $+$, $\cdot$, $0$ and $1$, be a commutative ring, and let $x\in r$. Then $x+(-x)=0$, where $-x$ is the negative of $x$.

(ii) Tuples in a smaller set. Let $X$ and $Y$ be sets with $X\subseteq Y$, and let $n\in\mathbb{N}_{0}$. Then $X^{n}\subseteq Y^{n}$.

(iii) Restricted operations on classes. Let $a$ and $b$ be classes with $b\subseteq a$, and let $\ast:a\times a\to a$ be a map with $u\ast v\in b$ for all $u,v\in b$, where $u\ast v$ denotes $\ast((u,v))$. Then $\ast|_{b\times b}$ is a map $b\times b\to b$, and

$$(\ast|_{b\times b})((u,v))=u\ast v\qquad(u,v\in b).$$

(iv) Restricting a map on a product. Let $A$, $B$ and $C$ be classes with $C\subseteq B$, and let $F:A\times B\to B$ be a map with $F((a,c))\in C$ for all $a\in A$ and $c\in C$. Then $F|_{A\times C}:A\times C\to C$ is a map, and

$$(F|_{A\times C})((a,c))=F((a,c))\qquad(a\in A,\ c\in C).$$

(v) Iterated operations in a sub-carrier. Let $X$ be a set, let $\ast$ be an associative and commutative binary operation on $X$ with neutral element $e$, let $Y\subseteq X$ be a set, and let $\diamond$ be an associative and commutative binary operation on $Y$ with neutral element $e$ such that $x\diamond y=x\ast y$ for all $x,y\in Y$. Let $A$ be a finite set and $f:A\to Y$ a map. Then

$$\mathop{\diamond}\limits_{x\in A}f(x)=\mathop{\ast}\limits_{x\in A}f(x).$$

(vi) Iterated operations over $\{1,\dots,m\}$ in a sub-carrier. Let $X$, $\ast$, $e$, $Y$ and $\diamond$ be as in (v), let $m\in\mathbb{N}_{0}$ and let $x\in Y^{m}$. Then

$$\mathop{\diamond}\limits_{k=1}^{m}x_{k}=\mathop{\ast}\limits_{k=1}^{m}x_{k}.$$

(vii) Terms of a linear combination in a smaller space. Let $K$ be a field, and let $V'$ and $V$ be vector spaces over $K$ with $V'\subseteq V$ such that the scalar multiple $\lambda v$ formed in $V'$ equals the one formed in $V$ for all $\lambda\in K$ and $v\in V'$. Let $n\in\mathbb{N}_{0}$, $\lambda\in K^{n}$ and $v\in V'^{n}$. Then the $n$-tuple $(\lambda_{1}v_{1},\dots,\lambda_{n}v_{n})$ of the terms of the linear combination of $v$ with coefficients $\lambda$ is the same whether it is formed in $V'$ or in $V$.

(viii) Addition of linear maps as a binary operation. Let $K$ be a field and let $V$ and $W$ be vector spaces over $K$. There is a binary operation $A$ on $\mathcal{L}(V,W)$ with

$$A((S,T))=S+T\qquad(S,T\in\mathcal{L}(V,W)).$$

(ix) Scalar multiplication of linear maps as a map. Let $K$ be a field and let $V$ and $W$ be vector spaces over $K$. There is a map $M:K\times\mathcal{L}(V,W)\to\mathcal{L}(V,W)$ with

$$M((\lambda,T))=\lambda T\qquad(\lambda\in K,\ T\in\mathcal{L}(V,W)).$$

(x) Composition of linear operators as a binary operation. Let $K$ be a field and let $V$ be a vector space over $K$. There is a binary operation $C$ on $\mathcal{L}(V)$ with

$$C((S,T))=ST\qquad(S,T\in\mathcal{L}(V)).$$

(xi) Values of the inverse of a bijection. Let $A$ and $B$ be classes and let $F:A\to B$ be a bijection. Then $F^{-1}:B\to A$ is a map,

$$F(F^{-1}(w))=w\quad(w\in B)\qquad\text{and}\qquad F^{-1}(F(v))=v\quad(v\in A).$$

(xii) Mutual inclusion. Let $X$ and $Y$ be classes with $X\subseteq Y$ and $Y\subseteq X$, where $\subseteq$ is the subclass relation. Then $X=Y$.

(xiii) Values of a bijection. Let $A$ and $B$ be classes, let $G:A\to B$ be a bijection and let $u\in A$. Then $G(u)\in B$.

(xiv) Removing one element. Let $A$ and $i$ be classes and let $j$ be a set. Then $i\in A\setminus\{j\}$ if and only if $i\in A$ and $i\neq j$.

(xv) Tuples combined termwise. Let $X$ be a set, let $\ast$ be a binary operation on $X$, let $n\in\mathbb{N}_{0}$ and let $f,g\in X^{n}$. Then there is $s\in X^{n}$ with $s_{k}=f_{k}\ast g_{k}$ for every $k\in[n]$.

(xvi) Constant tuples. Let $X$ be a set, let $c\in X$ and let $n\in\mathbb{N}_{0}$. Then there is $s\in X^{n}$ with $s_{k}=c$ for every $k\in[n]$.

(xvii) Tuples with one distinguished component. Let $X$ be a set, let $a,b\in X$, let $n\in\mathbb{N}_{0}$ and let $j\in[n]$. Then there is $s\in X^{n}$ with $s_{j}=a$ and $s_{k}=b$ for every $k\in[n]$ with $k\neq j$.

(xviii) Equality of tuples. Let $X$ be a set, let $n\in\mathbb{N}_{0}$ and let $s,t\in X^{n}$ with $s_{k}=t_{k}$ for every $k\in[n]$. Then $s=t$.

(xix) Nonempty segments. Let $n\in\mathbb{N}_{0}$ and let $j\in[n]$. Then $n=m+1$ for some $m\in\mathbb{N}_{0}$.

(xx) The class of lengths of independent extensions. Let $K$ be a field, let $V$ be a vector space over $K$, let $m\in\mathbb{N}_{0}$ and let $u\in V^{m}$. Then there is a class $A$ such that, for every class $p$, $p\in A$ if and only if $p\in\mathbb{N}_{0}$ and there are $w\in V^{p}$ and $c\in V^{m+p}$ with

$$c_{i}=u_{i}\quad(i\in[m]),\qquad c_{m+j}=w_{j}\quad(j\in[p]),$$

and $c$ linearly independent.

(xxi) The class of lengths of independent families in a class. Let $K$ be a field, let $V$ be a vector space over $K$, and let $W$ be a subclass of $V$. Then there is a class $A$ such that, for every class $q$, $q\in A$ if and only if $q\in\mathbb{N}_{0}$ and there is $c\in W^{q}$ that is linearly independent.

(xxii) A common source is predicative. Let $A$, $F$ and $G$ be class variables, parameters whose fixed values are classes, also denoted $A$, $F$ and $G$. Then the condition on $x_{0}$ and $x_{1}$

$$\text{there is a set } l\in A \text{ with } (l,x_{0})\in F \text{ and } (l,x_{1})\in G,$$

with $(l,x_{0})$ and $(l,x_{1})$ ordered pairs, is expressed by a predicative formula.