Smooth algebras have Noetherian models

In this file, we show if S is a smooth R-algebra, there exists a ℤ-subalgebra of finite type R₀ and a smooth R₀-algebra S₀ such that S ≃ₐ R ⊗[R₀] S₀.

The analogous result for etale algebras is also provided.

theorem Algebra.Smooth.exists_subalgebra_fg (R : Type u_1) [CommRing R] (A : Type u) (B : Type u_2) [CommRing A] [Algebra R A] [CommRing B] [Algebra A B] [Smooth A B] : ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀), A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct (↥A₀) A B₀)

Let A be an R-algebra. If B is a smooth A-algebra, there exists an R-subalgebra of finite type A₀ of A and a smooth A₀-algebra B₀ such that B ≃ₐ A ⊗[A₀] B₀. See Algebra.Smooth.exists_finiteType for a version in terms of Function.Injective.

@[deprecated Algebra.Smooth.exists_subalgebra_fg (since := "2026-01-07")]

theorem Algebra.Smooth.exists_subalgebra_finiteType (R : Type u_1) [CommRing R] (A : Type u) (B : Type u_2) [CommRing A] [Algebra R A] [CommRing B] [Algebra A B] [Smooth A B] : ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀), FiniteType R ↥A₀ ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct (↥A₀) A B₀)

theorem Algebra.Smooth.exists_finiteType (R : Type u_1) [CommRing R] (A : Type u) (B : Type u_2) [CommRing A] [Algebra R A] [CommRing B] [Algebra A B] [Smooth A B] : ∃ (A₀ : Type u) (B₀ : Type u) (x : CommRing A₀) (x_1 : CommRing B₀) (x_2 : Algebra R A₀) (x_3 : Algebra A₀ A) (x_4 : Algebra A₀ B₀), Function.Injective ⇑(algebraMap A₀ A) ∧ FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct A₀ A B₀)

Let A be an R-algebra. If B is a smooth A-algebra, there exists an R-algebra of finite type A₀ and a smooth A₀-algebra B₀ such that B ≃ₐ A ⊗[A₀] B₀ with A₀ → A injective. See Algebra.Smooth.exists_subalgebra_fg for a version in terms of Subalgebra.

theorem Algebra.IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg (R : Type u_1) [CommRing R] (A : Type u) (B : Type u_2) [CommRing A] [Algebra R A] [CommRing B] [Algebra A B] (n : ℕ) [IsStandardSmoothOfRelativeDimension n A B] : ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀), A₀.FG ∧ IsStandardSmoothOfRelativeDimension n (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct (↥A₀) A B₀)

theorem Algebra.Etale.exists_subalgebra_fg (R : Type u_1) [CommRing R] (A : Type u) (B : Type u_2) [CommRing A] [Algebra R A] [CommRing B] [Algebra A B] [Etale A B] : ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀), A₀.FG ∧ Etale (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] TensorProduct (↥A₀) A B₀)

Let A be an R-algebra. If B is an etale A-algebra, there exists an R-subalgebra of finite type A₀ of A and an etale A₀-algebra B₀ such that B ≃ₐ A ⊗[A₀] B₀.