toAlgAut — Mathlib

English

The same injectivity result for the action yields that the map toAlgAut from G to Aut_R(A) is injective when the action is faithful.

Русский

То же свойство инъективности для отображения toAlgAut: если действие верно, то карта из G в Aut_R(A) инъективна.

LaTeX

$$$[FaithfulSMul G A] :\\; \\text{toAlgEquiv} : G \\to Aut_R(A) \\text{ Injective}.$$$

Lean4

/-- Each element of the group defines an algebra equivalence.

This is a stronger version of `MulSemiringAction.toRingAut` and
`DistribMulAction.toModuleEnd`. -/
@[simps]
def toAlgAut : G →* A ≃ₐ[R] A where
  toFun := toAlgEquiv R A
  map_one' := AlgEquiv.ext <| one_smul _
  map_mul' g h := AlgEquiv.ext <| mul_smul g h

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