English
If f: A → B lands in a subalgebra S ≤ B, then f factors through S, giving a homomorphism A → S whose composition with the inclusion S ↪ B equals f.
Русский
Если гомоморфизм f: A → B имеет изображение в подалгебре S ⊆ B, то f факторизуется через S, образуя гомоморфизм A → S, после композиций с включением S ↪ B даёт f.
LaTeX
$$$\exists f_{S}: A \to_R S$ such that (i) f = (SetLike.coe) \circ f_{S}$ and (ii) ∀x, f(x) \in S$; equivalently, $f_{S}$ exists with $(f_{S}\text{ codRestrict } S hf) = f$$$
Lean4
/-- Restrict the codomain of an algebra homomorphism. -/
def codRestrict (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ x, f x ∈ S) : A →ₐ[R] S :=
{ RingHom.codRestrict (f : A →+* B) S hf with commutes' := fun r => Subtype.eq <| f.commutes r }
