Standard smooth ring homomorphisms

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

Main definitions

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

Notes

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

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.

theorem RingHom.isStandardSmooth_algebraMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] : (algebraMap R S).IsStandardSmooth ↔ Algebra.IsStandardSmooth R S

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

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.

theorem RingHom.isStandardSmoothOfRelativeDimension_algebraMap (n : ℕ) {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] : IsStandardSmoothOfRelativeDimension n (algebraMap R S) ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S

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

Helper lemma for the algebraize tactic

theorem RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth (n : ℕ) {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : IsStandardSmoothOfRelativeDimension n f) : f.IsStandardSmooth

theorem RingHom.IsStandardSmoothOfRelativeDimension.id (R : Type u) [CommRing R] : IsStandardSmoothOfRelativeDimension 0 (RingHom.id R)

theorem RingHom.IsStandardSmoothOfRelativeDimension.equiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] (e : R ≃+* S) : IsStandardSmoothOfRelativeDimension 0 ↑e

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

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 : IsStandardSmoothOfRelativeDimension n g) (hf : IsStandardSmoothOfRelativeDimension m f) : IsStandardSmoothOfRelativeDimension (n + m) (g.comp f)

theorem RingHom.isStandardSmooth_stableUnderComposition : StableUnderComposition @IsStandardSmooth

theorem RingHom.isStandardSmooth_respectsIso : RespectsIso @IsStandardSmooth

theorem RingHom.isStandardSmoothOfRelativeDimension_respectsIso {n : ℕ} : RespectsIso (@IsStandardSmoothOfRelativeDimension n)

theorem RingHom.isStandardSmooth_isStableUnderBaseChange : IsStableUnderBaseChange @IsStandardSmooth

theorem RingHom.isStandardSmoothOfRelativeDimension_isStableUnderBaseChange (n : ℕ) : IsStableUnderBaseChange (@IsStandardSmoothOfRelativeDimension n)

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ᵣ] : IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)

theorem RingHom.isStandardSmooth_localizationPreserves : LocalizationPreserves fun {R S : Type u_2} [CommRing R] [CommRing S] => IsStandardSmooth

theorem RingHom.isStandardSmoothOfRelativeDimension_localizationPreserves (n : ℕ) : LocalizationPreserves fun {R S : Type u_2} [CommRing R] [CommRing S] => IsStandardSmoothOfRelativeDimension n

theorem RingHom.isStandardSmooth_holdsForLocalizationAway : HoldsForLocalizationAway fun {R S : Type u_2} [CommRing R] [CommRing S] => IsStandardSmooth

theorem RingHom.isStandardSmoothOfRelativeDimension_holdsForLocalizationAway : HoldsForLocalizationAway fun {R S : Type u_2} [CommRing R] [CommRing S] => IsStandardSmoothOfRelativeDimension 0

theorem RingHom.isStandardSmooth_stableUnderCompositionWithLocalizationAway : StableUnderCompositionWithLocalizationAway fun {R S : Type u_2} [CommRing R] [CommRing S] => IsStandardSmooth

theorem RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway (n : ℕ) : StableUnderCompositionWithLocalizationAway fun {R S : Type u_2} [CommRing R] [CommRing S] => IsStandardSmoothOfRelativeDimension n

theorem Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial (n : ℕ) (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [IsStandardSmoothOfRelativeDimension n R S] : ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale

Every standard smooth homomorphism R → S factors into R -> R[X₁,...,Xₙ] → S where n is the relative dimension and R[X₁,...,Xₙ] → S is etale.

theorem RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} {n : ℕ} (hf : IsStandardSmoothOfRelativeDimension n f) : ∃ (g : MvPolynomial (Fin n) R →+* S), g.comp MvPolynomial.C = f ∧ g.Etale

Every standard smooth homomorphism R → S factors into R -> R[X₁,...,Xₙ] → S where n is the relative dimension and R[X₁,...,Xₙ] → S is etale.

theorem RingHom.IsStandardSmooth.exists_etale_mvPolynomial {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IsStandardSmooth) : ∃ (n : ℕ) (g : MvPolynomial (Fin n) R →+* S), g.comp MvPolynomial.C = f ∧ g.Etale