mem_lifts_iff_mem_alg — Mathlib

English

A polynomial p lifts iff it lies in the image of mapAlg, the polynomial map from R to S.

Русский

Многочлен p поднимается тогда и только тогда, когда он лежит в образе mapAlg — отображения полиномов с R в S.

LaTeX

$$$ p \in \mathrm{lifts}(\mathrm{algebraMap}\, R\, S) \iff p \in \mathrm{AlgHom}.range(\mathrm{mapAlg}\, R\, S) $$$

Lean4

/-- A polynomial `p` lifts if and only if it is in the image of `mapAlg`. -/
theorem mem_lifts_iff_mem_alg (R : Type u) [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] (p : S[X]) :
    p ∈ lifts (algebraMap R S) ↔ p ∈ AlgHom.range (@mapAlg R _ S _ _) := by
  simp only [coe_mapRingHom, lifts, mapAlg_eq_map, AlgHom.mem_range, RingHom.mem_rangeS]

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