English
The relative perfect closure of F in E consists of those elements x in E for which some p-power (p^n, where p is the characteristic exponent of F) of x lies in F; it is the maximal purely inseparable subextension of E/F.
Русский
Относительное совершенное замыкание F в E состоит из элементов x ∈ E, для которых некоторый p-юпоразряд (или p^n) элемента x принадлежит F; это максимальное чисто беспрерывное подрасширение E/F.
LaTeX
$$$\text{PerfectClosure}(F,E) = \{ x \in E \mid \exists n \in \mathbb{N}, \; x^{p^n} \in \mathrm{Im}(\mathrm{algebraMap}_{F,E}) \}$$$
Lean4
/-- The relative perfect closure of `F` in `E`, consists of the elements `x` of `E` such that there
exists a natural number `n` such that `x ^ (ringExpChar F) ^ n` is contained in `F`, where
`ringExpChar F` is the exponential characteristic of `F`. It is also the maximal purely inseparable
subextension of `E / F` (`le_perfectClosure_iff`). -/
@[stacks 09HH]
def perfectClosure : IntermediateField F E
where
__ :=
have := expChar_of_injective_algebraMap (algebraMap F E).injective (ringExpChar F)
Subalgebra.perfectClosure F E (ringExpChar F)
inv_mem' := by
rintro x ⟨n, hx⟩
use n; rw [inv_pow]
apply inv_mem (id hx : _ ∈ (⊥ : IntermediateField F E))
