Stability of finiteness conditions in commutative algebra

In this file we show that Algebra.FiniteType and Algebra.FinitePresentation are stable under base change.

theorem Algebra.FiniteType.baseChangeAux_surj {R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] {σ : Type u_1} {f : MvPolynomial σ R →ₐ[R] A} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(Algebra.TensorProduct.map (AlgHom.id B B) f)

instance Algebra.FiniteType.baseChange {R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] [hfa : Algebra.FiniteType R A] : Algebra.FiniteType B (TensorProduct R B A)

Equations

• ⋯ = ⋯

instance Algebra.FinitePresentation.baseChange {R : Type w₁} [CommRing R] {A : Type w₂} [CommRing A] [Algebra R A] (B : Type w₃) [CommRing B] [Algebra R B] [Algebra.FinitePresentation R A] : Algebra.FinitePresentation B (TensorProduct R B A)

Equations

• ⋯ = ⋯