English
If A is essentially of finite type over a field K, then A is formally étale over K if and only if A is a finite product of separable field extensions of K.
Русский
Если A над поля K является essFiniteType, то A формально étale над K тогда и только тогда, когда A является конечным произведением сепарабельных расширений K.
LaTeX
$$$[EssFiniteType K A] : \text{FormallyEtale } K A \iff \exists I, Finite I, (A_i)_{i\in I}, (A \cong_K \prod_{i\in I} A_i) \land \forall i, Algebra.IsSeparable K (A_i)$$$
Lean4
/-- If `A` is an essentially of finite type algebra over a field `K`, then `A` is formally étale
over `K` if and only if `A` is a finite product of separable field extensions.
-/
theorem iff_exists_algEquiv_prod [EssFiniteType K A] :
FormallyEtale K A ↔
∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (_ : ∀ i, Field (Ai i)) (_ : ∀ i, Algebra K (Ai i)) (_ :
A ≃ₐ[K] Π i, Ai i), ∀ i, Algebra.IsSeparable K (Ai i) :=
by
classical
constructor
· intro H
have := FormallyUnramified.finite_of_free K A
have := FormallyUnramified.isReduced_of_field K A
have : IsArtinianRing A := isArtinian_of_tower K inferInstance
letI : Fintype (MaximalSpectrum A) := (nonempty_fintype _).some
let v (i : MaximalSpectrum A) : A := (IsArtinianRing.equivPi A).symm (Pi.single i 1)
let e : A ≃ₐ[K] _ := { __ := IsArtinianRing.equivPi A, commutes' := fun r ↦ rfl }
have := (FormallyEtale.iff_of_equiv e).mp inferInstance
rw [FormallyEtale.pi_iff] at this
exact ⟨_, inferInstance, _, _, _, e, fun I ↦ (iff_isSeparable _ _).mp inferInstance⟩
· intro ⟨I, _, Ai, _, _, e, _⟩
rw [FormallyEtale.iff_of_equiv e, FormallyEtale.pi_iff]
exact fun I ↦ of_isSeparable K (Ai I)
