Theorems · Definition · commutative algebra

StandardEtalePair.homEquiv

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

Maps out of R[X][Y]/⟨f, Yg-1⟩ corresponds bijectively with x such that f(x) = 0 and g(x) is invertible.

Defined in

Mathlib.RingTheory.Etale.StandardEtale

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra