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

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

Main results

• TauCeti.image_reflectionPerm_self_posRoots says root negation exchanges the two sets.
• TauCeti.ncard_posRoots_eq_natCard_div_two says that, for a finite root index type, exactly half of the roots are positive, and TauCeti.posRootsFinset_eq_filter, TauCeti.card_posRootsFinset read TauCeti.posRootsFinset as the filter of the positivity predicate and its cardinality as the cardinality of TauCeti.posRoots.
• TauCeti.add_mem_posRoots and TauCeti.add_mem_negRoots say each of the two sets is closed under those sums of its members that are again roots, and TauCeti.reflectionPerm_self_notMem_posRoots, TauCeti.reflectionPerm_self_notMem_negRoots say neither contains a root together with its negative.
• TauCeti.bijOn_reflectionPerm_posRoots_diff_singleton says a simple reflection permutes the positive roots other than its own simple root, and TauCeti.sum_posRootsFinset_erase_comp_reflectionPerm is the resulting reindexing rule for sums over those roots.
• TauCeti.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 TauCeti.posRoots_flip restates it for the sets.
• TauCeti.mem_posRoots_iff_root_mem_posRootCone says the positive roots are exactly the roots lying in Q⁺, TauCeti.isPointed_posRootCone says Q⁺ is pointed, TauCeti.eq_zero_of_add_eq_zero_of_mem_posRootCone is the same fact as a cancellation rule, TauCeti.root_add_ne_zero_of_mem_posRoots_of_mem_posRootCone specializes that to a positive root added to a member of Q⁺, and TauCeti.sum_root_ne_zero_of_mem_posRoots deduces that a nonempty sum of positive roots is nonzero.
• TauCeti.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.
• TauCeti.one_le_height_of_mem_posRoots says every positive root has height at least one, and TauCeti.height_neg_of_mem_negRoots says every negative root has negative height.
• TauCeti.heightLinearMap_sum_nsmul_root computes the height of a nonnegative integer combination of the simple roots, whence TauCeti.exists_natCast_eq_heightLinearMap_of_mem_posRootCone, that the height functional takes natural-number values on Q⁺, and TauCeti.eq_zero_of_mem_posRootCone_of_heightLinearMap_eq_zero, that zero is the only member of Q⁺ of height zero.
• TauCeti.exists_intCast_eq_coroot'_of_mem_posRootCone says a coroot functional takes integer values on Q⁺.
• TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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

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

def TauCeti.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

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

@[simp]

theorem TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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

• TauCeti.posRootsFinset P b = ⋯.toFinset

noncomputable def TauCeti.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

• TauCeti.negRootsFinset P b = ⋯.toFinset

@[simp]

theorem TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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

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

theorem TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.eq_zero_of_add_eq_zero_of_mem_posRootCone forbids it.

theorem TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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.