eq_zero_of_apply_eq_zero_of_mem_corootSpace

English

If x ∈ corootSpace α and α(x) = 0, then x = 0.

Русский

Если x ∈ corootSpace α и α(x) = 0, то x = 0.

LaTeX

$$$x \in \operatorname{corootSpace}(\alpha) \land \alpha(x) = 0 \Rightarrow x = 0$$$

Lean4

/-- The contrapositive of this result is very useful, taking `x` to be the element of `H`
corresponding to a root `α` under the identification between `H` and `H^*` provided by the Killing
form. -/
theorem eq_zero_of_apply_eq_zero_of_mem_corootSpace (x : H) (α : H → K) (hαx : α x = 0) (hx : x ∈ corootSpace α) :
    x = 0 := by
  rcases eq_or_ne α 0 with rfl | hα; · simpa using hx
  replace hx : x ∈ ⨅ β : Weight K H L, β.ker :=
    by
    refine (Submodule.mem_iInf _).mpr fun β ↦ ?_
    obtain ⟨a, b, hb, hab⟩ := exists_forall_mem_corootSpace_smul_add_eq_zero L α β hα β.genWeightSpace_ne_bot
    simpa [hαx, hb.ne'] using hab _ hx
  simpa using hx

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