theorem Algebra.isGeometricallyReduced_of_isAlgClosed_of_isReduced (k : Type u_1) [Field k] [IsAlgClosed k] (A : Type u_2) [CommRing A] [Algebra k A] [IsReduced A] : IsGeometricallyReduced k A

Over an algebraically closed field k, a reduced k-algebra is geometrically reduced: tensoring with the algebraic closure preserves the absence of nilpotents.

theorem exists_algHom_ne_zero_of_ne_zero (k : Type u_1) [Field k] [IsAlgClosed k] (A : Type u_2) [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [IsReduced A] [Nontrivial A] {a : A} (ha : a ≠ 0) : ∃ (φ : A →ₐ[k] k), φ a ≠ 0

Nullstellensatz-style separating property: for a finitely generated reduced k-algebra over an algebraically closed field, any nonzero element is detected by some k-algebra homomorphism into k.

theorem repr_eval_eq_phi_coeff {k : Type u_1} [Field k] {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] {ι : Type u_4} [DecidableEq ι] (b : Module.Basis ι k B) (φ : A →ₐ[k] k) (x : TensorProduct k A B) (j : ι) (tensorIso : TensorProduct k A B ≃ₗ[k] ι →₀ A) (htiso : tensorIso = TensorProduct.congr (LinearEquiv.refl k A) b.repr ≪≫ₗ TensorProduct.finsuppScalarRight k k A ι) : (b.repr (((↑(Algebra.TensorProduct.lid k B)).comp (Algebra.TensorProduct.map φ (AlgHom.id k B))) x)) j = φ ((tensorIso x) j)

Commutation lemma: evaluating the B-basis representation of the image of x ∈ A ⊗ B under φ ⊗ id matches applying φ to the A-coordinate from the tensor-to-finsupp isomorphism.

theorem tensorProduct_isReduced_of_isAlgClosed_finiteType (k : Type u_1) [Field k] [IsAlgClosed k] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] [IsReduced A] [IsReduced B] [Algebra.FiniteType k A] : IsReduced (TensorProduct k A B)

Finite-type special case of Lemma 15, Lec 7: if A is a finite-type reduced k-algebra (over an algebraically closed k) and B is any reduced k-algebra, then A ⊗_k B is reduced.

theorem tensor_product_reduced_of_algClosed (k : Type u_1) [Field k] [IsAlgClosed k] (A : Type u_2) [CommRing A] [Algebra k A] [IsReduced A] (B : Type u_3) [CommRing B] [Algebra k B] [IsReduced B] : IsReduced (TensorProduct k A B)

Lemma 15, Lec 7: over an algebraically closed field k, the tensor product A ⊗_k B of two reduced k-algebras has no nilpotents.