toEndUnit — Mathlib

English

There is a canonical group isomorphism Aut(P) ≃* (End(P))ˣ between automorphisms of P and units of its endomorphism monoid.

Русский

Существует каноническое групповое изоморождение Aut(P) ≃* (End(P))ˣ между автоморфизмами P и единицами их эндоморфномоноида.

LaTeX

$$$\\\\mathrm{Aut}(P) \\\\simeq\\\\ (\\\\mathrm{End}(P))^{\\\\times}.$$$

Lean4

/-- The isomorphism between the automorphism group of a root pairing and the group of invertible
endomorphisms. -/
def toEndUnit (P : RootPairing ι R M N) : Aut P ≃* (End P)ˣ
    where
  toFun
    f :=
    { val := f.toHom
      inv := (Equiv.symm P P f).toHom
      val_inv := by ext <;> simp
      inv_val := by ext <;> simp }
  invFun
    f :=
    {
      f.val with
      bijective_weightMap := by
        refine bijective_iff_has_inverse.mpr ?_
        use f.inv.weightMap
        constructor
        · refine leftInverse_iff_comp.mpr ?_
          simp only [← @LinearMap.coe_comp]
          rw [← Hom.weightMap_mul, f.inv_val, Hom.weightMap_one, LinearMap.id_coe]
        · refine rightInverse_iff_comp.mpr ?_
          simp only [← @LinearMap.coe_comp]
          rw [← Hom.weightMap_mul, f.val_inv, Hom.weightMap_one, LinearMap.id_coe]
      bijective_coweightMap := by
        refine bijective_iff_has_inverse.mpr ?_
        use f.inv.coweightMap
        constructor
        · refine leftInverse_iff_comp.mpr ?_
          simp only [← @LinearMap.coe_comp]
          rw [← Hom.coweightMap_mul, f.val_inv, Hom.coweightMap_one, LinearMap.id_coe]
        · refine rightInverse_iff_comp.mpr ?_
          simp only [← @LinearMap.coe_comp]
          rw [← Hom.coweightMap_mul, f.inv_val, Hom.coweightMap_one, LinearMap.id_coe] }
  left_inv f := by simp
  right_inv f := by simp
  map_mul' f
    g := by
    simp only [Equiv.mul_eq_comp, Equiv.toHom_comp]
    ext <;> simp

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