ofRestrictScalars — Mathlib

English

There is an R-algebra homomorphism from U.restrictScalars R to B induced by an S-algebra homomorphism from U, i.e., a restriction-of-scalars map along the tower.

Русский

Существует R-алгебра гомоморфизм от U.restrictScalars R к B, индуцированный S-алгебра гомоморфизмом от U.

LaTeX

$$$\text{ofRestrictScalars}(U,f) : U.restrictScalars R \to_B B$$$

Lean4

/-- Produces an `R`-algebra map from `U.restrictScalars R` given an `S`-algebra map from `U`.

This is a special case of `AlgHom.restrictScalars` that can be helpful in elaboration. -/
@[simp]
def ofRestrictScalars (U : Subalgebra S A) (f : U →ₐ[S] B) : U.restrictScalars R →ₐ[R] B :=
  f.restrictScalars R

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