restrictScalars — Mathlib

English

Restriction of scalars extends to algebraic equivalences: an S-algEquiv f: A ≃ₐ[S] B induces an R-algEquiv.

Русский

Ограничение по скалярам распространяется на алгебраические эквивалентности: A ≃ₐ[S] B порождает R-алгебраическую эквивалентность.

LaTeX

$$$ restrictScalars\ R\ f : A \simeq_{{R}} B$$

Lean4

/-- R ⟶ S induces S-Alg ⥤ R-Alg -/
def restrictScalars (f : A ≃ₐ[S] B) : A ≃ₐ[R] B :=
  { (f : A ≃+* B) with
    commutes' := fun r => by
      rw [algebraMap_apply R S A, algebraMap_apply R S B]
      exact f.commutes (algebraMap R S r) }

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