ofFixingSubgroup_insert_map — Mathlib

English

The fixed subgroup map is defined as a morphism of actions that respects smul.

Русский

Фиксирующая подгруппа отображается как морфин действия, сохраняющий смул.

LaTeX

$${M,α,β} ->_ {fixingSubgroup} ...$$

Lean4

/-- The identity map of fixing subgroup of stabilizer
into the fixing subgroup of the extended set, as an equivariant map. -/
@[to_additive /-- The identity map of fixing additive subgroup of stabilizer
    into the fixing additive subgroup of the extended set, as an equivariant map. -/
    ]
def ofFixingSubgroup_insert_map (a : α) (s : Set (ofStabilizer M a)) :
    ofFixingSubgroup M (insert a (Subtype.val '' s)) →ₑ[fixingSubgroupInsertEquiv a s]
      ofFixingSubgroup (stabilizer M a) s
    where
  toFun
    x := by
    choose hx hx' using (mem_ofFixingSubgroup_insert_iff.mp x.prop)
    exact ⟨_, hx'⟩
  map_smul' _ _ := rfl

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