Documentation

Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

The canonical bilinear form on a finite root pairing #

Given a finite root pairing, we define a canonical map from weight space to coweight space, and the corresponding bilinear form. This form is symmetric and Weyl-invariant, and if the base ring is linearly ordered, then the form is root-positive, positive-semidefinite on the weight space, and positive-definite on the span of roots. From these facts, it is easy to show that Coxeter weights in a finite root pairing are bounded above by 4. Thus, the pairings of roots and coroots in a crystallographic root pairing are restricted to a small finite set of possibilities. Another application is to the faithfulness of the Weyl group action on roots, and finiteness of the Weyl group.

Main definitions: #

RootPairing.Polarization: A distinguished linear map from the weight space to the coweight space.
RootPairing.RootForm : The bilinear form on weight space corresponding to Polarization.

Main results: #

RootPairing.rootForm_self_sum_of_squares : The inner product of any weight vector is a sum of squares.
RootPairing.rootForm_reflection_reflection_apply : RootForm is invariant with respect to reflections.
RootPairing.rootForm_self_smul_coroot: The inner product of a root with itself times the corresponding coroot is equal to two times Polarization applied to the root.
RootPairing.exists_ge_zero_eq_rootForm: RootForm is positive semidefinite.

References: #

[N. Bourbaki, Lie groups and Lie algebras. Chapters 4--6][bourbaki1968]
[M. Demazure, SGA III, Exposé XXI, Données Radicielles][demazure1970]

def RootPairing.Polarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

An invariant linear map from weight space to coweight space.

Equations

P.Polarization = ∑ i : ι, LinearMap.toSpanSingleton R N (P.coroot i) ∘ₗ P.coroot' i

Instances For

@[simp]

theorem RootPairing.Polarization_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (x : M) :

P.Polarization x = ∑ i : ι, (P.coroot' i) x • P.coroot i

def RootPairing.CoPolarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

An invariant linear map from coweight space to weight space.

Equations

P.CoPolarization = P.flip.Polarization

Instances For

@[simp]

theorem RootPairing.CoPolarization_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (x : N) :

P.CoPolarization x = ∑ i : ι, (P.root' i) x • P.root i

theorem RootPairing.CoPolarization_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

P.CoPolarization = P.flip.Polarization

def RootPairing.RootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

LinearMap.BilinForm R M

An invariant inner product on the weight space.

Equations

P.RootForm = ∑ i : ι, LinearMap.smulRight (P.coroot' i) (P.coroot' i)

Instances For

def RootPairing.CorootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

LinearMap.BilinForm R N

An invariant inner product on the coweight space.

Equations

P.CorootForm = P.flip.RootForm

Instances For

theorem RootPairing.rootForm_apply_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (x y : M) :

(P.RootForm x) y = ∑ i : ι, (P.coroot' i) x * (P.coroot' i) y

theorem RootPairing.corootForm_apply_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (x y : N) :

(P.CorootForm x) y = ∑ i : ι, (P.root' i) x * (P.root' i) y

theorem RootPairing.toPerfectPairing_apply_apply_Polarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (x y : M) :

(P.toPerfectPairing y) (P.Polarization x) = (P.RootForm x) y

theorem RootPairing.toPerfectPairing_apply_CoPolarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (x : N) :

P.toPerfectPairing (P.CoPolarization x) = P.CorootForm x

theorem RootPairing.flip_comp_polarization_eq_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

P.flip.toLinearMap ∘ₗ P.Polarization = P.RootForm

theorem RootPairing.self_comp_coPolarization_eq_corootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

P.toLinearMap ∘ₗ P.CoPolarization = P.CorootForm

theorem RootPairing.polarization_apply_eq_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (m : M) :

P.Polarization m = 0 ↔ P.RootForm m = 0

theorem RootPairing.coPolarization_apply_eq_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (n : N) :

P.CoPolarization n = 0 ↔ P.CorootForm n = 0

theorem RootPairing.ker_polarization_eq_ker_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

LinearMap.ker P.Polarization = LinearMap.ker P.RootForm

theorem RootPairing.ker_copolarization_eq_ker_corootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

LinearMap.ker P.CoPolarization = LinearMap.ker P.CorootForm

theorem RootPairing.rootForm_symmetric {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

LinearMap.IsSymm P.RootForm

@[simp]

theorem RootPairing.rootForm_reflection_reflection_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (i : ι) (x y : M) :

(P.RootForm ((P.reflection i) x)) ((P.reflection i) y) = (P.RootForm x) y

theorem RootPairing.rootForm_self_sum_of_squares {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (x : M) :

IsSumSq ((P.RootForm x) x)

theorem RootPairing.rootForm_root_self {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (j : ι) :

(P.RootForm (P.root j)) (P.root j) = ∑ i : ι, P.pairing j i * P.pairing j i

theorem RootPairing.range_polarization_domRestrict_le_span_coroot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

LinearMap.range (P.Polarization.domRestrict (P.rootSpan R)) ≤ P.corootSpan R

theorem RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

Submodule.map P.toDualLeft.symm (P.corootSpan R).dualAnnihilator ≤ LinearMap.ker P.RootForm

theorem RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

Submodule.map P.toDualRight.symm (P.rootSpan R).dualAnnihilator ≤ LinearMap.ker P.CorootForm

def RootPairing.PolarizationIn {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [Module S N] [P.IsValuedIn S] [Fintype ι] :

↥(P.rootSpan S) →ₗ[S] N

Polarization restricted to S-span of roots.

Equations

P.PolarizationIn S = ∑ i : ι, LinearMap.toSpanSingleton S N (P.coroot i) ∘ₗ P.coroot'In S i

Instances For

theorem RootPairing.PolarizationIn_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [Module S N] [P.IsValuedIn S] [Fintype ι] (x : ↥(P.rootSpan S)) :

(P.PolarizationIn S) x = ∑ i : ι, (P.coroot'In S i) x • P.coroot i

theorem RootPairing.PolarizationIn_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] [Fintype ι] (x : ↥(P.rootSpan S)) :

(P.PolarizationIn S) x = P.Polarization ↑x

theorem RootPairing.range_polarizationIn {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] :

Submodule.map P.Polarization (P.rootSpan R) = LinearMap.range (P.PolarizationIn R)

def RootPairing.CoPolarizationIn {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] [Fintype ι] :

↥(P.corootSpan S) →ₗ[S] M

Polarization restricted to S-span of roots.

Equations

P.CoPolarizationIn S = P.flip.PolarizationIn S

Instances For

theorem RootPairing.CoPolarizationIn_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] [Fintype ι] (x : ↥(P.corootSpan S)) :

(P.CoPolarizationIn S) x = ∑ i : ι, (P.root'In S i) x • P.root i

theorem RootPairing.CoPolarizationIn_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] [Fintype ι] (x : ↥(P.corootSpan S)) :

(P.CoPolarizationIn S) x = P.CoPolarization ↑x

def RootPairing.RootFormIn {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [Fintype ι] :

LinearMap.BilinForm S ↥(P.rootSpan S)

A canonical bilinear form on the span of roots in a finite root pairing, taking values in a commutative ring, where the root-coroot pairing takes values in that ring.

Equations

P.RootFormIn S = ∑ i : ι, LinearMap.smulRight (P.coroot'In S i) (P.coroot'In S i)

Instances For

@[simp]

theorem RootPairing.algebraMap_rootFormIn {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [Fintype ι] (x y : ↥(P.rootSpan S)) :

(algebraMap S R) (((P.RootFormIn S) x) y) = (P.RootForm ↑x) ↑y

theorem RootPairing.toPerfectPairing_apply_PolarizationIn {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] [Fintype ι] (x y : ↥(P.rootSpan S)) :

(P.toPerfectPairing ↑y) ((P.PolarizationIn S) x) = (algebraMap S R) (((P.RootFormIn S) x) y)

theorem RootPairing.range_polarizationIn_le_span_coroot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [Module S N] [P.IsValuedIn S] [Fintype ι] :

LinearMap.range (P.PolarizationIn S) ≤ P.corootSpan S

theorem RootPairing.rootFormIn_self_smul_coroot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] [Fintype ι] (i : ι) :

((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i = 2 • (P.PolarizationIn S) (P.rootSpanMem S i)

A version of SGA3 XXI Lemma 1.2.1 (10), adapted to change of rings.

theorem RootPairing.prod_rootFormIn_smul_coroot_mem_range_PolarizationIn {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] [Fintype ι] (i : ι) :

(∏ j : ι, ((P.RootFormIn S) (P.rootSpanMem S j)) (P.rootSpanMem S j)) • P.coroot i ∈ LinearMap.range (P.PolarizationIn S)

theorem RootPairing.rootForm_self_smul_coroot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (i : ι) :

(P.RootForm (P.root i)) (P.root i) • P.coroot i = 2 • P.Polarization (P.root i)

A version of SGA3 XXI Lemma 1.2.1 (10).

theorem RootPairing.corootForm_self_smul_root {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (i : ι) :

(P.CorootForm (P.coroot i)) (P.coroot i) • P.root i = 2 • P.CoPolarization (P.coroot i)

theorem RootPairing.four_nsmul_coPolarization_compl_polarization_apply_root {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (i : ι) :

(4 • P.CoPolarization ∘ₗ P.Polarization) (P.root i) = ((P.RootForm (P.root i)) (P.root i) * (P.CorootForm (P.coroot i)) (P.coroot i)) • P.root i

theorem RootPairing.four_smul_rootForm_sq_eq_coxeterWeight_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (i j : ι) :

4 • (P.RootForm (P.root i)) (P.root j) ^ 2 = P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))

theorem RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Fintype ι] (i : ι) :

(∏ a : ι, (P.RootForm (P.root a)) (P.root a)) • P.coroot i ∈ LinearMap.range (P.Polarization.domRestrict (P.rootSpan R))

def RootPairing.posRootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] [Fintype ι] :

RootPositiveForm S P

The bilinear form of a finite root pairing taking values in a linearly-ordered ring, as a root-positive form.

Equations

P.posRootForm S = { form := P.RootForm, symm := ⋯, isOrthogonal_reflection := ⋯, exists_eq := ⋯, exists_pos_eq := ⋯ }

Instances For

theorem RootPairing.algebraMap_posRootForm_posForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [Fintype ι] (x y : ↥(Submodule.span S (Set.range ⇑P.root))) :

(algebraMap S R) (((P.posRootForm S).posForm x) y) = (P.RootForm ↑x) ↑y

@[simp]

theorem RootPairing.posRootForm_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [Fintype ι] :

(P.posRootForm S).posForm = P.RootFormIn S

theorem RootPairing.exists_ge_zero_eq_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [Fintype ι] (x : M) (hx : x ∈ Submodule.span S (Set.range ⇑P.root)) :

∃ s ≥ 0, (algebraMap S R) s = (P.RootForm x) x

theorem RootPairing.posRootForm_posForm_apply_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [Fintype ι] (x y : ↥(P.rootSpan S)) :

((P.posRootForm S).posForm x) y = ∑ i : ι, (P.coroot'In S i) x * (P.coroot'In S i) y

theorem RootPairing.zero_le_posForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] [Fintype ι] (x : ↥(Submodule.span S (Set.range ⇑P.root))) :

0 ≤ ((P.posRootForm S).posForm x) x

theorem RootPairing.zero_lt_pairingIn_iff' {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] {i j : ι} [Finite ι] :

0 < P.pairingIn S i j ↔ 0 < P.pairingIn S j i

theorem RootPairing.pairingIn_lt_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] {i j : ι} [Finite ι] :

P.pairingIn S i j < 0 ↔ P.pairingIn S j i < 0

theorem RootPairing.pairingIn_le_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] {i j : ι} [Finite ι] [NeZero 2] [NoZeroSMulDivisors R M] :

P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0