Theorems · Definition · ring theory

NonUnitalAlgHom.toAlgHom

{R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : SMulCommClass R A A] →
            [inst_4 : IsScalarTower R A A] →
              {C : Type u_5} → [inst_5 : Semiring C] → [inst_6 : Algebra R C] → (A →ₙₐ[R] C) → Unitization R A →ₐ[R] C

A non-unital algebra homomorphism from A into a unital R-algebra C lifts to a unital algebra homomorphism from the unitization into C. This is extended to an Equiv in Unitization.lift and that should be used instead. This declaration only exists for performance reasons.

Defined in

Mathlib.Algebra.Algebra.Unitization

Cited by

4 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringNonUnitalSemiringModuleSMulCommClassIsScalarTowerSemiringAlgebra