English
Conjugation induces an equivariant map between SubMulAction objects for fixingSubgroups of translates.
Русский
Конъюгация индуцирует эквивariant отображение между SubMulAction объектами фиксирующих подгрупп переносов.
LaTeX
$$$conjMap_ofFixingSubgroup hg : ofFixingSubgroup M t \to\ _e[fixingSubgroupEquivFixingSubgroup hg] ofFixingSubgroup M s$$$
Lean4
/-- Conjugation induces an equivariant map between the `SubMulAction` of
the fixing subgroup of a subset and that of a translate. -/
@[to_additive /-- Conjugation induces an equivariant map between the `SubAddAction` of
the fixing subgroup of a subset and that of a translate. -/
]
def conjMap_ofFixingSubgroup (hg : g • t = s) :
ofFixingSubgroup M t →ₑ[fixingSubgroupEquivFixingSubgroup hg] ofFixingSubgroup M s
where
toFun := fun ⟨x, hx⟩ =>
⟨g • x, by
intro hgxt; apply hx
rw [← hg] at hgxt
exact Set.smul_mem_smul_set_iff.mp hgxt⟩
map_smul' := fun ⟨m, hm⟩ ⟨x, hx⟩ => by
simp only [← SetLike.coe_eq_coe, subgroup_smul_def, SetLike.val_smul, fixingSubgroupEquivFixingSubgroup_coe_apply,
MulAut.conj_apply, mul_smul, inv_smul_smul]
