Theorems · Theorem · commutative algebra

Algebra.Etale.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.Etale A B],
  ∃ A₀ B₀ x x_1, A₀.FG ∧ Algebra.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₀.

Defined in

Mathlib.RingTheory.Smooth.NoetherianDescent

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebra.Etale