Definitions/Def_AlgebraicCurve_AffinoidCentre.lean

Throughout, L is a field with a valuation subring A, F is a field extension of L, and \bar F is a field extension of the residue field \kappa = \mathrm{ResidueField}(A); C is a ComponentChart A F Fbar, that is, a valuation subring C.integers of F together with a surjective ring map C.residue onto \bar F with kernel the maximal ideal, a set C.dom of places of F/L, a finite set C.nodes of places of \bar F/\kappa, a map C.placeMap from places of F/L to places of \bar F/\kappa avoiding the nodes on C.dom, and the compatibility axioms of that structure. Four notions are defined, plus a subring.

ComponentChart.tubeBounded C f says that for every place P \in C.\mathrm{dom} one has f \in \mathcal{O}_P and the value P.\mathrm{evalAt}\, f lies in A. ComponentChart.HasAffinoidLifting C N, for a finite set N of places of \bar F/\kappa, is the conjunction of: every tube-bounded f lies in C.integers; every g \in \bar F lying in \mathcal{O}_Q for all Q \notin N is the residue of some tube-bounded element of C.integers; and every h \in C.integers can be written as h = r/s with r, s tube-bounded, s \in C.integers and residue of s non-zero (stated as h\,s = r). ComponentChart.regOff N is the subring \bigcap_{Q \notin N} \mathcal{O}_Q of \bar F, formed as a lattice infimum of subrings. ComponentChart.HasPlaceDictionary N asserts a bijection between the maximal ideals of regOff N and the places Q \notin N: each maximal ideal \mathfrak{m} has a unique such Q with g \in \mathfrak{m} iff g = 0 or \mathrm{ord}_Q(g) > 0, and every Q \notin N arises from some maximal ideal so described. Finally ComponentChart.IsCentre C N O Q, for a valuation subring O of F and a place Q of \bar F/\kappa, says Q \notin N and, for every tube-bounded f \in C.integers, the residue of f vanishes at Q (i.e. is 0 or has positive Q-order) exactly when f lies in O and in the maximal ideal of O. The disjunct '=0' accommodates the convention for the order of 0.