English
If L is separable over K, then L is formally étale over K.
Русский
Если L над K разделимо, то L формально étale над K.
LaTeX
$$$[Algebra.IsSeparable K L] \Rightarrow \text{FormallyEtale } K L$$$
Lean4
theorem of_isSeparable [Algebra.IsSeparable K L] : FormallyEtale K L :=
by
constructor
intro B _ _ I h
refine ⟨FormallyUnramified.iff_comp_injective.mp (FormallyUnramified.of_isSeparable K L) I h, ?_⟩
intro f
have : ∀ k : L, ∃! g : K⟮k⟯ →ₐ[K] B, (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K _ L) :=
by
intro k
have := IsSeparable.of_algHom _ _ (IsScalarTower.toAlgHom K (K⟮k⟯) L)
have := IntermediateField.adjoin.finiteDimensional (Algebra.IsSeparable.isSeparable K k).isIntegral
have := FormallyEtale.of_isSeparable_aux K (K⟮k⟯)
have := FormallyEtale.comp_bijective (R := K) (A := K⟮k⟯) I h
exact this.existsUnique _
choose g hg₁ hg₂ using this
have hg₃ : ∀ x y (h : x ∈ K⟮y⟯), g y ⟨x, h⟩ = g x (IntermediateField.AdjoinSimple.gen K x) :=
by
intro x y h
have e : K⟮x⟯ ≤ K⟮y⟯ := by
rw [IntermediateField.adjoin_le_iff]
rintro _ rfl
exact h
rw [← hg₂ _ ((g _).comp (IntermediateField.inclusion e))]
· rfl
apply AlgHom.ext
intro ⟨a, _⟩
rw [← AlgHom.comp_assoc, hg₁, AlgHom.comp_assoc]
simp
have H : ∀ x y : L, ∃ α : L, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯ := by
intro x y
have : FiniteDimensional K K⟮x, y⟯ :=
by
apply IntermediateField.finiteDimensional_adjoin
intro x _; exact (Algebra.IsSeparable.isSeparable K x).isIntegral
have := IsSeparable.of_algHom _ _ (IsScalarTower.toAlgHom K (K⟮x, y⟯) L)
obtain ⟨⟨α, hα⟩, e⟩ := Field.exists_primitive_element K K⟮x, y⟯
apply_fun (IntermediateField.map (IntermediateField.val _)) at e
rw [IntermediateField.adjoin_map, ← AlgHom.fieldRange_eq_map] at e
simp only [IntermediateField.coe_val, Set.image_singleton, IntermediateField.fieldRange_val] at e
have hx : x ∈ K⟮α⟯ := e ▸ IntermediateField.subset_adjoin K { x, y } (by simp)
have hy : y ∈ K⟮α⟯ := e ▸ IntermediateField.subset_adjoin K { x, y } (by simp)
exact ⟨α, hx, hy⟩
refine ⟨⟨⟨⟨⟨fun x ↦ g x (IntermediateField.AdjoinSimple.gen K x), ?_⟩, ?_⟩, ?_, ?_⟩, ?_⟩, ?_⟩
· change g 1 1 = 1; rw [map_one]
· intro x y
obtain ⟨α, hx, hy⟩ := H x y
simp only [← hg₃ _ _ hx, ← hg₃ _ _ hy, ← map_mul, ← hg₃ _ _ (mul_mem hx hy)]
rfl
· change g 0 0 = 0; rw [map_zero]
· intro x y
obtain ⟨α, hx, hy⟩ := H x y
simp only [← hg₃ _ _ hx, ← hg₃ _ _ hy, ← map_add, ← hg₃ _ _ (add_mem hx hy)]
rfl
· intro r
change g _ (algebraMap K _ r) = _
rw [AlgHom.commutes]
· ext x
simpa using AlgHom.congr_fun (hg₁ x) (IntermediateField.AdjoinSimple.gen K x)
