Theorems · Definition · algebraic geometry

Algebra.IsSmoothAt

(R : Type u_1) →
  {A : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → (p : Ideal A) → [p.IsPrime] → Prop

An R-algebra A is smooth at a prime p of A if Aₚ is formally smooth over R. This does not imply Aₚ is smooth over R under the mathlib definition even if A is finitely presented, but it can be shown that this is equivalent to the stacks project definition that A is smooth at p if and only if there exists f ∉ p such that A_f is smooth over R. See Algebra.basicOpen_subset_smoothLocus_iff_smooth and Algebra.isOpen_smoothLocus.

Defined in

Mathlib.RingTheory.Smooth.Locus

Cited by

6 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

CommRingCommRingAlgebraIdeal.IsPrime