Documentation

Mathlib.LinearAlgebra.Reflection

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: #

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) :

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
Instances For
    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) :
    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) :
    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) :
    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) :

    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
    Instances For
      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) :
      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) :
      @[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) :
      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) :
      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)) Φ Φ) :
      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 : Module.Dual R M} {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 : Module.Dual R M} {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)