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
    Instances For
      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
        Instances For
          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.