PerfectClosure — Mathlib

English

Define the perfect closure as the smallest extension in which Frobenius is surjective; this is built as a quotient of a construction R K p.

Русский

Определим совершенное закрытие как наименьшее расширение, в котором Фробениус сюръективен; это строится как фактор по конструкции R K p.

LaTeX

$$$\text{PerfectClosure}(K,p) = \mathrm{Quot}(\mathrm{PerfectClosure.R}\; K\; p)$$$

Lean4

/-- The perfect closure is the smallest extension that makes frobenius surjective. -/
def PerfectClosure : Type u :=
  Quot (PerfectClosure.R K p)

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