separable_map — Mathlib

English

Let f: F →* S be a ring homomorphism with F,S fields. Then, for any p ∈ F[X], p.map f is separable in S[X] iff p is separable in F[X].

Русский

Пусть f: F →* S — кольцевой однородник между полями. Тогда для любого p ∈ F[X], p.map f сепарабелен в S[X] тогда и только тогда, когда p сепарабелен в F[X].

LaTeX

$$$ (p.map\ f).Separable \iff p.Separable$$$

Lean4

theorem separable_map {S} [CommRing S] [Nontrivial S] (f : F →+* S) {p : F[X]} : (p.map f).Separable ↔ p.Separable :=
  by
  refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
  obtain ⟨m, hm⟩ := Ideal.exists_maximal S
  have := Separable.map H (f := Ideal.Quotient.mk m)
  rwa [map_map, separable_def, derivative_map, isCoprime_map] at this

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