ofFixingSubgroup_of_singleton — Mathlib

English

There is an equivariant map between SubMulAction.ofStabilizer M a and ofFixingSubgroup M {a}.

Русский

Существует эквивариантное отображение между SubMulAction.ofStabilizer M a и ofFixingSubgroup M {a}.

LaTeX

$$$\text{Equivariant map }\mathrm{ofFixingSubgroup\_of\_singleton}(M,a) : SubMulAction.ofStabilizer M a \to \mathrm{ofFixingSubgroup M \{a\}}$$$

Lean4

/-- The equivariant map between `SubMulAction.ofStabilizer M a`
and `ofFixingSubgroup M {a}`. -/
@[to_additive /-- The equivariant map between `SubAddAction.ofStabilizer M a`
    and `ofFixingAddSubgroup M {a}`. -/
    ]
def ofFixingSubgroup_of_singleton (a : α) :
    let φ : fixingSubgroup M ({ a } : Set α) → stabilizer M a := fun ⟨m, hm⟩ =>
      ⟨m, ((mem_fixingSubgroup_iff M).mp hm) a (Set.mem_singleton a)⟩
    ofFixingSubgroup M ({ a } : Set α) →ₑ[φ] ofStabilizer M a
    where
  toFun x := ⟨x, by simp⟩
  map_smul' _ _ := rfl

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