equivApp — Mathlib

English

If k is a nontrivial ring, then the natural homomorphism equivHom: G → Aut(forget k G) is injective.

Русский

Если k ненулевое кольцо, то натуральный гомоморфизм equivHom: G → Aut(forget k G) инъективен.

LaTeX

$$$\\text{equivHom}: G \\to^* \\operatorname{Aut}(\\forget k G)\\ \\text{ is injective when } k \\text{ is nontrivial.}$$$

Lean4

/-- Definition of `equivHom g : Aut (forget k G)` by its components. -/
@[simps]
def equivApp (g : G) (X : FDRep k G) : X.V ≅ X.V
    where
  hom := ofHom (X.ρ g)
  inv := ofHom (X.ρ g⁻¹)
  hom_inv_id := by
    ext x
    simp
  inv_hom_id := by
    ext x
    simp

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