Theorems · Theorem · commutative algebra

Polynomial.induction_of_Splits_of_injective_of_surjective

∀ {R : Type u} [inst : CommRing R] (p : Polynomial R) (P : {R : Type u} → [inst : CommRing R] → Polynomial R → Prop),
  (∀ (R : Type u) [inst : Field R] (p : Polynomial R), p.Splits → P p) →
    (∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
        Function.Injective ⇑φ → ∀ (p : Polynomial R), P (Polynomial.map φ p) → P p) →
      (∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
          Function.Surjective ⇑φ → ∀ (p : Polynomial S), (∀ (q : Polynomial R), P q) → P p) →
        P p

An induction principle useful to prove statements about resultants. Let P be a predicate on a polynomial. If R → S injective implies (∀ p : S[X], P p) → (∀ p : R[X], P p), and if R → S surjective implies (∀ p : R[X], P p) → (∀ p : S[X], P p), then we may reduce to the case where R is a field and p splits.

Defined in

Mathlib.RingTheory.Polynomial.Resultant.Basic

Cited by

4 results in Mathlib

Foundations

Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing