Bases for root pairings / systems

This file contains a theory of bases for root pairings / systems.

Implementation details

For reduced root pairings RootSystem.Base is equivalent to the usual definition appearing in the informal literature (e.g., it follows from [Ser87](Ch. V, §8, Proposition 7) that RootSystem.Base is equivalent to both [Ser87](Ch. V, §8, Definition 5) and [Bou02](Ch. VI, §1.5) for reduced pairings). However for non-reduced root pairings, it is more restrictive because it includes axioms on coroots as well as on roots. For example by RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem it is clear that the 1-dimensional root system {-2, -1, 0, 1, 2} ⊆ ℝ has no base in the sense of RootSystem.Base.

It is also worth remembering that it is only for reduced root systems that one has the simply transitive action of the Weyl group on the set of bases, and that the Weyl group of a non-reduced root system is the same as that of the reduced root system obtained by passing to the indivisible roots.

For infinite root systems, RootSystem.Base is usually not the right notion: linear independence is too strong.

Main definitions / results:

• RootSystem.Base: a base of a root pairing.
• RootSystem.Base.IsPos: the predicate that a (co)root is positive relative to a base.
• RootSystem.Base.induction_add: an induction principle for predicates on (co)roots which respect addition of a simple root.
• RootSystem.Base.induction_reflect: an induction principle for predicates on (co)roots which respect reflection in a simple root.

TODO

• Develop a theory of base / separation / positive roots for infinite systems which specialises to the concept here for finite systems.

structure RootPairing.Base {ι : 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) : Type u_1

A base of a root pairing.

For reduced root pairings this definition is equivalent to the usual definition appearing in the informal literature but not for non-reduced root pairings it is more restrictive. See the module doc string for further remarks.

See also RootPairing.Base.mk'.

• support : Finset ι

  The indices of the simple roots / coroots.

• linearIndepOn_root : LinearIndepOn R ⇑P.root ↑self.support
• linearIndepOn_coroot : LinearIndepOn R ⇑P.coroot ↑self.support
• root_mem_or_neg_mem (i : ι) : P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑self.support) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑self.support)
• coroot_mem_or_neg_mem (i : ι) : P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑self.support) ∨ -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑self.support)

theorem RootPairing.Base.support_nonempty {ι : 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} (b : P.Base) [Nonempty ι] [NeZero 2] : b.support.Nonempty

def RootPairing.Base.flip {ι : 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} (b : P.Base) : P.flip.Base

Interchanging roots and coroots, one still has a base of a root pairing.

Equations

• b.flip = { support := b.support, linearIndepOn_root := ⋯, linearIndepOn_coroot := ⋯, root_mem_or_neg_mem := ⋯, coroot_mem_or_neg_mem := ⋯ }

@[simp]

theorem RootPairing.Base.flip_support {ι : 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} (b : P.Base) : b.flip.support = b.support

noncomputable def RootPairing.Base.map {ι : 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} (b : P.Base) {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P₂ : RootPairing ι₂ R M₂ N₂} (e : P.Equiv P₂) : P₂.Base

The push forward of a base along an equivalence.

Equations

• b.map e = { support := Finset.image (⇑(↑e).indexEquiv) b.support, linearIndepOn_root := ⋯, linearIndepOn_coroot := ⋯, root_mem_or_neg_mem := ⋯, coroot_mem_or_neg_mem := ⋯ }

@[simp]

theorem RootPairing.Base.support_map_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} (b : P.Base) {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P₂ : RootPairing ι₂ R M₂ N₂} (e : P.Equiv P₂) [DecidableEq ι₂] : (b.map e).support = Finset.image (⇑(↑e).indexEquiv) b.support

noncomputable def RootPairing.Base.supportMapEquiv {ι : 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} (b : P.Base) {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P₂ : RootPairing ι₂ R M₂ N₂} (e : P.Equiv P₂) [DecidableEq ι₂] : ↥b.support ≃ ↥(b.map e).support

The natural bijection between support of a base and that of its push forward.

Equations

• b.supportMapEquiv e = ((↑e).indexEquiv.imageFinset b.support).trans (Equiv.finsetCongr ⋯)

@[simp]

theorem RootPairing.Base.supportMapEquiv_apply_coe {ι : 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} (b : P.Base) {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P₂ : RootPairing ι₂ R M₂ N₂} (e : P.Equiv P₂) [DecidableEq ι₂] (a✝ : ↥b.support) : ↑((b.supportMapEquiv e) a✝) = (↑e).indexEquiv ↑a✝

@[simp]

theorem RootPairing.Base.supportMapEquiv_symm_apply_coe {ι : 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} (b : P.Base) {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P₂ : RootPairing ι₂ R M₂ N₂} (e : P.Equiv P₂) [DecidableEq ι₂] (a✝ : ↥(b.map e).support) : ↑((b.supportMapEquiv e).symm a✝) = (↑e).indexEquiv.symm ↑a✝

theorem RootPairing.Base.root_ne_neg_of_ne {ι : 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} (b : P.Base) [Nontrivial R] {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) (hij : i ≠ j) : P.root i ≠ -P.root j

theorem RootPairing.Base.linearIndependent_pair_of_ne {ι : 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} (b : P.Base) {i j : ↥b.support} (hij : i ≠ j) : LinearIndependent R ![P.root ↑i, P.root ↑j]

theorem RootPairing.Base.root_mem_span_int {ι : 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} (b : P.Base) (i : ι) : P.root i ∈ Submodule.span ℤ (⇑P.root '' ↑b.support)

theorem RootPairing.Base.coroot_mem_span_int {ι : 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} (b : P.Base) (i : ι) : P.coroot i ∈ Submodule.span ℤ (⇑P.coroot '' ↑b.support)

@[simp]

theorem RootPairing.Base.span_int_root_support {ι : 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} (b : P.Base) : Submodule.span ℤ (⇑P.root '' ↑b.support) = Submodule.span ℤ (Set.range ⇑P.root)

@[simp]

theorem RootPairing.Base.span_int_coroot_support {ι : 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} (b : P.Base) : Submodule.span ℤ (⇑P.coroot '' ↑b.support) = Submodule.span ℤ (Set.range ⇑P.coroot)

@[simp]

theorem RootPairing.Base.span_root_support {ι : 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} (b : P.Base) : Submodule.span R (⇑P.root '' ↑b.support) = P.rootSpan R

@[simp]

theorem RootPairing.Base.span_coroot_support {ι : 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} (b : P.Base) : Submodule.span R (⇑P.coroot '' ↑b.support) = P.corootSpan R

theorem RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux {ι : 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} (b : P.Base) [Finite ι] [IsAddTorsionFree M] [IsAddTorsionFree N] (i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ Set.range ⇑P.root) : ∃ (z : ℤ), ↑z * t = 1

theorem RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem {ι : 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} (b : P.Base) [CharZero R] [Finite ι] [IsAddTorsionFree M] [IsAddTorsionFree N] (i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ Set.range ⇑P.root) : t = 1 ∨ t = -1

theorem RootPairing.Base.pos_or_neg_of_sum_smul_root_mem {ι : 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} (b : P.Base) [CharZero R] (f : ι → ℤ) (hf : ∑ j ∈ b.support, f j • P.root j ∈ Set.range ⇑P.root) (hf₀ : Function.support f ⊆ ↑b.support) : 0 < f ∨ f < 0

theorem RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_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} (b : P.Base) [CharZero R] (f : ι → ℤ) (hf : ∑ j ∈ b.support, f j • P.root j ∈ Set.range ⇑P.root) (hf₀ : Function.support f ⊆ ↑b.support) : ¬f ≤ 0 ↔ 0 < f

theorem RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_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} (b : P.Base) [CharZero R] (f : ι → ℤ) (hf : ∑ j ∈ b.support, f j • P.root j ∈ Set.range ⇑P.root) (hf₀ : Function.support f ⊆ ↑b.support) : ¬0 ≤ f ↔ f < 0

theorem RootPairing.Base.sub_notMem_range_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} (b : P.Base) [CharZero R] {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) : P.root i - P.root j ∉ Set.range ⇑P.root

theorem RootPairing.Base.sub_notMem_range_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} (b : P.Base) [CharZero R] {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) : P.coroot i - P.coroot j ∉ Set.range ⇑P.coroot

theorem RootPairing.Base.pairingIn_le_zero_of_ne {ι : 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} (b : P.Base) [CharZero R] [IsDomain R] [P.IsCrystallographic] [Finite ι] {i j : ι} (hij : i ≠ j) (hi : i ∈ b.support) (hj : j ∈ b.support) : P.pairingIn ℤ i j ≤ 0

@[simp]

theorem RootPairing.Base.chainBotCoeff_eq_zero {ι : 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} {b : P.Base} [CharZero R] [IsDomain R] [P.IsCrystallographic] [Finite ι] {i j : ↥b.support} : chainBotCoeff ↑i ↑j = 0

theorem RootPairing.Base.chainTopCoeff_eq_of_ne {ι : 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} {b : P.Base} [CharZero R] [IsDomain R] [P.IsCrystallographic] [Finite ι] {i j : ↥b.support} (hij : i ≠ j) : ↑(chainTopCoeff ↑i ↑j) = -P.pairingIn ℤ ↑j ↑i

noncomputable def RootPairing.Base.toWeightBasis {ι : 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} (b : P.Base) [P.IsRootSystem] : Module.Basis (↥b.support) R M

A base of a root system yields a basis of the root space.

Equations

• b.toWeightBasis = Module.Basis.mk ⋯ ⋯

@[simp]

theorem RootPairing.Base.toWeightBasis_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} (b : P.Base) [P.IsRootSystem] (i : ↥b.support) : b.toWeightBasis i = P.root ↑i

@[simp]

theorem RootPairing.Base.toWeightBasis_repr_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} (b : P.Base) [P.IsRootSystem] (i : ↥b.support) : b.toWeightBasis.repr (P.root ↑i) = Finsupp.single i 1

noncomputable def RootPairing.Base.toCoweightBasis {ι : 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} (b : P.Base) [P.IsRootSystem] : Module.Basis (↥b.support) R N

A base of a root system yields a basis of the coroot space.

Equations

• b.toCoweightBasis = b.flip.toWeightBasis

@[simp]

theorem RootPairing.Base.toCoweightBasis_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} (b : P.Base) [P.IsRootSystem] (i : ↥b.support) : b.toCoweightBasis i = P.coroot ↑i

@[simp]

theorem RootPairing.Base.toCoweightBasis_repr_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} (b : P.Base) [P.IsRootSystem] (i : ↥b.support) : b.toCoweightBasis.repr (P.coroot ↑i) = Finsupp.single i 1

@[simp]

theorem RootPairing.Base.spanIntRootSupport {ι : 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} (b : P.Base) : Submodule.span ℤ (P.rootSpanMem ℤ '' ↑b.support) = ⊤

theorem RootPairing.Base.linearIndependentInt {ι : 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} (b : P.Base) [CharZero R] : LinearIndependent ℤ fun (i : ↥b.support) => P.rootSpanMem ℤ ↑i

noncomputable def RootPairing.Base.toWeightBasisInt {ι : 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} (b : P.Base) [CharZero R] : Module.Basis ↥b.support ℤ ↥(P.rootSpan ℤ)

A base for a root system gives a ℤ-basis for the ℤ-span of the roots.

Equations

• b.toWeightBasisInt = Module.Basis.mk ⋯ ⋯

@[simp]

theorem RootPairing.Base.coe_toWeightBasisInt_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} (b : P.Base) [CharZero R] (i : ↥b.support) : ↑(b.toWeightBasisInt i) = P.root ↑i

theorem RootPairing.Base.exists_root_eq_sum_nat_or_neg {ι : 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} (b : P.Base) (i : ι) : ∃ (f : ι → ℕ), Function.support f ⊆ ↑b.support ∧ (P.root i = ∑ j ∈ b.support, f j • P.root j ∨ P.root i = -∑ j ∈ b.support, f j • P.root j)

theorem RootPairing.Base.exists_root_eq_sum_int {ι : 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} (b : P.Base) [CharZero R] (i : ι) : ∃ (f : ι → ℤ), Function.support f ⊆ ↑b.support ∧ (0 < f ∨ f < 0) ∧ P.root i = ∑ j ∈ b.support, f j • P.root j

noncomputable def RootPairing.Base.height {ι : 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} (b : P.Base) [CharZero R] (i : ι) : ℤ

Given a base α₁, α₂, …, the height of a root ∑ zᵢαᵢ relative to this base is ∑ zᵢ.

Equations

• b.height i = ∑ j ∈ b.support, ⋯.choose j

theorem RootPairing.Base.height_eq_sum {ι : 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} {b : P.Base} [CharZero R] {i : ι} {f : ι → ℤ} (heq : P.root i = ∑ j ∈ b.support, f j • P.root j) : b.height i = ∑ j ∈ b.support, f j

theorem RootPairing.Base.height_ne_zero {ι : 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} (b : P.Base) [CharZero R] (i : ι) : b.height i ≠ 0

theorem RootPairing.Base.height_reflectionPerm_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} (b : P.Base) [CharZero R] (i : ι) : b.height (-i) = -b.height i

theorem RootPairing.Base.height_one_of_mem_support {ι : 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} {b : P.Base} [CharZero R] {i : ι} (hi : i ∈ b.support) : b.height i = 1

theorem RootPairing.Base.height_add {ι : 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} (b : P.Base) [CharZero R] {i j k : ι} (hk : P.root k = P.root i + P.root j) : b.height k = b.height i + b.height j

theorem RootPairing.Base.height_sub {ι : 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} (b : P.Base) [CharZero R] {i j k : ι} (hk : P.root k = P.root i - P.root j) : b.height k = b.height i - b.height j

theorem RootPairing.Base.height_add_zsmul {ι : 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} (b : P.Base) [CharZero R] {i j k : ι} {z : ℤ} (hk : P.root k = P.root i + z • P.root j) : b.height k = b.height i + z • b.height j

def RootPairing.Base.IsPos {ι : 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} (b : P.Base) [CharZero R] (i : ι) : Prop

The predicate that a (co)root is positive with respect to a base.

Equations

• b.IsPos i = (0 < b.height i)

theorem RootPairing.Base.isPos_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} (b : P.Base) [CharZero R] {i : ι} : b.IsPos i ↔ 0 < b.height i

theorem RootPairing.Base.isPos_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} (b : P.Base) [CharZero R] {i : ι} : b.IsPos i ↔ 0 ≤ b.height i

theorem RootPairing.Base.IsPos.or_neg {ι : 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} (b : P.Base) [CharZero R] (i : ι) : b.IsPos i ∨ b.IsPos (-i)

theorem RootPairing.Base.IsPos.neg_iff_not {ι : 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} (b : P.Base) [CharZero R] (i : ι) : b.IsPos (-i) ↔ ¬b.IsPos i

theorem RootPairing.Base.isPos_of_mem_support {ι : 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} {b : P.Base} [CharZero R] {i : ι} (h : i ∈ b.support) : b.IsPos i

theorem RootPairing.Base.IsPos.add {ι : 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} {b : P.Base} [CharZero R] {i j k : ι} (hi : b.IsPos i) (hj : b.IsPos j) (hk : P.root k = P.root i + P.root j) : b.IsPos k

theorem RootPairing.Base.IsPos.sub {ι : 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} {b : P.Base} [CharZero R] {i j k : ι} (hi : b.IsPos i) (hj : j ∈ b.support) (hk : P.root k = P.root i - P.root j) : b.IsPos k

theorem RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn {ι : 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} {b : P.Base} [CharZero R] [P.IsCrystallographic] {i : ι} (h₀ : b.IsPos i) : ∃ j ∈ b.support, 0 < P.pairingIn ℤ j i

theorem RootPairing.Base.exists_mem_support_pos_pairingIn_ne_zero {ι : 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} {b : P.Base} [CharZero R] [P.IsCrystallographic] (i : ι) : ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

theorem RootPairing.Base.IsPos.add_zsmul {ι : 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} {b : P.Base} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i j k : ι} {z : ℤ} (hij : i ≠ j) (hi : b.IsPos i) (hj : j ∈ b.support) (hk : P.root k = P.root i + z • P.root j) : b.IsPos k

theorem RootPairing.Base.IsPos.reflectionPerm {ι : 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} {b : P.Base} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i j : ι} (hi : b.IsPos i) (hj : j ∈ b.support) (hij : i ≠ j) : b.IsPos ((P.reflectionPerm j) i)

theorem RootPairing.Base.IsPos.induction_on_add {ι : 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} {b : P.Base} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] {i : ι} (h₀ : b.IsPos i) {p : ι → Prop} (h₁ : ∀ i ∈ b.support, p i) (h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k) : p i

theorem RootPairing.Base.exists_eq_sum_and_forall_sum_mem_of_isPos {ι : 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} {b : P.Base} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] {i : ι} (hi : b.IsPos i) : ∃ (n : ℕ) (f : Fin n → ι), Set.range f ⊆ ↑b.support ∧ P.root i = ∑ m : Fin n, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ Set.range ⇑P.root

This lemma is included mostly for comparison with the informal literature. Usually RootPairing.Base.IsPos.induction_on_add will be more useful.

theorem RootPairing.Base.induction_add {ι : 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} {b : P.Base} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] (i : ι) {p : ι → Prop} (h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)) (h₁ : ∀ i ∈ b.support, p i) (h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k) : p i

theorem RootPairing.Base.IsPos.induction_on_reflect {ι : 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} {b : P.Base} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (h₀ : b.IsPos i) {p : ι → Prop} (h₁ : ∀ i ∈ b.support, p i) (h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)) : p i

theorem RootPairing.Base.induction_reflect {ι : 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} {b : P.Base} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (i : ι) {p : ι → Prop} (h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)) (h₁ : ∀ i ∈ b.support, p i) (h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)) : p i

theorem RootPairing.Base.forall_mem_support_invtSubmodule_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} {b : P.Base} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (q : Submodule R M) : (∀ i ∈ b.support, q ∈ Module.End.invtSubmodule ↑(P.reflection i)) ↔ ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)