Commit 2023-09-12 09:41 da2f8a8b

feat: maps from the unitization of non-unital subobjects of unital algebras (#6372) If S is non-unital subalgebra of a unital R-algebra A, there is a natural map Unitization R S →ₐ[R] A whose range is Algebra.adjoin R (S : Set A). When 1 ∉ S and R is a field, this map is injective, and so we can restrict the codomain to Algebra.adjoin R (S : Set A) and turn it into an AlgEquiv. We specialize this to the ℕ-unitization of a non-unital subsemiring and its Subsemiring.closure, as well as the ℤ-unitization of a non-unital subring and its Subring.closure. We also extend the above map to a StarAlgHom in the case of NonUnitalStarSubalgebras. This continues the non-unital-ization of mathlib.