Definitions/Def_AlgebraicCurve_TotallyDegenerateCovering.lean

Throughout, L is a field, A \subseteq L a valuation subring with residue field k = ResidueField A, F a field extension of L, and \varpi an element of A. The structure AlgebraicCurve.TotallyDegenerateCovering A F ϖ packages a bipartite totally degenerate semistable covering of the places of F/L by charts and annuli. Its fields require \varpi to lie in the maximal ideal of A and to be non-zero in L, and then supply: a finite vertex type V with a two-valued function side : V → Fin 2; a finite edge type E; for each v \in V a ComponentChart A F (RatFunc k), that is, a valuation subring integers of F contracting to A on L, a surjective reduction map onto the rational function field k(t) whose kernel is the maximal ideal, a domain of places of F/L, a finite set nodes of places of k(t)/k, and a map on places compatible with evaluation at rational places and with divisors of functions away from the nodes; for each e \in E two annuli annOut e, annIn e (each a set of places together with a parameter and a modulus in the maximal ideal of A, the places of the domain being parametrised bijectively by the admissible values of the parameter, with the unit principle for functions without zeros or poles); endpoint maps src, tgt with side (src e) = 0, side (tgt e) = 1; nodes nodeOut e, nodeIn e at which the outer and inner annuli are attached to the charts of src e and tgt e in the sense of Annulus.IsAttached; the conditions that the two presentations of e have the same domain and modulus and that the product of the two parameters is the image of the modulus; a width width e in \mathbb{N}^{+} with A-valuation of the modulus equal to the \mathrm{width}(e)-th power of that of \varpi; the requirement that the nodes of chart v are exactly the nodeOut of edges leaving v and the nodeIn of edges entering v, each occurring once; and finally that the chart domains and annulus domains are pairwise disjoint and cover all places of F/L.

The definition toDegeneracyData reads off the weighted dual graph as the DegeneracyData E V with a = src, b = tgt, w = width, with the three projections computed by simp lemmas; src_ne_tgt records that no edge joins a vertex to itself, which follows from the two side conditions.