English
There exists a construction that, given an injective RingHom f: R → S, yields a RingHom from WithTop R to WithTop S extending f, built componentwise from the ring hom and the top-map.
Русский
Существуют такие построения, что при данном инъективном кольцевом гомоморфизме f: R → S получается кольцевой гомоморфизм From WithTop R к WithTop S, который расширяет f и действует по компонентам.
LaTeX
$$$\\\\exists F : \\mathrm{RingHom}(\\\\mathrm{WithTop} R, \\\\mathrm{WithTop} S), \\\\text{F extends } f$$$
Lean4
/-- A version of `WithTop.map` for `RingHom`s. -/
@[simps -fullyApplied]
protected def _root_.RingHom.withTopMap {R S : Type*} [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R]
[DecidableEq R] [Nontrivial R] [NonAssocSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S] [DecidableEq S]
[Nontrivial S] (f : R →+* S) (hf : Function.Injective f) : WithTop R →+* WithTop S :=
{ MonoidWithZeroHom.withTopMap f.toMonoidWithZeroHom hf, f.toAddMonoidHom.withTopMap with }
