Reflections in linear algebra #
Given an element x in a module M together with a linear form f on M such that f x = 2, the
map y ↦ y - (f y) • x is an involutive endomorphism of M, such that:
- the kernel of
fis fixed, - the point
x ↦ -x.
Such endomorphisms are often called reflections of the module M. When M carries an inner product
for which x is perpendicular to the kernel of f, then (with mild assumptions) the endomorphism
is characterised by properties 1 and 2 above, and is a linear isometry.
Main definitions / results: #
Module.preReflection: the definition of the mapy ↦ y - (f y) • x. Its main utility lies in the fact that it does not require the assumptionf x = 2, giving the user freedom to defer discharging this proof obligation.Module.reflection: the definition of the mapy ↦ y - (f y) • x. This requires the assumption thatf x = 2but by way of compensation it produces a linear equivalence rather than a mere linear map.Module.reflection_mul_reflection_pow_apply: a formula for $(r_1 r_2)^m z$, where $r_1$ and $r_2$ are reflections and $z \in M$. It involves the Chebyshev polynomials and holds over any commutative ring. This is used to define reflection representations of Coxeter groups.Module.Dual.eq_of_preReflection_mapsTo: a uniqueness result about reflections preserving finite spanning sets that is useful in the theory of root data / systems.
TODO #
Related definitions of reflection exists elsewhere in the library. These more specialised
definitions, which require an ambient InnerProductSpace structure, are reflection (of type
LinearIsometryEquiv) and EuclideanGeometry.reflection (of type AffineIsometryEquiv). We
should connect (or unify) these definitions with Module.reflecton defined here.
Given an element x in a module M and a linear form f on M, we define the endomorphism
of M for which y ↦ y - (f y) • x.
One is typically interested in this endomorphism when f x = 2; this definition exists to allow the
user defer discharging this proof obligation. See also Module.reflection.
Equations
- Module.preReflection x f = LinearMap.id - LinearMap.smulRight f x
Instances For
Given an element x in a module M and a linear form f on M for which f x = 2, we define
the endomorphism of M for which y ↦ y - (f y) • x.
It is an involutive endomorphism of M fixing the kernel of f for which x ↦ -x.
Equations
- Module.reflection h = { toLinearMap := Module.preReflection x f, invFun := (Function.Involutive.toPerm ⇑(Module.preReflection x f) ⋯).invFun, left_inv := ⋯, right_inv := ⋯ }
Instances For
Powers of the product of two reflections #
Let $M$ be a module over a commutative ring $R$. Let $x, y \in M$ and $f, g \in M^*$ with
$f(x) = g(y) = 2$. The corresponding reflections $r_1, r_2 \colon M \to M$ (Module.reflection) are
given by $r_1z = z - f(z) x$ and $r_2 z = z - g(z) y$. These are linear automorphisms of $M$.
To define reflection representations of a Coxeter group, it is important to be able to compute the order of the composition $r_1 r_2$.
Note that if $M$ is a real inner product space and $r_1$ and $r_2$ are both orthogonal reflections (i.e. $f(z) = 2 \langle x, z \rangle / \langle x, x \rangle$ and $g(z) = 2 \langle y, z\rangle / \langle y, y\rangle$ for all $z \in M$), then $r_1 r_2$ is a rotation by the angle $$\cos^{-1}\left(\frac{f(y) g(x) - 2}{2}\right)$$ and one may determine the order of $r_1 r_2$ accordingly.
However, if $M$ does not have an inner product, and even if $R$ is not $\mathbb{R}$, then we may
instead use the formulas in this section. These formulas all involve evaluating Chebyshev
$S$-polynomials (Polynomial.Chebyshev.S) at $t = f(y) g(x) - 2$, and they hold over any
commutative ring.
A formula for $(r_1 r_2)^m z$, where $m$ is a natural number and $z \in M$.
A formula for $(r_1 r_2)^m$, where $m$ is a natural number.
A formula for $(r_1 r_2)^m z$, where $m$ is an integer and $z \in M$.
A formula for $(r_1 r_2)^m$, where $m$ is an integer.
A formula for $(r_1 r_2)^m x$, where $m$ is an integer. This is the special case of
Module.reflection_mul_reflection_zpow_apply with $z = x$.
A formula for $(r_1 r_2)^m x$, where $m$ is a natural number. This is the special case of
Module.reflection_mul_reflection_pow_apply with $z = x$.
A formula for $r_2 (r_1 r_2)^m x$, where $m$ is an integer.
A formula for $r_2 (r_1 r_2)^m x$, where $m$ is a natural number.
Lemmas used to prove uniqueness results for root data #
See also Module.Dual.eq_of_preReflection_mapsTo' for a variant of this lemma which
applies when Φ does not span.
This rather technical-looking lemma exists because it is exactly what is needed to establish various uniqueness results for root data / systems. One might regard this lemma as lying at the boundary of linear algebra and combinatorics since the finiteness assumption is the key.
This rather technical-looking lemma exists because it is exactly what is needed to establish a
uniqueness result for root data. See the doc string of Module.Dual.eq_of_preReflection_mapsTo for
further remarks.
Composite of reflections in "parallel" hyperplanes is a shear (special case).