Theorems · Definition · algebraic geometry

HasStandardEtaleSurjectionOn

(R : Type u_1) → {S : Type u_3} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → S → Prop

The predicate "there exists a standard etale algebra A over R that surjects onto S[1/f]". We shall show if S is R-unramified at Q then there exists f ∉ Q satisfying it.

Defined in

Mathlib.RingTheory.Unramified.LocalStructure

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra