Theorems · Theorem · commutative algebra

Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat

∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {R' : Type u_3} {S' : Type u_4}
  [inst_2 : CommRing R'] [inst_3 : CommRing S'] [inst_4 : Algebra R S] [inst_5 : Algebra R R'] [inst_6 : Algebra R' S']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [IsScalarTower R S S'] [IsScalarTower R R' S'] [Module.Flat R S],
  Function.Surjective ⇑(algebraMap R R') →
    Function.Surjective ⇑(algebraMap S S') →
      RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R')) →
        RingHom.ker (algebraMap R R') ^ 2 = ⊥ → Algebra.FormallySmooth R' S' → Algebra.FormallySmooth R S

For flat ring homomorphism f : R →+* S, I an ideal of R which is square zero, if R ⧸ I →+* S ⧸ IS is formally smooth, so is f.

Defined in

Mathlib.RingTheory.Smooth.Quotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingCommRingAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerModule.Flat