Some lemmas about formally smooth under quotient #
In this file, we formalize the result [Stacks 031L] : 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.
theorem
LinearMap.ker_inf_smul_top_eq_smul_of_flat
{R : Type u_1}
[CommRing R]
{M : Type u_2}
{N : Type u_3}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(I : Ideal R)
(f : M →ₗ[R] N)
(surj : Function.Surjective ⇑f)
[Module.Flat R N]
:
For any surjection f : M →ₗ[R] N, with N a flat R-module,
we have K ⊓ IM = IK for any I : Ideal R.
theorem
Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{R' : Type u_3}
{S' : Type u_4}
[CommRing R']
[CommRing S']
[Algebra R S]
[Algebra R R']
[Algebra R' S']
[Algebra S S']
[Algebra R S']
[IsScalarTower R S S']
[IsScalarTower R R' S']
[Module.Flat R S]
(surj : Function.Surjective ⇑(algebraMap R R'))
(surjS : Function.Surjective ⇑(algebraMap S S'))
(eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R')))
(sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥)
(smoothq : FormallySmooth R' S')
:
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.
theorem
RingHom.FormallySmooth.of_flat_of_ker_eq_map_of_square_zero
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{R' : Type u_3}
{S' : Type u_4}
[CommRing R']
[CommRing S']
(f : R →+* S)
(flat : f.Flat)
(qR : R →+* R')
(qS : S →+* S')
(g : R' →+* S')
(surjR : Function.Surjective ⇑qR)
(surjS : Function.Surjective ⇑qS)
(comm : qS.comp f = g.comp qR)
(sq0 : ker qR ^ 2 = ⊥)
(eqmap : ker qS = Ideal.map f (ker qR))
(smoothq : g.FormallySmooth)
:
A pure RingHom variant of Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat