ofFixingSubgroup_equivariantMap — Mathlib

English

Let M be a group acting on a set α and s a subset of α. The identity map from the SubMulAction fixingSubgroup M s into α is an M-equivariant map.

Русский

Пусть M — группа, действующая на множество α, и s — подмножество α. Единичное отображение из SubMulAction fixingSubgroup M s в α является M-эквивариантным отображением.

LaTeX

$$$ i_s: (\,\mathrm{fixingSubgroup}\ M\ s\,) \to \\alpha$, \$i_s(x)=x\$; \\forall m\\in M,\\ x\\in \\mathrm{fixingSubgroup}\ M\ s:\\ i_s(m\\cdot x)=m\\cdot i_s(x). $$$

Lean4

/-- The identity map of the `SubMulAction` of the `fixingSubgroup`
into the ambient set, as an equivariant map. -/
@[to_additive /-- The identity map of the `SubAddAction` of the `fixingAddSubgroup`
    into the ambient set, as an equivariant map. -/
    ]
def ofFixingSubgroup_equivariantMap : ofFixingSubgroup M s →ₑ[(fixingSubgroup M s).subtype] α
    where
  toFun x := x
  map_smul' _ _ := rfl

Похожие утверждения