Theorems · Definition · commutative algebra

StandardEtalePair.HasMap

{R : Type u_1} →
  {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → StandardEtalePair R → S → Prop

There is a map from a standard etale algebra R[X][Y]/⟨f, Yg-1⟩ to S sending X to x iff f(x) = 0 and g(x) is invertible. Also see StandardEtalePair.homEquiv.

Defined in

Mathlib.RingTheory.Etale.StandardEtale

Cited by

14 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra