restrictScalars — Mathlib

English

Restriction of scalars from S to R preserves the action and yields a nonunital star-algebra homomorphism A →⋆ₙₐ[R] B from one with scalars S.

Русский

Ограничение скаляров от S к R сохраняет действие и даёт ненулевой ⋆-алгоморфизм A →⋆ₙₐ[R] B, полученный из одного со скалярами S.

LaTeX

$$"restrictScalars" applied to f gives a new homomorphism with the same underlying map and star-structure adjusted to R$$

Lean4

/-- If a monoid `R` acts on another monoid `S`, then a non-unital star algebra homomorphism
over `S` can be viewed as a non-unital star algebra homomorphism over `R`. -/
def restrictScalars (f : A →⋆ₙₐ[S] B) : A →⋆ₙₐ[R] B :=
  { (f : A →ₙₐ[S] B).restrictScalars R with map_star' := map_star f }

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