English
The range of the weight hom restricted to the Weyl group equals the closure of the range of reflections.
Русский
Образ весового отображения, ограниченного Weyl-группой, равен замыканию образа отражений.
LaTeX
$$$\\operatorname{range}((\\operatorname{Equiv.weightHom}(P)).restrict P.weylGroup) = \\operatorname{Subgroup.closure}(\\operatorname{range}(P.reflection)).$$$
Lean4
theorem range_weylGroup_weightHom :
MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup) = Subgroup.closure (range P.reflection) :=
by
refine (Subgroup.closure_eq_of_le _ ?_ ?_).symm
· rintro - ⟨i, rfl⟩
simp only [MonoidHom.restrict_range, Subgroup.coe_map, Equiv.weightHom_apply, mem_image, SetLike.mem_coe]
use Equiv.reflection P i
exact ⟨reflection_mem_weylGroup P i, Equiv.reflection_weightEquiv P i⟩
· rintro fg ⟨⟨w, hw⟩, rfl⟩
induction hw using Subgroup.closure_induction'' with
| one =>
change ((Equiv.weightHom P).restrict P.weylGroup) 1 ∈ _
simp only [map_one, one_mem]
| mem w' hw' =>
obtain ⟨i, rfl⟩ := hw'
simp only [MonoidHom.restrict_apply, Equiv.weightHom_apply, Equiv.reflection_weightEquiv]
simpa only [reflection_mem_weylGroup] using Subgroup.subset_closure (mem_range_self i)
| inv_mem w' hw' =>
obtain ⟨i, rfl⟩ := hw'
simp only [Equiv.reflection_inv, MonoidHom.restrict_apply, Equiv.weightHom_apply, Equiv.reflection_weightEquiv]
simpa only [reflection_mem_weylGroup] using Subgroup.subset_closure (mem_range_self i)
| mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>
simpa only [← Submonoid.mk_mul_mk _ w₁ w₂ hw₁ hw₂, map_mul] using Subgroup.mul_mem _ h₁ h₂
