Smooth is locally standard smooth

In this file we show that a ring homomorphism is smooth if and only if it is locally standard smooth.

theorem RingHom.IsStandardSmooth.smooth {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IsStandardSmooth) : f.Smooth

Any standard smooth ring homomorphism is smooth.

theorem RingHom.Smooth.locally_isStandardSmooth {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Smooth) : Locally (fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardSmooth) f

Any smooth ring homomorphism is locally standard smooth.

theorem RingHom.smooth_iff_locally_isStandardSmooth {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} : f.Smooth ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardSmooth) f

A ring homomorphism is smooth if and only if it is locally standard smooth.

theorem RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} : f.Etale ↔ IsStandardSmoothOfRelativeDimension 0 f

A ring homomorphism is étale if and only if it is standard smooth of relative dimension 0.