fixingSubgroupInsertEquiv — Mathlib

English

There is a natural isomorphism between fixingSubgroup insert and the corresponding map.

Русский

Существует естественный изоморфизм между fixingSubgroup insert и соответствующим отображением.

LaTeX

$$$fixingSubgroupInsertEquiv\ M\ a\ s : fixingSubgroup M (insert a (Subtype.val'' s)) \cong* fixingSubgroup (stabilizer M a) s$$$

Lean4

/-- The natural group isomorphism between fixing subgroups. -/
@[to_additive /-- The natural additive group isomorphism between fixing additive subgroups. -/
    ]
def fixingSubgroupInsertEquiv (a : α) (s : Set (ofStabilizer M a)) :
    fixingSubgroup M (insert a (Subtype.val '' s)) ≃* fixingSubgroup (stabilizer M a) s
    where
  toFun
    m :=
    ⟨⟨(m : M), (mem_fixingSubgroup_iff M).mp m.prop a (Set.mem_insert _ _)⟩, fun ⟨x, hx⟩ =>
      by
      simp only [← SetLike.coe_eq_coe]
      refine (mem_fixingSubgroup_iff M).mp m.prop _ (Set.mem_insert_of_mem a ?_)
      exact ⟨⟨x, (SubMulAction.mem_ofStabilizer_iff M a).mp x.prop⟩, hx, rfl⟩⟩
  map_mul' _ _ := by simp [← Subtype.coe_inj]
  invFun m := ⟨m, by simp [fixingSubgroup_of_insert]⟩
  left_inv _ := by simp
  right_inv _ := by simp

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