transvections, reflections, symmetries

Stream: mathlib4

[Antoine Chambert-Loir]

In classical mathematics,

• transvections are linear maps of the form $x\mapsto x+f(x) v$ where $f$ is a linear form and $v$ a vector such that $f(v)= 0$.
• symmetries are linear maps which are identity on a subspace and minus identity on a complement
• reflections are (non identical) symmetries that preserve a hyperplane. They can be defined by $x\mapsto x-f(x)v$ where $f$ is a linear form and $v$ is a vector such that $f(v)=2$.

In mathlib, the maps $x\mapsto x+f(x)v$ are known as docs#LinearMap.transvection (once #31164 is merged), while those of the form $x\mapsto x-f(x)v$ are known as docs#Module.preReflection.
On the other hand, docs#Submodule.reflection are orthogonal symmetries (essentially, in an complete inner product space).

[Antoine Chambert-Loir]

It seems that some unification and terminological clarification would be useful, if not necessary.

• What should their namespace be? LinearMap or Module, resp. Submodule?

• I suggest that docs#Submodule.reflection be renamed orthSymmetry.

• Regarding transvections/preReflections, the issues are the minus sign in the definition of docs#Module.preReflection (so that the type of scalars needs to be a ring), and having f v = -2 as a condition would not be so nice. So maybe both could coexist.

[Oliver Nash]

I like the naming of #31164. If we followed that, and the suggestion above about Submodule.reflection, we would have:

• LinearMap.transvection, LinearEquiv.transvection
• LinearMap.reflection, LinearEquiv.reflection
• Submodule.orthSymmetry

[Eric Wieser]

(double $$ for Zulip LaTeX)

[Joseph Myers]

Note that Submodule.reflection is in a pair with the affine version EuclideanGeometry.reflection (which arguably ought to be in the AffineSubspace namespace to support dot notation, but we ought to get #27378 and its dependency over the line before doing further refactors in that area).