Reduced root pairings #
This file contains basic definitions and results related to reduced root pairings.
Main definitions: #
RootPairing.IsReduced: A root pairing is said to be reduced if two linearly dependent roots are always related by a sign.RootPairing.linInd_iff_coxeterWeight_ne_four: for a finite root pairing, two roots are linearly independent iff their Coxeter weight is not four.
Implementation details: #
For convenience we provide two versions of many lemmas, according to whether we know that the root
pairing is valued in a smaller ring (in the sense of RootPairing.IsValuedIn). For example we
provide both RootPairing.linInd_iff_coxeterWeight_ne_four and
RootPairing.linInd_iff_coxeterWeightIn_ne_four.
Several ways to avoid this duplication exist. We leave explorations of this for future work. One
possible solution is to drop RootPairing.pairing and RootPairing.coxeterWeight entirely and rely
solely on RootPairing.pairingIn and RootPairing.coxeterWeightIn.`
class
RootPairing.IsReduced
{ι : 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)
:
A root pairing is said to be reduced if any linearly dependent pair of roots is related by a sign.
Instances
theorem
RootPairing.isReduced_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)
:
theorem
RootPairing.isReduced_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)
:
theorem
RootPairing.IsReduced.linearIndependent
{ι : 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)
{i j : ι}
[P.IsReduced]
(h : i ≠ j)
(h' : P.root i ≠ -P.root j)
:
theorem
RootPairing.IsReduced.linearIndependent_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)
{i j : ι}
[Nontrivial R]
[P.IsReduced]
:
theorem
RootPairing.infinite_of_linInd_coxeterWeight_four
{ι : 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)
{i j : ι}
[NeZero 2]
[NoZeroSMulDivisors ℤ M]
(hl : LinearIndependent R ![P.root i, P.root j])
(hc : P.coxeterWeight i j = 4)
:
Infinite ι
theorem
RootPairing.pairing_smul_root_eq_of_not_linInd
{ι : 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)
{i j : ι}
[NeZero 2]
[NoZeroSMulDivisors R M]
(h : ¬LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.coxeterWeight_ne_four_of_linearIndependent
{ι : 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)
{i j : ι}
[Finite ι]
[NeZero 2]
[NoZeroSMulDivisors ℤ M]
(hl : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.linearIndependent_iff_coxeterWeight_ne_four
{ι : 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)
{i j : ι}
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
:
See also RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four.
theorem
RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent
{ι : 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)
{i j : ι}
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
:
See also RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent.
@[simp]
theorem
RootPairing.pairing_two_two_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)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
:
See also RootPairing.pairingIn_two_two_iff.
@[simp]
theorem
RootPairing.pairing_neg_two_neg_two_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)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
:
theorem
RootPairing.pairing_one_four_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)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[NoZeroSMulDivisors R N]
(h2 : IsSMulRegular R 2)
:
theorem
RootPairing.pairing_neg_one_neg_four_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)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[NoZeroSMulDivisors R N]
(h2 : IsSMulRegular R 2)
:
@[simp]
theorem
RootPairing.pairing_one_four_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)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[NoZeroSMulDivisors R N]
[NoZeroDivisors R]
:
See also RootPairing.pairingIn_one_four_iff.
@[simp]
theorem
RootPairing.pairing_neg_one_neg_four_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)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[NoZeroSMulDivisors R N]
[NoZeroDivisors R]
:
theorem
RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(S : Type u_5)
{i j : ι}
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[LinearOrderedCommRing S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
:
theorem
RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(S : Type u_5)
{i j : ι}
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[LinearOrderedCommRing S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
:
theorem
RootPairing.coxeterWeightIn_ne_four
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(S : Type u_5)
{i j : ι}
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[LinearOrderedCommRing S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[P.IsReduced]
(h : i ≠ j)
(h' : P.root i ≠ -P.root j)
:
@[simp]
theorem
RootPairing.pairingIn_two_two_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(S : Type u_5)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[LinearOrderedCommRing S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
:
theorem
RootPairing.pairingIn_neg_two_neg_two_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(S : Type u_5)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[LinearOrderedCommRing S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
:
theorem
RootPairing.pairingIn_one_four_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(S : Type u_5)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[LinearOrderedCommRing S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[NoZeroSMulDivisors R N]
[NoZeroDivisors R]
:
theorem
RootPairing.pairingIn_neg_one_neg_four_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
(S : Type u_5)
(i j : ι)
[Finite ι]
[CharZero R]
[NoZeroSMulDivisors R M]
[LinearOrderedCommRing S]
[Algebra S R]
[FaithfulSMul S R]
[P.IsValuedIn S]
[NoZeroSMulDivisors R N]
[NoZeroDivisors R]
: