English
For a group M acting on α and sets s,t ⊆ α, there is a canonical equivariant map between the iterated fixing-subgroups corresponding to the union s ∪ t and the fixing-subgroup of s with preimage t.
Русский
Пусть группа M действует на α и существуют подмножества s,t ⊆ α. Существует каноническое эквивариантное отображение между повторно фиксируемыми подподгруппами, соответствующими объединению s ∪ t и фиксации подгруппы, получаемой из s через предобраз t.
LaTeX
$$$\exists \psi: fixingSubgroup(M, s\cup t) \to_{\text{equivariant}} fixingSubgroup(fixingSubgroup(M, s), \mathrm{preimage}(Subtype.val, t)).$$$
Lean4
/-- The identity between the iterated `SubMulAction`
of the `fixingSubgroup` and the `SubMulAction` of the `fixingSubgroup`
of the union, as an equivariant map. -/
@[to_additive /-- The identity between the iterated `SubAddAction`
of the `fixingAddSubgroup` and the `SubAddAction` of the `fixingAddSubgroup`
of the union, as an equivariant map. -/
]
def map_ofFixingSubgroupUnion :
let ψ :
fixingSubgroup M (s ∪ t) → fixingSubgroup (fixingSubgroup M s) (Subtype.val ⁻¹' t : Set (ofFixingSubgroup M s)) :=
fun m ↦
⟨⟨m, by
let hm := m.prop
simp only [fixingSubgroup_union, Subgroup.mem_inf] at hm
exact hm.left⟩,
by
let hm := m.prop
simp only [fixingSubgroup_union, Subgroup.mem_inf] at hm
rintro ⟨⟨x, hx⟩, hx'⟩
simp only [Set.mem_preimage] at hx'
simp only [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower]
exact hm.right ⟨x, hx'⟩⟩
ofFixingSubgroup M (s ∪ t) →ₑ[ψ]
ofFixingSubgroup (fixingSubgroup M s) (Subtype.val ⁻¹' t : Set (ofFixingSubgroup M s))
where
toFun
x :=
⟨⟨x, fun hx => x.prop (Set.mem_union_left t hx)⟩, fun hx =>
x.prop
(by
apply Set.mem_union_right s
simpa only [Set.mem_preimage, Subtype.coe_mk] using hx)⟩
map_smul' := fun ⟨m, hm⟩ ⟨x, hx⟩ =>
by
rw [← SetLike.coe_eq_coe, ← SetLike.coe_eq_coe]
exact subgroup_smul_def ⟨m, hm⟩ x
