apply_eq_lift — Mathlib

English

Unicity of lift: if a map g : S → T is R-algebra map that agrees with i on R and sends h.root to x, then g = h.lift i x hx.

Русский

Уникальность подъема: если g : S → T — R-алгебраом, который совпадает с i на R и отправляет h.root в x, то g = h.lift i x hx.

LaTeX

$$$ \forall g,\; (\forall a, g(\text{algebraMap } R S a)=i a) \land (g\, h.root = x) \Rightarrow g = h.lift i x hx $$$

Lean4

/-- Auxiliary lemma for `apply_eq_lift` -/
theorem apply_eq_lift (g : S →+* T) (hmap : ∀ a, g (algebraMap R S a) = i a) (hroot : g h.root = x) (a : S) :
    g a = h.lift i x hx a :=
  by
  rw [← h.map_repr a, Polynomial.as_sum_range_C_mul_X_pow (h.repr a)]
  simp [← h.algebraMap_apply, *]

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