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:

1. the kernel of f is fixed,
2. 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 map y ↦ y - (f y) • x. Its main utility lies in the fact that it does not require the assumption f x = 2, giving the user freedom to defer discharging this proof obligation.
• Module.reflection: the definition of the map y ↦ y - (f y) • x. This requires the assumption that f x = 2 but 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.

def Module.preReflection {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (x : M) (f : Dual R M) : End R M

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

theorem Module.preReflection_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (x : M) (f : Dual R M) (y : M) : (preReflection x f) y = y - f y • x

theorem Module.preReflection_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (h : f x = 2) : (preReflection x f) x = -x

theorem Module.involutive_preReflection {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (h : f x = 2) : Function.Involutive ⇑(preReflection x f)

theorem Module.preReflection_preReflection {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (y : M) (g : Dual R M) (h : f x = 2) : preReflection ((preReflection x f) y) ((preReflection f ((Dual.eval R M) x)) g) = preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f

def Module.reflection {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (h : f x = 2) : M ≃ₗ[R] M

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 := ⋯ }

theorem Module.reflection_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (y : M) (h : f x = 2) : (reflection h) y = y - f y • x

@[simp]

theorem Module.reflection_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (h : f x = 2) : (reflection h) x = -x

theorem Module.involutive_reflection {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (h : f x = 2) : Function.Involutive ⇑(reflection h)

@[simp]

theorem Module.reflection_inv {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (h : f x = 2) : (reflection h)⁻¹ = reflection h

@[simp]

theorem Module.reflection_symm {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} (h : f x = 2) : (reflection h).symm = reflection h

theorem Module.invOn_reflection_of_mapsTo {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} {Φ : Set M} (h : f x = 2) : Set.InvOn (⇑(reflection h)) (⇑(reflection h)) Φ Φ

theorem Module.bijOn_reflection_of_mapsTo {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} {Φ : Set M} (h : f x = 2) (h' : Set.MapsTo (⇑(reflection h)) Φ Φ) : Set.BijOn (⇑(reflection h)) Φ Φ

theorem Submodule.mem_invtSubmodule_reflection_of_mem {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Module.Dual R M} (h : f x = 2) (p : Submodule R M) (hx : x ∈ p) : p ∈ Module.End.invtSubmodule ↑(Module.reflection h)

theorem Submodule.mem_invtSubmodule_reflection_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Module.Dual R M} [NeZero 2] [NoZeroSMulDivisors R M] (h : f x = 2) {p : Submodule R M} (hp : Disjoint p (span R {x})) : p ∈ Module.End.invtSubmodule ↑(Module.reflection h) ↔ p ≤ LinearMap.ker f

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^{\ast }$ with $f(x)=g(y)=2$. The corresponding reflections $r_1,r_2:M\to M$ (Module.reflection) are given by $r_{1}z=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⟨x,z⟩/⟨x,x⟩$ and $g(z)=2⟨y,z⟩/⟨y,y⟩$ 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.

theorem Module.reflection_mul_reflection_pow_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x y : M} {f g : Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℕ) (z : M) (t : R := f y * g x - 2) (ht : t = f y * g x - 2 := by rfl) : ((reflection hf * reflection hg) ^ m) z = z + (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)) * (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) + Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 3) / 2)))) • ((g x * f z - g z) • y - f z • x) + (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) * (Polynomial.eval t (Polynomial.Chebyshev.S R (↑m / 2)) + Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)))) • ((f y * g z - f z) • x - g z • y)

A formula for $(r_1{r}_2{)}^{m}z$, where $m$ is a natural number and $z\in M$.

theorem Module.reflection_mul_reflection_pow {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x y : M} {f g : Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℕ) (t : R := f y * g x - 2) (ht : t = f y * g x - 2 := by rfl) : ↑((reflection hf * reflection hg) ^ m) = LinearMap.id + (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)) * (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) + Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 3) / 2)))) • (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) + (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) * (Polynomial.eval t (Polynomial.Chebyshev.S R (↑m / 2)) + Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)))) • (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y)

A formula for $(r_1{r}_2{)}^m$, where $m$ is a natural number.

theorem Module.reflection_mul_reflection_zpow_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x y : M} {f g : Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℤ) (z : M) (t : R := f y * g x - 2) (ht : t = f y * g x - 2 := by rfl) : ((reflection hf * reflection hg) ^ m) z = z + (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 2) / 2)) * (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 1) / 2)) + Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 3) / 2)))) • ((g x * f z - g z) • y - f z • x) + (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 1) / 2)) * (Polynomial.eval t (Polynomial.Chebyshev.S R (m / 2)) + Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 2) / 2)))) • ((f y * g z - f z) • x - g z • y)

A formula for $(r_1{r}_2{)}^{m}z$, where $m$ is an integer and $z\in M$.

theorem Module.reflection_mul_reflection_zpow {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x y : M} {f g : Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℤ) (t : R := f y * g x - 2) (ht : t = f y * g x - 2 := by rfl) : ↑((reflection hf * reflection hg) ^ m) = LinearMap.id + (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 2) / 2)) * (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 1) / 2)) + Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 3) / 2)))) • (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) + (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 1) / 2)) * (Polynomial.eval t (Polynomial.Chebyshev.S R (m / 2)) + Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 2) / 2)))) • (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y)

A formula for $(r_1{r}_2{)}^m$, where $m$ is an integer.

theorem Module.reflection_mul_reflection_zpow_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x y : M} {f g : Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℤ) (t : R := f y * g x - 2) (ht : t = f y * g x - 2 := by rfl) : ((reflection hf * reflection hg) ^ m) x = (Polynomial.eval t (Polynomial.Chebyshev.S R m) + Polynomial.eval t (Polynomial.Chebyshev.S R (m - 1))) • x + (Polynomial.eval t (Polynomial.Chebyshev.S R (m - 1)) * -g x) • y

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$.

theorem Module.reflection_mul_reflection_pow_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x y : M} {f g : Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℕ) (t : R := f y * g x - 2) (ht : t = f y * g x - 2 := by rfl) : ((reflection hf * reflection hg) ^ m) x = (Polynomial.eval t (Polynomial.Chebyshev.S R ↑m) + Polynomial.eval t (Polynomial.Chebyshev.S R (↑m - 1))) • x + (Polynomial.eval t (Polynomial.Chebyshev.S R (↑m - 1)) * -g x) • y

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$.

theorem Module.reflection_mul_reflection_mul_reflection_zpow_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x y : M} {f g : Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℤ) (t : R := f y * g x - 2) (ht : t = f y * g x - 2 := by rfl) : (reflection hg * (reflection hf * reflection hg) ^ m) x = (Polynomial.eval t (Polynomial.Chebyshev.S R m) + Polynomial.eval t (Polynomial.Chebyshev.S R (m - 1))) • x + (Polynomial.eval t (Polynomial.Chebyshev.S R m) * -g x) • y

A formula for $r_2(r_1{r}_2{)}^{m}x$, where $m$ is an integer.

theorem Module.reflection_mul_reflection_mul_reflection_pow_apply_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x y : M} {f g : Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℕ) (t : R := f y * g x - 2) (ht : t = f y * g x - 2 := by rfl) : (reflection hg * (reflection hf * reflection hg) ^ m) x = (Polynomial.eval t (Polynomial.Chebyshev.S R ↑m) + Polynomial.eval t (Polynomial.Chebyshev.S R (↑m - 1))) • x + (Polynomial.eval t (Polynomial.Chebyshev.S R ↑m) * -g x) • y

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

theorem Module.Dual.eq_of_preReflection_mapsTo {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [CharZero R] [NoZeroSMulDivisors R M] {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite) (hΦ₂ : Submodule.span R Φ = ⊤) {f g : Dual R M} (hf₁ : f x = 2) (hf₂ : Set.MapsTo (⇑(preReflection x f)) Φ Φ) (hg₁ : g x = 2) (hg₂ : Set.MapsTo (⇑(preReflection x g)) Φ Φ) : f = g

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.

theorem Module.Dual.eq_of_preReflection_mapsTo' {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [CharZero R] [NoZeroSMulDivisors R M] {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite) (hx : x ∈ Submodule.span R Φ) {f g : Dual R M} (hf₁ : f x = 2) (hf₂ : Set.MapsTo (⇑(preReflection x f)) Φ Φ) (hg₁ : g x = 2) (hg₂ : Set.MapsTo (⇑(preReflection x g)) Φ Φ) : (Submodule.span R Φ).subtype.dualMap f = (Submodule.span R Φ).subtype.dualMap g

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.

theorem Module.reflection_reflection_iterate {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} {y : M} {g : Dual R M} (hfx : f x = 2) (hgy : g y = 2) (hgxfy : f y * g x = 4) (n : ℕ) : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)

Composite of reflections in "parallel" hyperplanes is a shear (special case).

theorem Module.infinite_range_reflection_reflection_iterate_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} {y : M} {g : Dual R M} [NoZeroSMulDivisors ℤ M] (hfx : f x = 2) (hgy : g y = 2) (hgxfy : f y * g x = 4) : (Set.range fun (n : ℕ) => (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y).Infinite ↔ f y • x ≠ 2 • y

theorem Module.eq_of_mapsTo_reflection_of_mem {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : M} {f : Dual R M} {y : M} {g : Dual R M} [NoZeroSMulDivisors ℤ M] {Φ : Set M} (hΦ : Φ.Finite) (hfx : f x = 2) (hgy : g y = 2) (hgx : g x = 2) (hfy : f y = 2) (hxfΦ : Set.MapsTo (⇑(preReflection x f)) Φ Φ) (hygΦ : Set.MapsTo (⇑(preReflection y g)) Φ Φ) (hyΦ : y ∈ Φ) : x = y

theorem Module.injOn_dualMap_subtype_span_range_range {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [NoZeroSMulDivisors ℤ M] {r : ι ↪ M} {c : ι → Dual R M} (hfin : (Set.range ⇑r).Finite) (h_two : ∀ (i : ι), (c i) (r i) = 2) (h_mapsTo : ∀ (i : ι), Set.MapsTo (⇑(preReflection (r i) (c i))) (Set.range ⇑r) (Set.range ⇑r)) : Set.InjOn (⇑(Submodule.span R (Set.range ⇑r)).subtype.dualMap) (Set.range c)