map_leftInverse — Mathlib

English

If f is a left inverse of g, then map f is a left inverse of map g (repeat).

Русский

Если f — левый обратный к g, то map f — левый обратный к map g (повтор).

LaTeX

$$$$\text{If } f \circ g = \mathrm{id}, \ \operatorname{map} f \;\bigl(\operatorname{map} g\; p\bigr) = p.$$$$

Lean4

/-- If `f` is a left-inverse of `g` then `map f` is a left-inverse of `map g`. -/
theorem map_leftInverse {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.LeftInverse f g) :
    Function.LeftInverse (map f : MvPolynomial σ R → MvPolynomial σ S₁) (map g) := fun X => by
  rw [map_map, (RingHom.ext hf : f.comp g = RingHom.id _), map_id]

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