Chains of roots #
Given roots α and β, the α-chain through β is the set of roots of the form α + z • β
for an integer z. This is known as a "root chain" and also a "root string". For linearly
independent roots in finite crystallographic root pairings, these chains are always unbroken, i.e.,
of the form: β - q • α, ..., β - α, β, β + α, ..., β + p • α for natural numbers p, q, and the
length, p + q is at most 3.
Main definitions / results: #
RootPairing.chainTopCoeff: the natural numberpin the chainβ - q • α, ..., β - α, β, β + α, ..., β + p • αRootPairing.chainTopCoeff: the natural numberqin the chainβ - q • α, ..., β - α, β, β + α, ..., β + p • αRootPairing.root_add_zsmul_mem_range_iff: every chain is an interval (aka unbroken).RootPairing.chainBotCoeff_add_chainTopCoeff_le: every chain has length at most three.
theorem
RootPairing.setOf_root_add_zsmul_eq_Icc_of_linearIndependent
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
Note that it is often more convenient to use RootPairing.root_add_zsmul_mem_range_iff than
to invoke this lemma directly.
def
RootPairing.chainTopCoeff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
(i j : ι)
:
If α = P.root i and β = P.root j are linearly independent, this is the value p ≥ 0 where
β - q • α, ..., β - α, β, β + α, ..., β + p • α is the α-chain through β.
In the absence of linear independence, it takes a junk value.
Equations
- RootPairing.chainTopCoeff i j = if h : LinearIndependent R ![P.root i, P.root j] then ⋯.choose.toNat else 0
Instances For
def
RootPairing.chainBotCoeff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
(i j : ι)
:
If α = P.root i and β = P.root j are linearly independent, this is the value q ≥ 0 where
β - q • α, ..., β - α, β, β + α, ..., β + p • α is the α-chain through β.
In the absence of linear independence, it takes a junk value.
Equations
Instances For
theorem
RootPairing.chainTopCoeff_of_not_linearIndependent
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : ¬LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.chainBotCoeff_of_not_linearIndependent
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : ¬LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.root_add_nsmul_mem_range_iff_le_chainTopCoeff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
{n : ℕ}
:
theorem
RootPairing.root_sub_nsmul_mem_range_iff_le_chainBotCoeff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
{n : ℕ}
:
theorem
RootPairing.Iic_chainTopCoeff_eq
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.Iic_chainBotCoeff_eq
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.one_le_chainTopCoeff_of_root_add_mem
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
[P.IsReduced]
(h : P.root i + P.root j ∈ Set.range ⇑P.root)
:
theorem
RootPairing.one_le_chainBotCoeff_of_root_add_mem
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
[P.IsReduced]
(h : P.root i - P.root j ∈ Set.range ⇑P.root)
:
theorem
RootPairing.root_add_zsmul_mem_range_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
{z : ℤ}
:
theorem
RootPairing.root_sub_zsmul_mem_range_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
{z : ℤ}
:
theorem
RootPairing.setOf_root_add_zsmul_mem_eq_Icc
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.setOf_root_sub_zsmul_mem_eq_Icc
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.chainTopCoeff_eq_sSup
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.chainBotCoeff_eq_sSup
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.coe_chainTopCoeff_eq_sSup
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.coe_chainBotCoeff_eq_sSup
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
@[deprecated _private.Mathlib.LinearAlgebra.RootSystem.Chain.0.RootPairing.chainCoeff_reflectionPerm_left_aux (since := "2025-05-28")]
theorem
RootPairing.chainCoeff_reflection_perm_left_aux
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
Set.Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) = Set.Icc (-↑(chainBotCoeff (-i) j)) ↑(chainTopCoeff (-i) j)
Alias of _private.Mathlib.LinearAlgebra.RootSystem.Chain.0.RootPairing.chainCoeff_reflectionPerm_left_aux.
@[deprecated _private.Mathlib.LinearAlgebra.RootSystem.Chain.0.RootPairing.chainCoeff_reflectionPerm_right_aux (since := "2025-05-28")]
theorem
RootPairing.chainCoeff_reflection_perm_right_aux
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
Set.Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) = Set.Icc (-↑(chainBotCoeff i (-j))) ↑(chainTopCoeff i (-j))
Alias of _private.Mathlib.LinearAlgebra.RootSystem.Chain.0.RootPairing.chainCoeff_reflectionPerm_right_aux.
@[simp]
theorem
RootPairing.chainTopCoeff_reflectionPerm_left
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
@[deprecated RootPairing.chainTopCoeff_reflectionPerm_left (since := "2025-05-28")]
theorem
RootPairing.chainTopCoeff_reflection_perm_left
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
@[simp]
theorem
RootPairing.chainBotCoeff_reflectionPerm_left
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
@[deprecated RootPairing.chainBotCoeff_reflectionPerm_left (since := "2025-05-28")]
theorem
RootPairing.chainBotCoeff_reflection_perm_left
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
@[simp]
theorem
RootPairing.chainTopCoeff_reflectionPerm_right
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
@[deprecated RootPairing.chainTopCoeff_reflectionPerm_right (since := "2025-05-28")]
theorem
RootPairing.chainTopCoeff_reflection_perm_right
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
@[simp]
theorem
RootPairing.chainBotCoeff_reflectionPerm_right
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
theorem
RootPairing.chainBotCoeff_eq_zero_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
theorem
RootPairing.chainTopCoeff_eq_zero_iff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
theorem
RootPairing.chainBotCoeff_of_add
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
{k : ι}
(hk : P.root k = P.root j + P.root i)
:
theorem
RootPairing.chainTopCoeff_of_sub
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
{k : ι}
(hk : P.root k = P.root j - P.root i)
:
theorem
RootPairing.chainTopCoeff_of_add
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
{k : ι}
(hk : P.root k = P.root j + P.root i)
:
@[deprecated RootPairing.chainBotCoeff_reflectionPerm_right (since := "2025-05-28")]
theorem
RootPairing.chainBotCoeff_reflection_perm_right
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
def
RootPairing.chainTopIdx
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
(i j : ι)
:
ι
If α = P.root i and β = P.root j are linearly independent, this is the index of the root
β + p • α where β - q • α, ..., β - α, β, β + α, ..., β + p • α is the α-chain through β.
In the absence of linear independence, it takes a junk value.
Equations
- RootPairing.chainTopIdx i j = if h : LinearIndependent R ![P.root i, P.root j] then Exists.choose ⋯ else j
Instances For
def
RootPairing.chainBotIdx
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
(i j : ι)
:
ι
If α = P.root i and β = P.root j are linearly independent, this is the index of the root
β - q • α where β - q • α, ..., β - α, β, β + α, ..., β + p • α is the α-chain through β.
In the absence of linear independence, it takes a junk value.
Equations
- RootPairing.chainBotIdx i j = if h : LinearIndependent R ![P.root i, P.root j] then Exists.choose ⋯ else j
Instances For
@[simp]
theorem
RootPairing.root_chainTopIdx
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
@[simp]
theorem
RootPairing.root_chainBotIdx
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
theorem
RootPairing.chainBotCoeff_sub_chainTopCoeff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.chainTopCoeff_sub_chainBotCoeff
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.chainCoeff_chainTopIdx_aux
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
chainBotCoeff i (chainTopIdx i j) = chainBotCoeff i j + chainTopCoeff i j ∧ chainTopCoeff i (chainTopIdx i j) = 0
@[simp]
theorem
RootPairing.chainBotCoeff_chainTopIdx
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
@[simp]
theorem
RootPairing.chainTopCoeff_chainTopIdx
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
:
theorem
RootPairing.chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.chainBotCoeff_add_chainTopCoeff_le_three
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Finite ι]
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{P : RootPairing ι R M N}
[P.IsCrystallographic]
{i j : ι}
[P.IsReduced]
: