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 : Type u_1} {S : Type u_2} [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
Instances For
    source
    theorem RingHom.FormallySmooth.toAlgebra {R : Type u_1} {S : Type u_2} [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 : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] :
    (algebraMap R S).FormallySmooth ↔ Algebra.FormallySmooth R S
    source
    theorem RingHom.FormallySmooth.comp {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {T : Type u_3} [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.FormallySmooth) (hg : g.FormallySmooth) :
    (g.comp f).FormallySmooth

    Composition of formally smooth ring homomorphisms is formally smooth.

    source
    theorem RingHom.FormallySmooth.of_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Bijective ⇑f) :
    f.FormallySmooth
    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 : Type u_1} {S : Type u_2} [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
    Instances For
      source
      theorem RingHom.Smooth.toAlgebra {R : Type u_1} {S : Type u_2} [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 : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] :
      (algebraMap R S).Smooth ↔ Algebra.Smooth R S
      source
      theorem RingHom.smooth_def {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} :
      f.Smooth ↔ f.FormallySmooth ∧ f.FinitePresentation
      source
      theorem RingHom.Smooth.formallySmooth {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Smooth) :
      f.FormallySmooth
      source
      theorem RingHom.Smooth.finitePresentation {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Smooth) :
      f.FinitePresentation
      source
      theorem RingHom.Smooth.comp {R : Type u_3} {S : Type u_4} {T : Type u_5} [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.stableUnderComposition :
      StableUnderComposition fun {R S : Type u_6} [CommRing R] [CommRing S] => Smooth
      source
      theorem RingHom.Smooth.isStableUnderBaseChange :
      IsStableUnderBaseChange fun {R S : Type u_6} [CommRing R] [CommRing S] => Smooth
      source
      theorem RingHom.Smooth.holdsForLocalizationAway :
      HoldsForLocalizationAway fun {R S : Type u_6} [CommRing R] [CommRing S] => Smooth
      source
      theorem RingHom.Smooth.of_bijective {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Bijective ⇑f) :
      f.Smooth
      source
      theorem RingHom.Smooth.id (R : Type u_3) [CommRing R] :
      (RingHom.id R).Smooth

      The identity of a ring is smooth.

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

      Smoothness is a local property of ring homomorphisms.

      source
      theorem RingHom.Smooth.respectsIso :
      RespectsIso fun {R S : Type u_6} [CommRing R] [CommRing S] => Smooth