unitsCentralizerEquiv — Mathlib

English

There is a natural isomorphism between the group of units centralizing a unit x ∈ Mˣ and the stabilizer of x under the conjugation action of ConjAct (Mˣ) on units.

Русский

Существует естественное изоморфизм между группой единиц, центральизированных относительно x ∈ Mˣ, и стабилизатором x под действием сопряжения ConjAct (Mˣ) на единицы.

LaTeX

$$$ (Submonoid.centralizer {\lvert x \rvert})^{\,\}^\{\,\} ^{\; } \cong MulAction.stabilizer (ConjAct (Units M)) x $$$

Lean4

/-- The stabilizer of `Mˣ` acting on itself by conjugation at `x : Mˣ` is exactly the
units of the centralizer of `x : M`. -/
@[simps! apply_coe_val symm_apply_val_coe]
def unitsCentralizerEquiv (x : Mˣ) : (Submonoid.centralizer ({↑x} : Set M))ˣ ≃* MulAction.stabilizer (ConjAct Mˣ) x :=
  MulEquiv.symm
    { toFun :=
        MonoidHom.toHomUnits <|
          {
            toFun := fun u ↦
              ⟨↑(ConjAct.ofConjAct u.1 : Mˣ), by
                rintro x ⟨rfl⟩
                have : (u : ConjAct Mˣ) • x = x := u.2
                rwa [ConjAct.smul_def, mul_inv_eq_iff_eq_mul, Units.ext_iff, eq_comm] at this⟩,
            map_one' := rfl, map_mul' := fun _ _ ↦ rfl }
      invFun := fun u ↦
        ⟨ConjAct.toConjAct (Units.map (Submonoid.centralizer ({↑x} : Set M)).subtype u),
          by
          change _ • _ = _
          simp only [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, mul_inv_eq_iff_eq_mul]
          exact Units.ext <| (u.1.2 x <| Set.mem_singleton _).symm⟩
      map_mul' := map_mul _ }

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