ext — Mathlib

English

The restriction preserves the root-pairing map: sending i,j via the restricted map and composing with algebra maps yields the original root-pairing value.

Русский

Ограничение сохраняет отображение пары корней: применение ограниченного отображения к i,j и последующее применение алгебраической карты даёт исходное значение парирования.

LaTeX

$$$\\bigl\\text{algebraMap}_{KL}((P.restrictScalars' K hP).pairing(i,j)\\bigr) = P.pairing(i,j)$$$

Lean4

/-- In characteristic zero if there is no torsion, a finite root system is determined entirely by
its roots. -/
@[ext]
protected theorem ext [CharZero R] [NoZeroSMulDivisors R M] {P₁ P₂ : RootSystem ι R M N}
    (he : P₁.toLinearMap = P₂.toLinearMap) (hr : P₁.root = P₂.root) : P₁ = P₂ :=
  by
  suffices
    ∀ P₁ P₂ : RootSystem ι R M N,
      P₁.toLinearMap = P₂.toLinearMap → P₁.root = P₂.root → range P₁.coroot ⊆ range P₂.coroot
    by
    have h₁ := this P₁ P₂ he hr
    have h₂ := this P₂ P₁ he.symm hr.symm
    obtain ⟨P₁⟩ := P₁
    obtain ⟨P₂⟩ := P₂
    congr
    exact RootPairing.ext he hr (le_antisymm h₁ h₂)
  clear! P₁ P₂
  rintro P₁ P₂ he hr - ⟨i, rfl⟩
  use i
  apply P₁.flip.toPerfPair.injective
  apply Dual.eq_of_preReflection_mapsTo (finite_range P₁.root) P₁.span_root_eq_top
  · exact hr ▸ he ▸ P₂.coroot_root_two i
  · change MapsTo (preReflection _ (P₁.toLinearMap.flip.toPerfPair _)) _ _
    simp_rw [hr, he]
    exact P₂.mapsTo_reflection_root i
  · exact P₁.coroot_root_two i
  · exact P₁.mapsTo_reflection_root i

Похожие утверждения