Definitions/Def_PadicComplex_TateTrace.lean

Fix a prime p and work with \overline{\mathbb{Q}}_p (PadicAlgCl p) and its completion \mathbb{C}_p, on which the group \operatorname{Gal}(\overline{\mathbb{Q}}_p/\mathbb{Q}_p) acts by the isometric, continuous extension of its action on \overline{\mathbb{Q}}_p. Given a family (K_m)_{m\in\mathbb{N}} of intermediate fields \mathbb{Q}_p \subseteq K_m \subseteq \overline{\mathbb{Q}}_p, PadicComplex.towerClosure p Km is the subset X \subseteq \mathbb{C}_p obtained as the topological closure of \bigcup_m K_m, each K_m being viewed in \mathbb{C}_p through \overline{\mathbb{Q}}_p \hookrightarrow \mathbb{C}_p; no monotonicity of the family is imposed, so in general X is the closure of the union of the images, which in the intended applications is the closure of K_\infty = \bigcup_m K_m.

PadicComplex.IsTateTrace p Km m d R is a predicate (a structure all of whose fields are propositions) on a level m \in \mathbb{N}, a real constant d and an arbitrary function R \colon \mathbb{C}_p \to \mathbb{C}_p, asserting six conditions, all of which constrain R only on X = towerClosure p Km: R is additive on X; R(kx) = kR(x) for k \in K_m and x \in X; R(k) = k for every k \in K_m; for each x \in X there is k \in K_m with R(x) = k, so R maps X into K_m; R(\sigma \cdot x) = R(x) for all x \in X and all \sigma in the fixing subgroup of K_m; and finally the estimate \lVert x - R(x)\rVert \le d\,\lVert \sigma \cdot x - x\rVert for all x \in X and every \sigma fixing K_m pointwise but not lying in the fixing subgroup of K_{m+1}. Thus R behaves on X as a K_m-linear projector onto K_m, commuting with the Galois action over K_m and controlling the distance from x to its projection by the displacement of x under any such \sigma.