Documentation

Mathlib.RingTheory.RingHom.Smooth

Smooth ring homomorphisms #

In this file we define smooth ring homomorphisms and show their meta properties.

source
def RingHom.FormallySmooth {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) :
Prop

A ring homomorphism f : R →+* S is formally smooth if S is formally smooth as an R algebra.

Equations
source
theorem RingHom.FormallySmooth.toAlgebra {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.FormallySmooth) :
Algebra.FormallySmooth R S

Helper lemma for the algebraize tactic

source
theorem RingHom.formallySmooth_algebraMap {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] :
(algebraMap R S).FormallySmooth ↔ Algebra.FormallySmooth R S
source
theorem RingHom.FormallySmooth.holdsForLocalizationAway :
HoldsForLocalizationAway @FormallySmooth
source
theorem RingHom.FormallySmooth.stableUnderComposition :
StableUnderComposition @FormallySmooth
source
theorem RingHom.FormallySmooth.respectsIso :
RespectsIso @FormallySmooth
source
theorem RingHom.FormallySmooth.isStableUnderBaseChange :
IsStableUnderBaseChange @FormallySmooth
source
theorem RingHom.FormallySmooth.localizationPreserves :
LocalizationPreserves @FormallySmooth
source
def RingHom.Smooth {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) :
Prop

A ring homomorphism f : R →+* S is smooth if S is smooth as an R algebra.

Equations
source
theorem RingHom.Smooth.toAlgebra {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Smooth) :
Algebra.Smooth R S

Helper lemma for the algebraize tactic

source
theorem RingHom.smooth_algebraMap {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] :
(algebraMap R S).Smooth ↔ Algebra.Smooth R S
source
theorem RingHom.smooth_def {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} :
f.Smooth ↔ f.FormallySmooth ∧ f.FinitePresentation
source
theorem RingHom.Smooth.stableUnderComposition :
StableUnderComposition fun {R S : Type u_1} [CommRing R] [CommRing S] => Smooth
source
theorem RingHom.Smooth.isStableUnderBaseChange :
IsStableUnderBaseChange fun {R S : Type u_1} [CommRing R] [CommRing S] => Smooth
source
theorem RingHom.Smooth.holdsForLocalizationAway :
HoldsForLocalizationAway fun {R S : Type u_1} [CommRing R] [CommRing S] => Smooth
source
theorem RingHom.Smooth.id (R : Type u) [CommRing R] :
(RingHom.id R).Smooth

The identity of a ring is smooth.

source
theorem RingHom.Smooth.comp {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.Smooth) (hg : g.Smooth) :
(g.comp f).Smooth

Composition of smooth ring homomorphisms is smooth.

source
theorem RingHom.Smooth.ofLocalizationSpanTarget :
OfLocalizationSpanTarget fun {R S : Type u_1} [CommRing R] [CommRing S] => Smooth
source
theorem RingHom.Smooth.propertyIsLocal :
PropertyIsLocal fun {R S : Type u_1} [CommRing R] [CommRing S] => Smooth

Smoothness is a local property of ring homomorphisms.