Tracking issue: The Tilting Equivalence of Perfectoid Fields

This issue is meant to track PRs on the development of the theory of perfectoid fields. This issue belongs to a broader project of proving the Fontaine-Wintenberger theorem.

Rough roadmap

• define Fontaine's theta map
• build the tilting equivalence for integral perfectoid rings
• define the perfectoid fields and show its relation with integral perfectoid rings
• show that the tilt of a perfectoid field is still perfectoid (to be decomposed later)
• define the tilt of the morphism
• define the category of perfectoid fields and the tilting functor
• show that char p perfectoid field is just a rank 1 valued perfect char p field

Open or already closed PRs on this topic

Preliminaries

• #21582 [IsAdicComplete]

Krasner's lemma

Witt vectors

• #21295 [p-adic completeness]
• #21564 [Fontaine's theta map]

Integral perfectoid rings

• #21563 [the untilt map]
• Integral perfectoid ring and perfectoid pseudo-uniformizer

Perfectoid fields

• Valued perfectoid field and perfectoid field, char p case

Almost mathemetics

The final result

Start with the roadmap and the referenced PRs, especially #21564 and #21563, to understand which parts of the tilting-equivalence development remain open. The issue does not name files, tests, or a single concrete deliverable, so completion criteria must be clarified before implementation.