English
A refinement stating that the range of the weylGroupToPerm is the closure of the range of reflectionPerm.
Русский
Уточнение: образ weylGroupToPerm равен замыканию образа reflectionPerm.
LaTeX
$$$P.weylGroupToPerm.range = \\operatorname{Subgroup.closure}(\\operatorname{range}(P.reflectionPerm)).$$$
Lean4
theorem range_weylGroupToPerm : P.weylGroupToPerm.range = Subgroup.closure (range P.reflectionPerm) :=
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.indexHom P).restrict P.weylGroup) 1 ∈ _
simp only [map_one, one_mem]
| mem w' hw' =>
obtain ⟨i, rfl⟩ := hw'
simp only [MonoidHom.restrict_apply, Equiv.indexHom_apply, Equiv.reflection_indexEquiv]
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.indexHom_apply, Equiv.reflection_indexEquiv]
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₂
