English
The range of the coweight hom restricted to the Weyl group equals the closure of the coreflection range.
Русский
Образ сопряженного весового отображения, ограниченного Weyl-группой, равен замыканию образа(coreflection).
LaTeX
$$$\\operatorname{range}((\\operatorname{Equiv.coweightHom}(P)).restrict P.weylGroup) = \\operatorname{Subgroup.closure}(\\operatorname{range}(\\operatorname{MulOpposite.op} \\circ P.coreflection)).$$$
Lean4
theorem range_weylGroup_coweightHom :
MonoidHom.range ((Equiv.coweightHom P).restrict P.weylGroup) =
Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)) :=
by
refine (Subgroup.closure_eq_of_le _ ?_ ?_).symm
· rintro - ⟨i, rfl⟩
simp only [MonoidHom.restrict_range, Subgroup.coe_map, mem_image, SetLike.mem_coe]
use Equiv.reflection P i
refine ⟨reflection_mem_weylGroup P i, by simp⟩
· rintro fg ⟨⟨w, hw⟩, rfl⟩
induction hw using Subgroup.closure_induction'' with
| one =>
change ((Equiv.coweightHom P).restrict P.weylGroup) 1 ∈ _
simp only [map_one, one_mem]
| mem w' hw' =>
obtain ⟨i, rfl⟩ := hw'
simp only [MonoidHom.restrict_apply, Equiv.coweightHom_apply, Equiv.reflection_coweightEquiv]
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.coweightHom_apply,
Equiv.reflection_coweightEquiv]
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₂
