English
Let S be a subalgebra of A over a commutative ring R. Then the underlying subring of S inside A coincides with the subring structure obtained from S via its carrier map; equivalently, the inclusion map of S into A is the same whether viewed as a subring inclusion or via the subalgebra’s inner ring hom.
Русский
Пусть S — подалгебра A над R, где R коммутативное кольцо. Тогда подкольцо S внутри A совпадает с подкольцом, полученным из носителя S; то есть встроенная в A инклюзия S совпадает с подкольбной структурой, заданной через отображение-носитель S.
LaTeX
$$$\iota_S = (S\text{.val}) : S \to A$$$
Lean4
@[simp]
theorem toSubring_subtype {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
S.toSubring.subtype = (S.val : S →+* A) :=
rfl
