English
Iff coroot α equals coroot β then α equals β.
Русский
Если корот α равен короту β, то α = β.
LaTeX
$$coroot α = coroot β ↔ α = β$$
Lean4
@[simp]
theorem coroot_eq_iff (α β : Weight K H L) : coroot α = coroot β ↔ α = β :=
by
refine ⟨fun hyp ↦ ?_, fun h ↦ by rw [h]⟩
if hα : α.IsZero then
have hβ : β.IsZero := by
rw [← coroot_eq_zero_iff] at hα ⊢
rwa [← hyp]
ext
simp [hα.eq, hβ.eq]
else
have hβ : β.IsNonZero := by
contrapose! hα
simp only [← coroot_eq_zero_iff] at hα ⊢
rwa [hyp]
have : α.ker = β.ker := by rw [← orthogonal_span_coroot_eq_ker α, hyp, orthogonal_span_coroot_eq_ker]
suffices (α : H →ₗ[K] K) = β by ext x; simpa using LinearMap.congr_fun this x
apply Module.Dual.eq_of_ker_eq_of_apply_eq (coroot α) this
· rw [Weight.toLinear_apply, root_apply_coroot hα, hyp, Weight.toLinear_apply, root_apply_coroot hβ]
· simp [root_apply_coroot hα]
