isoPerm — Mathlib

English

The forgetful-in Aut α isomorphic to Equiv.Perm α; the automorphism group of a type is isomorphic to the permutation group on that type.

Русский

Автоморфизмной группе типа α сопоставим группpermutations на α; Aut α ≅ Perm α.

LaTeX

$$$$ \mathrm{Aut}(\alpha) \cong \mathrm{Perm}(\alpha). $$$$

Lean4

/-- The (bundled) group of automorphisms of a type is isomorphic to the (bundled) group
of permutations. -/
def isoPerm {α : Type u} : GrpCat.of (Aut α) ≅ GrpCat.of (Equiv.Perm α)
    where
  hom :=
    GrpCat.ofHom
      { toFun := fun g => g.toEquiv
        map_one' := by aesop
        map_mul' := by aesop }
  inv :=
    GrpCat.ofHom
      { toFun := fun g => g.toIso
        map_one' := by aesop
        map_mul' := by aesop }

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