indexHom — Mathlib

English

The index Hom map sends an automorphism to its action on the index set, i.e., induces a permutation of indices.

Русский

Отображение indexHom отправляет автоморфизм на его действие на множество индексов, то есть порождает перестановку индексов.

LaTeX

$$$\\\\text{indexHom}(P): Aut(P) \\\\to (\\\\iota \\\\simeq \\\\iota).$$$

Lean4

/-- The permutation representation of the automorphism group on the root index set -/
@[simps]
def indexHom (P : RootPairing ι R M N) : Aut P →* (ι ≃ ι)
    where
  toFun g := g.toHom.indexEquiv
  map_one' := by ext; simp
  map_mul' x y := by ext; simp

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