Theorems · Theorem · ring theory

Unitization.starMap_id

∀ {R : Type u_1} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring B]
  [inst_3 : StarRing B] [inst_4 : Module R B] [inst_5 : SMulCommClass R B B] [inst_6 : IsScalarTower R B B]
  [inst_7 : StarModule R B], Unitization.starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B)

starMap is functorial: starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B).

Defined in

Mathlib.Algebra.Algebra.Unitization

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingNonUnitalSemiringStarRingModuleSMulCommClassIsScalarTowerStarModule