perfectField_of_perfectClosure_eq_bot

English

Repeated q-powers yield a basis under separability.

Русский

Повторное возведение в q-ую степень сохраняет базис.

LaTeX

$$$\text{Basis}^{q^n}$ is a basis$$

Lean4

theorem perfectField_of_perfectClosure_eq_bot [h : PerfectField E] (eq : perfectClosure F E = ⊥) : PerfectField F :=
  by
  let p := ringExpChar F
  haveI := expChar_of_injective_algebraMap (algebraMap F E).injective p
  haveI :=
    PerfectRing.ofSurjective F p fun x ↦
      by
      obtain ⟨y, h⟩ := surjective_frobenius E p (algebraMap F E x)
      have : y ∈ perfectClosure F E := ⟨1, x, by rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]⟩
      obtain ⟨z, rfl⟩ := eq ▸ this
      simp only [Algebra.ofId] at h
      exact ⟨z, (algebraMap F E).injective (by rw [RingHom.map_frobenius]; rw [h])⟩
  exact PerfectRing.toPerfectField F p

Похожие утверждения