Theorems · Theorem · commutative algebra

RingHom.FinitePresentation.polynomial_induction

∀ (P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop)
  (Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop),
  (∀ (R : Type u) [inst : CommRing R], P R (Polynomial R) Polynomial.C) →
    (∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
        Function.Surjective ⇑f → (RingHom.ker f).FG → Q R S f) →
      (∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T]
          (f : R →+* S) (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)) →
        ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
          f.FinitePresentation → Q R S f

Induction principle for finitely presented ring homomorphisms. For a property to hold for all finitely presented ring homs, it suffices for it to hold for Polynomial.C : R → R[X], surjective ring homs with finitely generated kernels, and to be closed under composition. Note that to state this conveniently for ring homs between rings of different universes, we carry around two predicates P and Q, which should be "the same" apart from universes: * P, for ring homs (R : Type u) → (S : Type u). * Q, for ring homs (R : Type u) → (S : Type v).

Defined in

Mathlib.RingTheory.FinitePresentation

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRing