English
There is a canonical group morphism from fixingSubgroup M (s ∪ t) to fixingSubgroup (fixingSubgroup M s) of t, mapping an element to its appropriate action, with explicit lifting through subtype.
Русский
Существует каноническое отображение группы от fixingSubgroup M (s ∪ t) к fixingSubgroup (fixingSubgroup M s) через подмножество и продолжение через подтекст, задающее действие элемента.
LaTeX
$$$ \\text{fixingSubgroup}_{M}(s \\cup t) \\to^* \\text{fixingSubgroup}_{\\,\\text{fixingSubgroup}_{M}(s)}(\\operatorname{Subtype} \\circ \\operatorname{val})$$$
Lean4
/-- The group morphism from `fixingSubgroup` of a union to the iterated `fixingSubgroup`. -/
@[to_additive /-- The additive group morphism from `fixingAddSubgroup` of a union
to the iterated `fixingAddSubgroup`. -/
]
def fixingSubgroup_union_to_fixingSubgroup_of_fixingSubgroup :
fixingSubgroup M (s ∪ t) →* fixingSubgroup (fixingSubgroup M s) (Subtype.val ⁻¹' t : Set (ofFixingSubgroup M s))
where
toFun
m :=
⟨⟨m, (mem_fixingSubgroup_union_iff.mp m.prop).1⟩,
by
rintro ⟨⟨x, hx⟩, hx'⟩
simp only [Set.mem_preimage] at hx'
simp only [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower]
exact (mem_fixingSubgroup_union_iff.mp m.prop).2 ⟨x, hx'⟩⟩
map_one' := by simp
map_mul' _ _ := by simp [← Subtype.coe_inj]
