Theorems · Theorem · commutative algebra

IsReduced.tensorProduct_of_flat_of_forall_fg

∀ {R : Type u_1} {C : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring C] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : Algebra R C] [Module.Flat R C],
  (∀ (B : Subalgebra R A), B.FG → IsReduced (TensorProduct R C ↥B)) → IsReduced (TensorProduct R C A)

Let R be a commutative semiring, let C be a commutative R-algebra, and let A be an R-algebra. If C ⊗[R] B is reduced for all finitely generated subalgebras B of A, then C ⊗[R] A is also reduced.

Defined in

Mathlib.RingTheory.Flat.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringSemiringAlgebraAlgebraModule.Flat