Theorems · Definition · commutative algebra

StandardEtalePair.lift

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : StandardEtalePair R) → (x : S) → P.HasMap x → P.Ring →ₐ[R] S

The map R[X][Y]/⟨f, Yg-1⟩ →ₐ[R] S sending X to x, given P.HasMap x.

Defined in

Mathlib.RingTheory.Etale.StandardEtale

Cited by

15 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra