English
Let A be an algebra over a field K. Then A is étale over K if and only if A is isomorphic to a finite direct product of finite separable field extensions of K; equivalently, there exists a finite indexing set I and a family of fields {A_i} each carrying a K-algebra structure such that A ≅ ∏_{i∈I} A_i and, for every i, A_i is a finite separable extension of K.
Русский
Пусть A — алгебра над полем K. Тогда A эквивалентна (соответственно изоморфна) конечному произведению полей, полученных как конечные сепаровские расширения K, то есть A ≅ ∏_{i∈I} A_i, где I — конечное множество, и для каждого i алгебра Ai над K является конечным сепарабельным расширением K.
LaTeX
$$$\\operatorname{Etale}(K,A) \\iff \\exists I : \\text{Type}, \\#I < \\infty \\land (\\forall i \\in I, \\text{Field}(A_i) \\land \\text{Algebra}_K(A_i) ) \\land A \\cong_K \\prod_{i \\in I} A_i \\land \\forall i, \\operatorname{Fin}(A_i) \\land \\operatorname{IsSeparable}(K,A_i).$$$
Lean4
/-- `A` is étale over a field `K` if and only if
`A` is a finite product of finite separable field extensions.
-/
theorem iff_exists_algEquiv_prod :
Etale 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, Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i) :=
by
constructor
· intro H
obtain ⟨I, _, Ai, _, _, e, _⟩ := (FormallyEtale.iff_exists_algEquiv_prod K A).mp inferInstance
have := FormallyUnramified.finite_of_free K A
exact
⟨_, ‹_›, _, _, _, e, fun i ↦
⟨.of_surjective ((LinearMap.proj i).comp e.toLinearMap) ((Function.surjective_eval i).comp e.surjective),
inferInstance⟩⟩
· intro ⟨I, _, Ai, _, _, e, H⟩
choose h₁ h₂ using H
have := Module.Finite.of_surjective e.symm.toLinearMap e.symm.surjective
refine ⟨?_, FinitePresentation.of_finiteType.mp inferInstance⟩
exact (FormallyEtale.iff_exists_algEquiv_prod K A).mpr ⟨_, inferInstance, _, _, _, e, h₂⟩
