theorem
formallyUnramified_baseChange
{K : Type u_1}
[Field K]
{B : Type u_2}
[CommRing B]
[Algebra K B]
[Algebra.FormallyUnramified K B]
{Ω : Type u_3}
[CommRing Ω]
[Algebra K Ω]
:
Algebra.FormallyUnramified Ω (TensorProduct K Ω B)
theorem
sep_tensor_reduced
(K : Type u_1)
[Field K]
(L : Type u_2)
[Field L]
[Algebra K L]
[Algebra.IsSeparable K L]
(Ω : Type u_3)
[Field Ω]
[Algebra K Ω]
:
IsReduced (TensorProduct K L Ω)
theorem
isReduced_pi_tensor
(K : Type u_1)
[Field K]
(ι : Type)
[Fintype ι]
(F : ι → Type)
[(i : ι) → Field (F i)]
[(i : ι) → Algebra K (F i)]
[∀ (i : ι), Algebra.IsSeparable K (F i)]
(Ω : Type u_2)
[Field Ω]
[Algebra K Ω]
:
IsReduced (TensorProduct K ((i : ι) → F i) Ω)
theorem
isEtaleAlgebra_of_isSemisimpleRing_tensor_algClosure
(K : Type u)
[Field K]
(B : Type v)
[CommRing B]
[Algebra K B]
[Module.Finite K B]
(h : IsSemisimpleRing (TensorProduct K B (AlgebraicClosure K)))
: