Documentation

Mathlib.RingTheory.RingHom.StandardSmooth

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) :

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

Equations

Instances For

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) :

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

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