range_algebraMap — Mathlib

English

In the ring setting, the range of algebraMap from S to A equals the underlying Subring of S.

Русский

В кольцевом случае образ algebraMap из S в A равен подкольцу, выходящему из S.

LaTeX

$$$\operatorname{range}(\mathrm{algebraMap}_{S}^{A}) = S^{\text{toSubring}}$$$

Lean4

@[simp]
theorem range_algebraMap {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) :
    (algebraMap S A).range = S.toSubring := by
  rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubring_subtype, Subring.range_subtype]

Похожие утверждения