rootSpace_comap_eq_genWeightSpace

English

For χ: H → R, the comap of rootSpace H χ along the inclusion H → L equals genWeightSpace H χ.

Русский

Для χ: H → R комап корневого пространства по включению H ↪ L равен genWeightSpace H χ.

LaTeX

$$$(\mathrm{rootSpace} H \chi).\mathrm{comap} \; H.\mathrm incl' = \mathrm{genWeightSpace} H \chi$$$

Lean4

@[simp]
theorem rootSpace_comap_eq_genWeightSpace (χ : H → R) : (rootSpace H χ).comap H.incl' = genWeightSpace H χ :=
  comap_genWeightSpace_eq_of_injective Subtype.coe_injective

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