RootSystem.coroot_eq_coreflection_of_root_eq
theorem RootSystem.coroot_eq_coreflection_of_root_eq :
∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Finite ι] (P : RootSystem ι R M N)
[inst_6 : CharZero R] [inst_7 : NoZeroSMulDivisors R M] {i j k : ι},
P.root k = (P.reflection i) (P.root j) → P.coroot k = (P.coreflection i) (P.coroot j)
In the context of root systems for commutative rings with characteristic zero and non-zero scalar multiplication divisors, the theorem states that given any types `ι`, `R`, `M`, `N`, and assuming that `P` is a root system, if the `k`th root is the `i`th reflection of the `j`th root, then the `k`th coroot would be the `i`th coreflection of the `j`th coroot. This means, the reflection relation between roots extends to the corresponding coroots.
More concisely: In the context of root systems for commutative rings with characteristic zero and non-zero scalar multiplication divisors, the reflection relation between roots translates to the corresponding coreflections for the coroots.
|
RootPairing.ext
theorem RootPairing.ext :
∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Finite ι] [inst_6 : CharZero R]
[inst_7 : NoZeroSMulDivisors R M] {P₁ P₂ : RootPairing ι R M N},
P₁.toLin = P₂.toLin → P₁.root = P₂.root → Set.range ⇑P₁.coroot = Set.range ⇑P₂.coroot → P₁ = P₂
The theorem `RootPairing.ext` states that in a context where the ring `R` is a commutative ring with characteristic zero and does not allow nonzero scalar multiplication to result in zero (`NoZeroSMulDivisors R M`), given two root pairings `P₁` and `P₂` between the types `ι`, `R`, `M`, and `N` (with `M` and `N` being `R`-modules and `ι` is finite), if their linear transformations, roots, and the ranges of their coroot mappings are all equal, then the two root pairings are equal. Here `P₁.toLin = P₂.toLin` states that the linear transformations of `P₁` and `P₂` are equal, `P₁.root = P₂.root` states that the roots of `P₁` and `P₂` are equal, and `Set.range ⇑P₁.coroot = Set.range ⇑P₂.coroot` states that the ranges of the coroot mappings of `P₁` and `P₂` are equal. The hypothesis `hc` is implied by the condition on the ranges of the coroot mappings.
More concisely: If `R` is a commutative ring with characteristic zero and does not allow nonzero scalar multiplication to result in zero, and given two root pairings `P₁` and `P₂` between finite types `ι`, `R`, `M`, and `N` (where `M` and `N` are `R`-modules), with equal linear transformations, roots, and ranges of coroot mappings, then `P₁` and `P₂` are equal.
|
RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top'
theorem RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top' :
∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Finite ι] [inst_6 : CharZero R]
[inst_7 : NoZeroSMulDivisors R M] (p : PerfectPairing R M N) (root : ι ↪ M) (coroot : ι ↪ N),
(∀ (i : ι), (p.toLin (root i)) (coroot i) = 2) →
(∀ (i : ι),
Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root)
(Set.range ⇑root)) →
Submodule.span R (Set.range ⇑root) = ⊤ →
∀ {i j k : ι},
root k = (Module.preReflection (root i) (p.toLin.flip (coroot i))) (root j) →
coroot k = (Module.preReflection (coroot i) (p.toLin (root i))) (coroot j)
This theorem, `RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top'`, asserts that given a perfect pairing `p` on two modules `M` and `N` over a commutative ring `R`, along with injective maps `root` and `coroot` from a finite index set `ι` to `M` and `N` respectively, the following conditions must hold:
1. The linear map of the perfect pairing applied to each pair of `root i` and `coroot i` equals 2.
2. The pre-reflection of each `root i` under `p.toLin.flip (coroot i)` maps the range of `root` into itself.
3. The submodule spanned by the range of `root` equals the entire module `M`.
Under these circumstances, for any indices `i`, `j`, and `k`, if the `root` at `k` equals the application of the pre-reflection of `root i` under `p.toLin.flip (coroot i)` to `root j`, then the `coroot` at `k` must equal the application of the pre-reflection of `coroot i` under `p.toLin (root i)` to `coroot j`. This theorem is primarily used to support the definition of a root system and is typically not used directly.
More concisely: Given a perfect pairing `p` on modules `M` and `N` over a commutative ring `R` with injective maps `root` and `coroot` from a finite index set `ι` to `M` and `N` respectively, if for all `i`, `j`, and `k`, `root i ⋅ coroot k = root j ⋅ coroot k` implies `coroot i ⋅ root k = coroot j ⋅ root i`, then the range of `root` spans `M` and the pre-reflection of `root i` under `p.toLin.flip (coroot i)` maps the range of `root` into itself.
|
RootSystem.ext
theorem RootSystem.ext :
∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Finite ι] [inst_6 : CharZero R]
[inst_7 : NoZeroSMulDivisors R M] {P₁ P₂ : RootSystem ι R M N},
P₁.toLin = P₂.toLin → P₁.root = P₂.root → P₁ = P₂
This theorem states that for any two root systems P₁ and P₂ in a characteristic zero environment where there is no torsion, and where these systems are defined over a commutative ring R with additive commutative groups M and N as modules, if the systems have the same finite set of roots and the same linear transformation, then the two root systems are indeed the same. This theorem essentially asserts that in this specific context, a finite root system is completely determined by its roots and the associated linear transformation.
More concisely: In a characteristic zero environment with no torsion, two root systems with the same finite set of roots and identical linear transformations are equal.
|
RootPairing.coroot_root_two
theorem RootPairing.coroot_root_two :
∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
(P.toLin.flip (P.coroot i)) (P.root i) = 2
This theorem states that for any RootPairing `P` over types `ι`, `R`, `M`, and `N`, with `R` being a commutative ring, `M` and `N` being additive commutative groups and also `R`-modules, if you take the coroot associated with some index `i` from `P`, flip the linear map of `P`, and apply this map to the root associated with the same index `i`, you will always get 2.
More concisely: For any RootPairing P over commutative rings R, additive commutative groups and R-modules M and N, the coroot at index i flipped and applied to the root at index i equals 2.
|
RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top
theorem RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top :
∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
[inst_5 : Finite ι] [inst_6 : CharZero R] [inst_7 : NoZeroSMulDivisors R M],
Submodule.span R (Set.range ⇑P.root) = ⊤ →
∀ {i j k : ι}, P.root k = (P.reflection i) (P.root j) → P.coroot k = (P.coreflection i) (P.coroot j)
This theorem is about root pairings in the setting of characteristic zero ring 'R' and additive commutative groups 'M' and 'N' which are modules over 'R'. It states that if there are no zero scalars that can divide elements in 'M' and the range of the root function spans the entire module 'M' (i.e., every element of 'M' can be expressed as a linear combination of the roots), then for any three elements 'i', 'j', and 'k' from a finite index set 'ι', if the 'k'th root equals the 'i'th reflection of the 'j'th root, then the 'k'th coroot equals the 'i'th coreflection of the 'j'th coroot. In simpler terms, if certain relationship holds for roots under the conditions of characteristic zero and no torsion, then the same relationship holds for the corresponding coroots.
More concisely: If in a characteristic zero ring 'R' with no torsion modules 'M' and 'N', every element of 'M' is a linear combination of roots, and the 'k'th root of an element equals the 'i'th reflection of the 'j'th root, then the 'k'th coroot of the 'j'th coroot equals the 'i'th coreflection.
|