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.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 : Module.Dual R M) : Module.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 : Module.Dual R M) (y : M) : (Module.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 : Module.Dual R M} (h : f x = 2) : (Module.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 : Module.Dual R M} (h : f x = 2) : Function.Involutive ⇑(Module.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 : Module.Dual R M} (y : M) (g : Module.Dual R M) (h : f x = 2) : Module.preReflection ((Module.preReflection x f) y) ((Module.preReflection f ((Module.Dual.eval R M) x)) g) = Module.preReflection x f ∘ₗ Module.preReflection y g ∘ₗ Module.preReflection x f

def Module.reflection {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) : 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 : Module.Dual R M} (y : M) (h : f x = 2) : (Module.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 : Module.Dual R M} (h : f x = 2) : (Module.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 : Module.Dual R M} (h : f x = 2) : Function.Involutive ⇑(Module.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 : Module.Dual R M} (h : f x = 2) : (Module.reflection h).symm = Module.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 : Module.Dual R M} {Φ : Set M} (h : f x = 2) : Set.InvOn (⇑(Module.reflection h)) (⇑(Module.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 : Module.Dual R M} {Φ : Set M} (h : f x = 2) (h' : Set.MapsTo (⇑(Module.reflection h)) Φ Φ) : Set.BijOn (⇑(Module.reflection h)) Φ Φ

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} (hx : x ≠ 0) {Φ : Set M} (hΦ₁ : Φ.Finite) (hΦ₂ : Submodule.span R Φ = ⊤) {f g : Module.Dual R M} (hf₁ : f x = 2) (hf₂ : Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ) (hg₁ : g x = 2) (hg₂ : Set.MapsTo (⇑(Module.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} (hx : x ≠ 0) {Φ : Set M} (hΦ₁ : Φ.Finite) (hx' : x ∈ Submodule.span R Φ) {f g : Module.Dual R M} (hf₁ : f x = 2) (hf₂ : Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ) (hg₁ : g x = 2) (hg₂ : Set.MapsTo (⇑(Module.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 : Module.Dual R M} {y : M} {g : Module.Dual R M} (hfx : f x = 2) (hgy : g y = 2) (hgxfy : f y * g x = 4) (n : ℕ) : (⇑(Module.reflection hgy ≪≫ₗ Module.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 : Module.Dual R M} {y : M} {g : Module.Dual R M} [NoZeroSMulDivisors ℤ M] (hfx : f x = 2) (hgy : g y = 2) (hgxfy : f y * g x = 4) : (Set.range fun (n : ℕ) => (⇑(Module.reflection hgy ≪≫ₗ Module.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 : Module.Dual R M} {y : M} {g : Module.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 (⇑(Module.preReflection x f)) Φ Φ) (hygΦ : Set.MapsTo (⇑(Module.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 : ι → Module.Dual R M} (hfin : (Set.range ⇑r).Finite) (h_two : ∀ (i : ι), (c i) (r i) = 2) (h_mapsTo : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (r i) (c i))) (Set.range ⇑r) (Set.range ⇑r)) : Set.InjOn (⇑(Submodule.span R (Set.range ⇑r)).subtype.dualMap) (Set.range c)