Module.Dual.eq_of_preReflection_mapsTo
theorem Module.Dual.eq_of_preReflection_mapsTo :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : CharZero R] [inst_4 : NoZeroSMulDivisors R M] {x : M},
x ≠ 0 →
∀ {Φ : Set M},
Φ.Finite →
Submodule.span R Φ = ⊤ →
∀ {f g : Module.Dual R M},
f x = 2 →
Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ →
g x = 2 → Set.MapsTo (⇑(Module.preReflection x g)) Φ Φ → f = g
This theorem, named `Module.Dual.eq_of_preReflection_mapsTo`, establishes uniqueness of a linear form on a module. Given a commutative ring `R`, an additive commutative group `M`, a module `R M` with characteristics zero and no zero scalar multiplication divisors, and a non-zero element `x` of `M`, the theorem states that for any finite set `Φ` that spans the module, if two linear forms `f` and `g` from the dual space of the module satisfy that `f x = g x = 2` and the preReflective map of `x` through `f` and `g` respectively maps `Φ` to itself, then `f` must be equal to `g`. In other words, within these conditions, a linear form is uniquely determined. This theorem is crucial for establishing various uniqueness results for root data/systems and plays a role where linear algebra meets combinatorics.
More concisely: Given a commutative ring with characteristic zero and a finitely generated, torsion-free module, if two linear forms agree on a basis and map it to itself via the pre reflection map, then they are equal.
|
Module.Dual.eq_of_preReflection_mapsTo'
theorem Module.Dual.eq_of_preReflection_mapsTo' :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : CharZero R] [inst_4 : NoZeroSMulDivisors R M] {x : M},
x ≠ 0 →
∀ {Φ : Set M},
Φ.Finite →
x ∈ Submodule.span R Φ →
∀ {f g : Module.Dual R M},
f x = 2 →
Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ →
g x = 2 →
Set.MapsTo (⇑(Module.preReflection x g)) Φ Φ →
(Submodule.span R Φ).subtype.dualMap f = (Submodule.span R Φ).subtype.dualMap g
This theorem, although technical in nature, is crucial for establishing uniqueness results for root data. It states that for any commutative ring `R` with no zero divisors, an additive commutative group `M`, and given that `R` is a module over `M` with characteristic zero, if `x` is an element of `M` which is non-zero, and `Φ` is a finite set of `M` such that `x` is in the span of `Φ`, and if `f` and `g` are elements of the dual module of `R` and `M` such that both `f` and `g` map `x` to 2 and the pre-reflection of `x` under `f` and `g` maps `Φ` to `Φ`, then the dual map of the subtype of the span of `Φ` under `f` and `g` are equal. This theorem is often used in the context of reflection maps in module theory.
More concisely: Given a commutative ring `R` with no zero divisors, an additive commutative group `M` with `R` as its module, and `x` being a non-zero element in `M` of characteristic zero, if `Φ` is a finite subset of `M` containing `x`, and `f` and `g` are elements of the dual module such that `x` maps to 2 under both `f` and `g` and `Φ` is mapped to itself under the pre-reflections of `x` under `f` and `g`, then the subspaces of `M` spanned by `Φ` under `f` and `g` have equal dual maps.
|
Module.preReflection_apply
theorem Module.preReflection_apply :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M)
(f : Module.Dual R M) (y : M), (Module.preReflection x f) y = y - f y • x
This theorem states that for any commutative ring `R`, any additive commutative group `M`, and any `R`-module structure on `M`, and for any element `x` in `M`, any linear map `f` from `M` to `R`, and any element `y` in `M`, the application of the pre-reflection endomorphism (defined by `x` and `f`) to `y` results in `y - f y • x`. In other words, if we imagine executing the pre-reflection transformation on `y`, it would shift `y` by a scalar multiple of `x`, where the scalar is given by the linear map `f` applied to `y`.
More concisely: For any commutative ring `R`, additive commutative group `M`, and `R`-module structure on `M`, and for any `x` in `M`, linear map `f` from `M` to `R`, and element `y` in `M`, the pre-reflection endomorphism of `y` by `x` and `f` equals `y - f(y) * x`.
|