Theorems · Definition · ring theory

IsScalarTower.toAlgHom

(R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R S] → [inst_4 : Algebra S A] → [inst_5 : Algebra R A] → [IsScalarTower R S A] → S →ₐ[R] A

In a tower, the canonical map from the middle element to the top element is an algebra homomorphism over the bottom element.

Defined in

Mathlib.Algebra.Algebra.Hom

Cited by

232 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 153 definitions · uses no axioms

Assumes

CommSemiringCommSemiringSemiringAlgebraAlgebraAlgebraIsScalarTower