Supporting lemmas for Geck's construction of a Lie algebra associated to a root system #
theorem
RootPairing.Base.root_sub_root_mem_of_mem_of_mem
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[Finite ι]
[P.IsCrystallographic]
{b : P.Base}
(i j k : ι)
(hij : i ≠ j)
(hi : i ∈ b.support)
(hj : j ∈ b.support)
(hk : P.root k + P.root i - P.root j ∈ Set.range ⇑P.root)
(hkj : k ≠ j)
(hk' : P.root k + P.root i ∈ Set.range ⇑P.root)
:
This is Lemma 2.5 (a) from Geck.
theorem
RootPairing.Base.root_add_root_mem_of_mem_of_mem
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[Finite ι]
[P.IsCrystallographic]
{b : P.Base}
(i j k : ι)
(hij : i ≠ j)
(hi : i ∈ b.support)
(hj : j ∈ b.support)
(hk : P.root k + P.root i - P.root j ∈ Set.range ⇑P.root)
(hkj : P.root k ≠ -P.root i)
(hk' : P.root k - P.root j ∈ Set.range ⇑P.root)
:
This is Lemma 2.5 (b) from Geck.
theorem
RootPairing.Base.root_sub_mem_iff_root_add_mem
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[Finite ι]
[P.IsCrystallographic]
{b : P.Base}
(i j k : ι)
(hij : i ≠ j)
(hi : i ∈ b.support)
(hj : j ∈ b.support)
(hkj : k ≠ j)
(hkj' : P.root k ≠ -P.root i)
(hk : P.root k + P.root i - P.root j ∈ Set.range ⇑P.root)
:
The proof of Lemma 2.6 from Geck.
theorem
RootPairing.chainBotCoeff_mul_chainTopCoeff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[Finite ι]
[P.IsCrystallographic]
{b : P.Base}
{i j k l m : ι}
(hi : i ∈ b.support)
(hj : j ∈ b.support)
(hij : i ≠ j)
(h₁ : P.root k + P.root i = P.root l)
(h₂ : P.root k - P.root j = P.root m)
(h₃ : P.root k + P.root i - P.root j ∈ Set.range ⇑P.root)
[P.IsNotG2]
:
(chainBotCoeff i m + 1) * (chainTopCoeff j k + 1) = (chainTopCoeff j l + 1) * (chainBotCoeff i k + 1)
This is Lemma 2.6 from Geck.