Documentation

Mathlib.RingTheory.RingHom.StandardSmooth

Standard smooth ring homomorphisms #

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

Notes #

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

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

A ring homomorphism R →+* S is standard smooth if S is standard smooth as R-algebra.

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

    Helper lemma for the algebraize tactic.

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

    A ring homomorphism R →+* S is standard smooth of relative dimension n if S is standard smooth of relative dimension n as R-algebra.

    Equations
    Instances For
      source
      theorem RingHom.IsStandardSmoothOfRelativeDimension.toAlgebra (n : ℕ) {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} (hf : RingHom.IsStandardSmoothOfRelativeDimension n f) :
      Algebra.IsStandardSmoothOfRelativeDimension n R S

      Helper lemma for the algebraize tactic.

      source
      theorem RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth (n : ℕ) {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : RingHom.IsStandardSmoothOfRelativeDimension n f) :
      f.IsStandardSmooth
      source
      theorem RingHom.IsStandardSmoothOfRelativeDimension.id (R : Type u) [CommRing R] :
      RingHom.IsStandardSmoothOfRelativeDimension 0 (RingHom.id R)
      source
      theorem RingHom.IsStandardSmoothOfRelativeDimension.equiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] (e : R ≃+* S) :
      RingHom.IsStandardSmoothOfRelativeDimension 0 ↑e
      source
      theorem RingHom.IsStandardSmooth.comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] {T : Type u_1} [CommRing T] {g : S →+* T} {f : R →+* S} (hg : g.IsStandardSmooth) (hf : f.IsStandardSmooth) :
      (g.comp f).IsStandardSmooth
      source
      theorem RingHom.IsStandardSmoothOfRelativeDimension.comp {n : ℕ} {m : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {T : Type u_1} [CommRing T] {g : S →+* T} {f : R →+* S} (hg : RingHom.IsStandardSmoothOfRelativeDimension n g) (hf : RingHom.IsStandardSmoothOfRelativeDimension m f) :
      RingHom.IsStandardSmoothOfRelativeDimension (n + m) (g.comp f)
      source
      theorem RingHom.isStandardSmooth_stableUnderComposition :
      RingHom.StableUnderComposition @RingHom.IsStandardSmooth
      source
      theorem RingHom.isStandardSmooth_respectsIso :
      RingHom.RespectsIso @RingHom.IsStandardSmooth
      source
      theorem RingHom.isStandardSmoothOfRelativeDimension_respectsIso {n : ℕ} :
      RingHom.RespectsIso (@RingHom.IsStandardSmoothOfRelativeDimension n)
      source
      theorem RingHom.isStandardSmooth_stableUnderBaseChange :
      RingHom.StableUnderBaseChange @RingHom.IsStandardSmooth
      source
      theorem RingHom.isStandardSmoothOfRelativeDimension_stableUnderBaseChange (n : ℕ) :
      RingHom.StableUnderBaseChange (@RingHom.IsStandardSmoothOfRelativeDimension n)
      source
      theorem RingHom.IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway {R : Type u} [CommRing R] {Rᵣ : Type u_2} [CommRing Rᵣ] [Algebra R Rᵣ] (r : R) [IsLocalization.Away r Rᵣ] :
      RingHom.IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)
      source
      theorem RingHom.isStandardSmooth_localizationPreserves :
      RingHom.LocalizationPreserves fun {R S : Type u_2} [CommRing R] [CommRing S] => RingHom.IsStandardSmooth
      source
      theorem RingHom.isStandardSmoothOfRelativeDimension_localizationPreserves (n : ℕ) :
      RingHom.LocalizationPreserves fun {R S : Type u_2} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension n
      source
      theorem RingHom.isStandardSmooth_holdsForLocalizationAway :
      RingHom.HoldsForLocalizationAway fun {R S : Type u_2} [CommRing R] [CommRing S] => RingHom.IsStandardSmooth
      source
      theorem RingHom.isStandardSmoothOfRelativeDimension_holdsForLocalizationAway :
      RingHom.HoldsForLocalizationAway fun {R S : Type u_2} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension 0
      source
      theorem RingHom.isStandardSmooth_stableUnderCompositionWithLocalizationAway :
      RingHom.StableUnderCompositionWithLocalizationAway fun {R S : Type u_2} [CommRing R] [CommRing S] => RingHom.IsStandardSmooth
      source
      theorem RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway (n : ℕ) :
      RingHom.StableUnderCompositionWithLocalizationAway fun {R S : Type u_2} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension n