English
Restricting the nonunital star-algebra homomorphism inrNonUnitalStarAlgHom to its range yields a star-algebra equivalence between A and the range of inrNonUnitalStarAlgHom R A.
Русский
Ограничение неунитального звездного алгебро-гомоморфизма inrNonUnitalStarAlgHom до его образа даёт звездно-алгебраическое эквидив между A и образцом inrNonUnitalStarAlgHom R A.
LaTeX
$$$A \cong_{\text{StarAlg}} \operatorname{range}(\mathrm{inrNonUnitalStarAlgHom}(R,A)).$$$
Lean4
/-- The star algebra equivalence obtained by restricting `Unitization.inrNonUnitalStarAlgHom`
to its range. -/
@[simps!]
def inrRangeEquiv (R A : Type*) [CommSemiring R] [StarAddMonoid R] [NonUnitalSemiring A] [Star A] [Module R A]
[IsScalarTower R A A] [SMulCommClass R A A] : A ≃⋆ₐ[R] NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom R A) :=
StarAlgEquiv.ofLeftInverse' (snd_inr R)
