Positive and negative roots

This file packages Mathlib's positivity predicate for a root-pairing base as the sets of positive and negative root indices. It records their partition, their exchange under root negation, and the fact that a simple reflection permutes the positive roots other than its own simple root.

A base b of a root pairing P is simultaneously a base b.flip of the flipped pairing P.flip, so the same positivity predicate measures both a root against the simple roots and the corresponding coroot against the simple coroots. The last part of the file proves that the two measurements agree, so that a base and its flip have the same positive roots and the coroot of a positive root is a nonnegative integer combination of the simple coroots.

Main definitions

• Ado.posRoots is the set of positive roots relative to a base.
• Ado.negRoots is its complementary set of negative roots.
• Ado.posRootsFinset and Ado.negRootsFinset are the same two sets as finsets, for a finite root index type, so that they can be summed over.
• Ado.posRootCone is the additive monoid Q⁺ of nonnegative integer combinations of the simple roots.

Main results

• Ado.image_reflectionPerm_self_posRoots says root negation exchanges the two sets.
• Ado.ncard_posRoots_eq_natCard_div_two says that, for a finite root index type, exactly half of the roots are positive, and Ado.posRootsFinset_eq_filter, Ado.card_posRootsFinset read Ado.posRootsFinset as the filter of the positivity predicate and its cardinality as the cardinality of Ado.posRoots.
• Ado.add_mem_posRoots and Ado.add_mem_negRoots say each of the two sets is closed under those sums of its members that are again roots, and Ado.reflectionPerm_self_notMem_posRoots, Ado.reflectionPerm_self_notMem_negRoots say neither contains a root together with its negative.
• Ado.bijOn_reflectionPerm_posRoots_diff_singleton says a simple reflection permutes the positive roots other than its own simple root, and Ado.sum_posRootsFinset_erase_comp_reflectionPerm is the resulting reindexing rule for sums over those roots.
• Ado.mem_support_iff_isPos_and_forall_ne_add says the simple roots are exactly the indecomposable positive roots: those that are not the sum of two positive roots.
• RootPairing.Base.isPos_flip_iff says a root is positive for a base exactly when its coroot is positive for that base, and Ado.posRoots_flip restates it for the sets.
• Ado.mem_posRoots_iff_root_mem_posRootCone says the positive roots are exactly the roots lying in Q⁺, Ado.isPointed_posRootCone says Q⁺ is pointed, Ado.eq_zero_of_add_eq_zero_of_mem_posRootCone is the same fact as a cancellation rule, Ado.root_add_ne_zero_of_mem_posRoots_of_mem_posRootCone specializes that to a positive root added to a member of Q⁺, and Ado.sum_root_ne_zero_of_mem_posRoots deduces that a nonempty sum of positive roots is nonzero.
• Ado.eq_of_nsmul_root_sub_root_mem_posRootCone says that the only positive root lying below a natural multiple of a simple root, in the order defined by Q⁺, is that simple root itself.
• Ado.one_le_height_of_mem_posRoots says every positive root has height at least one, and Ado.height_neg_of_mem_negRoots says every negative root has negative height.
• Ado.heightLinearMap_sum_nsmul_root computes the height of a nonnegative integer combination of the simple roots, whence Ado.exists_natCast_eq_heightLinearMap_of_mem_posRootCone, that the height functional takes natural-number values on Q⁺, and Ado.eq_zero_of_mem_posRootCone_of_heightLinearMap_eq_zero, that zero is the only member of Q⁺ of height zero.
• Ado.exists_intCast_eq_coroot'_of_mem_posRootCone says a coroot functional takes integer values on Q⁺.
• Ado.exists_coroot_eq_sum_nat_of_mem_posRoots says the coroot of a positive root is a nonnegative integer combination of the simple coroots, and Ado.exists_coroot'_eq_sum_nat_of_mem_posRoots restates that on the coroot functionals.

Implementation notes

The indecomposability characterisation is stated with root vectors rather than with an index-level sum, matching Mathlib's RootPairing.Base.height_add and RootPairing.Base.IsPos.add, whose hypothesis is an equation between root vectors: an index-level statement would need a chosen index for the sum, which need not be unique for a non-reduced pairing.

References

This file implements the “Positive and negative roots” item in Layer 1 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, following the target signatures in TauCetiRoadmap/RepresentationTheory/RootSystems/Suggested.lean. The coroot-side positivity at the end of the file is the prerequisite that the fundamental-domain item of Layer 4 consumes; that argument is the one in J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §10. The decomposition half of Ado.mem_support_iff_isPos_and_forall_ne_add is the step that Mathlib currently performs only inside the proof of RootPairing.Base.IsPos.induction_on_add, isolated here as a statement of its own.

theorem Ado.reflectionPerm_self_involutive {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : Function.Involutive fun (i : ι) => (P.reflectionPerm i) i

Root negation is an involution of the root index type: it is the InvolutiveNeg supplied by RootPairing.indexNeg, written through the self-reflection permutation.

def Ado.posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : Set ι

The positive roots relative to a base.

Equations

• Ado.posRoots P b = {i : ι | b.IsPos i}

def Ado.negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : Set ι

The negative roots relative to a base.

Equations

• Ado.negRoots P b = {i : ι | ¬b.IsPos i}

@[simp]

theorem Ado.mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (i : ι) : i ∈ posRoots P b ↔ b.IsPos i

Membership in the set of positive roots.

theorem Ado.one_le_height_of_mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i : ι} (hi : i ∈ posRoots P b) : 1 ≤ b.height i

A positive root has height at least one.

@[simp]

theorem Ado.mem_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (i : ι) : i ∈ negRoots P b ↔ ¬b.IsPos i

Membership in the set of negative roots.

theorem Ado.height_neg_of_mem_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i : ι} (hi : i ∈ negRoots P b) : b.height i < 0

A negative root has negative height.

theorem Ado.compl_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : (posRoots P b)ᶜ = negRoots P b

The negative roots are the complement of the positive roots.

theorem Ado.negRoots_eq_compl {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : negRoots P b = (posRoots P b)ᶜ

The negative roots are the complement of the positive roots.

theorem Ado.disjoint_posRoots_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : Disjoint (posRoots P b) (negRoots P b)

No root is both positive and negative.

theorem Ado.posRoots_union_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : posRoots P b ∪ negRoots P b = Set.univ

Every root is either positive or negative.

theorem Ado.mem_posRoots_or_mem_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (i : ι) : i ∈ posRoots P b ∨ i ∈ negRoots P b

Every root is either positive or negative.

theorem Ado.not_mem_posRoots_iff_mem_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (i : ι) : i ∉ posRoots P b ↔ i ∈ negRoots P b

A root is negative exactly when it is not positive.

theorem Ado.posRoots_finite {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : (posRoots P b).Finite

The positive roots form a finite set when the root index type is finite.

theorem Ado.negRoots_finite {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : (negRoots P b).Finite

The negative roots form a finite set when the root index type is finite.

noncomputable def Ado.posRootsFinset {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : Finset ι

The positive roots of a base, as a finset, so that they can be summed over.

Equations

• Ado.posRootsFinset P b = ⋯.toFinset

noncomputable def Ado.negRootsFinset {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : Finset ι

The negative roots of a base, as a finset, so that they can be summed over.

Equations

• Ado.negRootsFinset P b = ⋯.toFinset

@[simp]

theorem Ado.mem_posRootsFinset {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] (i : ι) : i ∈ posRootsFinset P b ↔ i ∈ posRoots P b

@[simp]

theorem Ado.mem_negRootsFinset {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] (i : ι) : i ∈ negRootsFinset P b ↔ i ∈ negRoots P b

theorem Ado.posRootsFinset_eq_filter {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Fintype ι] [DecidablePred b.IsPos] : posRootsFinset P b = {i : ι | b.IsPos i}

The finset of positive roots is the filter of the positivity predicate, which is the shape a consumer that counts positive roots by Finset.filter meets them in.

theorem Ado.card_posRootsFinset {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : (posRootsFinset P b).card = (posRoots P b).ncard

Counting the positive roots as a finset agrees with counting them as a set.

theorem Ado.support_subset_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : ↑b.support ⊆ posRoots P b

Every simple root is positive.

theorem Ado.posRoots_nonempty {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Nonempty ι] : (posRoots P b).Nonempty

A nonempty root index type has a positive root.

theorem Ado.reflectionPerm_self_mem_negRoots_iff_mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (i : ι) : (P.reflectionPerm i) i ∈ negRoots P b ↔ i ∈ posRoots P b

The negative of a positive root is negative.

@[simp]

theorem Ado.isPos_reflectionPerm_self_iff_mem_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (i : ι) : b.IsPos ((P.reflectionPerm i) i) ↔ i ∈ negRoots P b

The self-reflection of a root is positive exactly when the root is negative.

theorem Ado.reflectionPerm_self_mem_posRoots_iff_mem_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (i : ι) : (P.reflectionPerm i) i ∈ posRoots P b ↔ i ∈ negRoots P b

The negative of a negative root is positive.

theorem Ado.reflectionPerm_self_notMem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i : ι} (hi : i ∈ posRoots P b) : (P.reflectionPerm i) i ∉ posRoots P b

Neither set contains a root together with its negative.

theorem Ado.reflectionPerm_self_notMem_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i : ι} (hi : i ∈ negRoots P b) : (P.reflectionPerm i) i ∉ negRoots P b

Neither set contains a root together with its negative.

theorem Ado.add_mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i j k : ι} (hi : i ∈ posRoots P b) (hj : j ∈ posRoots P b) (hk : P.root k = P.root i + P.root j) : k ∈ posRoots P b

The positive roots are closed under addition: a root that is the sum of two positive roots is positive, because heights add.

theorem Ado.add_mem_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i j k : ι} (hi : i ∈ negRoots P b) (hj : j ∈ negRoots P b) (hk : P.root k = P.root i + P.root j) : k ∈ negRoots P b

The negative roots are closed under addition: a root that is the sum of two negative roots is negative.

theorem Ado.exists_root_eq_sum_nat_of_mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i : ι} (hi : i ∈ posRoots P b) : ∃ (f : ι → ℕ), Function.support f ⊆ ↑b.support ∧ P.root i = ∑ j ∈ b.support, f j • P.root j

A positive root is a nonnegative natural-number combination of simple roots.

The cone of nonnegative combinations of the simple roots

def Ado.posRootCone {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (b : P.Base) : AddSubmonoid M

The positive root cone Q⁺ of a base: the additive submonoid generated by the simple roots, that is the set of nonnegative integer combinations of them.

Equations

• Ado.posRootCone P b = AddSubmonoid.closure (⇑P.root '' ↑b.support)

theorem Ado.mem_posRootCone {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (b : P.Base) {v : M} : v ∈ posRootCone P b ↔ ∃ (f : ι → ℕ), v = ∑ j ∈ b.support, f j • P.root j

Membership in the positive root cone, spelled out as a nonnegative integer combination of the simple roots.

theorem Ado.root_mem_posRootCone_of_mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i : ι} (hi : i ∈ posRoots P b) : P.root i ∈ posRootCone P b

Every positive root lies in the positive root cone.

theorem Ado.mem_posRoots_iff_root_mem_posRootCone {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i : ι} : i ∈ posRoots P b ↔ P.root i ∈ posRootCone P b

A root is positive exactly when it lies in the positive root cone.

theorem Ado.heightLinearMap_sum_nsmul_root {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (b : P.Base) [P.IsRootSystem] (f : ι → ℕ) : (heightLinearMap P b) (∑ j ∈ b.support, f j • P.root j) = ↑(∑ j ∈ b.support, f j)

The height of a nonnegative integer combination of the simple roots is the total number of simple roots occurring in it, every simple root having height one.

theorem Ado.exists_natCast_eq_heightLinearMap_of_mem_posRootCone {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (b : P.Base) [P.IsRootSystem] {u : M} (hu : u ∈ posRootCone P b) : ∃ (n : ℕ), (heightLinearMap P b) u = ↑n

The height functional takes natural-number values on the positive root cone: the height of a nonnegative integer combination of simple roots is the total number of simple roots in it, every simple root having height one. This is what makes the height of a cone member a legitimate induction parameter.

theorem Ado.eq_zero_of_mem_posRootCone_of_heightLinearMap_eq_zero {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [P.IsRootSystem] {u : M} (hu : u ∈ posRootCone P b) (hheight : (heightLinearMap P b) u = 0) : u = 0

The only member of the positive root cone of height zero is zero. The height counts the simple roots occurring in a member, so a member of height zero has no summand at all.

theorem Ado.exists_intCast_eq_coroot'_of_mem_posRootCone {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (b : P.Base) [P.IsCrystallographic] {u : M} (hu : u ∈ posRootCone P b) (i : ι) : ∃ (m : ℤ), (P.coroot' i) u = ↑m

A coroot functional takes integer values on the positive root cone: a nonnegative integer combination of the simple roots pairs with a coroot to the matching combination of Cartan integers.

theorem Ado.isPointed_posRootCone {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : (posRootCone P b).IsPointed

The positive root cone is pointed: the only member whose negative is again a member is zero. Expanding a member and its negative in the simple roots, the total coefficient vector is nonnegative and sums to zero and, the simple roots being linearly independent, must vanish, so each coefficient vector does.

This is what makes the cone an order on weights: μ ≤ λ defined by λ - μ ∈ Q⁺ is antisymmetric, and a weight cannot be reached from itself through a nonempty chain of positive roots.

theorem Ado.eq_zero_of_add_eq_zero_of_mem_posRootCone {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {u v : M} (hu : u ∈ posRootCone P b) (hv : v ∈ posRootCone P b) (huv : u + v = 0) : u = 0

A member of the positive root cone that is cancelled by another member is zero: pointedness of the cone, in the additive form the weight order uses.

theorem Ado.root_add_ne_zero_of_mem_posRoots_of_mem_posRootCone {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i : ι} (hi : i ∈ posRoots P b) {v : M} (hv : v ∈ posRootCone P b) : P.root i + v ≠ 0

A positive root is never cancelled inside the positive root cone. A positive root is a nonzero member of the cone, so Ado.eq_zero_of_add_eq_zero_of_mem_posRootCone forbids it.

theorem Ado.sum_root_ne_zero_of_mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {κ : Type u_1} {s : Finset κ} (hs : s.Nonempty) {f : κ → ι} (hf : ∀ x ∈ s, f x ∈ posRoots P b) : ∑ x ∈ s, P.root (f x) ≠ 0

A nonempty sum of positive roots is nonzero. Splitting off one summand, the rest is a nonnegative integer combination of the simple roots, and a positive root is never cancelled inside that cone.

This is the integral form of the statement that the positive roots lie in an open half space. It is what rules out a cycle of weights each obtained from the previous one by adding a positive root, and so is the reason a maximal weight exists.

theorem Ado.eq_of_nsmul_root_sub_root_mem_posRootCone {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsAddTorsionFree M] [IsAddTorsionFree N] {i : ι} (hi : i ∈ b.support) {j : ι} (hj : j ∈ posRoots P b) {n : ℕ} (h : n • P.root i - P.root j ∈ posRootCone P b) : j = i

A simple root dominates only itself. If a natural multiple of a simple root αᵢ exceeds a positive root αⱼ inside the cone Q⁺, then αⱼ is αᵢ.

Expanding both αⱼ and the difference in the simple roots and comparing coefficients, which is legitimate because the simple roots are linearly independent, leaves αⱼ a natural multiple of αᵢ; the multiple is 1 because a base contains no proper multiple of one of its members (RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem).

This is the combinatorial input to the integrability relation of a highest weight module: it is what confines a positive root vector raising the weight lam - (n + 1) αᵢ to the single direction αᵢ.

theorem Ado.image_reflectionPerm_self_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : (fun (i : ι) => (P.reflectionPerm i) i) '' posRoots P b = negRoots P b

Root negation exchanges positive and negative roots.

theorem Ado.image_reflectionPerm_self_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : (fun (i : ι) => (P.reflectionPerm i) i) '' negRoots P b = posRoots P b

Root negation exchanges negative and positive roots.

The number of positive roots

@[simp]

theorem Ado.ncard_negRoots_eq_ncard_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : (negRoots P b).ncard = (posRoots P b).ncard

A root pairing has equally many positive and negative roots. Root negation gives the bijection between the two sets.

theorem Ado.ncard_posRoots_add_ncard_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : (posRoots P b).ncard + (negRoots P b).ncard = Nat.card ι

The numbers of positive and negative roots add up to the total number of roots.

theorem Ado.two_mul_ncard_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : 2 * (posRoots P b).ncard = Nat.card ι

Twice the number of positive roots is the total number of roots.

theorem Ado.ncard_posRoots_eq_natCard_div_two {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] : (posRoots P b).ncard = Nat.card ι / 2

Exactly half of a finite root index type consists of positive roots.

theorem Ado.reflectionPerm_ne_of_mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {i j : ι} (hi : i ∈ b.support) (hj : j ∈ posRoots P b) : (P.reflectionPerm i) j ≠ i

Reflecting a positive root in a simple root never produces that simple root: the only root sent to a simple root αᵢ by sᵢ is -αᵢ, which is negative.

The simple roots are the indecomposable positive roots

theorem Ado.root_ne_add_of_mem_support {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [CharZero R] {b : P.Base} {i : ι} (hi : i ∈ b.support) {j k : ι} (hj : b.IsPos j) (hk : b.IsPos k) : P.root i ≠ P.root j + P.root k

A simple root is not the sum of two positive roots.

theorem Ado.exists_isPos_root_eq_add_of_notMem_support {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [CharZero R] {b : P.Base} [Finite ι] [IsDomain R] [P.IsCrystallographic] {i : ι} (hi : b.IsPos i) (hi' : i ∉ b.support) : ∃ j ∈ b.support, ∃ (k : ι), b.IsPos k ∧ P.root i = P.root k + P.root j

A positive root that is not simple is a positive root plus a simple root.

theorem Ado.mem_support_iff_isPos_and_forall_ne_add {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [CharZero R] {b : P.Base} [Finite ι] [IsDomain R] [P.IsCrystallographic] {i : ι} : i ∈ b.support ↔ b.IsPos i ∧ ∀ (j k : ι), b.IsPos j → b.IsPos k → P.root i ≠ P.root j + P.root k

The simple roots are exactly the indecomposable positive roots. This is the description of the base that mentions only the additive structure of the positive roots, so it is the one that transports along an additive bijection of the positive roots.

theorem Ado.reflectionPerm_mem_posRoots_diff_singleton_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) (j : ι) : (P.reflectionPerm i) j ∈ posRoots P b \ {i} ↔ j ∈ posRoots P b \ {i}

A simple reflection preserves the set of positive roots other than its own simple root. Both directions follow from the forward implication because P.reflectionPerm i is an involution.

theorem Ado.bijOn_reflectionPerm_posRoots_diff_singleton {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) : Set.BijOn (⇑(P.reflectionPerm i)) (posRoots P b \ {i}) (posRoots P b \ {i})

A simple reflection permutes the positive roots other than its own simple root.

theorem Ado.image_reflectionPerm_posRoots_diff_singleton {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) : ⇑(P.reflectionPerm i) '' (posRoots P b \ {i}) = posRoots P b \ {i}

The image form of bijOn_reflectionPerm_posRoots_diff_singleton: a simple reflection maps the positive roots other than its own simple root onto themselves.

theorem Ado.reflectionPerm_mem_posRootsFinset_erase_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [DecidableEq ι] {i : ι} (hi : i ∈ b.support) (j : ι) : (P.reflectionPerm i) j ∈ (posRootsFinset P b).erase i ↔ j ∈ (posRootsFinset P b).erase i

The finset form of reflectionPerm_mem_posRoots_diff_singleton_iff.

theorem Ado.sum_posRootsFinset_erase_comp_reflectionPerm {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [DecidableEq ι] {A : Type u_1} [AddCommMonoid A] {i : ι} (hi : i ∈ b.support) (f : ι → A) : ∑ j ∈ (posRootsFinset P b).erase i, f ((P.reflectionPerm i) j) = ∑ j ∈ (posRootsFinset P b).erase i, f j

Reindexing along a simple reflection leaves a sum over the other positive roots unchanged. Since sᵢ permutes the positive roots other than αᵢ, summing any function over them is insensitive to precomposition with sᵢ.

theorem RootPairing.Base.isPos_reflectionPerm_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i j : ι} (hj : j ∈ b.support) (hij : i ≠ j) (hij' : i ≠ (P.reflectionPerm j) j) : b.IsPos ((P.reflectionPerm j) i) ↔ b.IsPos i

A simple reflection preserves and reflects positivity of every root other than its own simple root and the negative of that simple root.

@[simp]

theorem RootPairing.Base.isPos_flip_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] (i : ι) : b.flip.IsPos i ↔ b.IsPos i

A root is positive for a base exactly when its coroot is positive for that base.

@[simp]

theorem Ado.posRoots_flip {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] : posRoots P.flip b.flip = posRoots P b

A base and its flip have the same positive roots.

@[simp]

theorem Ado.negRoots_flip {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] : negRoots P.flip b.flip = negRoots P b

A base and its flip have the same negative roots.

theorem Ado.exists_coroot_eq_sum_nat_of_mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {i : ι} (hi : i ∈ posRoots P b) : ∃ (f : ι → ℕ), Function.support f ⊆ ↑b.support ∧ P.coroot i = ∑ j ∈ b.support, f j • P.coroot j

The coroot of a positive root is a nonnegative integer combination of the simple coroots.

theorem Ado.exists_coroot'_eq_sum_nat_of_mem_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {i : ι} (hi : i ∈ posRoots P b) : ∃ (f : ι → ℕ), (∃ j ∈ b.support, f j ≠ 0) ∧ P.coroot' i = ∑ j ∈ b.support, ↑(f j) • P.coroot' j

A positive coroot functional is a nonnegative integer combination of the simple coroot functionals, with at least one simple coroot genuinely occurring.