Finitely generated subalgebras of a base change obtained from an element

Main results

• exists_fg_and_mem_baseChange: given an element x of a tensor product A ⊗[R] B of two R-algebras A and B, there exists a finitely generated subalgebra C of B such that x is contained in C ⊗[R] B.

theorem exists_fg_and_mem_baseChange {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] (x : TensorProduct R A B) : ∃ (C : Subalgebra R B), C.FG ∧ x ∈ Subalgebra.baseChange A C