of_algHom — Mathlib

English

From an R-algebra hom f: A →ₐ[R] B, one obtains a tower-compatible IsScalarTower R S A and R S B trivial extension via f.

Русский

Из алгеброморфизма f: A →ₐ[R] B получаем башню IsScalarTower R S A и IsScalarTower R S B через f.

LaTeX

$$$ IsScalarTower\ R\ S\ A\;\text{and}\; IsScalarTower\ R\ S\ B$$

Lean4

instance (priority := 999) of_algHom {R A B : Type*} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A]
    [Algebra R B] (f : A →ₐ[R] B) : @IsScalarTower R A B _ f.toRingHom.toAlgebra.toSMul _ :=
  letI := (f : A →+* B).toAlgebra
  of_algebraMap_eq fun x => (f.commutes x).symm

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