splits_comp_of_splits — Mathlib

English

Let i: R→K and j: K→L be ring homomorphisms. If f splits after the composition j ∘ i, then f splits after i provided the image roots lie in the range of j.

Русский

Пусть i: R→K и j: K→L — гомоморфизмы колец. Если f распадается после композиции j ∘ i, то распадается после i при условии, что корни отображаются в образе j.

LaTeX

$$$\forall i: R\toK,\, j: K\to L,\forall f: R[X],\ Splits (j\circ i) f \Rightarrow (\forall a\in (f.map (j\circ i)).roots, a\in j.range) \Rightarrow Splits i f$$$

Lean4

theorem splits_comp_of_splits (i : R →+* K) (j : K →+* L) {f : R[X]} (h : Splits i f) : Splits (j.comp i) f :=
  (splits_map_iff i j).mp (splits_of_splits_id _ <| (splits_map_iff i <| .id K).mpr h)

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