Anabelian geometry

Geometric fundamental groups of curves, Kummer theory, cuspidal inertia, and arithmetic reconstruction. This library is under development toward the formalization of Grothendieck's anabelian conjecture.

A nonidentity element of a closed abelian subgroup disjoint from a compact family away from the identity survives in the abelianization of some open overgroup, even after killing the compact family. The proof constructs…

Choosing one boundary label identifies the module modulo its diagonal with functions on all remaining labels. This gives an integral coordinate system; in particular, no inversion of the number of boundary points is need…

The boundary permutation module is taken modulo its diagonal relation. With at least two labels, each coordinate injects into the quotient. With three distinct labels, two coordinate lines have zero intersection. These a…

Permuting boundary labels preserves the diagonal relation and induces a linear equivalence on the reduced boundary module. The equivalence sends each boundary coordinate to its permuted coordinate.

Differences of coordinate evaluations vanish on the diagonal relation and therefore descend to the reduced boundary module. They recover a boundary coefficient integrally, without division by the number of punctures.

A continuous discrete-valued character of a closed subgroup extends to an open overgroup. If it vanishes on the intersection with a compact family, the extension can be chosen to vanish on that family's entire intersecti…

A closed subgroup of a profinite group has an open overgroup avoiding any prescribed compact set disjoint from it. A single finite quotient separates the entire compact set, so the construction also handles all conjugate…

Two disjoint compact subsets of a profinite group remain disjoint in one finite quotient. This permits extending characters while controlling an entire compact family of inertia elements.

The closure of the powers of an element is commutative. Compact character separation therefore detects that element in an open relative abelianization unless its closed cyclic subgroup meets the prescribed family nontriv…

A fixed element that commutes with no member of a compact set still commutes with none of their images in one finite quotient. The quotient is chosen uniformly for the whole compact set, rather than separately for each g…

If a subgroup embeds into an abelian image of the ambient group, its normalizer centralizes it. This supplies the abelianization step in self-normalization arguments for boundary inertia. No assertion about centralizers…

Uniform noncommutation in a finite quotient gives an open subgroup containing one prescribed element and avoiding a whole compact family. Applying this to a conjugacy-saturated family makes the avoidance stable under con…

For a nondegenerate bilinear pairing with multiplier c, the absence of fixed vectors in finite dimension excludes eigenvectors of eigenvalue c. The proof uses the surjectivity of F - 1 and does not require an eigenvalue…

An etale normalization of the polynomial ring is unramified away from infinity. Riemann--Hurwitz therefore makes its fraction field trivial in characteristic zero. For a finite etale domain over the polynomial ring, this…

A connected finite etale cover of Spec K[T] is affine and integral. Its actual section algebra is a finite etale domain over K[T], hence trivial by the normalization and Riemann--Hurwitz argument. The original scheme mor…

A place whose valuation ring contains a Dedekind affine coordinate ring has an actual centre in that affine chart. Localizing the normalization at this centre identifies its base with the valuation ring, so etaleness on…

Geometric fundamental groups and their presentations.

A finite surjective morphism of smooth proper curve models supplies its own function-field homomorphism and place correspondence. At a point where its actual stalk map is formally unramified, the associated place has ram…

Equivariant identifications of actual Kummer fibres preserve their root fields. Simultaneous pointwise stabilizers detect the compositum of two root fields; their common-twist family detects the root field of the ratio.

+# The étale fundamental group of a proper genus-zero curve We construct two distinct places and a generating rational parameter from the genus-zero hypothesis. The resulting function-field isomorphism gives an actual ra…

On a genus-zero function field over an algebraically closed field, two distinct places determine a rational parameter with a simple zero and a simple pole there. Principality comes from the proved genus-zero Picard theor…

A parameter with its unique pole at the prescribed puncture identifies that place with infinity. The induced curve-model isomorphism identifies the given open complement with the actual affine line. The fundamental group…

The genus-zero parameter with a prescribed simple zero and pole determines a rational-function field isomorphism carrying zero and infinity to precisely those places. The actual curve-model isomorphism therefore identifi…

The original cover is affine. Its actual section algebra is finite etale over the Laurent polynomial ring and has connected spectrum. Pullback of sections by inverse cover automorphisms gives an injective group homomorph…

Connectedness of the spectrum supplies domain and normality from the finite-etale hypotheses. Thus the original algebra is its base ring's integral closure in its actual fraction field. Restriction of automorphisms ident…

The rational function field acts on the actual fraction field of the given finite etale domain by the fraction-field lift of its original algebra map. The generic fibre surjects onto this field, proving finiteness and pr…

The stabilizers of pointed Galois covers form a neighbourhood basis for the actual fibre-functor automorphism group. Each such stabilizer is the kernel of the quotient to the opposite cover automorphism group. The proved…

The algebra is the actual quotient adjoining an nth root of the Laurent coordinate. Eisenstein irreducibility before localization proves that it is a domain. The monic power basis gives its rank, and the invertible deriv…

The canonical Galois action on the geometric fibre of the pulled-back finite-etale scheme agrees with postcomposition on the root algebra points. Its pointwise stabilizer therefore recovers the full root field. This is a…

Pull the named Kummer cover back along a rational point to obtain an actual finite-etale scheme over the base field. Its geometric fibre is identified with the algebra-point description, through the actual pullback squar…

Taking the spectrum of the explicit Kummer algebra produces the cover. Its source is connected because the algebra is a domain, and its actual geometric fibre has the prescribed cardinality by the power basis and the fin…

The points of the actual Laurent Kummer algebra above a nonzero scalar are exactly the roots of its Kummer equation. Both directions are explicit ring homomorphisms and the inverse laws follow from the quotient universal…

Postcomposition gives the actual Galois action on the algebra points of a Laurent Kummer fibre. Its point stabilizer fixes exactly the radical field. This identifies the arithmetic point data without a roots-of-unity ass…

The quotient-algebra description is compared with scheme morphisms using full faithfulness of Spec, and then with the existing geometric fibre functor. Consequently the actual finite-etale fibre is equivalent to the set…

The pointwise stabilizer of all algebra points of a Laurent Kummer fibre fixes precisely its full root field. After choosing one fibre point this is the field generated by its coordinate and the corresponding roots of un…

We use the actual Laurent evaluation into the rational function field. Its fraction-field property follows from localization of the polynomial ring, and its image is regular at every place except zero and infinity. Thus…

The finite-etale geometry supplies both a topological generator and actual quotients of every positive order. The normalized-coefficient construction identifies the fibre-functor automorphism group, with its original top…

The degree-n Kummer cover supplies a transitive action on n actual geometric points. Its finite image is cyclic by the already proved geometric quotient theorem. Evaluation at one point is then injective as well as surje…

The valuation ring of an extending place is the localization of the actual integral closure at its centre. If that integral closure is etale over the base valuation ring, the inclusion of valuation rings is unramified. I…

The input genus is the dimension of the actual structure-sheaf H¹. We construct the curve model, transport the specified closed point and its open complement, and obtain an actual affine-line isomorphism. This proves the…

Actual compactification, interior unramifiedness and boundary Riemann--Hurwitz force a strict increase in actual finite H¹ cardinality. No Euler characteristic or cohomological comparison is an input assumption.

Arbitrary open subgroups, including nonnormal ones, are realized by actual connected finite étale covers. Their actual compactifications and boundary Riemann--Hurwitz prove hyperbolicity. The geometric H¹ argument then k…

A nonidentity element would yield its actual cyclic intermediate cover. Choosing coefficients after constructing that cover avoids any coprimality assumption. Transfer would make all H¹ descend, contradicting the geometr…

Riemann--Hurwitz makes the genus strictly increase in a nontrivial finite étale cover of a proper hyperbolic curve. Actual finite-coefficient H¹ therefore cannot all descend. For a Galois cover, the proved transfer and d…

Every actual open subgroup is realized by an actual connected finite étale cover. Its smooth proper model remains hyperbolic by Riemann--Hurwitz. Geometric deck H¹ faithfulness proves its center trivial, and the existing…

A nonidentity element would yield its actual cyclic intermediate cover. Choosing coefficients after constructing that cover avoids any coprimality assumption. Transfer would make all H¹ descend, contradicting the geometr…

The genus is the dimension of the actual structure-sheaf H¹ on a two-affine cover. Its proved comparison with function-field cohomology, followed by the actual curve-model construction and pullback equivalence, proves tr…

Both intermediate schemes are realized by curve models, with their actual maps and deck transformations transported through proved isomorphism squares. Riemann--Hurwitz and actual finite H¹ cardinality then obstruct surj…

A connected finite etale cover of a proper rational curve model is an isomorphism in characteristic zero. No curve model, function field, surjectivity, or integrality of the cover is assumed. Smoothness gives domain stal…

In characteristic zero, a finite extension of an algebraically closed rational function field unramified away from two places is Galois and cyclic. Its actual automorphism group identifies with the degree-th roots of uni…

In characteristic zero, a finite etale surjective morphism from a smooth proper integral curve model to a rational curve model induces an isomorphism of function fields. The isomorphism retains the actual morphism's corr…

In characteristic zero, a finite etale surjection from an integral curve model to a proper rational curve model is itself an isomorphism. The function-field equivalence constructs a model isomorphism. Its action on valua…

The actual etale fundamental group of a proper rational curve model over an algebraically closed field of characteristic zero is trivial at every geometric point. Connected finite etale covers are isomorphisms by the geo…

The tame two-branch theorem supplies genus zero and the two singleton fibres. The genus-zero parameter theorem then supplies actual generating coordinates on both fields. Comparing their divisors makes the pulled-back ba…

Riemann--Hurwitz and the fundamental identity of a place show that a finite separable extension of an algebraically closed rational function field, tame everywhere and unramified away from one place, has degree one. In c…

Affineness is obtained from the proved finite-coordinate construction for pointed proper curves. The actual image of the section ring in the function field is then identified with the intersection of the finite valuation…

A finite separable extension of an algebraically closed rational function field, tame everywhere and unramified away from two distinct places, has genus zero and exactly one place above each of the two possible branch pl…

The complements of zero and infinity are affine. Their intersection has its actual section ring embedded in the function field, with image equal to the Laurent polynomial image. This constructs the scheme isomorphism wit…

Genus is measured by the dimension of actual coherent H¹. The constructed Laurent-chart isomorphism and the actual finite-etale pullback equivalence transport the full profinite integer comparison to the original open cu…

Starting from the actual structure-sheaf H¹ dimension of a smooth proper integral curve, we construct its curve model and transport both specified punctures. The resulting scheme isomorphism identifies their complement w…

The genus is the dimension of actual coherent H¹. The proved Laurent-chart isomorphism and the actual pullback equivalence of finite etale covers transport a topological generator to the original curve. Procyclicity does…

If an n-th radical lies in an abelian Galois extension containing the n-th roots of unity, its power-class order is the order of a root of unity in the original base field. This follows from the explicit cyclotomic desce…

Conjugation transports a radical ratio by the action on roots of unity. Only the automorphism being conjugated is required to fix those roots; the conjugating automorphism may act nontrivially on them. This is the finite…

Norms descend powers across extensions of coprime degree. A central cyclotomic automorphism gives a second exact descent criterion when its displacement is coprime to the exponent.

Equality of powered cyclic subgroups determines a non-torsion generator up to inversion and a root of unity of the prescribed exponent.

A central Galois automorphism acting on n-th roots of unity by the (m + 1)-st power forces an n-th radical from the base to descend after raising its power class to m. The proof is the explicit radical-cocycle calculatio…

A finite extension contained in a directed union already lies in one member. In particular, its intersection with the entire union is attained at a finite level. This is the finite-level input for cyclotomic towers.

The structure theorem for finitely generated abelian groups supplies an integer-valued character nonzero on any prescribed non-torsion element. Applying that character to a power relation yields an integral divisibility…

The number of roots of unity in the original number field annihilates any power class that acquires a radical in an abelian Galois extension containing the relevant roots of unity. The bound is independent of the radical…

For a fixed non-torsion element a, one positive integer M controls all relations a^e = d^n in the original number field: n divides eM. A fixed S-unit group contains both a and every possible d in these relations.

Although the entire multiplicative group of a number field is not finitely generated, two prescribed elements lie in one finitely generated S-unit group. This subgroup is saturated under roots in the original field. Cons…

It suffices to compare cyclic subgroups modulo prime powers. The proof uses one saturated finitely generated S-unit group for both generators.

We construct the relevant cyclotomic intermediate field in an algebraic closure and descend the resulting Kummer relation with the fixed loss given by the original field's roots-of-unity order. Equality at every exponent…

In a finitely generated abelian group, an element divisible by every positive integer is trivial. Applying this to a quotient shows that every subgroup is the intersection of its enlargements by ambient power subgroups.

Prime powers suffice to recover subgroups of finitely generated abelian groups. The saturated-subgroup version also applies to S-unit groups.

If a field is generated by a set of constants and one nonzero radical, automorphisms agreeing on the constants are determined by their radical ratios. In particular the ratio map is injective on the subgroup fixing the c…

If a ^ n belongs to the base field, the intersection of the fields K(r a, r b), over nonzero r whose n-th power belongs to K, is exactly K(b / a). The proof constructs the normalizing twist r = a⁻¹. This is the field-the…

When the relevant roots of unity belong to the base field, a nonzero radical defines a unit-valued Galois character. Its kernel fixes precisely the field generated by that radical in an arbitrary Galois ambient extension…

Over a base containing the relevant roots of unity, replacing a radical by another root of the same power equation leaves its Galois cocycle unchanged.

The quotient of a conjugate radical by the original radical satisfies the crossed-homomorphism law. Its values are roots of unity when the radical has a power in the base field. When those roots of unity are in the base,…

After choosing one nonzero root, adjoining all roots of the equation is exactly adjoining that root and all roots of unity of the same order. The equality is proved inside the given ambient field without assuming that ro…

Over a field containing the relevant roots of unity, the full root field of a unit determines its cyclic subgroup modulo powers. The statement retains the roots-of-unity hypothesis; it does not assert descent through an…

Equality of full root fields first gives a power relation after extending the base to a field containing the roots of unity. A central cyclotomic automorphism then gives an explicit power relation over the original base.…

Intersecting the composita of the full root fields of c x and c y over all nonzero base-field twists c recovers the full root field of y / x. Roots of unity are retained throughout, so the base need not contain them.

A complex parameter whose value and complement both have norm one lies on the quadratic exceptional locus. This supplies the archimedean step for the simultaneous torsion case in multiplicative reconstruction.

Normalize a reference triple and compare the remaining affine coordinates. Equal cross ratios then give an explicit projective coordinate equivalence carrying every label of one configuration to the corresponding label o…

An invertible two-by-two coordinate matrix gives an actual equivalence of projective points. Its action preserves the projective cross ratio.

The convention sends the first three ordered points to 0, ∞, 1. Homogeneous coordinates include infinity without a separate affine chart. Independent rescaling does not change the ratio, and the projective definition is…

For a fixed nondegenerate ordered triple, the cross ratio separates fourth points in its affine chart. This is proved for homogeneous representatives and then for the actual projectivization quotient.

The archimedean argument handles the mixed torsion/non-torsion case. Together with the purely algebraic inversion argument, two cyclic multiplicative subgroups determine a parameter outside the explicit quadratic excepti…

If both a parameter and its complement are known up to inversion, the only possible ambiguity lies on the polynomial X² - X + 1. These field identities are independent of the arithmetic mechanism that reconstructs the pa…

For a unit and its complementary unit of infinite order, their cyclic subgroups determine the original parameter. This is the algebraic, non-torsion step; no reconstruction of these subgroups from Galois data is postulat…

Three distinct ordered points admit an explicit invertible coordinate change sending them to zero, infinity, and one. Its affine coordinate is the cross ratio.

Two cyclic multiplicative subgroups recover a normalized parameter up to an explicit quadratic exception. The same data for one chosen square root eliminates that exception. These statements concern actual field elements…

Restriction of finite étale covers defines the map. For a normal locally Noetherian integral compactification, this map is surjective; its kernel is the image of the kernel before abelianization. Identifying this kernel…

The canonical scheme pullback and restriction of field automorphisms agree on cohomology characters. The inner conjugator in the geometric-fiber comparison disappears because the coefficient group is commutative.

This is finiteness of morphisms over the base, not finiteness of the underlying topological fiber. The affine scheme may have positive dimension.

A homomorphism is determined by its values on finitely many algebra generators. This gives the affine finiteness input for rational points over finite fields, without a zero-dimensional or module-finite hypothesis.

Restriction to the function field commutes with dominant scheme pullback. Both sides use the existing derived-sheaf maps, rather than a replacement cohomology model or an assumed compatibility square.

The proper and open normalization covers give the same root quotient under restriction of field automorphisms. The proof computes both actual monodromy characters on one common root.

The canonical function-field map commutes with the maps from the generic stalk spectra. This is used when comparing the actual Kummer characters on an open curve with geometric pullback from its compactification.

The kernel has n^(2g) elements and the residue image has n^(r-1) elements. These counts apply to the actual cohomology maps constructed from Kummer covers. Intrinsic recognition of this filtration from arithmetic Galois…

The residue map is defined on genuine derived étale H¹ through the proved comparison with actual Kummer covers. Its kernel is the proper divisorial Kummer quotient, and its image is the sum-zero boundary module. The comp…

The proof restricts the two actual derived H¹ classes to the function field, computes their characters on the same root, and uses generic injectivity.

For an exponent greater than one, the kernel determines the genus and the image determines the size of a nonempty boundary. These are explicit numerical formulas. Recognition of the filtration from arithmetic group data…

This is the group-theoretic input for ruling out fixed Tate vectors after identifying fixed geometric points with a finite rational-point group. The geometric identification and finiteness are separate requirements.