Theorems · Theorem · commutative algebra

Algebra.FormallySmooth.of_formallySmooth_residueField_tensor

∀ {R : Type u_1} {S : Type u_2} {P : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Module.Flat R S] [inst_4 : CommRing P] [inst_5 : Algebra R P] [inst_6 : Algebra P S] [IsScalarTower R P S]
  [inst_8 : IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
  [Algebra.FormallySmooth (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) S)]
  (M : Submonoid P) [IsLocalization M S] [Algebra.FinitePresentation R P], Algebra.FormallySmooth R S

Let (R, m, k) be a local ring, S be a local R-algebra that is flat, essentially of finite presentation, and k ⊗[R] S is k-formally smooth. Then S is R-formally smooth. Since we don't have an "essentially of finite presentation" type class yet, we explicitly require a P that is of finite presentation over R and that S is a localization of it.

Defined in

Mathlib.RingTheory.Smooth.Fiber

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraModule.FlatCommRingAlgebraAlgebraIsScalarTowerIsLocalRingIsLocalRingIsLocalHomAlgebra.FormallySmoothIsLocalizationAlgebra.FinitePresentation