Theorems · Theorem · nonassociative algebras

RootPairing.ext

∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Finite ι] [CharZero R] [IsDomain R]
  [Module.IsTorsionFree R M] {P₁ P₂ : RootPairing ι R M N},
  P₁.toLinearMap = P₂.toLinearMap → P₁.root = P₂.root → Set.range ⇑P₁.coroot = Set.range ⇑P₂.coroot → P₁ = P₂

In characteristic zero if there is no torsion, the correspondence between roots and coroots is unique. Formally, the point is that the hypothesis hc depends only on the range of the coroot mappings.

Defined in

Mathlib.LinearAlgebra.RootSystem.Basic

Cited by

2 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleFiniteCharZeroIsDomainModule.IsTorsionFree