Theorems · Theorem · commutative algebra

Algebra.Smooth.exists_subalgebra_fg

∀ (R : Type u_1) [inst : CommRing R] (A : Type u) (B : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [Algebra.Smooth A B],
  ∃ A₀ B₀ x x_1, A₀.FG ∧ Algebra.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.

Defined in

Mathlib.RingTheory.Smooth.NoetherianDescent

Cited by

2 results in Mathlib

Foundations

Depth 130 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebra.Smooth