Étale fundamental groups

Finite étale covers and the étale fundamental group, with Galois categories, ramification, inertia, purity and specialization. Includes Kummer covers and comparison constructions.

For a connected scheme and a geometric point, the actual topological abelianization is the Pontryagin dual of the discrete direct limit of its ordinary finite-coefficient étale H¹ groups. Both maps and both continuity st…

This comparison is the mate of the identity between the actual direct-image functors. Its invertibility is detected on geometric stalks. The mate formula retains the adjunction compatibility needed to transport constant…

The comparison is transported through the existing integer-module equivalence. It reuses the geometric-stalk proof for modules and its actual inverse-image functor. This is the comparison needed to pull back the sheaf of…

The finite-coefficient comparison is compatible with reduction. It therefore identifies classical ℓ-adic H¹, defined on the ordinary étale site, with compatible systems of continuous characters into ℤ/ℓ^(n+1)ℤ. Neither p…

Actual degree-one cohomology is identified with continuous finite-coefficient characters of the fundamental group and its topological abelianization. The coefficient-natural comparison identifies classical integral ℓ-adi…

The constant-sheaf comparison is the unique comparison of left adjoints. Its adjoint carries each constant section to the same section on the base-changed étale object. In particular it preserves the integer section used…

The stalk of a constant abelian étale sheaf is canonically its coefficient group. This follows from the connectedness of the filtered neighborhood category and the fact that sheafification does not change stalks. The com…

This is a reduction by contradiction: a nonidentity kernel element would produce an actual nontrivial relative Galois cover whose whole deck group acts trivially. The intermediate scheme and all action comparisons are co…

The existing duality is reused. Its scheme naturality and base-point naturality give equivariance for any specified pointed geometric pullback. For a deck transformation, the actual comparison with conjugation is the one…

For a geometric deck transformation selected by ambient monodromy, an element centralizing the covering subgroup acts trivially on the actual derived H¹. This comparison does not assume H¹ faithfulness. The geometric pro…

Compatibility of the actual derived extension classes with a kernel map gives a morphism of short exact sequences which is the identity on the quotient. The morphism is constructed using the two Ext exact sequences: firs…

The lift sheaf of an abelian extension is pulled back using its categorical fiber square. The comparison uses the actual abelian inverse image and the actual underlying-set comparison; no compatibility is imposed as a hy…

The sectionwise construction used for extension monodromy satisfies the pullback universal property in the category of étale sheaves. This allows exact inverse image to transport the original sheaf of lifts.

The inverse image of a global section of the quotient of a short exact sequence is an actual sheaf of sets. It has sections étale locally, and any section identifies that fiber with the kernel by translation. These are t…

The actual geometric monodromy of the finite locally constant sheaf of lifts commutes with constant coefficient translations. Its geometric fiber is a torsor for those coefficients, so displacement defines a continuous c…

The actual sheaf of lifts maps to the middle term of the extension. A map from that middle term to a descended finite representation therefore gives an equivariant map on geometric monodromy. Its value is computed in the…

The middle object is the actual categorical pullback. Its kernel is identified using a specified isomorphism to the original kernel, and its short exactness is proved from the pullback and kernel universal properties.

The actual connecting class of a short exact sequence vanishes precisely when the quotient map has a section. This is the exact-sequence criterion used to detect trivial degree-one cohomology classes.

For finite constant abelian coefficients on a connected scheme, the character of an actual extension is trivial precisely when its derived extension class vanishes. This uses descent of a fixed monodromy point to a genui…

The map induced by a morphism of extensions carries translation by a constant coefficient to translation by its image. The coefficient comparison is the actual constant-sheaf functor map, with its sheafification unit nat…

A morphism of extensions which is the identity on kernel and quotient induces a morphism of their lift sheaves. This morphism commutes with every constant coefficient translation, directly from the original additive shea…

Translations on the fiber over one are restrictions of additive shears. Their compatibility with inverse image therefore follows from the genuine abelian inverse-image functor and its constant-coefficient comparison.

The sheaf of lifts is the actual pullback over the chosen quotient section. Since geometric stalks preserve finite limits, its stalk is the fiber of the stalk homomorphism. The comparison uses the forgetful functor's fil…

Every original coefficient acts by a morphism of the actual fiber sheaf. On a geometric stalk this is translation by the same coefficient under the canonical constant-stalk isomorphism. Naturality of these sheaf morphism…

For a trivial finite abelian representation, constant equivariant functions give sections of the descended finite étale group. These sections respect addition and define a map from the actual constant abelian sheaf.

The finite étale representing covers and their abelian sheaves carry the original maps on actual geometric stalks. Consequently an exact sequence of finite continuous representations descends to an exact sequence of actu…

+# Representing finite abelian monodromy A finite abelian group with continuous action of the actual étale fundamental group determines a finite étale cover. Its group structure is constructed from the represented preshe…

The abelian operations constructed on the finite étale representing cover give an actual sheaf of abelian groups on the small étale site. The underlying set sheaf is the represented sheaf of that cover. All group operati…

The actual geometric stalk of the descended abelian sheaf is additively isomorphic to the original finite representation. Naturality for both projections and their sum proves compatibility with addition.

For an additive abelian group A, a character acts on A × End(A) by g • (a, f) = (a + f(χ(g)), f). Thus both the kernel A and the quotient End(A) have trivial action. The inverse image of the identity endomorphism has dis…

The triangular representation on A × End(A) descends to a short exact sequence of actual étale abelian sheaves. The two end terms have trivial monodromy; the middle term retains the given character. All exactness stateme…

For a connected scheme and a geometric point, actual derived étale H¹ with finite constant abelian coefficients is naturally the group of continuous characters of the étale fundamental group, or equivalently of its topol…

The subgroup laws are proved from the composition and identity laws of the actual derived-sheaf pullback. In particular triviality propagates to the cyclic subgroup generated by a deck transformation.

This is the composition law for the existing derived-sheaf pullback, obtained from the faithful character comparison, including its geometric base points.

On a connected scheme, bijectivity at one geometric stalk detects an isomorphism of finite locally constant sheaves. This is deduced from the actual monodromy equivalence and its comparison with the geometric stalk. The…

For finite local systems on a connected scheme, a surjective stalk map at one geometric point gives an epimorphism of actual abelian sheaves. Faithful Galois fiber functors reflect epimorphisms and every geometric fiber…

Kernels are pullbacks along a zero object. The actual stalk functor detects these pullbacks and detects epimorphisms for finite local systems on a connected scheme. This proves short exactness of the descended sheaves, w…

The monodromy equivalence makes one geometric stalk faithful on finite local systems on a connected scheme. The comparison with the underlying set stalk then detects equality of morphisms of the actual abelian sheaves.

The finite étale realization preserves finite limits, and the Galois fiber functor reflects them. Hence a square of finite locally constant abelian sheaves is cartesian if its actual geometric stalk square is cartesian.…

The map is induced level by level by the derived cohomology inverse image. Compatibility with the original finite coefficient inclusions follows from coefficient naturality, independently of fundamental-group characters.

For coefficient order coprime to the covering subgroup index, a class fixed by every actual geometric deck pullback descends to the base. The proof constructs the descended character by normalized continuous transfer, us…

The generic absolute Galois map identifies the characters of a normal integral scheme with the characters that kill its actual normalization inertia groups. The inertia groups are those of the literal integral closures o…

The closure is arbitrary. This allows a geometric comparison made in the chosen constant-field extension to determine the actual global H¹ class.

The comparison is additive because it is natural for both projections and addition on the product coefficient group. These operations use the existing additive cohomology functor. Combined with the proved zero detection,…

Every derived étale cohomology class with finite constant abelian coefficients defines a continuous character of the actual étale fundamental group. Comparison of extension representatives proves that the character is ca…

The actual comparison character removes the choice of pullback comparison. The proof uses the existing geometric base-point naturality.

The finite lift cover of the actual inverse-image extension is the geometric pullback of the original cover. Its comparison preserves original coefficient translations. Naturality of finite-cover monodromy therefore iden…

Every class in the existing derived-functor étale cohomology Sheaf.H F 1 is represented by a short exact sequence with kernel F and quotient the constant integer sheaf. The sequence is constructed by embedding F into an…

After identifying both constant coefficients, the inverse image of the original lift sheaf is the lift sheaf over the original integer section on the new base. This is the lift sheaf of the extension representing the act…

For finite abelian constant coefficients, the inverse image of the integer section 1 in an extension representing a cohomology class is represented by a finite étale scheme. Both the extension and the representer are con…

The open kernel of the actual cohomology character is realized by an actual connected finite étale cover. Geometric naturality proves that the original derived cohomology class pulls back to zero. This supplies the degre…

Changing finite constant coefficients commutes with the canonical continuous character. The comparison of extensions is constructed from equality of their actual derived extension classes after applying the coefficient m…

A character gives a finite triangular representation on A × End(A). Its descended short exact sequence is pulled back along the constant map ℤ → End(A) sending 1 to the identity. Evaluation in the actual middle stalk rec…

On the fiber of an extension over the integer section one, translation by a coefficient is the restriction of the additive endomorphism e ↦ e + i(a p(e)). This realizes the torsor action using genuine abelian-sheaf morph…

A global section of the fiber over the constant integer section 1 gives a splitting of the original quotient morphism, by taking integral multiples and using the sheafification adjunction. Conversely a splitting gives su…

The character group carries pointwise p-adic scalar multiplication. The comparison respects this actual action because finite-coefficient H¹ is natural for the scalar endomorphisms of its constant coefficient sheaf.

An actual local lift of the quotient section translates the restricted kernel onto the extension fiber. Epimorphy supplies a cover with such lifts. In particular, a finite constant kernel makes the fiber finite locally c…

A morphism from a finite locally constant sheaf into the direct image of another one gives a morphism between their representing finite étale covers after base change. On geometric fibers this is equivariant for the actu…

For a finite locally constant étale sheaf on a connected scheme, existence of a global section is equivalent to existence of a fixed point in its actual finite monodromy representation. The reverse implication uses fulln…

Compatible finite characters determine actual p-adic integers, whose topology is detected by reduction at every level. Consequently their pointwise limit is continuous. Combined with the finite-coefficient étale H¹ compa…

The naturality of the actual derived H¹ character holds for every isomorphism comparing geometric pullback with a chosen target fiber. This lets geometric deck comparisons be used without postulating a cohomological acti…

Compactness of the actual étale fundamental group gives a common integral denominator for each continuous Qℓ-valued character. Consequently its module of continuous Qℓ-valued characters is the scalar extension of its int…

The unit of finite étale representability identifies the monodromy of a represented sheaf with the original geometric fiber. Its comparison with the actual stalk is the existing represented-sheaf stalk comparison.

Inverse image of the actual sheaf of a finite étale cover is the sheaf of its scheme-theoretic base change. Consequently an arbitrary finite locally constant sheaf pulls back to the base change of its existing represente…

The map is induced on Ext by the exact inverse-image functor of abelian étale sheaves, with both constant objects identified by the actual constant-sheaf comparison. Its degree-one value is represented by the inverse ima…

A fiber of a short exact sequence of abelian groups is a torsor for its actual kernel. Applying the exact geometric stalk functor gives this structure for extensions of étale abelian sheaves. No splitting of the extensio…

The direct limit of actual finite-coefficient étale H¹ is the discrete Pontryagin character group of the actual topological abelianization. Factorization through finite quotients proves surjectivity. Thus finite torsion…

A continuous action on a discrete abelian torsor, commuting with translation, determines a continuous character. Its value is displacement of any chosen point; commutativity makes the answer independent of that point. Th…

An equivariant map of torsors compatible with a coefficient homomorphism carries displacement to the image displacement. This is the group-theoretic naturality needed to prove additivity of the étale H¹ comparison.

Canonical aggregate for EtaleFundamentalGroups.Completions.Adic.

For a finite integral extension of a Dedekind domain, completion along the extension of a nonzero maximal ideal first splits over the primes above it. Power-adic cofinality removes the ramification exponent in each facto…

For an R-algebra S and an ideal I of R, the module completion used by AdicCompletion.ofTensorProduct is built from the quotients S / I^n S. The ring completion of S at the mapped ideal is built from the same quotients, v…

For a positive integer e, the filtrations I ^ n and (I ^ e) ^ n are cofinal. This file realizes that cofinality at the finite quotient levels and produces the resulting canonical equivalence of adic completions.

Adic, DVR, tensor, chosen-factor, and retained-component completion results. Canonical aggregate for EtaleFundamentalGroups.Completions.

Canonical aggregate for EtaleFundamentalGroups.Completions.Chosen.

For a finite Dedekind extension of a DVR, the completed tensor product is the product of the completed local DVRs. This file proves that the closed prime and the generic prime selected from a fixed prime Q become, respec…

The product decomposition of the completed finite model identifies the closed prime selected from Q with the maximal ideal in the Q-coordinate. This file combines that identification with flat base-change invariance of r…

Let C / R be a finite extension of domains, with R a DVR, and let Q be a maximal ideal of C above the closed point. For a faithfully flat local base change R → R' which preserves the closed point and residue field, the e…

The completed product decomposition selects a finite complete DVR over the completed base DVR. Its fraction field is identified with the already chosen generic tensor component; pulling the standard complete valuation ba…

Starting from the closed prime Q, the preceding completed-component construction fixes a maximal ideal m of K' ⊗[K] L. This file maps the finite completed model R' ⊗[R] C into the field component selected by m, then rest…

Canonical aggregate for EtaleFundamentalGroups.Completions.DVR.

For a finite integral Dedekind extension of a DVR, completion at the closed point splits canonically as the product of the completed local factors. If every factor is etale over the completed base DVR, the completed tens…

For a finite Dedekind extension C / V, base change to the actual valued-field completion of the fraction field of V is the product of the completed local rings at the primes of C above the closed point. Each local comple…

Canonical aggregate for EtaleFundamentalGroups.Completions.FiniteEtale.

Suppose R → B is a local map inducing an isomorphism on residue fields and D / B is finite étale local. Lift the actual finite separable residue field κ(D) / κ(R) to the explicit finite étale local R-algebra constructed…

The residue-lift classification identifies a chosen finite étale factor D / B with B ⊗[A] C, where C / A is the explicit finite étale lift of the actual residue extension. This file reads that same equivalence in the oth…

The closed prime selected in a finite algebra need not be the unique closed prime. Nevertheless, extension along a faithfully flat local base change with unchanged residue field carries that particular prime to a maximal…

Over a Noetherian complete local base, a finite étale local algebra is complete, hence Henselian, for its own maximal ideal. Two such algebras with isomorphic residue extensions are isomorphic over the base. This is the…

Let R be a local ring and let l / κ(R) be finite separable. We choose a power-basis generator of l, lift its minimal polynomial coefficientwise to a monic polynomial over R, and adjoin a root. The resulting algebra is lo…

Let p be a chosen closed prime in a finite etale algebra E / R. After maximal-adic completion put T = Rhat ⊗[R] E and pHat = p.map (algebraMap E T). Completion may split a non-Henselian local factor, so in general one mu…

Canonical aggregate for EtaleFundamentalGroups.Completions.GenericTensor.

For a finite Dedekind extension of a DVR, every maximal component of the completed generic tensor product is the component canonically selected by a unique completed local coordinate (existence is all that is needed here…

Canonical aggregate for EtaleFundamentalGroups.Completions.Ramification.

The usual normalization-inertia comparison in this project obtains a DVR from regularity and a height-one calculation. A maximal-adically separated local domain needs neither global Noetherianity nor regularity at a prin…

Canonical aggregate for EtaleFundamentalGroups.Completions.Retained.

Canonical aggregate for EtaleFundamentalGroups.Completions.Retained.Component.

A retained generic prime N selects a literal field component Omega of the completed generic tensor product. If N lies below a tensor prime Q, the component map sends every element outside Q to a unit and hence extends ca…

Let N ≤ P be a retained generic/closed-prime pair in a completed finite model. Once the localization at P has been source-produced as a domain, the literal generic tensor component selected by N is its fraction field. Th…

A generic prime in an upper completed finite model contracts to a generic prime in every lower finite model. Localizing both models at the generic point and then taking their literal field-tensor coordinates gives a cano…

Let q ≤ p be a height-one/closed prime chain in a finite flat domain over a two-dimensional regular local ring. If q lies over a prime regular parameter and has a prescribed ramification index, maximal-adic completion re…

Let N ≤ Q be the generic/branch part of a retained completed tensor-prime chain. The localization at Q is assumed to have already been source-produced as a DVR. Its fraction field is the literal tensor component selected…

A generic/height-one/closed prime chain in the completed finite model fixes a literal component of the completed generic tensor product. This file maps the finite model into that component and then into its normalization…

An Away-etale normalization of a finite prefix field component remains Away-etale after maximal-adic completion, component by component. The component is the literal one selected by a retained generic tensor prime. The f…

Let q ≤ p be a prime and a closed prime in a finite model over a local base. A closed-point-preserving faithfully flat base change sends p to a specified maximal ideal P of the tensor product. Flat going-down then select…

This file specializes the retained completion prime chain to a regular parameter pair. In addition to retaining the supplied right-hand prime and closed point, it identifies the contraction of the retained prime to the c…

Suppose two finite models over the same local base are connected by an algebra map. After a common base change, the canonical tensor map contracts any prime chain in the upper model to a prime chain in the lower model. T…

The standard height-one valuation of a DVR gives two concrete completion models: the completion of its fixed real-valued adic absolute value, and the valued-field completion used by standardDVFCompletionField. This file…

Canonical aggregate for EtaleFundamentalGroups.Completions.StandardDVF.

The standard rank-one valuation attached to a DVR becomes a CompleteDVF when the DVR is complete for its maximal-ideal-adic topology. This is the base object needed to apply the finite-integral-closure construction after…

The standard valuation attached to a DVR has a canonical metric completion. This file equips that actual completion field with a CompleteDVF, records the canonical map from the original fraction field, proves that the co…

Starting from a DVR V and a chosen fraction field K, this file compares the maximalIdeal V-adic completion of V with the valuation subring in the actual valued-field completion of the standard valuation on K.

The valuation subring of the valued-field completion has the same residue field as the original standard DVR valuation subring. Surjectivity is proved directly from density: every integral completed element is congruent…

For a finite separable field extension L / K, the completion tensor decomposition identifies L ⊗[K] K̂ with the finite product of the completions Lₓ over all exact extensions w of a fixed nontrivial absolute value on K.…

Canonical aggregate for EtaleFundamentalGroups.Completions.Tensor.

A faithfully flat local base change which maps the old maximal ideal onto the new maximal ideal carries the maximal ideal of every local algebra to a maximal ideal of the tensor product. For maximal-adic completion the t…

Canonical aggregate for EtaleFundamentalGroups.ContinuousActions.

An element belongs to the closed normal subgroup generated by a set exactly when every finite continuous action on which the generators act trivially also makes that element act trivially.

Finite limits and finite colimits of continuous actions on finite discrete spaces are again continuous. Consequently the inherited forgetful functor from finite continuous actions to finite sets preserves both. This is t…

This file supplies the finite-orbit construction used internally for Stacks Project, Tag 03QR. Every orbit of a discrete continuous action of a compact topological group is finite.

A continuous homomorphism of profinite groups is injective exactly when every nonempty transitive finite continuous action of the source has the epi--mono span of Stacks Project, Tag 0BN7.

The range of a continuous homomorphism of profinite groups is normal exactly when, on every transitive finite continuous action of the target, one point fixed by the range forces every point to be fixed by the range. Thi…

For a surjective continuous group homomorphism, a finite continuous action is obtained by restriction exactly when the kernel acts trivially.

Restriction of continuous actions along a surjective continuous monoid homomorphism is full.

HasForget₂ deliberately has no general self-instance. The continuous-action API nevertheless needs the canonical identity forgetful functor when its ambient concrete category is TopCat itself.

Starting from a finite étale cover of X × Spec (A / I), successive thickening invariance constructs covers of X × Spec (A / I^(n+1)). The transition morphisms are obtained from the actual Limits.pullback recovery isomorp…

This facade collects the geometric-fiber equivalence, covering-family criterion, and Galois-cover characterizations over the scheme-theoretic finite étale foundation. Canonical aggregate for EtaleFundamentalGroups.Finite…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.Away.

The existing finite-extension transport derives finite presentation from module finiteness over a Noetherian base. Maximal-adic completions used by the one-point inertia construction do not currently carry a global IsNoe…

A connected finite-etale cover of Spec (A[1/f]) determines a canonical extension of the fraction field of A. This file identifies the algebra structure supplied by the cover with the canonical localization algebra and re…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.Away.GenericTensor.

This file closes the height-one branch disjoint from a boundary equation. For a prime q disjoint from the powers of f, the element f is a unit in Dq. A chosen fraction field of D[1/f] maps canonically to a chosen fractio…

Let A → C be finite etale away from f, and let a normal domain D carry an A-algebra structure. At a prime of D disjoint from the image of f, the original away algebra base-changes directly to the local ring Dq. Consequen…

An algebra which is finite etale on an original boundary complement remains finite etale after arbitrary normal base change and passage to a specified generic tensor component. This file returns the result for the litera…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.BaseChange.

This file packages the generic-fibre bookkeeping needed after a finite-etale base change. The generic fibre of B ⊗[A] T over a fraction field K of B is canonically K ⊗[A] T. A surjective map from that tensor product to a…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.BaseChange.GenericTensor.

Let C / A be finite etale, with fraction fields KC / F, and fix a literal maximal ideal m of KC tensor[F] M. A prime of the normalization of A in M lifts to the normalization of C in the quotient component selected by th…

Let T / A be finite etale and let E / F be its generic fibre, where F and E are fraction fields of A and T. After replacing A by a normal domain B with fraction field K, a specified maximal ideal of K tensor[F] E selects…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.Boundary.

Every height-one stalk prime containing a pulled-back effective Cartier boundary is the generic point of an irreducible boundary component. The arithmetic geometric-integrality condition therefore forces characteristic z…

Every component of an arithmetic Galois pullback contains a residue- characteristic-two normal-crossings point. The component generic point determines a canonical height-one prime in the ambient stalk at that point.

The residue field of the canonical height-one branch at any specialization is canonically the residue field at the component generic point. Consequently the geometric-integrality conclusion in the arithmetic boundary con…

The arithmetic boundary condition already supplies all point-free inputs at the generic point of a component after a finite-etale Galois pullback. This file packages those inputs at the canonical component generic point:…

The canonical generic point of a pulled-back arithmetic boundary component defines a height-one prime in its ambient local ring. The generic-fibre residue comparison supplies the geometric-integrality input for cyclotomi…

For a connected finite-etale cover, the normalization of every base stalk in the cover's function field is etale. At a height-one arithmetic component this forces the canonical normalization prime to have ramification in…

The geometrically integral generic fibre supplied by the arithmetic boundary condition determines a geometrically integral residue field at the canonical generic point of every pulled-back boundary component.

This module owns the boundary conditions whose statements quantify over finite étale Galois covers.

The full residue-characteristic-two boundary condition is inherited by a connected finite-etale Galois pullback. In particular, the result includes the geometric-integrality clause after every further connected Galois co…

If the equation of a boundary is a finite product of component parameters, then every parameter occurring in that product becomes a unit on the boundary complement. This is the elementary algebraic input used by the expl…

The ambient scheme need not be integral or normal. Only the selected reduced component is integral. Its dominance over the integral arithmetic base and the geometric integrality of its generic fibre supply the base-field…

The geometric-integrality clause for boundary components after Galois finite-etale covers is inherited after a connected Galois pullback. The proof dominates a composite cover by a Galois cover of the original base and d…

The declarations in this module are the categorical Galois-cover layer over the general finite étale divisor lemmas in SchemeTheory.

This file packages the ideal-sheaf base-change results as an effective Cartier divisor and records all conclusions for a fixed connected finite etale Galois cover. The hypotheses use local Noetherianity; there is no fini…

Away, chosen-prime, Henselian, and local finite-étale results used in one-point inertia arguments.

The affine-cochain tensor equivalence has an explicit formula in terms of the pullback adjunction unit. Using that formula and actual sheaf gluing, surjectivity of the pullback map on sections supplies surjectivity of th…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.ChosenPrime.

Tag 00UJ chooses an étale base change and a prime in one finite idempotent factor above a specified prime q. For the one-point inertia argument we also have a smaller, height-one prime r ≤ q. Flat going down produces a p…

The boundary-complement hypothesis belongs to the original finite normalization. After the Tag 00UJ etale base change, it is first transported to the tensor product, then to the finite idempotent factor, and finally to t…

Let C / R be finite and let L be a field over the fraction field of R. The literal generic algebra C ⊗[R] L is canonically the field tensor product FractionRing C ⊗[FractionRing R] L. This file transports a specified max…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.ChosenPrime.Henselian.

The Tag 00UJ factor used in the boundary argument is an Away localization at one idempotent. Thus its map from the tensor product is etale outright; it need not be treated merely as a finite formally-etale extension. Com…

Over a Henselian local base, the pointed etale neighbourhood produced by Tag 00UJ becomes the base itself after localization at its selected point. Consequently the prime-local ring of the chosen idempotent factor is the…

At the intermediate Henselian local stage, a pointed etale neighbourhood with unchanged residue field is canonically the base itself. This file uses that equivalence to move the primitive boundary Away map on the Tag loc…

The idempotent furnished by Tag 00UJ cuts out a finite factor after an etale change of the base. Its chosen prime remains the unique prime over the pointed prime after inverting the idempotent. Consequently the prime loc…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.ChosenPrime.PointedBase.

The Tag prime first selects an actual generic-fibre component and a prime in its normalization. Refinement back along the pointed base fraction field preserves that same prime-local factor. Combining those source-produce…

A pointed etale localization over a Henselian base is the base itself. On fraction fields this gives inverse scalar actions. Consequently the actual generic component produced from the Tag prime can be refined back along…

For an actual cartesian model along a local map, the two closed fibres are related by the native residue-field extension. Geometric reducedness of the original family therefore supplies the étale section algebra of the m…

A cover of an actual local spectrum compatible with a cover of a retrocompact open extends to an open neighborhood with the same overlap isomorphism. First spread the local cover, then spread the overlap isomorphism insi…

For a connected base scheme, categorical connectedness in the Galois category of finite etale covers agrees with connectedness of the underlying source scheme. This file records both directions, together with the nonempt…

Finite étale morphisms are open and closed. The image of the complement of the relative equalizer of two maps is therefore clopen in the base. If the maps agree after a base change whose image meets every connected compo…

Clopen descent gives a bijection on clopen subsets. For quasi-compact and quasi-separated schemes, the resulting map on connected components is a homeomorphism, as asserted in Stacks Project, Tag 0BQA.

A finite-etale cover of a connected scheme is a finite coproduct of connected covers. Since pullback preserves finite coproducts, extending every connected cover is therefore enough to extend an arbitrary (possibly disco…

Stacks Project, Tag 0BQE: finite étale morphisms can be distinguished after base change along any scheme morphism with dense image.

A dominant quasi-compact preimmersion from a connected scheme into a normal integral scheme preserves connected finite-etale covers. If the original cover is a Galois object, faithfulness of pullback and invariance of th…

Pullback along a dominant quasi-compact preimmersion preserves not only the Galois property but also commutativity of the cover automorphism group. The automorphism map is injective by faithfulness and is surjective beca…

A finite étale cover of the literal constant extension of an affine scheme descends to an actual finite intermediate field, with its literal inclusion map.

Finite-field models of finite étale covers.

The literal pullbacks of two charts along a coefficient map form a cartesian overlap. The comparison with their fiber product preserves both chart projections.

The general constructions live in SchemeTheory.

The constant-field base change of an open cover retains its index type and literal pullback charts. Its chart inclusions preserve both projections, and affine charts remain affine.

For any field extension, the base change of a scheme is the inverse limit of its base changes by the intermediate fields generated by finite coefficient sets. The transition maps are affine, and the stages inherit quasi-…

The standard iterated cover chart is the original chart after extending coefficients.

Rebase a constant extension through an actual intermediate field.

A single Frobenius power sends every element of a finite purely inseparable extension into the original field.

The canonical finite étale comparison for two successive pullbacks, with the composite map and category explicitly fixed.

Two finite coefficient extensions give the model over their actual composite subfield.

Actual recovered local models glue to a finite-stage model that recovers the original finite étale cover as an object of the finite étale category.

The general construction is owned by SchemeTheory; this file retains its existing finite-field consumer name.

An actual finite étale cover of Spec (R ⊗[k] L) for an algebraic extension L/k is the pullback of an actual finite étale cover over a finite constant extension. The pullback uses the literal tensor map of the field inclu…

The total-space and overlap comparisons identify coefficient extension with iterated pullbacks and preserve the original projections and maps to the base.

Compatibility names for the general coefficient-pullback cover owner.

The general constructions live in SchemeTheory.

Actual recovered overlap transitions descend together to one finite coefficient stage, retaining both structure maps and the recovery equation.

The Frobenius power on every algebra, including the zero algebra.

Recovery on a literal coefficient chart gives recovery on the standard pullback chart, with both structure maps fixed.

Actual finite étale covers descend through an arbitrary purely inseparable extension of the constant field.

The literal coefficient extension of a local model, over its coefficient base.

The recovered literal coefficient charts form an actual cover of the input scheme.

Recovered overlap maps are transported to literal coefficient extensions. Their transitions preserve the coefficient projections and recover the original chart maps.

The actually descended transition with its coefficient structure.

Compatibility import for the general recovered-local-model owner.

The actual recovered finite-stage charts form an open cover of the input scheme.

The general construction is owned by SchemeTheory; this file retains its existing finite-field consumer name.

For a qcqs scheme over a field, a morphism from an algebraic constant extension to a fixed locally finitely presented scheme descends to an actual finite intermediate field. The structure map and recovery equality use th…

A morphism from a qcqs constant extension to a locally finitely presented constant extension descends to one finite coefficient field, with both structure maps and recovery preserved.

A constant-field stage with its coefficient structure.

A connected finite-etale cover of a normal integral scheme has a canonical finite separable extension of function fields.

For a connected finite-etale cover Y ⟶ X of an affine normal integral scheme, the integral closure of Γ(X, ⊤) in the function field of Y is finite etale over Γ(X, ⊤). The algebra structures are the canonical ones coming…

Every connected finite-etale cover of a connected scheme is dominated by a Galois object. This file specializes the abstract Galois-category theorem to finite-etale schemes, choosing a geometric fiber functor canonically…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.GenericFiber.

For a finite cover of integral affine schemes, a number field in the cover's function field gives an actual map to the integral constant extension. Geometric integrality of the base's function field makes this map domina…

An integral subring of a geometrically integral function field remains disjoint from the integers of a number field. This proves injectivity of the actual multiplication map used in the arithmetic constants argument.

An affine open of an integral arithmetic scheme stays nonempty after a characteristic-zero field extension: its coordinate ring embeds in the tensor product. Geometric integrality of the generic fiber then makes this ten…

Every point of a characteristic-zero field maps to the generic point of Spec ℤ. The fiber base-change square therefore transports geometric integrality of the generic fiber to every such field extension.

For a finite etale algebra over a normal domain, a maximal ideal of the generic fibre selects one field component. This file descends the primitive idempotent of that specified component through smooth integral-closure b…

The normalization of a selected generic component of a finite-etale algebra is finite etale over a normal base. In dimension two, regular-local geometry produces that normality internally, so it need not be supplied as a…

A connected finite-etale algebra over an integrally closed domain has only one generic-fibre field component. The selected-component normalization is an idempotent factor of the algebra; connectedness makes that factor t…

The generic fibre of an open morphism to an irreducible scheme is dense in the source. If that fibre is geometrically connected, its image is connected and dense, so the source is connected as well. For Remark 2.3 this s…

Let T / R be a finite-etale extension of domains, let K be a fraction field of R, and let L be a fraction field of T. Compatible maps from K and T to L induce a surjection T ⊗[R] K ⟶ L. Consequently the integral closure…

A number field admitting a faithfully flat algebra which is smooth over the integers is unramified at every finite prime. Smoothness gives reduced special fibers; faithful flatness descends this reducedness to the ring o…

For a smooth algebra over a normal domain, every idempotent in the generic fibre is the image of a unique idempotent of the original algebra. Indeed, idempotents are integral and smooth base change commutes with integral…

The arithmetic constant-field theorem, applied to the actual finite étale cover, gives geometric integrality of its generic fiber. All connectedness, integrality, normality and characteristic-zero inputs are constructed…

The coordinate rings of a finite affine cover are assembled into a faithfully flat algebra over the ring of integers of a constant field. The resulting smooth arithmetic algebra forces that field to have degree one. All…

A finite affine cover and its inverse image supply the rings and maps in the arithmetic constants theorem. Normality extends integral constants on every chart, and the actual covering of Spec ℤ supplies faithful flatness…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.Henselian.

A finite complete family of orthogonal idempotents lifts along a surjective ring homomorphism whose kernel is a Henselian ideal. Individual idempotents lift by Hensel's lemma. Their lifts are automatically orthogonal bec…

For the complete-local chosen-factor argument, Noetherianity is not needed to make a finite étale local factor Henselian. Such a factor is finite free over the base. Adic completion commutes with finite products, so comp…

The affine equivalence identifies pullback of finite étale covers with tensor-product base change of finite étale algebras. The algebraic Henselian equivalence therefore gives Stacks Project, Tag 09ZS. The public stateme…

Hermite–Minkowski excludes a nontrivial number field whose ring of integers is unramified over ℤ: no prime can divide its discriminant, whereas a number field of degree greater than one has absolute discriminant greater…

This file passes from the generic-component calculation for finite-etale algebras to connected finite-etale covers of normal integral schemes.

Stacks Project, Tag 0BL7: the relative internal Hom of two finite étale schemes is represented by a finite étale scheme. Its pullback represents the internal Hom of the pulled-back schemes after every base change. The st…

Actual finite étale object and morphism descent supply the two inputs to automorphism assembly. The resulting bijection is the already-constructed comparison whose coordinates are the original fundamental-group maps. Com…

The functors and cone maps are the canonical scheme pullbacks. Their unit and composition coherence is proved from the projection-based pullback coherence theorems, including all equalities of the original diagram's sche…

The concrete colimit category is the localization of actual finite-étale models at their cartesian arrows. Its stage inclusions, canonical pullback-transition isomorphisms, unit/composition equations, and functor-categor…

For a directed system of schemes with any cone, equality of arrows after restriction to the cone vertex implies equality in the cartesian model localization whenever it is detected at a later stage. The proof factors arb…

A common refinement first brings two objects to the same original stage. The existing scheme morphism-descent theorem then descends their morphism. The proved pullback coherence returns it to the exact transition objects…

Geometric equality descent for the original inverse limit supplies eventual equality at an actual stage. The categorical fraction argument then makes the comparison from the cartesian model localization faithful.

Directedness supplies a common stage, and the cartesian square supplies the unique lifted numerator. Thus the native model localization has genuine right-fraction representatives, independently of geometric descent.

Actual finite-étale Hom descent produces a right fraction representing each morphism over the limiting scheme. Fullness is a conclusion of that geometric theorem, with the original qcqs and affine-transition inputs.

The canonical pullback-fiber isomorphisms identify stage automorphisms with the original geometric-point fundamental groups. The intertwining equation retains the given scheme transition and the cone-induced point equali…

This is the stagewise transport of the actual pullback automorphism system. Both the transition maps and the forward comparison coordinates are proved equal to the existing fundamental-group homomorphisms.

Objects and arrows are the native finite-étale comma category. Base change along a cone defines a functor on this category, and it inverts the cartesian arrows used in the colimit construction. No descent statement is as…

The cartesian stage transitions respect the canonical identity and composition isomorphisms of pullback. Applying the localization functor therefore gives the actual coherent cocone used in its 2-colimit presentation.

The stage inclusions and cartesian transition maps are actual functors and natural transformations. Every model arrow factors through its canonical cartesian refinement. These identify the stagewise meaning of the locali…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.Local.

An etale algebra which is local over a discrete valuation ring, with a local structure map, is again a discrete valuation ring. No module-finiteness of the localized target is needed: finite presentation gives Noetherian…

For a map between finite free modules over a local ring, surjectivity of the kernel comparison on the residue field forces both its kernel and cokernel to split. In particular, its kernel is finite projective and commute…

The existing finite-presentation approximation gives a proper flat model over a finitely generated integer algebra. The existing local-subalgebra construction makes its base Noetherian local inside the original local rin…

Splitting the cokernel makes the image a projective direct summand. Splitting the surjection onto this image makes the kernel a finite projective direct summand and proves its canonical arbitrary base change.

For a proper scheme over a Noetherian local ring, an etale closed-fibre section algebra implies surjectivity of the actual restriction map. A finite separable splitting field is lifted to a concrete faithfully flat local…

The global section algebra is finite by proper coherent cohomology. Its extension to an algebraic closure is reduced because flat base change identifies it with the actual sections of the reduced geometric fibre. The res…

This proves the full-faithfulness part of the proper henselian-local comparison without a Noetherian hypothesis. Essential surjectivity, and hence the full equivalence in Stacks 0A48, is separate. Fullness uses the exist…

An idempotent on a closed fibre lifts through every infinitesimal thickening because the thickenings have the same underlying space. The proper-cohomology stabilization theorem then produces a global section with that re…

A proper flat finitely presented family has an actual Noetherian local model. Its closed-fibre section algebra is étale by descent along the residue-field extension, without assuming that the model has geometrically redu…

For a proper flat geometrically reduced family over a Noetherian local ring, the actual closed-fibre section map is surjective. Its Čech comparison transfers this surjectivity to the finite free cohomology model. The loc…

The actual section algebra computed by Noetherian approximation identifies the second map of relative normalization as finite étale. Its first map has geometrically connected fibres by the unrestricted scalar-section com…

For a proper flat finitely presented geometrically reduced family over any local ring, an isomorphism on the actual global-section map persists after arbitrary base change. This uses the proved section-algebra comparison…

The actual section-module comparison respects multiplication on pure tensors. It therefore gives an algebra equivalence with the actual section ring of every base change. The original section algebra is finite projective…

The closed-fibre theorem supplies finite projectivity and kernel base change without a reduced-base or higher-cohomology-vanishing assumption. The final section/cochain construction is adapted from the attributed FLT sou…

The actual pushforward section isomorphism survives localization to each target stalk and then the nonflat change to its residue field. Scalar sections over that field imply geometric connectedness. For a proper flat geo…

The closed-fibre comparison yields a pushout of the actual section maps. This form retains the maps needed to compare a Noetherian model with an arbitrary base and its localizations.

For a proper flat geometrically reduced family over a locally Noetherian scheme, the actual native relative normalization has finite étale second map. On an affine base this follows from the computed section algebra and…

Actual flat base change identifies each localization of the section algebra with sections of the localized family. The proved local-family theorem gives finite projectivity and étaleness there. Localization detects proje…

Over an arbitrary scheme, the actual native relative normalization has finite étale second map and geometrically connected first map. The affine calculation uses actual Noetherian approximation of the section algebra; no…

An actual Noetherian model supplies finite presentation of global sections through canonical base change. Localizations then detect projectivity and étaleness. No finiteness is inferred merely from finiteness at stalks.

The actual flat section comparison identifies the extended section algebra with the global sections of the field-base-changed scheme. Geometric reducedness there supplies étaleness, which faithfully flat descent reflects…

For a proper scheme over a Noetherian local base, each closed-fibre idempotent is lifted by the proper cohomology theorem. If the closed-fibre section algebra is split, these lifts and lifts of residue coefficients give…

A finite étale local algebra is faithfully flat over its local base. Hence a regular system remains regular after applying the algebra map. Formal unramifiedness identifies the extension of the source maximal ideal with…

A connected finite-etale cover of a normal locally Noetherian integral scheme normalizes every local ring to an etale algebra. The proof first works on an affine neighbourhood and then localizes its normalization at the…

The stalk is the colimit of the rings of sections on open neighborhoods. Finite-etale inverse-limit descent supplies a cover of the spectrum of one such ring. Pulling it back by the neighborhood's affinization gives an a…

Evaluation of the sheaf isomorphism gives the native section-module equivalence. Restriction of scalars uses the existing base-ring action and its existing scalar tower.

A thickening is a surjective closed immersion. The affine equivalence for nil ideals supplies unique local lifts of maps and finite étale objects. Gluing on the directed affine cover gives the equivalence for arbitrary s…

Canonical aggregate for EtaleFundamentalGroups.FiniteEtale.Towers.

An integral etale algebra is finite. Over a Noetherian base, a preceding finite tower therefore makes the literal composite map finitely presented. Combining this with target-prime local Away etaleness gives etaleness of…

The tensor spectrum is identified with the literal finite-etale pullback. The fiber comparison then turns triviality of the induced fundamental-group action into a splitting of the actual tensor algebra.

The finite terminal-coproduct decomposition supplied by the Galois category is transported to the actual spectrum of a finite product of the base ring.

Every affine chart of the lower scheme has an actual finite étale model of the upper cover. The models and their recovery isomorphisms supply the transition maps, whose equations are detected by fully faithful radicial p…

This facade collects reconstruction, fiber-functor comparison, functoriality, and exact-sequence results for Galois categories. Canonical aggregate for EtaleFundamentalGroups.GaloisCategories.

The maps induced by composite functors compose strictly with the composite comparison. Replacing a functor by a naturally isomorphic one, and using that isomorphism in the fiber comparison, leaves the induced map unchang…

Objects and morphisms descend through a family of stage functors. A family of automorphisms compatible with refinement consequently glues to a unique automorphism. The descent assumptions concern objects and morphisms in…

The transition homomorphisms are restriction followed by the specified cone isomorphism. Identity and composition follow from ordinary functor coherence. Joint essential surjectivity and eventual morphism descent make th…

This file proves Stacks Project, Tag 0BMU: the automorphism group of the forgetful functor on finite continuous actions of a topological group is its profinite completion.

For a fiber functor on a Galois category, an object with nonempty fiber is connected if the canonical fundamental-group action on its fiber is pretransitive.

A trivial restriction has trivial restrictions on each connected component. Fixed points give actual terminal sections, so descent of the connected components assembles by finite coproducts to descent of the whole object…

The chosen inverse to the finite continuous-action equivalence supplies a canonical comparison isomorphism for the functor induced by a continuous homomorphism. The equivariance of the chosen counit shows that the result…

A continuous character of the fundamental group with discrete target factors through a pointed Galois object. The induced homomorphism from the opposite deck group is injective: the object is constructed from the actual…

For two composable functors of Galois categories, exactness of the induced sequence of profinite automorphism groups is equivalent to the two standard categorical essential-image criteria.

An exact functor from a Galois category to finite sets is isomorphic to any chosen fiber functor. As a consequence, exact functors between Galois categories commute with fiber functors up to isomorphism.

Fiber functors from Galois categories preserve finite colimits. This follows from the equivalence with finite continuous actions and exactness of the underlying-set functor on those actions.

This file proves Stacks Project, Tag 0BMV.

A natural isomorphism of finite-set-valued functors induces an isomorphism of their topological automorphism groups. For fiber functors, the associated finite continuous-action functors agree after restriction along this…

A natural isomorphism transports the kernel of restriction to another fiber functor. It also transports fixed points of the induced automorphisms. These are the two compatibility statements needed to use arbitrary geomet…

A continuous homomorphism between the automorphism groups of two fiber functors induces a functor between the corresponding Galois categories by restriction of finite continuous actions.

Precomposition of a finite-set-valued functor induces a continuous map on its automorphism groups. Conjugating by a natural isomorphism is continuous as well, so the two operations combine into a canonical continuous mon…

The point stabilizer of a Galois object fixes every point because its deck transformations act transitively and commute with the fundamental group. The proof below was extracted unchanged from EtaleFundamentalGroups.Fini…

A pointed Galois object identifies its fiber with its categorical automorphism group. Since categorical automorphisms act on the right of the fiber while the fundamental group acts on the left, the resulting quotient has…

The map on profinite automorphism groups induced by a functor of Galois categories is injective exactly when every connected target object admits the epi--mono span of Stacks Project, Tag 0BN7.

The image of the homomorphism induced by a functor of Galois categories is normal exactly when the connected objects having a point after applying the functor become finite coproducts of terminal objects, as in Stacks Pr…

For connected objects, inclusion of the actual stabilizers of two fiber points gives a morphism taking the first point to the second. The map is constructed as an equivariant map and lifted by the full fiber-action funct…

An automorphism of the covering object acts by inverse postcomposition on its over-category. Choosing an ambient monodromy element with the same effect on the distinguished point compares its induced fundamental-group ma…

For a finite fiber functor F, an object X, and a point x of its fiber, we compare the automorphisms of F fixing x with the automorphisms of the fiber-over-x functor on Over X.

An actual automorphism of a finite fiber functor transports fibers over a point to fibers over its translate. Under the existing stabilizer comparison, this transport is conjugation by that same automorphism.

A Galois object remains Galois over an intermediate object. Here the essential transitivity assertion is proved directly on the actual fiber-over-a-point functor, constructing each relative deck automorphism.

Actual factorizations of all terminal sections assemble to an epimorphism from the image whenever the target becomes a finite coproduct of terminals.

The continuous homomorphism on automorphism groups induced by a functor of Galois categories is surjective exactly when the functor is fully faithful. Equivalently, it preserves connected objects, lifts points of connect…

The composite homomorphism on automorphism groups induced by two composable functors is trivial exactly when every object in the image of the composite functor is a finite coproduct of terminal objects.

An epimorphic image of a finite coproduct of terminal objects in a Galois category is again a finite coproduct of terminal objects.

Canonical aggregate for EtaleFundamentalGroups.GaloisCovers.

This file supplies the abstract Galois-category part of the four equivalent characterizations of a finite étale Galois cover in Stacks Project, Section 58.7 (03SF). It uses the canonical mathlib notion CategoryTheory.Pre…

The original connected finite étale cover embeds openly in the normalization of the ambient proper scheme in its own function field. Its complement is exactly the inverse image of the original boundary. No extension acro…

Smoothness, properness, integrality and the hyperbolic genus inequality are supplied by the actual cover, rather than assumed for an intermediate object selected by Galois-category arguments.

Every subgroup of the original deck group is realized by an intermediate scheme. Relative deck transformations are identified on their actual scheme maps, not through an assumed comparison field.

The inverse image of a deck subgroup is open because it contains the point stabilizer. Its connected geometric realization gives a quotient morphism with exactly the prescribed subgroup of deck transformations.

The action of the fundamental group on a connected two-element fiber is transitive. A point stabilizer therefore has index two and is normal. The stabilizer is open for the actual fiber-functor topology, so its quotient…

If a finite-etale cover on the source of a scheme morphism is the pullback of an actual finite-etale cover on the target, the kernel of the induced map on fundamental groups fixes every point of its geometric fibre. For…

An extension problem is unchanged when its source is replaced by an isomorphic scheme. This file records the comparison at the level of actual finite-etale objects and actual pullback isomorphisms.

A chosen point of the geometric fiber of a finite-etale Galois cover gives the corresponding surjective finite quotient of the etale fundamental group. For a normal integral locally Noetherian base, this quotient is also…

This file expresses the canonical point of a field cover at a literal composite geometric point and transports its pointed quotient.

A finite Galois extension gives a categorical Galois finite-etale cover of the base field spectrum. This file identifies its deck group and its pointed fiber-functor quotient with the usual restriction homomorphism on Ga…

Finiteness of a dense function-field extension transports to the residue fields at the source generic point. In particular, the generic residue-field extension of a connected finite-etale cover is finite-dimensional.

A continuous homomorphism from an etale fundamental group to a finite discrete group has open normal kernel. The Galois-category equivalence therefore realizes that kernel by a pointed connected finite-etale Galois cover…

This file compares the generic geometric fiber of a connected finite-etale cover with embeddings of its function field. It then transports categorical Galoisness to the resulting finite separable field extension.

The pullback of rational functions is contravariant. Accordingly, this file compares the opposite of the categorical automorphism group of a finite-etale Galois cover with the Galois group of its function field.

For a dense morphism of integral schemes, the function field of the target is canonically the residue field at the image of the source generic point. The resulting equivalence is compatible with the residue-field map to…

The canonical identification of the function field of an integral scheme with the residue field at its generic point is natural for dense morphisms. This is the comparison needed to transport tensor-product maps between…

Pullback to the generic point preserves the full deck-transformation group of a finite-etale Galois cover over a normal integral locally Noetherian scheme.

The function field, its scalar map and its finite extension map are taken from the original finite étale scheme cover. Existing smooth proper model construction and finite-map extension then produce the proper curve map.

The proper source model, the original source open, its boundary and the Euler-characteristic formula are constructed from the actual cover.

The comparison is over the original base curve. It identifies the chosen smooth proper function-field model with the actual normalization containing the original open cover.

An open immersion between integral schemes identifies their function fields. The equivalence below is the literal function-field map induced by the open immersion, so it can be used in scalar-tower comparisons.

For a nonempty open immersion into a normal locally Noetherian integral scheme, the pullback of a connected finite-etale cover is connected. Hence the connected component occurring in an open-normal pullback model is the…

This file packages the normal-subgroup part of the fundamental equivalence between a Galois category and finite continuous actions of its fundamental group.

Finite discrete abelian kernel tests are invariant under isomorphisms of the source and target groups. Consequently, actual finite-etale extensions on a family of geometric local models provide the kernel condition over…

An open normal subgroup of an étale fundamental group is represented by a finite étale Galois cover. Choosing the point above the original geometric point identifies the fundamental group of the cover with that subgroup…

The source of an open-normal pullback model is canonically the complement of the pulled boundary. This file transports a cover across that isomorphism, uses the canonical function-field normalization as its extension, an…

Every open normal subgroup of the target fundamental group determines an actual pointed finite-etale Galois cover and an actual pointed Galois component of its pullback. This file packages those choices uniformly, so the…

The usual quotient construction for a fiber functor can live in a larger universe than its finite fibers. This file removes that presentation-level restriction by switching the universe of the fiber functor, applying the…

The quotient action of an arbitrary open subgroup is realized by a connected object, with no normality assumption and no restriction on the fiber universe. For a scheme this gives a pointed connected finite étale cover w…

An open subgroup containing the stabilizer of a connected cover is realized by an intermediate connected object and an actual morphism. An original deck transformation lies over this intermediate object exactly when its…

The quotient attached to a Galois object is natural under an isomorphism between fiber functors, provided that the chosen point is transported along the same isomorphism.

This file assembles the group-theoretic endpoint of the boundary argument. The geometric normalization-extension input is kept private until the purity theorem producing it is available.

This is the public categorical endpoint of the boundary argument. It does not assume injectivity, essential surjectivity, or the desired prosolvable comparison. Its input is an actual finite-etale extension object, toget…

Pullback of a connected Galois cover need not remain connected. Nevertheless, the connected component containing the pullback of a chosen geometric-fiber point is again Galois. This is the componentwise form that is vali…

The homomorphism from the deck group of a pointed pullback component to the original deck group is defined using the two pointed fundamental-group quotients. This file proves that it intertwines the actual component incl…

This file ties an actual connected component of a pulled-back finite-etale cover to the corresponding component of the tensor product of function fields. In particular, the comparison is selected by the given component m…

For a connected component of the pullback of a connected finite-etale cover along a dense morphism, the residue tensor at the component's generic point is Artinian. This is the pointwise finiteness input for comparing th…

A connected Galois component containing the chosen point of a pulled-back Galois cover realizes the restriction of the original fundamental-group map. The unavoidable comparison between two factorizations is an inner aut…

A pointed connected Galois component of the pullback of a pointed Galois cover has the same stabilizer kernel as the restricted original quotient. The component quotient therefore induces an injective homomorphism from t…

The image of the canonical deck-group homomorphism for a pointed Galois pullback component consists exactly of the original deck transformations preserving the component's geometric-fiber range. In fact, it suffices that…

The residue tensor of a pullback point has its two factor maps given by the two pullback projections. At the image of the generic point of an integral closed component, these factor maps identify with the corresponding f…

A point in the geometric fiber of a finite étale cover determines a lift of the geometric point to every pullback of that cover. The fundamental group at this lifted point is the inverse image of the original point stabi…

An open normal subgroup at the target of a morphism of connected schemes is represented by a finite étale Galois cover of the target. After pullback, the fundamental group at the canonical lifted point is the inverse ima…

The relative deck transformations are constructed from the original ones. Their transitivity on each actual geometric fiber proves the Galois property.

The graphs of deck transformations decompose the self-product of a Galois object. Applied to finite etale covers, the categorical product is the actual fiber product over the base scheme. This supplies the geometric rela…

The function field of the open complement of an ideal sheaf is the ambient function field. The algebra structure below remembers the canonical map from a chosen ambient stalk, which is needed for normalization at a bound…

This file provides a small algebraic bridge used when a geometric pullback describes a tensor product in the order opposite to the desired function- field tensor product. Surjectivity is transported using equivalences of…

The finite-etale base-change theorem constructs a normalization in an actual compositum, but its proof previously hid the maximal generic-fibre component used to select that compositum. This file exposes the canonical ma…

Selected generic tensor components, towers, and filtered-colimit descent. Canonical aggregate for EtaleFundamentalGroups.GenericTensor.

Fix a literal maximal ideal m of F ⊗[ K ] L, write M for its quotient-field component, and fix a prime q of the normalization of an integral model B in M. The fraction field of the prime localization at q is canonically…

For field towers K₀ → K₁ → F and K₀ → K₁ → L, the canonical balancing map F ⊗[K₀] L → F ⊗[K₁] L is onto. Consequently a fixed literal maximal component on the right is the same quotient field as the component cut out by…

Canonical aggregate for EtaleFundamentalGroups.GenericTensor.FieldComponent.

Let K' / K be any field extension and let L / K be finite. A maximal ideal of K' ⊗K L selects a field component. This file constructs the two canonical embeddings into that component, proves that their images generate th…

A field component selected from K' tensor[K] L is a quotient of that base-changed finite-dimensional algebra. Its degree over K' is therefore bounded by the original degree of L / K. This supplies one common factorial ex…

Suppose an integral enlargement A → B acts on the same field L, and the fraction field used on the left of a generic tensor product already acts on L. The multiplication component is then literally L. Combining that prod…

If K' already acts on L over K, multiplication gives a surjective map K' ⊗[K] L → L. Its kernel is therefore a maximal ideal, and the corresponding generic tensor component is canonically L as a K'-algebra. This is the c…

When K' already acts on L over K, the multiplication map selects a canonical maximal component of K' ⊗[K] L whose field is L. Consequently, etaleness of the integral closures of all tensor components implies etaleness of…

A component of F' ⊗[K] L canonically determines a component after first extending only to an intermediate field F. This file keeps the original maximal ideal and constructs the second-stage quotient map rather than postu…

For a finite field extension F'/F, scalar extension makes F' ⊗[K] L a finite faithfully-flat algebra over F ⊗[K] L. Consequently every fixed maximal intermediate component has a maximal final component above it. This fil…

A finite presentation over a base ring is compact with respect to filtered colimits. Applying this twice, to the forward and inverse maps of an equivalence after base change, and then moving the two inverse equations to…

Canonical aggregate for EtaleFundamentalGroups.GenericTensor.FilteredColimit.

The only compactness inputs are finite presentability of the two original models. No descent map, comparison, or inverse equation is an input field.

The actual pushout adjunction transports maps as coefficients change.

The tensor functor is Mathlib's existing CommRingCat.tensorProd. Its native maps and functor laws are retained. Descent is transported across the proved tensorProdIsoPushout, without calling the former raw descent theore…

The categorical base-change functor stores its objects with the algebra structure induced by an object of Under. Downstream algebra calculations use the canonical tensor-product algebra structure instead. This file is th…

Native tensor algebras are compared directly with their categorical pushouts. The original algebra actions are retained throughout, and the literal field inclusion squares follow from the native pushout comparison's natu…

Finite intermediate fields index the actual algebras R ⊗[k] F. Their inclusions form a filtered diagram with colimit R ⊗[k] L for an algebraic extension L/k. We use the existing finite-coefficient tensor lift and flat te…

A complete orthogonal family determines a map from a finite product of the base ring. The existing finite-presentation descent theorem descends that map. Its values on the standard idempotents give the required family, w…

The finite subsets of an extension field index the intermediate fields they generate. The transition maps and cocone maps are the literal inclusions. For an algebraic extension these fields are finite dimensional, by the…

Each tensor product is constructed with its original algebra instances in a one-tensor scope. The categorical interface is then identified with that native object. The equivalence below has arbitrary native algebra equiv…

The native tensor product is compared directly with the categorical pushout. The comparison uses the original algebra instances, never the algebras reconstructed from an Under object. Its coefficient naturality is proved…

For algebra models over R ⊗[k] F₀, morphisms and isomorphisms after extension of coefficients to an algebraic field extension L/k descend to an actual finite intermediate field containing F₀. The coefficient legs are the…

Fix an actual finite intermediate field F₀. The upper interval of finite fields containing F₀ is Under F₀, since the original index is a preorder. Each stage is the literal tensor ring R ⊗[k] E, read under R ⊗[k] F₀ thro…

The tensor universal property extends a map along an actual coefficient algebra homomorphism. The same construction on its inverse produces the extended equivalence. Both compatibility squares with a later coefficient al…

The fibre point is converted to the additive group of actual algebraic points. Its division equation and monodromy translation are consequences of the original finite étale cover and group scheme law.

The full Tate comparison and the explicit kernel calculation show that a character killed by n factors through monodromy of the actual n-multiplication cover. This uses the same integer n, without a larger auxiliary leve…

Multiplication by the order of a finite fibre permutation group kills its monodromy action. The actual pullback cover consequently has a section, constructed by fullness of the finite monodromy functor. This gives an act…

For a proper smooth commutative relative group law in characteristic zero, multiplication by a positive integer is finite étale. Geometric connectedness makes this an actual connected cover. At its unit point, its geomet…

In every characteristic, a connected finite étale cover of a proper smooth geometrically connected group is dominated by multiplication by its actual geometric fibre cardinality. Commutativity of the fundamental group ma…

Transport through a path to the unit identifies actual monodromy with translation by the same torsion point on every geometric fibre. Naturality against the deck translation proves the comparison; it is not an input.

The coefficient-field action on an actual division point agrees with the action on the geometric fibre. Consequently its displacement is the actual multiplication-monodromy torsion point. No comparison of actions is assu…

Evaluation at the unit of each multiplication cover gives a surjective continuous map to its actual torsion fibre. The collection of these maps separates the actual fundamental group: commutativity and transitivity recov…

The torsion comparison preserves the underlying scheme point. Translation by that same point therefore acts on the actual geometric fibre by torsion addition. Naturality of a fibre-functor automorphism against these deck…

Multiplication by m gives an actual morphism from the (nm) multiplication cover to the n multiplication cover. Under the identification of their geometric fibres with torsion points, this morphism induces the multiplicat…

Translation by an actual torsion section preserves the multiplication morphism. Its inverse is translation by the inverse section, so it gives an automorphism of the actual finite étale multiplication cover. On relative…

The kernel of all invertible multiplication coordinates is the actual residual core for finite groups of order prime to the characteristic. One inclusion uses the actual finite torsion groups and Cauchy's theorem. The ot…

Unit monodromy on the actual multiplication covers identifies the fundamental group with compatible families of actual torsion points. The group law is proved using deck translations, and the bijection and topology come…

The maps of multiplication covers give compatibility of monodromy at every positive torsion level. Compactness then realizes every compatible family: finitely many prescribed coordinates are realized at the product of th…

For every invertible positive integer, the actual multiplication fibre is a torsor under its torsion points. Deck translations prove that unit monodromy is an additive map to the actual torsion group.

The stabilizer of the actual unit point is the image of the fundamental group of the multiplication cover. The actual pointed map of multiplication induces the corresponding power map on the fundamental group.

The actual multiplication map is finite étale whenever its integer is a unit. Combined with the degree lifting theorem, this supplies a multiplication cover over every connected finite étale cover whose degree is inverti…

Unit monodromy gives actual compatible torsion points. Every such family is realized by compactness: any finite set of its coordinates is realized at the product of their indices, which remains invertible in the ground f…

The indices form the multiplicative submonoid of positive integers invertible in the ground field. The actual fibre comparison and its transition formula work in arbitrary characteristic over a separably closed field.

An extension of separably closed fields induces a canonical map of geometric fiber functors by precomposition on geometric points. This map is invertible: after comparison with any isomorphism of fiber functors, it is an…

The actual projection from the constant extension to its maximal separable intermediate extension.

For any scheme over an algebraically closed field, every extension of constants induces a fully faithful functor on finite etale covers. The extension may be transcendental and its target need not be algebraically closed…

Canonical aggregate for EtaleFundamentalGroups.GeometricFiber.

Arithmetic fundamental-group maps, descent, and exactness.

The geometric map is injective after extension to an algebraic closure.

The fundamental group of a separably closed field at any geometric point is trivial.

Connectedness after a separably closed constant extension descends to the base.

Exactness at the middle fundamental group for the separable constant extension of a qcqs scheme whose geometric base change is connected.

The arithmetic short exact sequence over a separable closure. Both maps are the actual continuous maps on geometric fiber automorphism groups.

Identifying the field fundamental group with its absolute Galois group preserves the kernel of the arithmetic map.

The geometric fundamental group has normal image after extension to a separable closure with connected base change.

Every categorical section after a separable constant extension factors through the pullback of an actual finite étale constant cover.

A section after a separable algebraic constant extension factors through an actual finite étale constant cover of the base.

A geometrically connected scheme over a field induces a surjection on the fundamental group of that field.

The geometric fiber functors at any two geometric points of a connected scheme are isomorphic. Each such isomorphism identifies their fundamental groups as topological groups and compares their finite-action equivalences…

The pullback pentagon identifies the composite fiber comparison with the canonical one. Consequently the original fundamental-group homomorphisms compose after transport along the specified equality of geometric points.

Transport along an equality of geometric points gives the actual pointed fundamental-group map. Its composition and identity laws follow from the canonical pullback comparisons. A map factoring through a separably closed…

This file constructs the forward functor in Stacks Project, Tag 03QR. For a separable closure K/k, an étale k-scheme is sent to its set of geometric points, with the discrete topology and the natural continuous action of…

This file proves Stacks Project, Tag 03QS: under the geometric-fiber correspondence, covering families in the small étale site of a field correspond to jointly surjective families of maps of sets.

The deck pullback here is the scheme-theoretic pullback functor. Its pointed fiber comparison is obtained from the actual over-category comparison and ambient monodromy. Under the canonical inclusion of the covering fund…

Pullback along an actual deck automorphism of a finite étale cover is identified with inverse postcomposition in its over-category. The comparison is the actual first projection of the scheme pullback.

This file assembles the finite Galois equivalence orbit by orbit. Its inverse sends a discrete continuous Galois set to the coproduct of the finite étale schemes corresponding to its finite orbits.

For a morphism inducing a surjective homomorphism on fundamental groups, its kernel is the intersection of the pointed Galois quotient kernels for covers which are actually pullbacks from the target. The descent conditio…

The canonical extension of the separable-closure fiber carries a compatible automorphism to its actual spectrum action on the larger geometric point. The original fundamental-group morphism preserves this same point acti…

For a tower of fields k → K → Ω, base change from k to K is compatible with the two geometric fiber functors valued in Ω. The comparison below is written directly on geometric points; this makes its compatibility with sc…

The field-specific comparison of geometric fibers agrees with the usual fundamental-group map after transporting the composite geometric point to the chosen point. The only remaining ambiguity is the explicit inner conju…

The homomorphism induced by an actual field-valued scheme morphism sends the field Galois action to precomposition of the actual geometric lift by Spec σ. This includes generic points and does not require a connected cov…

The actual field comparison used for the inertia image is whiskered through the original scheme pullback. This constructs the target base-point comparison and proves the map square exactly, including its inner conjugator…

The field source is a dominant preimmersion, so it is the actual generic point, rather than a further extension of the function field. The ambient separable closure is supplied explicitly. Finite fixed subfields are char…

This computation is proved over abstract fields, so callers retain their original field structures without unfolding the construction of the fiber automorphism group at those concrete fields.

This file supplies the finite part of the equivalence in Stacks Project, Tag 03QR. It directly transports the canonical Galois-category equivalence along the canonical topological group isomorphism from the absolute Galo…

Fullness of the actual geometric fiber action functor descends a fixed point to a section. No connectedness of the covering scheme is assumed.

Pullback along a morphism of schemes commutes with taking the fiber at a field-valued point, in particular at a geometric point. The resulting comparison isomorphism induces the continuous homomorphism on automorphism gr…

This module identifies geometric fibers of finite étale schemes with morphisms from the field point and with algebra homomorphisms from their section rings.

The canonical pullback comparisons for two successive scheme morphisms give the same map on fundamental groups as the corresponding composite pullback comparison. Two factorizations of one scheme morphism therefore induc…

For an arbitrary normal integral scheme, the actual generic absolute Galois kernel is the intersection of the restriction kernels of its finite Galois subextensions with etale normalization. The classifier is the existin…

The absolute Galois action on a generic fiber is restriction of the action of the fundamental group. A finite continuous absolute Galois action comes from a finite étale cover precisely when the generic kernel acts trivi…

A finite subfield of the separable closure is fixed by the generic kernel exactly when its spectrum occurs as the generic fiber of a finite étale cover. The comparison uses the literal spectrum and postcomposition of fie…

The kernel of the generic absolute Galois map is closed and normal. Its fixed field is Galois over the function field. For a normal integral scheme, the fundamental group is canonically the Galois group of this fixed fie…

For an irreducible scheme, the residue field of the generic point maps surjectively onto the spectrum of its actual stalk. The map is a closed immersion and hence a universal homeomorphism, even for nonreduced schemes. A…

The canonical extension from the separable closure to the algebraic closure compares the two actual generic fiber functors. Under this comparison, the canonical generic absolute Galois map is exactly the scheme-induced m…

The geometric generic point determines a continuous map from the absolute Galois group of the function field to the étale fundamental group. For a normal integral scheme this map is surjective, because dominant preimmers…

Full faithfulness of pullback for a flat finitely presented morphism with geometrically connected fibres descends an actual map into a finite etale cover of the base. The construction preserves its equality with the orig…

The existing henselian finite étale equivalence and the canonical extension of a separably closed geometric-point field identify the residue Galois group with the fundamental group at the actual closed geometric point. A…

Finite étale points in the fraction field of a normal henselian local ring specialize bijectively to residue-field points. The canonical section correspondence turns this same specialization into a natural isomorphism of…

This is the pointwise square for the constructed natural isomorphism, using actual spectrum precomposition on both geometric points.

The entire comparison of the generic and residue point actions is performed over abstract rings and fields. Callers supply their proved ambient and native residue ring-map computations and their actual point-action laws.…

The explicit natural fiber comparison transports the actual generic point action to the actual residue point action. Equality of geometric-point maps also preserves the literal point-action formula.

For the actual geometric-fiber pullback, the two original fundamental-group maps have trivial composite. The proof factors their composite through the fundamental group of the separably closed field, preserving the canon…

If pullback of finite-etale covers along a scheme morphism is essentially surjective, then the induced homomorphism on automorphism groups of geometric fiber functors is injective. The categorical result requires no full…

For a nonempty open subscheme of a normal locally Noetherian integral scheme, the induced map on etale fundamental groups is always surjective. If every finite-etale cover of the open subscheme actually extends across th…

For a normal locally Noetherian integral scheme, restriction to a nonempty open subscheme induces a surjection on etale fundamental groups. The proof uses the connected-object criterion for surjectivity: a connected fini…

Purely inseparable extension of the constant field preserves connectedness for an arbitrary scheme. The existing descent theorem for actual finite étale covers then identifies the canonical fundamental-group homomorphism…

The collapse of three actual pullbacks is independent of parenthesization. This is the comparison needed when an inverse-system transition preserves a specified geometric point by an equality of morphisms.

A finite étale scheme over the source of a finite étale cover is the same as a finite étale scheme over the base equipped with a map to that cover. Under this equivalence, the geometric fiber at a lifted point is the cor…

The existing stabilizer equivalence identifies the induced homomorphism with the inclusion of that stabilizer, including the chosen basepoint equality.

A monodromy-fixed geometric point of a finite étale cover gives an actual section with that value. Connectedness makes this section unique.

A section over one field-valued fibre identifies a connected finite etale cover with the pullback of its native Stein factor. The section determines a point of the Stein factor by actual section descent. The connected St…

The actual multiplication morphism, the two unit embeddings and the proper Künneth comparison identify its induced map with group multiplication. Consequently the fundamental group is commutative. Multiplication by an in…

The kernel at the middle term is the actual image of the geometric-fibre fundamental group. Stein descent supplies descent of connected covers; finite connected-component decomposition then supplies the categorical exact…

The native Stein comparison identifies a connected cover with a pullback from the base whenever the cover has a section on one fibre. Over a separably closed fibre this proves the finite-cover criterion for normality of…

For a proper smooth geometrically connected scheme over a separably closed field and a connected locally Noetherian second factor, the actual pair of projection homomorphisms is an isomorphism on fundamental groups at an…

The comparison isomorphisms are determined by the projections of the actual pullbacks. Their associativity supplies strict composition of pointed fundamental-group maps, rather than composition only up to conjugation.

An equivalence on finite étale covers makes the canonical map on fundamental groups bijective. Its inverse is continuous because these automorphism groups are compact Hausdorff. This gives the fundamental-group conclusio…

The canonical comparison between a pullback fiber and a composite geometric fiber is compatible with the first projection of the scheme pullback.

Regularity is required only along the boundary. Applying connectedness of Cartier complements to each connected finite étale cover proves the surjectivity assertion of Lemma 1.1 by the connected-object criterion.

The chosen coefficient component embeds in the pullback of the composite cover.

The supplied Galois comparison, the actual scheme-induced map, equality of geometric points, and the final projection to a geometric point are computed at abstract field and scheme structures. A caller supplies its prove…

The local hypothesis uses the original definition through normalization of each stalk's reduction. Its actual geometric stalk has irreducible spectrum. Outside the nonempty open, the generic point lifts to a nonclosed pr…

Both original conclusions of Stacks Project, Lemma 58.10.7 (Tag 0BQI), for arbitrary irreducible geometrically unibranch schemes. The hypotheses use the normalization definition at every actual scheme stalk. Both maps ar…

The inertia calculation in EtaleFundamentalGroups.TameRamification.Abhyankar.Basic proves that the normalization of the compositum is unramified over the chosen factor at every maximal ideal. The factor normalization is…

A prime in the normalization inside one separable closure defines one absolute inertia subgroup. This file maps elements of that single source into the etale fundamental group and compares all of their finite Galois cove…

An automorphism of a fixed separable closure of the function field maps to the fundamental group at the generic geometric point. This file compares its image on every pointed connected finite Galois cover with restrictio…

One prime in the normalization inside a fixed separable closure defines an absolute inertia source in the generic etale fundamental group. Its elements land in normalization-prime ideal inertia in every pointed connected…

This file isolates the arrow-level naturality needed to identify the finite pointed quotient of the absolute generic Galois map with ordinary restriction to the function field selected by the fiber point. Keeping this co…

The existing finite-level subalgebra and normalization owners construct the actual integral closures and their literal ring map. Prime contraction and localization are performed on those native objects, without introduci…

Fixing a prime in the normalization inside one separable closure gives a single absolute inertia subgroup. Its restriction to every finite normal subextension lies in the inertia subgroup of the contracted prime. This is…

The ambient radical producer chooses the finite Galois field and uniformizer. Its literal membership and proved integrality construct the root in the native finite normalization. The original power equation is retained u…

The established separably closed fraction-field theorem applies to the prime residue field. At a maximal ideal its canonical quotient map is bijective, so algebraic closedness transfers to the actual quotient. A separate…

The chosen finite Galois normalization contains an actual root of a base uniformizer. The finite-ring divisibility theorem supplies its actual tame order as a multiple of the prescribed exponent. Thus the literal finite…

The index subset is the literal range of the constructed finite-stage tame indices. The coefficients are the original maximal quotient of the absolute normalization. Thus both the index set and the restricted roots syste…

The established finite-field radical construction is exposed through its literal ambient element and finite-level membership. The later native normalization owner can consume this without opening the finite field's scala…

The finite field is the normal closure of the field generated by an actual root. A separate integral-closure owner constructs the integral radical from its equation, without mixing the ambient separable closure or prime…

The field-only constructor shares the existing coefficient fields and algebra. The group constructor shares the original 5-F group objects, independent P, maps and topologies. The last constructor inserts the SAME absolu…

Postcompose the SAME actual character with the proved full separable-roots comparison. Continuity, surjectivity, the SAME independent wild kernel and the original decomposition equivariance follow from their actual suppl…

Compose the existing continuous quotient equivalence with the actual separable-roots equivalence. The representative law retains the original quotient projection and the literal postcomposed character.

The already proved actual finite arithmetic supplies coprimality of n and e/n. The native coefficient theorem proves that this actual normalization preserves the independent principal-unit kernel.

Constructs the canonical tame morphism from finite normalization inertia to its residue-root group using the original DVR, Galois extension, and chosen prime.

Projects the SAME finite canonical character and actual residue-root embedding to their ambient residue scalar. The one-stage construction closes the finite root group before the finite inertia tower compares two stages.

The existing original coefficient decomposition morphism fixes the upper prime. Its literal normalization inclusion square then fixes the contracted finite prime. These proved facts construct the actual finite restrictio…

The proved finite field decomposition image supplies original decomposition lifts. The actual coefficient-automorphism surjection then identifies the target with the existing intrinsic finite-normalization stabilizer.

The constructed finite decomposition restriction is the literal restriction of coefficient automorphisms along the actual finite normalization inclusion. Its square follows from an actual original decomposition lift and…

The actual coefficient cancellation theorem shows that the kernel of the larger-stage restriction lies in the kernel of the smaller-stage restriction. No factor map or kernel inclusion is supplied as an assumption.

The actual surjective original-decomposition maps and their proved kernel inclusion construct the canonical restriction between finite intrinsic decomposition groups. Its computation law proves surjectivity and finite to…

Proves that the localized finite inertia action fixes the coefficient map into the original ambient residue field.

Transfers the ambient normalization inertia difference condition to the contracted finite normalization prime through the coefficient inclusion square.

The coefficient automorphism underlying the SAME intrinsic finite inertia restriction factors through the locally constant finite Galois restriction. Injectivity of the intrinsic subgroup inclusion then proves local cons…

Constructs the local ring maps induced by finite restrictions of original inertia. Proves their coefficient equations and compatibility with finite normalization towers.

Shows that a coefficient map satisfying the inertia difference condition becomes residue-trivial after localization, and applies this to the finite inertia action.

Constructs the inclusion of original inertia into the ambient Galois group and its restriction to the intrinsic inertia group of a finite normalization.

Both restrictions project to the same constructed normalization ring map. The group calculation is closed in its sparse full-Galois owner before the four original and finite D/I groups occur together.

Finite normalization faithfulness and finite Galois closure separation are both proved from the original inputs. No separation premise is added.

An intrinsic finite-normalization inertia element first lifts to the actual finite Galois group. The proved profinite inertia image then lifts it to the original, possibly infinite normalization inertia. Both lifts use t…

The constructed finite inertia restriction is the literal restriction of coefficient automorphisms along the actual finite normalization inclusion. Its square follows from an actual original inertia lift and the existing…

The actual coefficient cancellation theorem shows that the kernel of the larger-stage restriction lies in the kernel of the smaller-stage restriction. No factor map or kernel inclusion is supplied as an assumption.

The actual surjective original-inertia maps and their proved kernel inclusion construct the canonical restriction between finite intrinsic inertia groups. Its computation law proves surjectivity and finite tower composit…

Actual surjectivity lifts each intrinsic finite inertia element to the original inertia. The proved restriction factor equation and the SAME canonical scalar normalization tower then give the nF/nE power square. Restrict…

Maps finite local normalizations into the original residue field. Identifies these maps with the finite residue embeddings and proves their finite tower compatibility.

Defines the ring maps underlying finite normalization restriction and ambient inclusion, and proves that their Galois action square commutes.

The actual coefficient homomorphism preserves group multiplication. This calculation is proved before an upper prime or D/I group is introduced.

This ambient coefficient restriction is proved locally constant before the original inertia and the intrinsic finite inertia subgroups enter the scope.

Factors the finite ambient inclusion through the original normalization and proves compatibility of this inclusion with restricted Galois automorphisms.

Constructs the local ring map at nested finite normalization primes and establishes its injectivity under the DVR and Galois hypotheses.

Proves the multiplicative tower identity for ramification indices using the algebra structure induced by the finite normalization inclusion.

Constructs the residue-field embedding from a finite contracted normalization prime into the residue field of the original prime.

Constructs the finite Galois action on its normalization and the homomorphism restricting ambient Galois automorphisms to those coefficient automorphisms.

Constructs injective ring maps between nested finite normalizations. Proves their ambient inclusion triangle and the contraction identity for chosen primes.

Proves that the two restricted Galois automorphisms commute with the inclusion between nested finite normalizations.

An ambient automorphism fixing a larger finite normalization fixes every smaller finite normalization. The actual coefficient square and the literal injective normalization inclusion supply the implication.

Relates the upper ramification index to the lower index and the additive valuation of a lower uniformizer under the local inclusion.

This single-stage owner applies the SAME canonical maximal quotient/residue comparison before a second degree or a finite-stage ordering is introduced.

The existing canonical maximal-quotient equivalence transports the proved finite scalar action to the SAME quotient coordinate used by global theta.

The proved original finite-coordinate properties are preserved by the SAME canonical quotient comparison. Its root carriers and coefficient dictionaries remain inside their existing single-stage owners.

The scalar is the projection of the SAME constructed quotient coordinate. Its canonical normalized-raw evaluation closes the root group at one stage; subsequent tower comparisons can work entirely with scalars.

The common-upper-stage calculation uses the existing normalized raw maps. No finite root group is opened while the third finite stage is in scope.

Proves the power relation between raw coefficient-ratio residues of the same original inertia element at nested finite local normalizations.

Constructs the ambient residue of a finite local uniformizer ratio and supplies its unit coefficient witness. Expresses the canonical tame coordinate as its normalization power.

This is the existing intrinsic stabilizer residue morphism evaluated on the actual finite restriction, with its literal coefficient formula.

The canonical residue embedding intertwines the actual finite stabilizer action and the original decomposition residue action. Every coefficient formula and the underlying inclusion square are independently proved.

Constructs the homomorphism from finite tame-degree residue roots into roots of the same degree in the original ambient residue field.

Identifies the local ring map in the character composite with the finite inertia action and evaluates the ambient coordinate through a uniformizer ratio.

The SAME constructed canonical coordinate is the composite of the locally constant actual finite inertia restriction with its finite character and residue-root inclusion. Its source keeps the original Krull subgroup topo…

Constructs the ambient residue-root coordinate on original inertia by composing finite restriction, the canonical tame character, and residue embedding.

Combines the proved canonical character conjugation and the independently proved literal residue-embedding action square at this SAME finite stage.

The ambient residue-field embedding is injective. Composing it with the SAME normalized finite character therefore leaves the actual wild kernel unchanged, before pulling it back through original inertia restriction.

Proves compatibility of finite tame coordinates with the power maps determined by tame-order ratios. Deduces independence of the finite stage when tame orders agree.

The literal range of the actual tame index is nonempty and directed by divisibility. Its upper bounds are supplied by finite Galois composita.

Defines the intrinsic finite normalization inertia group and the full residue-root group of its tame degree.

Proves positivity and base-ring invertibility of the finite tame degree, and uses them to construct an index of the canonical roots system.

Defines the ambient residue power map with exponent given by the ramification index divided by the tame order, and factors the canonical coordinate through it.

Supplies the finite-stage tame arithmetic and proves that tame orders divide along inclusions of finite Galois stages.

The literal finite normalization supplies a primitive root in its own residue field. The existing residue embedding transports it into the original ambient residue field.

The factory closes the finite root interface before original inertia and decomposition elements occur. Every field is the already constructed map.

Proves nonvanishing of the finite contracted normalization prime and defines the tame and wild orders for its intrinsic coefficient-automorphism action.

The finite canonical character is onto its full native root group. The finite residue embedding preserves that full root group, and the actual original inertia restriction is onto. Their SAME existing composite is theref…

Actual intrinsic finite inertia restriction is onto. The SAME actual wild subgroups have proved primary cardinalities, prime-to-characteristic indices and target normality. The original field environment is closed before…

Literal prime contraction identifies the finite prime residue characteristic with the original base residue characteristic. No subgroup or inertia group is introduced during this arithmetic step.

The normalization group and field constructors are already closed. These proofs use only the actual subgroup's cardinality, actual tame/wild orders, and the original residue field.

The induced map uses the literal actual inertia restriction. Its image equality was proved from the original data, so preservation and surjectivity are conclusions, with no comparison premise supplied by a caller.

The original DVR, Galois extension and chosen prime supply the same native principal-unit subgroup at every finite stage. Its cardinality and index remain the previously constructed wild and tame orders.

The topology is the original Krull topology restricted to the literal normalization inertia subgroup. Closedness comes from the already proved openness of the original coefficient stabilizers.

The two original action names use the identical normalization action value. The inclusion is the standard inclusion supplied by ideal inertia stability.

The native actual inertia group inherits exactly the subspace topology of its literal subgroup in the original Krull Galois group. Its topological group and separation properties are inherited from that same subgroup.

This identifies its localization and quotient presentations using the already fixed canonical maximal-quotient equivalence.

Every stored object, map, action and topology is supplied by its existing original-input owner. The residue-only construction computes exactly the existing actual-degree roots system and group, as the computation theorem…

The quotient automorphism is the SAME original normalization residue morphism. Its localization presentation retains the already proved coefficient equation.

The actual inclusion is injective. Mapping into the original Galois group identifies its range with the original inertia subgroup; the already proved residue-kernel image then gives literal equality of subgroups of D.

The finite principal-unit groups vanish by their actual arithmetic theorem. The proved faithfulness of all actual restrictions then detects the identity in the original inertia group.

Only proved kernels of the actual normalized coordinates enter this comparison. The global subgroup itself retains its principal-unit definition.

The independently defined principal-unit subgroup is detected by the SAME finite canonical coordinates. Their proved equivariance preserves identity.

The independent subgroup is included by the actual I-to-D inclusion. Its proved stability under original conjugation yields normality in D.

The maps are the restrictions of the already constructed original inertia maps to the independently defined subgroups. Their joint faithfulness is inherited from actual finite inertia separation.

Its actual finite wild coordinates are p-groups, locally constant and jointly faithful. Closed-product permanence for pro-p groups therefore applies to the SAME original wild subgroup in its inherited topology.

An original inertia element is wild exactly when all its actual finite restrictions are in the existing principal-unit wild subgroups. This construction does not use the tame character or a kernel definition.

Every finite wild condition is closed because its actual restriction is locally constant. The original wild subgroup is their intersection, hence compact in the existing Krull/subgroup topology.

This is the coefficient action of the SAME original absolute residue morphism. Its scalar square is obtained from the concrete residue square and the coordinate formula of the full roots action.

Constructs the group homomorphism from the original inertia into the literal inverse limit of roots in the original normalization quotient. Evaluation at a degree is the stage-independent actual canonical finite coordina…

The original finite coordinates are locally constant in the original Krull subgroup topology. Their quotient-valued, degree-indexed coordinates retain local constancy, so the constructed map into the literal root limit i…

The existing character and root limit retain their native group owners. Their proved scalar evaluation and action laws reduce this equality to the actual canonical finite coordinate equivariance, with no comparison premi…

Both sides are evaluated through their already proved actual finite coordinates. No kernel or comparison assertion is an input.

The canonical quotient comparison preserves and reflects the identity. Consequently the constructed global character is trivial exactly when all of the SAME original finite canonical coordinates are trivial.

Compactness of the SAME original inertia, local constancy of the actual coordinates, their proved surjectivity, and directedness of the literal actual degree range supply the existing compact-limit theorem.

At an actual degree, choose a finite stage realizing that degree and apply the existing canonical e/n character. Its value is transported through the existing maximal-quotient residue equivalence. The evaluation theorem…

An arbitrary divisibility relation between actual tame degrees need not come from an inclusion of the selected finite stages. A common upper finite Galois stage proves the required power equation without such an assumpti…

The already proved stage-independent evaluation theorem transfers finite quotient scalar equivariance to the SAME coordinate of the original theta.

The SAME canonical quotient-root equivalence preserves and reflects identity. This comparison is proved before the global inverse-limit group is introduced.

The proved original finite-coordinate surjection is transported by the SAME canonical quotient comparison. Actual finite primitive roots are transported by that comparison as well. No root-existence or surjectivity is as…

Surjectivity and the proved independent wild kernel give the first isomorphism theorem. The actual quotient projection descends continuity, and compactness upgrades this SAME map to a continuous group equivalence.

The group, topology and quotient projection are the existing quotient constructions on the SAME original inertia and SAME independent subgroup. No character or kernel definition enters this native data owner.

The action is the original quotient-residue action on every existing root coordinate. Its plain application and scalar law close the action's native permutation data before the original character is compared with it.

The coefficient map acts on the existing root coordinates. Its group laws are proved here before an original decomposition element is introduced.

The carrier, group, and topology are exactly those of the existing actual roots limit. This native object is shared by the quotient isomorphism and the original decomposition action, so neither must reopen the raw index.

Supplies the exact stage-group family and group-system class on the existing actual roots system. Both are the original prime-to-roots groups and their literal restriction; no group operation or inverse system is replace…

The coefficient inclusion is restricted along the proved cofinality of the SAME actual finite tame-degree range. Its inverse is the requested continuous group equivalence from the SAME actual roots group to the full sepa…

The algebraic inverse comparison supplies the literal group map. Its function is the SAME continuous comparison; injectivity and surjectivity are proved before introducing topologies. The character consumes this actual m…

The existing roots system already chooses the discrete topology at every stage. Its existing inverse-limit topology is therefore Hausdorff, and the existing coordinatewise group operations are continuous.

Each data function is the underlying function of an existing actual map. The coefficient and conjugation comparisons are proved separately; none is a hypothesis or a field of the diagram.

Let a group G act on a commutative ring B. A geometric point Spec Ω ⟶ Spec B represented by φ : B →+ Ω is fixed by an element of G exactly when that element acts trivially modulo ker φ. Thus the scheme-theoretic geometri…

A morphism to an affine base supplies the algebra structure on global sections. The deck automorphism of those sections is obtained from the actual scheme automorphism. Naturality of isoSpec then compares its normalizati…

For a normal domain B over R, the integral closure of R inside B maps bijectively to the integral closure of R inside the fraction field of B. Indeed, an element integral over R is integral over B, so normality puts it b…

For an R-algebra B, an automorphism of B extends to the relative normalization of Spec B → Spec R by normalizationDesc. Under the canonical identification with Spec (integralClosure R B), this extension is exactly the sp…

The base localization is the scheme's literal local ring, using its germ map and the existing stalk-to-function-field map. The normalization prime is extended by the literal inclusion in the same Galois field, and become…

An element of the actual ramification subgroup restricts to ramification at every finite Galois layer. In residue characteristic zero those finite groups are trivial. Every field element belongs to a finite Galois layer,…

Localized inertia, normalization inertia, residue arithmetic, and ramification-index divisibility. Canonical aggregate for EtaleFundamentalGroups.Inertia.

The complement chart and the principal localization identify the same open subscheme as the inverse image of the original complement. Their canonical maps form pullback squares. This identifies the source of a base-chang…

The boundary-away square identifies the actual finite-etale pullback with the successive pullbacks through the etale chart and its localized stalk. This source isomorphism intertwines all pulled-back deck transformations…

At a point whose stalk is a domain, a local Cartier equation remains a nonzero element in the fraction field. Consequently the canonical map from the spectrum of that field to the ambient scheme factors through the compl…

At a divisor point with discrete valuation stalk, the inverse image of the complement is the spectrum of the actual fraction field. The horizontal map is the previously constructed canonical factorization through the com…

The actual fraction-stalk square identifies the finite-etale pullback over the local fraction field with the pullback over the stalk. The canonical normalization comparison is an isomorphism and therefore transports ever…

Every element of the fixed field of a closed normal subgroup lies in a finite Galois subfield of that same fixed field. Thus the subgroup is the intersection of the finite Galois restriction kernels containing it. This g…

profinite 群の部分集合 s が生成する閉正規部分群は、s を含む全ての開正規部分群の 共通部分である。開正規部分群は有限商への核なので、これは「生成元を殺す有限商の 核を交わす」という記述との比較である。 惰性群の和集合を s に取ると、原稿1.1の閉正規生成部分群に適用できる。 ただし、この群論だけで strict henselization の基本群の像を正規化の固定部分群と 同一視できるわけではなく、その幾何学的比較は別…

Constructs the canonical finite tame character on intrinsic coefficient inertia with values in its full residue-root group.

Evaluates a precomposed canonical tame character followed by a residue ring map. Supplies the corresponding local coefficient map and a uniformizer-ratio witness.

The existing primitive root determines the full root-group cardinality. Mathlib's coprime-power bijection then proves that the actual e/n power normalization preserves surjectivity and the independently defined wild kern…

Constructs the native residue action on canonical tame roots and identifies it with the localization action. Proves equivariance under stabilizer conjugation.

Packages the intrinsic canonical finite tame character as a morphism between its native inertia and residue-root group objects.

Defines the scalar projection and local coefficient map of intrinsic inertia, and evaluates the canonical character using a uniformizer-ratio coefficient.

The group is the existing native residue stabilizer, with the existing coefficient-automorphism action. Ring-only contraction and action comparison prove the stability and lifting statements used by actual finite restric…

Defines conjugation of intrinsic ideal inertia by a stabilizer element and identifies its underlying coefficient algebra automorphism.

Defines the group objects for coefficient-automorphism inertia and the full residue roots of its computed tame order.

Defines the tame order and principal-unit kernel order for the canonical coefficient- automorphism action on a native normalization algebra.

The actual local inertia-character image supplies a primitive root of the intrinsic tame order. Consequently its full root group is preserved by every residue-field embedding.

Proves positivity of the intrinsic finite tame order and its invertibility in the original local coefficient ring under the stated hypotheses.

The subgroup is literally the existing principal-unit subgroup in native coefficient-automorphism inertia. Its primary order, character kernel and tame quotient cardinality supply the three Sylow image inputs. No field p…

This is the same existing principal-unit subgroup. Its raw automorphism Group and action are retained inside the native owner, so original field consumers do not reopen them beside their scalar towers.

The native inertia subgroup retains its underlying coefficient automorphism. Consequently its identity is detected by the literal coefficient ring map.

Intrinsic algebra-automorphism operations are closed in this native owner. The output uses only composition of the actual coefficient ring maps.

Constructs a group morphism into intrinsic ideal inertia from a coefficient-automorphism map satisfying the inertia difference condition.

Extracts the coefficient ring map of an intrinsic inertia element and proves that this ring map determines the element.

Constructs local residue-root group objects and maps induced by quotient automorphisms. Identifies the native residue morphism with the localization roots action.

The existing native intrinsic residue morphism has its actual algebra- automorphism coefficient formula after canonical localization transport.

Proves coefficient preservation by intrinsic algebra automorphisms and constructs the resulting native quotient-residue morphism.

Only the ambient local rings along the Cartier divisor are required to be regular. In particular the ambient scheme is allowed to be reducible and nonnormal elsewhere. At the selected component's generic point we constru…

Every prime over the closed point is represented in the fixed algebraic closure of the base residue field. The actual affine normalization comparison then turns geometric fixed-point triviality into the ideal inertia con…

At every finite Galois cover, normalization-prime inertia has an actual canonical source: the fundamental group of the inertia fixed field. This file expresses a profinite element by compatible finite-level source lifts…

The canonical fundamental-group quotient of the inertia fixed field is transported from the function-field Galois group to the automorphism group of an actual finite-etale Galois cover. Its range is the categorical norma…

Membership in a divisorial inertia group can be expressed without constructing a strict henselization: in every pointed connected finite Galois cover, the image of the element belongs to normalization-prime inertia above…

The image of a geometric local fundamental group in a pointed finite Galois quotient is a finite subgroup of the deck group. Its order therefore divides the deck-group order, and more sharply divides the order of every s…

A finite ideal-inertia subgroup is trivial once its order is prime to every rational prime. The finite-etale specialization below applies this criterion to the range of the canonical inertia-fixed-field quotient, without…

This file constructs the actual pointed categorical quotient of the finite field cover after restriction along the normalization-prime inertia fixed field.

The pointed categorical quotient of the finite Galois field cover is the usual restriction quotient. Restricting that cover along the canonical inertia-field morphism therefore realizes the canonical divisorial quotient,…

The actual pointed quotient of the finite field cover along the inertia fixed field agrees with the canonical unconjugated divisorial quotient after transporting the deck group back to the finite Galois group. Its transp…

Coprimality of one actual pointed finite inertia image with every rational prime forces the corresponding normalization-prime ideal inertia subgroup to be trivial. The declaration is implemented in DivisorialPointedQuoti…

The actual pointed finite-cover quotient recovers normalization-prime ideal inertia after the canonical deck-group and base-point conjugation transports. Consequently, coprimality of its finite image with every prime for…

The finite quotient attached to the inertia fixed field factors through the usual fundamental-group map of spectra after transporting the equality of the two base points. The comparison of fiber functors contributes one…

For a normalization prime in a finite Galois extension, ideal inertia fixes an actual intermediate field. The Galois group over that fixed field maps to the original finite Galois group by scalar restriction, and its ima…

The inertia fixed field constructed from a normalization prime has an actual absolute Galois group. Via the geometric fiber functor of its spectrum, its canonical finite quotient has image exactly the selected ideal iner…

For a morphism j : T ⟶ U, functoriality of the geometric fiber gives the canonical homomorphism from the fundamental group of T to that of U. This file records its image and its finite monodromy on a pointed finite-etale…

First descend the complete orthogonal family by the existing finite-product algebra construction. All of its group-equivariance equations then descend in one further transition, using a polynomial algebra with finitely m…

First pull the specified point into an etale chart, then to the chosen prime localization of its stalk. The canonical normalization comparisons are actual isomorphisms at both steps. The resulting point has exactly the o…

Prime rigidity makes the intrinsic coefficient inertia trivial. The proved normalization-restriction equivalence transfers this result to the original finite-Galois inertia group, with its original action and original pr…

Surjectivity on fundamental groups makes restriction fully faithful. A deck transformation therefore extends to the given finite etale cover. The normalization maps canonically to that extension, compatibly with the deck…

The actual pointed quotient and its canonical restriction map are constructed and compared before choosing an intermediate field or a separable closure. Their geometric points therefore use the same field structures thro…

The two algebras are compared on actual maps of global sections and their germs. This keeps the canonical scalar structures of the local ramification theorems while connecting them to the actual relative normalization.

The coefficient algebras are compared before extracting a prime from the normalization point. The resulting prime and Galois action therefore use exactly the coefficient structures of the normal-crossings ramification th…

The normalization of the actual finite-etale cover is étale when all its closed geometric-point deck stabilizers are trivial. Its function field, scalar tower, Galois extension, and normalization comparison are construct…

The function-field automorphism defined using generic geometric fibers is exactly the pullback on rational functions of the actual deck transformation. In particular it intertwines the pullback on global sections with th…

For an affine connected finite etale cover, the algebra on its function field constructed from its structure morphism factors through the canonical function-field embedding of the cover. Consequently the normalization-po…

The coordinate homomorphism of a normalization point retains its actual map to the base. Its kernel inertia, with the intrinsic Galois action on the integral closure, is exactly the geometric fixed-point condition.

The original inertia image theorem and lying over show that a finite Galois restriction kills all inertia in an arbitrary Galois normalization exactly when every inertia group in the finite normalization is trivial. Neit…

For a finite Galois extension of the fraction field of a normal domain, the canonical Galois action on its actual integral closure has the original normal domain as its full invariants. The literal invariant-base map is…

The domain keeps its original Krull topology. Finite dimensionality makes the target's Krull topology discrete, so the existing continuous restriction is locally constant before any normalization or coefficient action is…

Defines the Galois group object of a finite intermediate field and the restriction homomorphism from the ambient Galois group.

Every coefficient belongs to its finite Galois closure. Agreement on all actual finite restrictions therefore gives agreement on every coefficient.

At each original prime, the actual finite-Galois invariant-neighborhood theorem supplies a principal localization of the inertia-fixed algebra which is etale over the original normal domain. Trivial inertia makes the lit…

Defines the ramification-index-to-tame-order normalization exponent and the resulting canonical character on finite ideal inertia.

Proves stabilizer-conjugation equivariance for powers of the finite ideal tame character and for its canonical normalization.

Evaluates powers of the finite ideal tame character through uniformizer ratios, including the canonical normalized character.

Proves that normalization preserves the finite principal-unit kernel and that the canonical character surjects onto its full root group.

Defines the canonical character scalar and localized inertia ring map. Produces a ratio unit giving both the local coefficient equation and scalar value.

Proves that an integer invertible in the original base ring is coprime to the finite ideal character normalization exponent.

Derives that the finite normalization exponent is a power of the residue exponential characteristic using wild-order and inertia-cardinality formulas.

The principal-unit kernel at the original prime has the power order proved by its actual localized automorphisms. An invertible radical exponent is coprime to that same residue characteristic, so it survives the genuine…

Constructs the original ideal-inertia group object, its localization comparison, and the finite tame character on that original group.

Transports the principal-unit wild subgroup to original ideal inertia and computes its cardinality. Proves surjectivity and the kernel formula for the finite tame character.

The actual finite tame and principal-unit wild orders multiply to the ramification index times the inseparable degree of the native residue extension. The existential factorization interface follows from this explicit id…

The coefficient map from the original local ring into the prime localization is local because the prime lies over the maximal ideal. Hence invertibility of the actual tame order in the upper local residue reflects to the…

Defines the finite tame and principal-unit kernel orders and factors the inertia cardinality. Establishes positivity and residue-field invertibility of the tame order.

The actual localization inertia equivalence transports the local tame-image cardinality to original ideal inertia modulo its independent wild subgroup.

Proves that the finite tame order at the original normalization prime divides its ramification index.

Proves that the principal-unit wild order of the original normalization action is a power of the residue exponential characteristic.

The already constructed localized finite-level colimit supplies an actual finite-level representative. A denominator for this representative becomes a unit on a genuine principal étale neighborhood. The two literal coeff…

Every object is the native principal localization constructed in the neighborhood index. Native localization lifts provide the transition maps and the maps to the literal upper invariant prime localization. Their generat…

The finite-Galois normalization theorem supplies an étale denominator at each actual invariant stage. Multiplying it by any prescribed denominator outside the contracted prime gives a further étale neighborhood. These ne…

Bundles a finite Galois intermediate field as a coefficient algebra and supplies its inherited field, scalar-tower, finite-dimensional, and Galois structures.

Compatibility import for the shared ring-theoretic owner.

Compatibility import for the shared ring-theoretic owner.

The existing native finite-normalization diagram supplies injectivity, equivariance and the full inertia image. The ring-only preimage theorem therefore identifies the already constructed normalization-preimage stage wit…

An actual intermediate level is first regarded as its inherited A-subalgebra of L. The generic normalization owner then constructs the normalization and the preimage of the actual upper invariant algebra, without K/Galoi…

The field constructors are finished before the ordinary ring/group image argument. All groups, rings, actions, maps, and primes are the existing literal objects. Every non-data input to the ordinary image theorem is prov…

Proves finiteness of the intrinsic coefficient-automorphism group of a finite normalization.

Proves that the native normalization at a finite Galois level is a Dedekind domain under the original base-ring hypotheses.

When the relative normalization of a finite étale cover of an open subscheme is finite étale, it is an extension of the original cover. The restriction isomorphism comes from the actual open pullback and normalization co…

Fraction-field uniqueness proves faithfulness in the native finite field owner. The actual finite-stage map then uses that closed result.

The fraction-field extension theorem is applied in the native coefficient field owner. The original ambient field does not enter that proof.

Transfers the inertia difference condition through normalization restriction and lifts intrinsic finite-normalization inertia to finite-field inertia.

Constructs an original finite-field inertia element whose coefficient ring map is the prescribed intrinsic normalization inertia map.

The actual finite Galois normalization supplies the finite-action hypotheses used to compare a uniformizer radical exponent with its tame inertia order.

Proves positivity of finite-normalization tame orders and their invertibility in the original local coefficient ring.

The native finite field supplies the already proved native normalization order theorem directly. Its scalar environment stays inside that theorem; no original prime or inertia group is opened in this adapter.

Identifies the kernel of the canonical finite normalization character with original wild inertia and proves surjectivity onto the full roots group.

These group-theoretic lemmas transport the range of a finite quotient through successive homomorphisms without unfolding the quotient construction.

Defines the finite intermediate field ring object, its ambient inclusion, and individual Galois restriction maps, and proves their commuting square.

A normal p-subgroup of prime-to-p index is the unique Sylow subgroup. Consequently a surjective homomorphism sends any p-subgroup of prime-to-p index onto that distinguished subgroup. No preservation premise is used.

The algebra defined by the structure morphism of Spec K agrees with the composite of the two canonical fraction-field maps. This comparison is made before installing the scalar tower, so the resulting fraction-ring struc…

Canonical aggregate for EtaleFundamentalGroups.Inertia.Galois.

At a characteristic-zero height-one prime, the ramification index is the order of the corresponding inertia subgroup. Lagrange's theorem therefore makes it divide the order of the full Galois group, which is the field de…

The chosen component is normalized using its actual structure morphism. Its point is transported from the component-inclusion normalization through the identity of source schemes over the base. The resulting deck lift an…

The generators are the original ideal inertia groups of the literal normalization rings on all nonempty affine charts. The existing actual normalization-chart pullbacks and the finite Galois inertia image theorem identif…

The generators here are original automorphisms fixing an actual point of the normalization in the separable closure and inducing its identity residue action. Their union equals the original affine ideal-inertia generator…

Every normalization prime on an affine chart localizes to a maximal prime over its actual scheme point. Conversely every maximal prime over an actual scheme stalk contracts to a prime on each affine neighborhood, and loc…

The local model is the constructed geometric etale stalk, its generic map is the actual Cartier-complement factorization, and its closed point is the evaluation into the originally specified algebraically closed field. T…

The categorical composition and its native group dictionaries are closed in this group-only owner before concrete field and normalization data enter.

The closed fiber of an integral algebra has dimension zero. If its set of primes is finite, its spectrum is discrete. Its singleton idempotents lift uniquely along the Henselian pair, giving actual idempotents in the int…

The unique idempotent isolating a closed-fiber prime has exactly that prime's stabilizer. Over a local base with separably closed residue field, integrality makes the residue quotient purely inseparable, so the prime sta…

The uniquely supplied isolating idempotents form a complete orthogonal family. Products of distinct members lie in every maximal ideal, as does the complement of their sum. Existing Jacobson idempotent rigidity then prov…

An element supported on an idempotent and fixed by its stabilizer can be transported over the finite orbit. Summing one transported element per orbit point gives a full invariant. Orthogonality ensures that projection on…

Proves that the ideal-to-local inertia comparison preserves the conjugate induced by an element of the original stabilizer.

Extends an intrinsic finite-normalization automorphism to a finite extension of fraction fields with the corresponding coefficient square.

Proves a residue-characteristic power order law for intrinsic normalization automorphisms whose prime localizations act by principal units, including triviality in residue characteristic zero.

Constructs a finite fraction-field lift of an integral automorphism together with the local principal-unit order laws.

The fraction-ring restriction used by ramification theory and the literal restriction used by normalization geometry agree on the embedded integral closure. The comparison follows by applying its injective inclusion into…

The action on the second tensor factor preserves inertia at every ideal and its contraction. In particular, this proves Stacks Project, Tag 0BSS for arbitrary base change from the fixed subring. No finiteness or primalit…

The existing flat invariant equivalence identifies the base-changed original fixed algebra with the fixed tensor algebra. Its composition with the right tensor inclusion and a principal localization gives the actual neig…

The actual geometric stalk supplies a finite family of isolating idempotents. Descending this family and its action to an étale neighborhood constructs a principal étale neighborhood in the original inertia-fixed algebra…

For a finite group, the fixed subalgebra is the kernel of the linear map r ↦ (g ↦ g • r - r). Flat tensor product preserves this kernel, and tensor product commutes with the finite product indexed by the group. Consequen…

The fixed subalgebra is computed using the original normalization inertia action. Its contracted-prime localization and native map to the normalization prime localization are the already constructed generic objects and R…

The generic action on a localized normalization and the action obtained from its integral-closure universal property have the same value on every element. Consequently, the two definitions of the inertia subgroup coincid…

Canonical aggregate for EtaleFundamentalGroups.Inertia.Localized.

This file defines the inertia subgroup at a normalization prime after localizing the base at a prime ideal. The construction uses only the canonical fraction-field maps and the generic action on an integral closure; it h…

This file passes from a height-one prime of a regular domain to its DVR localization, proves residue separability there from characteristic zero, and applies the Dedekind-domain inertia-cardinality theorem. All fraction-…

At a height-one prime with characteristic-zero residue field, the localized normalization inertia group is cyclic. This file turns that source theorem into a noncomputably chosen additive coordinate system indexed by the…

At a height-one prime, normality and Noetherianity already make the local base a discrete valuation ring. Thus the inertia-cardinality formula does not require regularity of the ambient ring.

This OUTPUT certificate includes literal residue algebraic and separable closures, the full invertible exponent index, both original exact sequences, normality and the complete pro-p/characteristic-zero laws for the SAME…

The group data are shared with the existing original DVR diagram. This retains its independent P, literal I/P and existing subgroup/quotient topologies once. The absolute diagram adds exactly the residue map and full-tar…

Store the original two fields and coefficient algebra once. The separable field, residue Galois group and roots group are computed from these data. The roots group is literally the full primeToRootsSystem inverse limit,…

Constructs bundled maximal quotient fields and their residue coefficient actions for integral algebras. Proves algebraicity of these actions and specializes them to normalization residue fields.

This data-only interface closes the native group and root carriers. It stores actual functions and no propositions. Its sole factory uses the existing canonical normalized character, conjugation and residue action; equiv…

Surjectivity on coefficient automorphisms and the proved action comparison transfer the literal inertia difference condition. No field or scalar tower occurs in this argument.

Establishes module and automorphism finiteness for native finite normalizations, then proves positivity and base-ring invertibility of their intrinsic tame orders.

Only the original finite separable field supplies normalization finiteness and torsion freeness. The field environment is closed before the prime and its residue field enter the principal-unit order proof.

The native group objects retain exactly Mathlib's original Krull topology. The finite native owner inherits its already proved discrete Krull topology. No normalization ring or inertia subgroup is opened in this field-on…

Constructs conjugation by an ideal stabilizer element on the original ideal inertia group and records its underlying group expression.

The subgroup order and pointwise ideal-action interfaces are closed here, with only a ring and its acting group. The map is the literal inclusion.

The native coefficient algebra owns the ring and coefficient action. Its field structure is opened only here. Restriction of the original field action is compared with normalization functoriality through their literal in…

Literal membership in the subalgebra and the already proved ambient integrality construct the actual normalization element. Its power equation is inherited through the two subtype inclusions. No fraction-field tower or c…

This is an output certificate on a concrete native diagram. It is never an input to the original-input theorem. Both exact sequences, the independent wild subgroup, the actual invertible degrees, the canonical continuous…

This stores group objects, their actual maps, the independent wild subgroup, and existing topologies. It stores no exactness, normality, surjectivity, comparison or other conclusion. The roots target is computed from the…

Only the two coefficient fields and the actual set of invertible natural exponents are stored. The target is computed as the literal root inverse limit over these degrees. No root group or comparison is supplied separate…

Forgetting coefficient linearity is a homomorphism. Transport through the fixed maximal-quotient equivalence preserves the literal coefficient equation.

Constructs the automorphism-group comparison between a stored algebraic closure and its relative separable closure. Records preservation of surjectivity and kernels under target group isomorphisms.

These group objects store exactly the existing compatible-family limits. The stored coefficient algebra is installed in this field-only owner, before any original fraction field or tame-degree subset is introduced.

The two constructed equivalences are composed only after the coefficient field and cofinal restriction owners have proved their own coordinate laws.

For a normal subgroup of the automorphism group of a normal field extension, fixing an intermediate field is equivalent to fixing every embedding of that field into the ambient extension. The intermediate field need not…

Canonical aggregate for EtaleFundamentalGroups.Inertia.Normalization.

At a characteristic-zero height-one divisor, the cardinality of the ideal-theoretic inertia subgroup equals the ramification index. A unit ramification index therefore remains prime to every prime residue characteristic…

The localized inertia subgroup at a height-one normalization prime determines an actual intermediate field of the generic Galois extension. In residue characteristic zero, the degree from this fixed field to the total fi…

For a normalization prime above a height-one prime, this file contracts its localized form to the normalization in the corresponding inertia fixed field. The construction is canonical and remains in the general integral-…

Localizing a normalization at a prime below Q does not change its inertia subgroup. This is the comparison needed to state the final one-point theorem using the original normalization prime, while applying the existing h…

The original decomposition morphism to the separable residue Galois group acts through the same literal quotient ring action used by the tame character.

Proves that the maximal quotient of the normalization of a DVR in a separable closure of its fraction field is algebraically closed.

Identifies the literal normalization residue as an algebraic closure of the base residue field and constructs the restriction isomorphism to its separable residue Galois group.

Constructs the decomposition-group morphism to the separable residue Galois group and proves surjectivity. Identifies its kernel image with original ideal inertia to obtain the absolute residue exact sequence.

The source is any qcqs morphism. Flat base change computes global sections by a tensor product, and localization commutes with integral closure. These identifications agree with the actual canonical normalizationPullback…

An endomorphism of X over S extends to the relative normalization of f : X → S by normalizationDesc. The actual normalization/base-change comparison commutes with this extension and the pulled-back endomorphism. This com…

A monomorphism between finite-etale covers is a direct summand in the Galois category. Forgetting to schemes preserves that coproduct, and relative normalization preserves the resulting decomposition. Consequently, the a…

The inverse image of a normalized component is the original finite-etale component. This supplies the passage from component preservation on the normalization to component preservation on the cover itself.

The finite connected decomposition of the original cover has clopen images in its normalization. Their union contains the dense image of the cover and is closed, so it covers the normalization. The open-immersion lifting…

The lift of a deck transformation fixing a point of a normalized component maps to the prescribed deck transformation under the actual pointed-component quotient. The map is the canonical quotient already defined using t…

For an arbitrary DVR, its fraction field, a separable closure and a maximal ideal of the literal integral closure, construct every conclusion of Stacks Project, Lemma 58.13.6. The two exact sequences retain original D, I…

For an arbitrary possibly infinite Galois extension of the fraction field of a DVR and a maximal ideal of its literal normalization, all conclusions of Stacks Project Tag 0BUA are assembled on one concretely constructed…

Every normalization point lifts to a normalized component of the pulled-back cover. These component inclusions are open immersions, and therefore supply an actual open cover on which étaleness can be checked.

If B is integrally closed, an element of its fraction field integral over R already belongs to B. Thus the two actual integral closures are canonically isomorphic. This isomorphism intertwines automorphisms and, on spect…

Let Rm be the localization of R at M, and let Bm be the localization of an R-algebra B at the image of M. The actual map between integral closures is constructed by mapping integral elements and extending scalars. Mathli…

The algebra automorphism on the localized cover is constructed from the original automorphism by the localization universal property. The cartesian normalization square then lifts each compatible geometric point, preserv…

The localization square of actual coordinate rings is a pushout. Its spectrum identifies the affine localized source with the categorical pullback. The corresponding source isomorphism extends to normalization, and uniqu…

At a point of the open, the map from the spectrum of the stalk factors through that open. The original finite etale cover is therefore already integral after base change, so its relative normalization is itself. The actu…

Normalization of an integral source is integral and its structure map is separated. If this structure map is unramified, fixing a nonempty test morphism forces an actual normalization endomorphism to be the identity.

Restricts the already constructed maximal-quotient residue equivalence to roots. Both the scalar evaluation and inverse needed for surjectivity use this same equivalence.

The actual coefficient map descends from the base local ring to its residue field at every prime lying over its maximal ideal. Its field-domain injectivity identifies the two residue characteristics, including mixed-char…

A maximal prime of the literal normalization contracts to the closed point by the existing integral-closure prime theorem. Thus the already constructed residue-action target is exactly the quotient automorphism group ove…

An actual normalization endomorphism fixing a point and acting trivially on its residue field fixes the canonical residue-field point morphism. The proved normalization rigidity therefore makes that endomorphism the iden…

Each element of the original normalization residue is represented by an integral element lying in a finite Galois intermediate field. At that finite stage the actual residue extension is normal by the finite invariant-ac…

Defines the native group object of roots of a fixed degree in the original normalization residue field.

Normality of the actual normalization residue extension gives the existing restriction equivalence with its relative separable closure. Composing this actual equivalence with the original residue action preserves its sur…

The residue field, its algebra, and the relative separable closure are constructed once in the existing field owner. This layer contains no fraction-field or original decomposition-group data.

The comparison is constructed in both directions by normalizationDesc. Its compatibility with endomorphisms follows from the same universal property. It can therefore transport an actual cover to its affine spectrum with…

A commuting square induces a map on relative normalizations, by applying the universal property to the pullback of the target normalization. The map preserves the base and commutes with compatible source endomorphisms.

The actual map from a localized stalk factors through an affine neighbourhood. Its section map is a localization, using the germ map and the standard localization-at-prime construction. The normalization comparison there…

Constructs the root map induced by an original residue automorphism and identifies it with the action of the corresponding normalization stabilizer image.

Proves that the canonical finite-field tame character intertwines decomposition-group conjugation with the roots action of the original normalization residue morphism.

Identifies the intrinsic canonical character with the normalized finite ideal character and evaluates the original finite-field character on its normalization inertia image.

Constructs the original finite-field canonical tame morphism and an independent principal-unit wild subgroup. Proves surjectivity and identifies that subgroup as the kernel.

The genuine normalization restriction equivalence preserves the cardinality of the already-defined wild comap and its inertia quotient. This yields the literal original-field wild-order and tame-order statements.

The independent original-field wild subgroup has prime-power cardinality for the characteristic of the base DVR residue field. The same subgroup is a p-group in positive residue characteristic and is trivial when that ba…

Proves the coefficient difference condition for restriction of original inertia to the contracted finite normalization prime.

Constructs the morphism from the original decomposition group to the intrinsic normalization stabilizer and records its automorphism and coefficient ring maps.

Constructs the normalization restriction on original finite-field inertia. Proves injectivity and surjectivity and packages the resulting equivalence with intrinsic normalization inertia.

Defines the original finite-field inertia conjugate and identifies its underlying element with the original field-automorphism expression.

Proves that normalization restriction intertwines original finite-field inertia conjugation with intrinsic normalization inertia conjugation.

Factors the original normalization residue morphism through decomposition restriction and the intrinsic native residue morphism.

Constructs the intrinsic canonical tame morphism and principal-unit wild subgroup from a finite Galois extension. Proves surjectivity onto the full roots group and identifies the wild subgroup as its kernel.

The tame and wild orders of a finite Galois normalization satisfy the ramification identity with its literal inseparable residue degree. The original DVR and field extension supply all normalization arithmetic before the…

The finite Galois field tower supplies the actual wild prime-power order. Its independent principal-unit subgroup realizes that cardinality, and the same tame degree is the literal normalization-inertia quotient cardinal…

Identifies the native normalization ring map with the original Galois action. Defines the original inertia group and derives its coefficient difference condition.

The localization model is arbitrary, so the theorem applies directly to the local ring of a scheme with its actual germ map. The normalization inclusion is the literal inclusion of integral elements in the same field, an…

A maximal prime of the actual localized normalization lies over the local base's maximal ideal. Its literal contraction therefore lies over the original base prime. Localization returns the same prime, and the original G…

Identifies the original normalization residue morphism with the quotient map induced by its prescribed normalization coefficient action.

The finite monodromy obtained from a scheme morphism is natural when the composite geometric fiber is transported to another chosen base point.

The supplied map is a field-coefficient map. Bijectivity at finite roots stages is used once to construct the stage equivalences. Their transition square is proved from the actual power-map naturality theorem. No inverse…

The index is the actual set of natural numbers invertible in the base field, ordered by divisibility. Every index is positive. The transition from degree n to a divisor m is the actual power map with exponent n / m. This…

Every coordinate is sent through the specified ring map. Compatibility is the proved coefficient/power transition square, and continuity follows from the existing inverse-limit topology and discrete root stages.

The stage maps are the canonical field inclusions on roots of unity. Their bijectivity was proved from polynomial separability, and the actual power transition theorem proves the required compatibility. The native stagew…

The inverse-system isomorphism uses the literal inclusion at every stage. Taking its proved projection equation and the underlying scalar gives the coefficient law without reopening a residue-field construction.

Canonical aggregate for EtaleFundamentalGroups.Inertia.Residue.

The one-point inertia argument ends by mapping a ramification index to a residue ring of characteristic p. If that image is a unit, the index is prime to p. This file records that arithmetic endpoint without mentioning r…

For a finite local extension of discrete valuation rings, a bijection on residue fields forces the inertia degree to be one. The local Dedekind identity e f = [L : K] then identifies the ramification index with the degre…

This ring-only lemma uses coefficient surjectivity at a maximal ideal. Its applications supply the two coefficient formulas and square from actual maps.

The full exponent group family is closed here, with only the two coefficient fields present. The result retains exactly the restricted prime-to-roots group family, so original DVR consumers need not reopen the full index…

The original power transitions commute with coefficient maps. Therefore every coefficient automorphism acts coordinatewise on this SAME limit.

The transport keeps the actual unit. Its scalar computation, inverse, and homomorphism structure are built together, before any field tower appears.

The source's global sections are a normal domain. Normalizing in those sections or in their function field therefore gives the same scheme. The algebra on the function field is constructed from the actual structure morph…

Restriction is surjective by normality. It is injective because a purely inseparable extension admits at most one extension of a field embedding. For an algebraic closure this is the residue-automorphism identification i…

The canonical inclusion from the relative separable closure induces an isomorphism on roots of unity of order invertible in the base field. This is the change of residue field needed in Stacks Project, Tag 0BUB. Referenc…

At every point the base is the actual scheme stalk. A maximal prime in its normalization specifies the geometric residue point used to construct the geometric stalk and its literal fraction-field embedding. The union of…

The actual function field of a connected finite etale cover is finite separable over the fraction field. Its integral closure is therefore a finite domain over the strict-Henselian DVR. A point over the prescribed closed…

The actual local generic morphism factors through the spectrum of its geometric etale stalk after composition with the open inclusion. The latter spectrum has trivial fundamental group. Comparing the two factorizations t…

Select the pointed Galois component of the actual generic pullback. Its normalization over the strict-Henselian DVR has a point fixed by every deck transformation over the prescribed residue-field embedding. The actual c…

The map is the literal ambient homomorphism on subgroup elements. A proved image equality supplies membership and every target element's actual lift.

The order of a finite p-group divides a power of p. Thus every divisor of the inertia order coprime to p divides the index of wild inertia. This converts the actual radical ramification divisibility into finite tame-orde…

The fundamental degree identity and orbit-stabilizer count show that trivial inertia forces both ramification index one and separability of the residue extension. No perfectness hypothesis on the residue field is needed.

The integral closure in a finite Galois extension is finite and torsion-free. Trivial inertia supplies unramifiedness even for imperfect residue fields, and flatness over the DVR supplies étaleness.

The length definition of the ramification index and additivity of order of vanishing give the divisibility used in Stacks Project, Tag 0BUB. The root need not be a uniformizer, and no residue separability or characterist…

The literal coefficient automorphisms in ideal inertia agree modulo the prime. Prime rigidity proves equality on the original domain itself, so the intrinsic inertia group has at most one element.

Canonical aggregate for EtaleFundamentalGroups.Kummer.AdjoinRoot.

A monic equation whose derivative is a unit at its adjoined root is formally etale. Choosing the derivative itself as the denominator in a standard etale presentation makes the Bezout condition tautological; localization…

Canonical aggregate for EtaleFundamentalGroups.Kummer.AdjoinRoot.Global.

A finite algebra over the local exact-root cover has a maximal ideal over the closed point by lying over. This file chooses that ideal internally and feeds the resulting literal prime to the global-Away same-prime comple…

For a prime radicand p, localizing R[X]/(X^N-p) at the prime generated by the root is the same as first localizing R at (p) and then adjoining the root. The latter root ring is already local, so no further localization i…

The positive root cover over AP is an actual localization of the original root algebra A[X] / (X ^ n - f). Its closed prime is constructed by pulling back the maximal ideal; no prime or local-ring comparison is assumed.…

For a positive exponent, the root of X ^ n - f is a nonzerodivisor if f is. If A / (f) is reduced, the ideal of that root is radical. Thus the root defines a reduced Cartier divisor on the Kummer cover, even when the amb…

Two nonzero roots of the same invertible power over an extension field differ by exactly one root of unity in the separably closed base field.

Multiplication of the adjoined root by a root of unity gives an actual algebra automorphism. No irreducibility or domain hypothesis on the Kummer algebra is needed, so the construction includes disconnected Kummer covers…

For a positive exponent n invertible in A, the actual map Spec (A[X] / (X ^ n - f)) → Spec A is finite, flat, and locally of finite presentation, with rank n at every point. Its coordinate algebra is free. The actual loc…

For a DVR R and a prime element π, the actual integral root algebra B = R[X] / (X ^ n - π) is a domain. Its fraction field is identified, as an algebra over Frac(R), with the root algebra of the same equation over Frac(R…

For a DVR R, a uniformizer π, and a positive integer n, the actual root algebra R[X] / (X ^ n - π) is a DVR whose ramification index over R is exactly n. The proof identifies the extended maximal ideal with the n-th powe…

Radical covers, selected components, completion arguments, and strict-normal-crossings terminals. Canonical aggregate for EtaleFundamentalGroups.Kummer.

Canonical aggregate for EtaleFundamentalGroups.Kummer.Boundary.

A formally unramified finite iterated radical on the full boundary complement makes every cyclic exponent a unit in the original ring. Hence the order of every concrete character subgroup of the corresponding product of…

Formal unramifiedness of an iterated Kummer radical on the complement of a finite boundary makes every exponent a unit on that complement. Prime multi-boundary unit descent then reflects all of those units to the origina…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Boundary.Lattice.

For a finite lattice cover over the complement of a prime normal-crossings boundary, formal unramifiedness makes every quotient subgroup order a unit on the complement. Componentwise characteristic zero then reflects tha…

The fraction-field Galois group of a finite lattice cover is its quotient character group. This file sends localized normalization inertia through that Galois equivalence and finite-character duality to an actual subgrou…

The explicit lattice-cover action supplies a finite Galois extension of fraction fields. At a height-one prime of a regular model, production inertia cardinality then identifies the already-produced unit inertia order wi…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.ChosenFactor.

Let A be a complete DVR, let B = A[X] / (X ^ N - varpi), and let D / B be the uniquely chosen local factor of a finite etale algebra. Complete finite-etale residue classification writes D as the base change of B to the e…

A local factor over a complete one-root cover need not be the root cover itself: its residue field can be a nontrivial finite separable extension. The finite-etale residue lift is therefore the correct base for an exact…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.ChosenFactor.ExponentUnit.

The complete-local construction used by the absolute Abhyankar argument eventually produces a finite etale factor with a unique prime over the closed point. Uniqueness makes that factor faithfully flat. The terminal obst…

This file combines the complete-local chosen-factor coordinates with formal unramifiedness on the boundary complement. It is the algebraic consumer needed after the absolute Abhyankar construction has made the chosen fac…

After localizing a normal-crossings chart at a height-two point, boundary parameters outside that point are units. This leaf combines the chosen finite-etale factor construction with the prime-or-unit terminal, so those…

The maximal-adic completion used in the one-root construction does not have a global Noetherian instance in the current library. Normality can instead be descended from the concrete normal chosen factor. If B / A is fait…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.ChosenFactor.PrefixEmbedding.

A concrete prefix embedding into a common target field determines a literal Frac(C) ⊗[Frac(A)] M component. The boundary-Away comparison for that component and finite-etale base change of the original normalization prime…

Let C be the finite etale residue lift of a complete regular pair and let P be the fraction field of its completed one-root chosen factor. A concrete embedding of a finite prefix field M into P selects an actual composit…

A chosen-factor equivalence B tensor[A] C = D embeds its right coordinate C into D whenever C/A is flat and B/A is faithful. Consequently a domain structure on the actual chosen factor pulls back to C. This avoids using…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.ChosenRoot.

A prime Q above the closed point of a DVR canonically selects a component of the completed generic fibre. We choose a post-root component above it, equip the intermediate component with its canonical complete valuation,…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.Conditional.

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.Conditional.ChosenFactor.

The completed conditional root cover has a chosen local normalization factor inside an already selected finite generic component M. Completeness and finite etaleness make that localization a genuine finite chosen factor,…

A uniquely selected finite-etale local factor over the completed conditional root cover already carries every radical coordinate through its structure map. If that factor is a domain, composing with its fraction field pu…

An inactive stage in the height-two root cover has exponent one. Its radicand need not belong to the closed point, but the stage is canonically the base ring. This file extends the completion and chosen-factor producers…

This leaf installs all completion plumbing around the literal same-prime terminal. A finite-etale algebra and one closed prime are chosen before completion. The exact mapped prime after completion then detects the expone…

The earlier same-prime completion bridge starts with a primitive Away map to the localization Ep of a finite-etale algebra. Such a localization need not be finite before completion when the source local ring is not Hense…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.GenericTensorTower.

Fix a literal component m of a two-step generic tensor tower and a prime p of the normalization of its final component. The contraction of p selects the canonical intermediate component, while localization at p has fract…

These two source theorems establish the domain inputs used by literal one-root comparisons: first for the one-stage iterated radical itself, then after passing to the explicit finite-etale residue lift. Chosen-factor and…

For a finite separable extension of a complete discrete valuation field, the actual integral closure supplies the target complete valuation and the finite extension of valuation rings. Consequently the higher-radical act…

For a family of completed field factors, their local ramification indices need not be equal. A single radical cover can nevertheless be used once a common upper bound for the local field degrees is known: every ramificat…

The factorial exponent is only one way to obtain a common multiple of local ramification indices. For the absolute Abhyankar argument the useful common multiple is instead built from the actual ramification indices above…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.HigherRadical.ActualTensor.

The degree factorial used by the original complete-DVF wrapper is only one possible common exponent. Here the exponent is an arbitrary positive natural number, and the only arithmetic input is that the actual ramificatio…

This is the arbitrary-exponent form of the complete higher-radical tensor tower. A fixed component after the root extension canonically determines its pre-root component and the second-stage component. Supplying the actu…

For a complete discrete valuation field K, this file equips the fraction field of the factorial uniformizer-root ring with its canonical K-algebra structure. The construction is the localization lift of the inclusion of…

The actual-factor theorem applies to each literal maximal component of the generic tensor product. Finite separability decomposes that tensor product into exactly those components, so their integral closures assemble int…

An arbitrary component of F' ⊗[K₀] L first selects a component of K ⊗[K₀] L, where K is the complete base field, and then a component after adjoining the factorial root. The two-stage quotient is canonically the original…

The completed normalization machinery first fixes an intermediate tensor component. The post-root tensor tower instead starts from a final component and contracts it. This file accepts the equality between those two idea…

Let K₀ → K be a complete-field base change and let F be the fraction field of the factorial uniformizer-root ring over the valuation ring of K. Every component of F ⊗[K₀] L has finite-etale normalization by the fixed-com…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.HigherRadical.

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.LocalDomain.

The maximal-adic completion used in the selected-branch construction does not currently carry a global IsNoetherianRing instance. The exact-degree sandwich only needs substantially less: the completed base is a complete…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.MaximalAdic.

If a finite family generates the maximal ideal of a Noetherian local ring, evaluation of multivariate formal power series at the images of that family surjects onto the maximal-adic completion. This works for an arbitrar…

Splitting a finite set of variables into one variable and the remaining variables identifies the corresponding multivariate power-series ring with an iterated univariate power-series ring. This gives the finite-variable…

Let B₀ be the one-root radical of a regular parameter y over a Noetherian local ring R, and let E / B₀ be finite etale with a chosen closed prime p. Put A = R̂, form the corresponding one-root radical B̂ / A, and retain…

Mathlib constructs the maximal-adic completion of a Noetherian local ring as a complete local ring, but does not currently provide its Noetherian-ring instance. For the two-parameter situation used by one-point inertia,…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.NormalizationPrime.

A prime Q in a finite DVR normalization selects one literal factor of the completed tensor product. The same Q also selects the generic tensor component and, inside its normalization, the prime used by the exact ramifica…

A normalization prime Q over the closed point of a DVR determines all of the completed data used by the selected-branch argument. This file keeps those choices synchronized: m is the literal maximal ideal of Khat ⊗[K] L…

The completed tensor product may have several factors, so it must not be identified with one localization. Once a factor Q and the corresponding generic component have been fixed, however, the normalization of that compo…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.RegularLocal.

Work over a complete two-dimensional regular local prefix A, with selected parameter y. The actual finite-etale local factor D of the one-root cover becomes the literal root cover after the explicit finite residue lift C…

The complete chosen-factor classification is not one-dimensional. Over a complete regular local ring A, a chosen finite-etale local factor of the one-root cover is the base change of that cover to the explicit finite-eta…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.RegularPair.

For a regular parameter pair generating the closed point, the quotient of the maximal-adic completion by either completed parameter is a DVR. This file records the second-parameter form needed by the iterated power-serie…

Mathlib does not currently provide a global IsNoetherianRing instance for the maximal-adic completion used here. The root-divisor argument only needs the corresponding height-one localization to be a DVR. For the first p…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.RootTensor.

Every component of the completed generic tensor product comes from a prime of the original finite DVR extension. If all of their ramification indices divide one positive exponent, the prescribed-root actual-factor theore…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Completions.SamePrime.

Suppose that a finite etale algebra over a finite radical cover has been localized at a chosen closed prime, and that its boundary Away map is etale. After a Henselian faithfully-flat pushout, the exact mapped prime in t…

This is the application-shaped one-variable specialization of the literal same-prime completion theorem. A prime parameter with regular quotient in a two-dimensional regular local ring is completed at the closed point. T…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Descent.

Formal unramifiedness of a composite descends across a formally etale, faithfully flat final map. The proof identifies the base change of the Kaehler differentials with the differentials of the composite and then uses fa…

After localizing a strict-normal-crossings chart at a prime, every boundary parameter is either still prime or has become a unit. This file extends the multi-away unit descent theorem to precisely that situation, without…

This file extends unit descent from one prime boundary parameter to a finite product of prime parameters. A divisor of a power of the boundary product which is divisible by none of its prime factors must be a unit.

For the final stage of a relative Kummer construction, formal unramifiedness over the prefix makes the derivative a unit. Monicity then makes the final stage formally etale. Its positive-degree monic presentation is fait…

The explicit Kummer calculation takes place after inverting a boundary parameter t. This file proves the descent step needed afterwards: an element not divisible by the prime element t was already a unit before the local…

Canonical aggregate for EtaleFundamentalGroups.Kummer.FieldTowers.

An injective map from a domain D into a field L extends canonically to a chosen fraction field K' of D. If D lies over another domain R, this file records that the resulting K'-action is compatible with the already chose…

An embedding of a finite Galois prefix field M/K into a field P which also contains a field extension F/K determines one literal component of F tensor[K] M. This file exposes that component and its embedding back into P,…

Canonical aggregate for EtaleFundamentalGroups.Kummer.FieldTowers.PrefixEmbedding.

The separable field Kummer equivalence supplies a function and a root for each finite Kummer character of the scheme fundamental group. Its generic kernel fixes the actual field generated by that root, so that field is t…

A root in the field forming the generic fiber of a finite étale cover has integral order at every point of the covering curve. The actual ramification index is one, so the original orders are divisible by the root expone…

Canonical aggregate for EtaleFundamentalGroups.Kummer.GenericTensor.

Canonical aggregate for EtaleFundamentalGroups.Kummer.GenericTensor.FieldComponent.

If the field map on the left tensor factor is bijective, the tensor product collapses to its right factor. Every maximal quotient component is therefore the literal collapse component, and its canonical right algebra map…

Canonical aggregate for EtaleFundamentalGroups.Kummer.GenericTensor.IntegralClosure.

If L / K is finite separable, then F ⊗[K] L is a reduced Artinian ring and hence is canonically the finite product of its residue fields at all maximal ideals. This file keeps those literal quotient fields as the compone…

Canonical aggregate for EtaleFundamentalGroups.Kummer.GenericTensor.Refinement.

The component-refinement map keeps a previously chosen intermediate tensor component while extending the left field. Its kernel produces an actual component of the original tensor product, and the resulting quotient-fiel…

The component-refinement equivalence preserves the literal right tensor coordinate. Consequently bijectivity of the right coordinate can be composed through an intermediate selected component without assuming a separate…

Canonical aggregate for EtaleFundamentalGroups.Kummer.GenericTensor.Tower.

Factoring a selected component of F' ⊗[K] L through an intermediate field produces a contracted component and then a second-stage component. The refinement of those two selected components is literally the original final…

Canonical aggregate for EtaleFundamentalGroups.Kummer.GenericTensor.Tower.Intermediate.

A maximal prime on the final normalization contracts to the closed point of the canonical intermediate normalization. The same literal final component, normalization map, and prime are retained throughout.

A selected component of F' \otimes[K] L canonically contracts to a component of F \otimes[K] L. This file constructs the induced field map over the smaller integral base and the resulting map between normalizations.

The normalization map selected by a literal final tensor component contracts a specified final normalization prime. Primality, maximality, and the exact lies-over relation are derived from that same map.

Canonical aggregate for EtaleFundamentalGroups.Kummer.Henselian.

Suppose that the base residue field is separably closed of characteristic zero and that the target valuation ring is finite over the base valuation ring. The residue extension is then finite and separable, hence trivial.…

The usual complete-DVF uniformizer decomposition is ideal-theoretic: it uses only the DVR structure of the two valuation rings and compatibility of their valuations. This file records the resulting stronger DVF statement…

If the residue field is separably closed and the exponent is a unit in that field, every unit of a Henselian local ring has a root of that exponent. This is the characteristic-zero-compatible unit-absorption step for tam…

Canonical aggregate for EtaleFundamentalGroups.Kummer.HigherRadical.ActualCompositum.

A maximal component of the tensor product of a pure-radical fraction field with a finite target is generated over the target by the image of the radical root. Embedding that finite component in the target's algebraic clo…

The canonical higher radical field is a subfield of the actual compositum. For an arbitrary HigherRadicalActualFactorData, its root-ring action agrees with the composite through that subfield. This supplies the scalar to…

Canonical aggregate for EtaleFundamentalGroups.Kummer.HigherRadical.

Canonical aggregate for EtaleFundamentalGroups.Kummer.HigherRadical.ExactRoot.

Fix an exact root field for the final right-hand valued field. A retained higher-radical factor for another fixed component identifies that component with the root field on its canonical left coordinate. Consequently the…

The field generated by a prescribed higher root is already represented as higherRadicalFieldOverLower inside the chosen algebraic closure. This file identifies it with the fraction field of the literal higher root ring a…

Canonical aggregate for EtaleFundamentalGroups.Kummer.HigherRadical.FixedComponent.

Strict-Henselian retained-factor data identifies every fixed higher-radical component with its canonical left root field. Tensoring that literal fixed component once more over the same root field therefore has no effect…

Canonical aggregate for EtaleFundamentalGroups.Kummer.HigherRadical.FixedTensor.

The lower-factor comparison needs positivity of the valuation ramification index, primality of a chosen uniformizer, and the lower-power coordinate of the fixed higher root. All three are intrinsic consequences of the va…

Canonical aggregate for EtaleFundamentalGroups.Kummer.HigherRadical.LowerFactor.

Canonical aggregate for EtaleFundamentalGroups.Kummer.HigherRadical.LowerFactor.FixedIntegral.

The same Cq selected by unit absorption is finite etale over the actual root ring and remains so after the auxiliary higher root base change. Here we identify the generic fibre of that literal base change with the lower…

The linear generic-fibre comparison and its underlying ring equivalence share one construction in FixedIntegral.Basic. This module retains the established import path for the higher-root-linear comparison.

The generic fibre of the literal higher base change of the retained lower unit factor is identified with the lower tensor product used to choose the fixed higher component. Pulling the already chosen maximal ideal back a…

The fixed quotient comparison is assembled from the higher-root-linear generic-fibre comparison, the canonical lower-factor quotient comparison, and the actual-compositum comparison. The scalar tower through the embedded…

The unit-absorption factor Cq first selects its actual component after the higher radical base change. A fixed generic tensor component supplies the higher root in the same algebraic closure. This file composes those two…

Strict-Henselian triviality makes the canonical left map into the retained unit-factor generic fibre bijective. Passing to its selected quotient and then through the higher-root-linear fixed-component comparison remains…

DVR unit absorption selects a literal integral factor Cq over the ramification-index root ring Rₑ. A prescribed larger root determines a specific extension K' of the lower radical field. This file records the maximal gen…

Canonical aggregate for EtaleFundamentalGroups.Kummer.HigherRadical.StrictHenselian.

The prime produced by strict-Henselian splitting is a closed prime of the retained lower factor. After base change to a higher root and passage to the fraction field of that higher root ring, its extension is the unit id…

Canonical aggregate for EtaleFundamentalGroups.Kummer.HigherRadical.UnitFactor.

A finite etale algebra over a strictly Henselian local ring need not be the base ring before a connected factor is selected. Nevertheless, every chosen closed localization has separable residue field over the separably c…

The retained lower unit factor is a domain. A chosen closed localization is the strict-Henselian base, and the localization map is injective; consequently the unit factor itself is already the base. Tensoring this biject…

The literal factor retained by HigherRadicalUnitFactorData is finite etale over the actual ramification-index radical. If it has a unique closed prime after passage to a strictly Henselian filtered colimit, finite presen…

HigherRadicalUnitFactorData retains the exact integral unit factor Cq selected at the actual ramification index. This file supplies its module finiteness over that lower radical and then base-changes the same factor to a…

Canonical aggregate for EtaleFundamentalGroups.Kummer.IteratedRadical.

The diagonal iterated radical construction commutes with arbitrary base change. The proof follows the recursive presentation and uses mathlib's canonical base-change equivalence for AdjoinRoot at each step.

This file adjoins finitely many roots of equations X ^ n i - a i, in the order indexed by Fin r. Every radicand comes from the original base ring; this is the diagonal presentation used after decomposing a finite abelian…

The iterated radical formed after completing the base is canonically the base change of the original iterated radical. This file fixes the induced algebra structure in the right-factor direction and records the local, re…

A uniquely chosen closed prime in a finite algebra remains unique after base change to the maximal-adic completion. The completed chosen prime is the exact extension of the original one. Its maximality is supplied by the…

Let B / A be the full positive diagonal iterated radical along prime boundary parameters. If D / B is formally etale and faithfully flat, and the underlying map A -> D is etale after removing the whole boundary, then eve…

The roots already adjoined in an iterated-radical prefix have canonical images in every algebra over that prefix. Thus the only new coordinate needed for one further stage is its final root. At the exact ramification ind…

Canonical aggregate for EtaleFundamentalGroups.Kummer.IteratedRadical.ExponentUnit.

This file connects the height-two purity output to the terminal radical exponent obstruction. An integral closure inside a field is a domain and is integral over the root cover. Once purity makes it étale, those facts ma…

The radical presentation may contain auxiliary exponent-one stages whose radicands are units or are unrelated to the boundary. This file separates the radical family from the prime boundary family used for the away local…

After localizing a normal-crossings chart, boundary parameters outside the chosen point become units. The terminal iterated-radical obstruction only uses residue characteristic along the factors that remain prime, so it…

This is the universe-polymorphic form of the terminal integral-closure obstruction: the field containing the generic component need not live in the same universe as the original base ring.

The full root cover used by the height-two strict-normal-crossings argument is presented as an iterated radical followed by one final AdjoinRoot. This file exposes the last-coordinate consequence of the prime-or-unit bou…

Compatible roots in a target field construct the iterated-radical action and its chosen fraction-field tower. Componentwise normalization etaleness then produces global normalization etaleness, which combines with primit…

A positive iterated radical cover of a two-dimensional regular parameter pair again has an explicit regular parameter pair generating its maximal ideal. The dimension-two conductor criterion therefore shows directly that…

An action of an iterated diagonal radical on a target algebra is determined by a compatible target root for every stage. This file packages the successive applications of AdjoinRoot.liftAlgHom and records all root coordi…

A compatible family of target roots constructs the full iterated-radical action on the target field. When the root ring is a domain and the base acts faithfully, that action is injective and hence extends to its chosen f…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Lattices.

Characters of the finite quotient lattice act diagonally on the ambient lattice algebra. When the coefficient domain has enough roots of unity, these characters separate the quotient degrees. Consequently their common fi…

An injective character-lattice map into a finite product of cyclic groups makes the lattice order divide the product of the Kummer exponents. Thus, if every exponent is a unit in the coefficient ring, the lattice order i…

For an additive subgroup H of a lattice L, the induced map of additive monoid algebras identifies R[H] with the degree-zero subalgebra of R[L] for the quotient grading by L ⧸ H.

A finite quotient lattice admits cyclic coordinates. Composing those coordinates with the quotient map gives a grading of the ambient lattice algebra whose degree-zero subalgebra is the original lattice algebra.

The Smith presentation of a finite-index lattice inclusion is an iterated monic radical extension. This file uses that presentation to prove that the induced monoid-algebra map is finite. Coefficient extension for monoid…

The quotient-character action on a lattice algebra extends canonically to its fraction field. The ring-level IsGaloisGroup producer and mathlib's fraction-ring transport then identify the same finite character group as a…

The character group of the finite quotient lattice acts diagonally on the ambient lattice algebra. This file packages that already constructed action as a local MulSemiringAction, equips the lattice cover with its canoni…

The Smith presentation of a finite-index lattice inclusion is an iterated monic radical extension. This file uses that presentation to prove that the original monoid-algebra map is integral. It is the first ring-theoreti…

The quotient-character action identifies the Galois group of a finite lattice cover with the character group of its quotient lattice. At a height-one prime of any regular model of the base fraction field, localized norma…

For a finite-index inclusion of finite free integer lattices, the target monoid algebra is integral over the source and is an integrally closed domain. Consequently it is the integral closure of the source in its own fra…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Lattices.Smith.

Smith normal form gives coordinates in which a finite-index inclusion of free integer lattices is diagonal. The same Smith choice identifies the quotient with a product of cyclic groups, while functoriality of additive m…

The Smith coefficients produced for an integer lattice are nonzero integers. Changing the sign of each negative target coordinate replaces them by their positive natural absolute values. Functoriality of additive monoid…

A formally unramified finite-index lattice cover produces synchronized Smith coordinates with unit exponents. Every subgroup of the lattice quotient therefore embeds in a product of cyclic groups of unit orders, so its o…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Laurent.

The endomorphism of the Laurent monomial algebra induced by multiplication by n on ℤ becomes, after adjoining an n-th root of the degree-one monomial, the original Laurent monomial algebra. The equivalence below keeps tr…

This file builds a finite diagonal Laurent cover one coordinate at a time. At each successor step, the preceding radical is extended by one Laurent coordinate and the one-variable cyclic Laurent equivalence removes the n…

A one-variable Laurent algebra is the localization of a polynomial ring away from X. Polynomial rings over integrally closed domains are integrally closed, and integral closedness survives this localization. Iterating th…

The radical presentation of a finite lattice cover is dependent: at each stage the new radicand is the new Laurent monomial over the preceding radical, rather than an element of the original coefficient ring. This file p…

Canonical aggregate for EtaleFundamentalGroups.Kummer.LocalGeometry.

Canonical aggregate for EtaleFundamentalGroups.Kummer.LocalGeometry.HeightOne.

For D = B[X] / (X^N - p), the root equation sharpens contraction data in two useful ways. A height-one prime of the domain D whose contraction is the principal radicand prime is exactly the principal root prime. Converse…

For a DVR V with fraction field K, its standard valued-field completion has valuation ring Vhat. A generator pi of the maximal ideal remains a uniformizer in Vhat, and adjoining an N-th root of pi commutes canonically wi…

Canonical aggregate for EtaleFundamentalGroups.Kummer.LocalGeometry.HeightTwo.

Mathlib does not currently expose a general theorem saying that the maximal-adic completion of a regular local ring is again a regular local ring. The height-two argument needs less. For a regular pair, quotienting by ei…

Let p be a prime element in a two-dimensional regular local domain. If the quotient by p is regular local, then the class of p in the cotangent space is nonzero. Thus p extends to a regular parameter pair, and every posi…

Canonical aggregate for EtaleFundamentalGroups.Kummer.LocalGeometry.Regular.

In a two-dimensional regular local ring presented by a regular parameter pair, every prime containing the first parameter is either its principal height-one prime or the closed point. This elementary dichotomy is useful…

This leaf records the final source-facing composition. The strict-normal- crossings chart, boundary characteristic-zero hypotheses, and primitive Away etaleness feed the produced local selected-exponent theorem. Height-t…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.

This file carries a height-one prime on an affine integral-closure chart of the generic-extension normalization to the corresponding prime over the ambient boundary stalk. The literal local-ring map on the original chart…

A height-one prime of a boundary stalk which contains the boundary ideal is the canonical branch prime of an irreducible component through the chosen point. This identifies the arbitrary prime with the input expected by…

The normal-crossings calculation gives etaleness after first localizing the base stalk and then taking its normalization. The affine normalization criterion instead asks for formal etaleness of the literal local-ring map…

This file records the canonical maps from an ambient stalk through a prime-localized etale chart and its boundary-away function field. In particular, the compatibility needed for finite-etale pullback components is produ…

The branch prime attached to a component at any of its specializations has the component generic stalk as its prime localization. This identifies the ramification index seen in every specialized stalk with one fixed inde…

The original complement only needs to be connected. Integrality and normality are constructed on the two-dimensional split chart and its connected Galois cover; neither is imposed on the ambient scheme or on the original…

The all-characteristic specialization argument makes every normalization inertia group over a fixed boundary component trivial. At the corresponding height-one localization, normality and Noetherianity make the base a DV…

Height-one primes contract to height-one primes along an etale stalk map. Consequently, characteristic zero along every branch of a horizontal boundary passes to the strict chart witnessing normal crossings.

This file transports the local normal-crossings calculation at a selected horizontal component to the inertia image in an explicitly prescribed finite quotient of the global complement's etale fundamental group.

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.Galois.ActiveRoot.

For an active conditional stage, its exponent and radicand are the common Galois branch index and the corresponding localized boundary parameter. This leaf performs those two rewrites before specializing the active-root…

This leaf converts the active-root normalization theorem to the literal localized normalization used by special local purity. Keeping the bridge in its own compiled module avoids re-elaborating the completed chosen-compo…

This file applies the selected-root normalization descent theorem to any active strict-normal-crossings branch through a height-two point. A finite faithful normal extension of the simple root cover and a prime above its…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.Galois.

For an active branch of a split strict-normal-crossings chart, this file supplies the two local inputs used by the selected-root normalization theorem: every normalization ramification index divides the exact Galois root…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.Galois.FullRootCover.ActualRootFirst.

The height-one prime and its contraction are fixed before the generic tensor component is introduced. This is the order used by the active-root source theorem, and keeps the actual-root-first coordinate calculation indep…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.Galois.FullRootCover.

An action of the full radical fraction field on the original target field selects a canonical multiplication component of their tensor product. The right coordinate of that component is automatically an isomorphism: this…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.Galois.FullRootCover.FixedComponent.

If the canonical right map from the original extension field to every fixed full-root tensor component is bijective, the original primitive boundary-away map transports first to that field component and then through the…

The full-root exponent obstruction previously accepted bijectivity of the right coordinate in a fixed generic tensor component. This file constructs that comparison from the actual exact-root field inside the full field.…

At a height-two strict-normal-crossings point, use the exact common Galois ramification index on every active branch. For one fixed generic tensor component, selected and actual-root height-one primes are handled by the…

Purity for every fixed generic tensor component supplies global etaleness of its normalization over the exact height-two full root cover. The localized strict-normal-crossings parameters supply the prime-or-unit boundary…

The exact full root cover is a two-dimensional regular local domain. The height-one analysis for a fixed generic tensor component therefore feeds directly into local purity, giving etaleness of the whole normalization ov…

The actual-root-first construction is compiled in the preceding source leaf. This module only installs the full-cover geometry and dispatches to it.

This module supplies the finite faithful map from the selected simple root cover to the full cover and applies the active-root localized-normalization theorem for one fixed generic tensor component.

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.Galois.Prefix.

Before adjoining the selected radical, the conditional cover contains only the roots of the other boundary branches through the chosen height-two point. This file proves that, in every fixed generic tensor component, the…

The conditional root cover and the final selected-root cover must use the same permutation of the other branches. This file keeps the permutation chosen by the conditional selected-away theorem, retains its regular quoti…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.Galois.SelectedComponent.

The same full generic-tensor component used by the prefix/full-root purity bridge has a normalization prime over the selected root. Contracting that prime along the literal right-coordinate embedding produces a prime of…

The pointed quotient ideal-inertia subgroup of a Galois pullback component maps injectively into the deck group of the original cover. Consequently, the local normal-crossings coprimality statement remains true for its a…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.HeightTwo.

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.HeightTwo.BranchProduct.

For a chosen normalization prime above one boundary branch, localization at that branch produces the canonical finite DVR normalization used by the completed actual-factor theorem. Its ramification index divides the bran…

The exponent on each boundary branch is the product of the actual ramification indices of the normalization primes above that branch. Non-boundary parameters already receive exponent one from the branch-product family. T…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.HeightTwo.ConditionalRootCover.

The completion API for a conditional iterated radical asks that every stage either be supported at the closed point or have exponent one. This is literal for the height-two conditional presentation: an other-branch stage…

Remove a selected branch from a finite regular parameter family and give every remaining branch a prescribed positive exponent only when it passes through the chosen height-two point. Non-boundary parameters and boundary…

At a height-two strict-normal-crossings point, remove a selected branch and adjoin roots only along the possible remaining boundary branch. The chosen permutation puts that branch first. Every height-one prime of the res…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.HeightTwo.FullRootCover.

At a boundary height-one prime of the full height-two root cover, the local ring is a DVR and its closed quotient has characteristic zero. Therefore the standard rank-one discrete valuation on its fraction field has char…

Start with the conditional root cover away from a selected branch at a height-two strict-normal-crossings point, and then adjoin a positive root of the selected branch itself. The resulting full cover is a two-dimensiona…

Characteristic zero along the active branches of the original strict-normal-crossings chart is transported first to the height-two localization and then through the conditional radical cover. For an actual radical branch…

For a finite Galois normalization, every prime above one boundary branch has the same ramification index. Using that exact common index on each active branch cancels the actual local factor without leaving the residual r…

At a height-two crossing, the selected parameter and the unique possible other active parameter form a regular pair. After adjoining the selected root, the other parameter therefore remains prime. Reordering the full cov…

The height-two exact-root calculation and the global normalization theorem meet here. Once the selected Galois root exponent is known to be a unit at every height-two localization above the chosen branch, the ramificatio…

This file specializes the explicit boundary lattice-cover inertia theorem to the boundary components of a split strict-normal-crossings chart. Association of the chart equation with the product of its labelled parameters…

This file specializes the boundary lattice-cover ramification theorem to a split strict-normal-crossings chart. The chart supplies the prime boundary parameters, while association with their product transports the given…

Only the boundary components through the chosen point need to dominate the base in order to obtain characteristic zero along all branches at that point. The canonical height-one prime of any specified incident component…

The selected exponent in the exact Galois full-root cover is the common ramification index along that boundary divisor. Localizing a chosen global normalization branch at a larger height-two prime preserves the same inde…

This file compares the scheme-theoretic strict-normal-crossings predicate with the explicit local-algebra data used by the Kummer inertia results. The scheme predicate itself produces the regular system, so domain, prima…

For an arithmetic boundary component specialized to residue characteristic two, the local Abhyankar coprimality theorem and cyclotomic inversion apply to the same height-one prime and the same normalization prime. Hence…

A horizontal normal-crossings branch in positive residue characteristic produces a height-two local chart. Every finite-etale Galois cover of the local complement then supplies, through the usual fundamental-group map of…

Characteristic zero along every height-one boundary branch and one positive residue-characteristic specialization produce the complete height-two split chart used by the finite-quotient Abhyankar argument. In particular…

A finite-etale cover of the complement of a divisor support restricts to the principal local chart supplied by a normal-crossings boundary equation. The resulting object has exactly the base scheme used by the local fini…

An abelian connected Galois cover of a global divisor complement remains an abelian connected Galois cover on the principal local chart supplied by a split normal-crossings equation.

A characteristic-zero boundary branch specialized to positive residue characteristic produces its height-two local chart together with the actual finite-quotient inertia coprimality statement. The height-two prime, the l…

A height-one divisor branch below a height-two point is selected by the scheme-theoretic strict-normal-crossings data. Every categorical Galois finite-etale cover of the resulting boundary complement then has tame normal…

The strict-normal-crossings chart at a height-two point selects a height-one branch. The normalization-prime inertia over that branch maps to a subgroup of every pointed finite Galois quotient whose order is prime to the…

At a strict-normal-crossings point, a height-one boundary prime is one of the active parameter ideals. A positive integer which is noninvertible on that branch then produces a height-two prime containing the branch. This…

A horizontal boundary branch has characteristic zero at its generic point. When it specializes to positive residue characteristic, the branch admits a height-two split chart. Every connected finite-etale Galois cover of…

A horizontal normal-crossings boundary admits an etale strict chart on which every height-one branch has characteristic zero. At a positive-characteristic specialization, the arithmetic height-two chart and a pointed Gal…

A height-two point in a local scheme carries a split strict-normal-crossings chart after prime localization. This file retains the equality between the localized boundary ideal and the product of the active parameters; l…

An etale strict chart can disconnect a connected Galois cover. The pointed connected component supplied by the pullback theorem is nevertheless Galois, and the split strict-normal-crossings inertia theorem applies direct…

The strict-normal-crossings chart at a height-two point of a local scheme is compatible with height-one divisor primes in the original stalk. After the canonical stalk/localization identification, such a prime is exactly…

Canonical aggregate for EtaleFundamentalGroups.Kummer.NormalCrossings.SelectedBranch.

The selected full-root component supplies a height-one/closed prime chain in its finite normalization. Maximal-adic completion retains that literal chain. Contracting it through the canonical intermediate normalization s…

The residue-lift description of a complete chosen finite-etale factor has two independent pieces of structure. a chosen-factor equivalence B ⊗[A] C ≃ D; the canonical separability idempotent in C ⊗[A] C. The second piece…

After passing to the DVR of the selected branch, all other regular parameters are units. Characteristic zero of the selected branch residue field makes every positive Galois root exponent a unit as well. Consequently the…

The other-root prefix is etale over the selected branch DVR. After tensoring it with a normalization factor, a prime chosen over the right tensor factor has two useful contractions. Its contraction to the etale prefix li…

The selected other-root prefix supplies a prime Q in the tensor product, its contraction P to the prefix, and DVR structures on the two local rings EP and TQ. This file fixes the literal fraction fields of those DVRs and…

This leaf retains the equality which lies behind the divisibility interface used by the selected-root theorem. It also records the formal passage of an exact ideal-theoretic ramification index to the complete valued targ…

If every irreducible component of a normal-crossings divisor is surjective over the integer base, a prescribed component contains a normal-crossings point in every rational-prime residue characteristic. Applying the loca…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Normalization.

Canonical aggregate for EtaleFundamentalGroups.Kummer.Normalization.ChosenPrime.

Canonical aggregate for EtaleFundamentalGroups.Kummer.Normalization.ChosenPrime.Arbitrary.

An arbitrary closed normalization prime is supplied directly to Tag 00UJ. The Henselian pointed comparison recovers that same input prime from the chosen idempotent factor, so the primitive boundary Away theorem transpor…

The older chosen-factor comparison starts with the Tag 00UJ data and then extracts a generic-fibre component. Here the direction is reversed: an arbitrary prime of the normalization is first supplied to 00UJ itself. The…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Normalization.ChosenPrime.Final.

The non-Henselian Tag construction produces the primitive boundary Away map on its chosen prime-local factor. If the already selected normalization chain identifies that local factor with the transported second-stage pri…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Normalization.ChosenPrime.FullField.

The Tag prime first selects an actual generic component over its pointed local base. The pointed fraction-field comparison turns that component into a literal component of K ⊗[K] L; its right coordinate is therefore an i…

This file extends the normalization-prime comparison from etale base change to the essentially etale maps which occur after localizing an etale stalk at a prime.

This file treats an etale map which need not be finite. A surjective product map selects an actual compositum field. Smooth base change for integral closure makes the selected normalization etale over the original normal…

This file combines the selected-component normalization theorem with the ramification-index square and the normal-Noetherian inertia-cardinality formula.

An etale base change supplies a canonical map between the two normalizations. Thus a prime in the selected base-changed normalization has a canonical contraction in the original normalization. This file packages the corr…

A selected generic tensor component is already generated by the two function fields. For an etale map of domains, its image is also generated by the smaller etale algebra and the old function field: that image is a finit…

For an abelian finite-etale Galois cover, geometric integrality of a rational height-one residue field and odd inertia force the image of the corrected canonical fundamental-group quotient to vanish.

The finite quotient cut out by the inertia fixed field is formed from the usual fundamental-group morphism of spectra. For a split normal-crossings boundary its image is the normalization-prime inertia group, and that im…

The automorphism group of a scheme acts contravariantly on rational functions, so the comparison with the function-field Galois group uses its opposite group. This file combines that comparison with cyclotomic conjugatio…

The normalization-prime inertia subgroup of a connected finite-etale Galois cover is transported from the function-field Galois group to the actual deck group of the cover. Cyclotomic inversion therefore holds in that de…

The local Abhyankar theorem gives coprimality for the normalization-prime ideal inertia in the function-field Galois group. This file transfers that result to the actual finite quotient represented by a pointed finite-et…

Decomposition and ideal inertia groups for a normalization prime are transported from the function-field Galois group to the categorical finite quotient represented by the cover.

For the surjective quotient represented by a pointed finite-etale Galois cover, the inverse image of normalization-prime ideal inertia maps back onto that exact subgroup. Combining this quotient statement with the functi…

Reader-facing facade for the transported normalization action, the decomposition/inertia subgroup comparisons, and the residue-action kernel.

The residue action of the normalization-prime decomposition group has ideal inertia as its kernel, both internally and after mapping the kernel into the full categorical finite quotient.

A categorical Galois cover of the complement Spec (A[1/f]) supplies all field-theoretic and boundary-etaleness inputs of the local Kummer inertia theorem. In particular, neither a separately postulated Galois extension n…

For a finite-etale Galois cover of a normal integral locally Noetherian scheme, the opposite categorical automorphism group is the Galois group of the induced function-field extension. This file transports the canonical…

The normalization-prime inertia subgroup in a pointed finite-etale Galois quotient is killed by the combination of cyclotomic inversion and coprimality with two. The conclusion concerns the actual image of the fundamenta…

An explicit finite quotient of an etale fundamental group can be realized by a pointed connected finite-etale Galois cover. This file transports coprimality of normalization-prime inertia in the cover's function-field Ga…

For a noetherian normal domain, the integral closure in a finite separable extension of its fraction field is finite. This supplies the finiteness input needed by the split normal-crossings inertia theorem without a Naga…

A height-one prime of a regular domain gives a discrete valuation ring after localization. Its residue field is the function field of the corresponding prime divisor. This file applies the divisorial-residue cyclotomic t…

This file runs the split normal-crossings inertia theorem over a prime localization and transports its conclusion back to the original normalization prime.

Canonical aggregate for EtaleFundamentalGroups.Kummer.Obstructions.

For an adjoined-root algebra, formal unramifiedness forces the derivative of the defining polynomial at the distinguished root to be a unit. The proof descends the usual polynomial derivative to the quotient by the deriv…

For the Kummer equation X ^ n - t on the complement of the prime parameter t, etaleness would force the derivative at the distinguished root to be a unit. When the residue characteristic divides n, unit descent from the…

For a prime element t, the polynomial X ^ n - t is Eisenstein at (t). If the original domain is integrally closed, Gauss's lemma then transports this irreducibility to its fraction field. This is the field shared by the…

For the equation X ^ n - t on the complement of the prime parameter t, the derivative at the adjoined root cannot be a unit when the residue characteristic divides n. The proof combines the explicit derivative calculatio…

The finite étale cover is the original geometric cover. Its given generic fiber identifies its function field, and the actual étale stalk map supplies the unramified local calculation. Properness is nowhere required.

Canonical aggregate for EtaleFundamentalGroups.Kummer.PureRadical.

This file supplies the non-Henselian roots-of-unity input in the DVR form of Stacks Project, Lemma 15.115.6 (tag 09EV). If a uniformizer acquires an n-th root and n is a unit in the base DVR, then every n-th root of unit…

Let Rₙ = V[X]/(Xⁿ-π), let F be its specified fraction field, and let a maximal ideal of F ⊗[K] L select a field component. This file proves that the image of the integral root generates the whole selected component over…

This is the height-one input consumed by the one-divisor Abhyankar argument. Localizing a Noetherian domain at the principal prime generated by t produces a DVR whose uniformizer is the image of t. Characteristic zero on…

The abstract intermediate-field theorem needs to know that the relevant roots of unity in the radical field already lie in the base field. This file produces that input from the integral local model used in the one-divis…

For a domain A with fraction field K, let F = K(β) and suppose that β ^ m = t. Once the monogenic root algebra A[X] / (X ^ m - t) is known to be a normal domain, it is the integral closure of A in F. The theorem below pr…

The intermediate-field equality is converted here into the concrete generator needed by the one-divisor normalization argument. If e = [L : K], d = [L : F], and m = [F : K], then the generator is β = α ^ d, it satisfies…

Let L = K(α) be finite, put e = [L : K], and suppose that α ^ e belongs to K. If every e-th root of unity in L already belongs to K, then every intermediate field F is generated by α ^ [L : F]. In particular, its exponen…

Canonical aggregate for EtaleFundamentalGroups.Kummer.Radicals.

This file records the first concrete algebra facts for the Kummer equation X ^ n - a. After the boundary parameter has been inverted, its adjoined root is a unit. Consequently the derivative at that root is a unit exactl…

This file treats the final stage of an iterated radical construction. If T is faithfully flat over A, formal unramifiedness of the radical over A restricts to formal unramifiedness over T. The explicit derivative calcula…

Canonical aggregate for EtaleFundamentalGroups.Kummer.RootCovers.

When a height-one prime lies on a non-selected actual branch, the existing reordering presents that branch root last. Swapping the final two independent roots instead presents the same full cover as a finite free extensi…

The actual-root-first presentation identifies a full conditional root cover with one further monic root extension of the simple actual-root cover. This file transports finiteness and faithful flatness through that equiva…

The actual-root-first algebra is defined by transporting the two-root cover through an R-algebra equivalence. This leaf records the resulting scalar tower once, so downstream branch theorems do not repeatedly elaborate t…

At a height-two normal-crossings point, all conditional radical stages except the actual second boundary branch have degree one. This file first removes those degree-one stages without changing the distinguished actual r…

Canonical aggregate for EtaleFundamentalGroups.Kummer.RootCovers.Full.

The full height-two radical cover contains the selected one-root cover by base change along the preceding iterated radical extension. This file makes that map canonical, proves that it is finite faithfully flat, and iden…

Canonical aggregate for EtaleFundamentalGroups.Kummer.RootCovers.Local.

This file identifies the closed point of the one-step root cover R[X] / (X ^ n - a) when R is local and a lies in its maximal ideal.

After localizing at a prime, a boundary parameter outside that prime is a unit. Such a parameter must not be adjoined with a nontrivial root if one wants the whole iterated cover to remain local. The conditional presenta…

If every radicand belongs to the closed point of a local base ring, adjoining positive roots of those radicands one after another stays local. The proof also keeps track of the closed point: the image of the original max…

A finite iterated positive root cover of closed-point elements is complete for its own maximal ideal when the Noetherian local base is complete. Finite-module completeness first gives completeness for the extended base m…

This file exposes the individual roots in a finite diagonal Kummer cover and uses their defining equations to classify the contractions of height-one primes meeting the boundary. It also extracts the corresponding divisi…

This file upgrades regular-locality of the finite diagonal root cover to the stronger geometry needed branch by branch: its explicit root-and-parameter list is a regular system generating the maximal ideal. Hence the ful…

This file treats a finite diagonal root cover all at once. Starting from a regular parameter list consisting of the radicands followed by the remaining parameters, it tracks the images of all adjoined roots and remaining…

Adjoining a positive root of the first member of a regular system replaces that member by the new root. The resulting list is again a regular system generating the maximal ideal. Consequently the root cover is a domain a…

This file proves the regular-local part of the one-step Kummer root construction. The key dimension input is produced here from going-up: a faithfully integral extension cannot decrease Krull dimension. For B = R[X] / (X…

A positive root cover R[X] / (X ^ n - a) of an element in the closed point is local, and its closed point is generated by the image of the base closed point and the adjoined root. Hence the canonical map on residue field…

Canonical aggregate for EtaleFundamentalGroups.Kummer.RootCovers.SelectedDivisor.

At a height-two point, after placing the sole possible non-selected boundary branch first, all remaining conditional root stages have exponent one. This file removes those degree-one stages by an explicit algebra equival…

Let [x, y] be a regular parameter pair generating the maximal ideal of a Noetherian local domain. After adjoining a positive-degree root of x, this file proves that the cover is a regular local domain, that the image of…

Canonical aggregate for EtaleFundamentalGroups.Kummer.SelectedRoot.

Canonical aggregate for EtaleFundamentalGroups.Kummer.SelectedRoot.Exact.

The exact-root degree sandwich makes the canonical target-field map to the chosen component bijective. Mapping integral closures along the resulting field equivalence transports the primitive boundary-away statement with…

First choose a closed local factor of the normalization over the strictly Henselian exact-root ring, using only its finite-etale structure. Its chosen component field is already a finite extension of the original fractio…

For the exact ramification-index root, the degree sandwich identifies the input DVR extension field Omega with the strict-stage chosen component field P. Mapping integral closures along that sourced field equivalence ide…

Let Omega / K be a finite extension of discretely valued fields with ramification index e, and let Froot be the fraction field of the integral root ring V[X] / (X ^ e - varpi). The latter has degree exactly e over K. If…

Canonical aggregate for EtaleFundamentalGroups.Kummer.SelectedRoot.Exact.FixedTensor.

The prefix normalization and the normalization after adjoining the selected exact root live in different ambient fields. Therefore their primitive Away maps cannot be related by integral-base transport alone. At a strict…

For a fixed component of the exact ramification-index radical tensor product, finite-etaleness of the component normalization lets the strict-Henselian exact-root source choose a closed local factor before any away state…

Canonical aggregate for EtaleFundamentalGroups.Kummer.SelectedRoot.Intermediate.

Let A be a two-parameter regular local domain with selected boundary parameter t, and let K be its fraction field. In a pure radical field extension L / K, every intermediate field F has a concrete generator β satisfying…

Canonical aggregate for EtaleFundamentalGroups.Kummer.SelectedRoot.Prime.

For a prime element a, the root of X ^ n - a is again prime. The proof uses the canonical map to R ⧸ (a) which sends the adjoined root to zero and identifies its kernel with the principal ideal generated by that root.

At the prime generated by a positive Kummer root, the local root cover is already the root cover of the localized radicand DVR. This file combines that localization comparison with the canonical DVR completion comparison…

This file connects the literal selected-root localization to the complete higher-radical factor theorem. The first junction below refines a fixed post-root tensor component after extending the left field. It is the exact…

For a fixed component of the generic tensor product after adjoining an N-th root of a DVR uniformizer, every completed normalization factor is identified with a refined component of the completed root tensor product. The…

The selected-root descent theorem produces an etale normalization over the selected root DVR. This file keeps the selected generic tensor component and then applies a further normal base change, selecting an arbitrary co…

The completed-base-change ring attached to the selected root divisor is not merely faithfully flat over the selected local ring: it is its canonical adic, hence valued-field, completion. The essential calculation is that…

The standard valued-field completion of the selected root DVR and the fraction field of the completed pure-root ring are canonically equivalent. This is the fraction-field lift of the valuation-subring equivalence alread…

A prime boundary parameter remains prime at every larger prime containing it, and becomes a unit at every other prime localization. In the first case, characteristic zero of its generic residue ring is preserved by the l…

Canonical aggregate for EtaleFundamentalGroups.Kummer.UnitAbsorption.

For a valued extension of discrete valuation fields, write the image of a base uniformizer as u pi ^ e. When the base residue field has characteristic zero, the ramification index e is a unit in both valuation rings. Thu…

The unit-root construction used in the characteristic-zero DVR case chooses delta over the target field and then puts alpha = delta pi. This file records two facts which are needed to use that construction as an Abhyanka…

If e ∣ N, the pure e-th root cover of an element maps canonically to the pure N-th root cover by sending the first root to the (N / e)-th power of the second. This is the integral map needed to base change the finite-eta…

This file connects the integral higher-root base change from FiniteEtaleUnitAbsorptionHigherRadical to its specified generic field factor. The first two constructions record the canonical generic-fibre coordinates needed…

Canonical aggregate for EtaleFundamentalGroups.Kummer.UnitAbsorption.LocalDVR.

For a genuinely finite local DVR factor, the standard-DVF bridge in FiniteLocalDVRStandardDVF supplies the finite valuation-subring extension and the exact ramification index. HigherRadicalUnitFactorData then retains an…

This file is intentionally developed after the actual-compositum witness.

Height-one and height-two local geometry, DVR ascent, and regular-local results. Canonical aggregate for EtaleFundamentalGroups.LocalGeometry.

Canonical aggregate for EtaleFundamentalGroups.LocalGeometry.DVR.

There are two logically separate steps between an ideal-theoretic ramification calculation and the DVF package used by the Kummer terminal. First, localizing a prime q and its contraction carries q.ramificationIdx R to t…

A flat local map out of a discrete valuation ring is faithfully flat. If the source closed point generates the target closed point, the image of a source uniformizer is therefore a one-element regular system of parameter…

Canonical aggregate for EtaleFundamentalGroups.LocalGeometry.HeightOne.

On a locally Noetherian scheme, the generic point of an effective Cartier divisor has codimension one. If the ambient scheme is regular along the divisor, its stalk there is a discrete valuation ring, even when the whole…

At the generic point of an integral closed subscheme, the ambient residue field is the function field of the subscheme. The comparison below also transports geometric integrality across this canonical field equivalence.

For a morphism of integral schemes whose generic point lies over the generic point of the base, geometric integrality of the generic fibre makes the residue field at the source generic point geometrically integral over t…

Localization at a containing prime does not change the residue field of a branch, so geometric integrality transports canonically to the localized branch used in a height-two chart.

A two-dimensional regular local domain is integrally closed. Localizing at a height-one prime preserves integral closedness and Noetherianity, and the localized ring has Krull dimension one. Thus it is a non-field normal…

A regular point of coheight one on an integral scheme has a discrete valuation local ring. This is the scheme-level entry point for divisorial normalization and inertia results.

A discrete valuation ring inside a chosen fraction field determines the adic rank-one discrete valuation of that field. This file packages that valuation as a DVF, transports a local map of DVRs to an extension of the pa…

The standard discrete valuation attached to a DVR uses a valuation subring canonically equivalent to the original DVR. This file descends that ring equivalence to the closed-point quotients. In particular, characteristic…

Canonical aggregate for EtaleFundamentalGroups.LocalGeometry.HeightTwo.

For the finite-normalization argument we do not need to prescribe the first parameter. In a two-dimensional regular local domain, lift any basis of the cotangent space. The two lifts generate the maximal ideal and form a…

For a prime divisor in a Noetherian local domain, failure of an integer to be a unit on the divisor is detected at a height-two localization. Thus a unit result at every such localization globalizes to the generic point…

Canonical aggregate for EtaleFundamentalGroups.LocalGeometry.RegularLocal.

Mathlib's current definition of a regular ring directly asks for regularity of every prime localization; it does not yet provide the converse theorem that a regular local ring is regular. In dimension two, the explicit r…

Mathlib defines a regular ring through regularity at every prime and does not yet contain the general theorem that a regular local ring is a regular ring. In the two-dimensional domain case needed here, the missing local…

Canonical aggregate for EtaleFundamentalGroups.LocalGeometry.RegularPair.

For a Noetherian local domain whose maximal ideal is generated by a regular pair, this file proves integral closedness directly. The proof avoids a factoriality detour. For an integral fraction z, consider the conductor…

The actual genericNormalizationChart pullback identifies etaleness of the global normalization with etaleness of its literal integral-closure charts. For a finite Galois field extension, the proved affine inertia criteri…

The field is defined as the supremum of the finite subfields of the supplied ambient field whose literal integral closures over A are unramified. The geometric criterion then proves that this is the field fixed by the ac…

Integral closures, normalization primes, localization comparisons, and product factors. Canonical aggregate for EtaleFundamentalGroups.Normalization.

Canonical aggregate for EtaleFundamentalGroups.Normalization.Branch.

Canonical aggregate for EtaleFundamentalGroups.Normalization.Branch.GaloisRamification.

Localizing first at a prime containing a height-one branch, and then at the image of that branch, does not change the common ramification index of a finite Galois normalization.

For a finite Galois extension, all normalization primes above one height-one branch have the same ramification index. This is the exponent needed by the root cover: unlike the product of all branch indices, it does not i…

For a finite normalization, the product of the ramification indices of all primes above one height-one branch is a common multiple of exactly the local ramification indices which must be cancelled by the Abhyankar root c…

A quotient of an étale algebra over a normal domain which is itself a domain and remains faithful over the base is an idempotent factor, hence étale. The generic fibre selects its primitive idempotent; smooth base change…

At each base prime, the actual integral-closure localization and the actual residue-field tensor identify the original fiber with the closed fiber of the local normalization. The normal-local criterion supplies étaleness…

If the actual generic fiber of a finite étale morphism is a field spectrum, its source is connected. Over a normal integral base it is therefore the normalization in its function field. The generic pullback identifies th…

If the actual generic fiber of a finite étale morphism is a field spectrum, its source is connected. Over a normal integral base it is therefore the normalization in its function field. The generic pullback identifies th…

Generators at the selected prime and at the generic point produce one finite subalgebra of the original extension field. The actual inclusion realizes both localizations, so its fraction field remains that same field.

Opening the unramified locus first avoids assuming finite presentation or Noetherianity. The dominant-domain criterion supplies étaleness afterwards. This is the spreading step for the original local criterion in Tag 0BT…

A finite subalgebra with the correct fraction field becomes the actual normalization on each neighborhood where it is étale. Local finiteness and étaleness at a base prime therefore spread without any Noetherian hypothes…

The normalization of an integral scheme in an algebraic extension of its function field recovers that extension on the generic fibre.

For an algebraic commutative algebra L over the fraction field K of a commutative ring R, localizing the integral closure of R in L at the nonzero elements of R gives L. Consequently its generic fibre is the literal sche…

A dominant preimmersion from the spectrum of a field into an integral scheme is its generic-point morphism, up to the actual isomorphism of source schemes induced by the map on the generic stalk.

The original field automorphism restricts to the integral closure on every nonempty affine chart. This restricted spectrum map and the actual global normalizationEndomorphism commute with genericNormalizationChart. Their…

Actual affine normalization pullback squares identify their residue-field tensors with the original scheme fibers after the canonical residue-field isomorphism. Their finite flat ranks therefore agree. The affine degree…

The actual affine normalization square and the affine-chart stalk isomorphism identify each base-prime localization with the literal pullback over the original scheme stalk. The non-Noetherian ring criterion then supplie…

Canonical aggregate for EtaleFundamentalGroups.Normalization.IntegralClosure.

An equivalence of base rings does not change which elements of a common ambient ring are integral. This file packages that observation as an algebra equivalence between the two literal integralClosure subrings and uses i…

When a map in a scalar tower of fields is bijective, it gives an algebra equivalence of the ambient fields. Mapping integral closures along that equivalence transports the literal boundary-away etaleness statement.

For a finite algebraic extension of the fraction field of a UFD, an element which is integral over every localization at a prime element is already integral over the UFD. We descend the coefficients of its minimal polyno…

Canonical aggregate for EtaleFundamentalGroups.Normalization.IntegralClosure.IntegralBase.

For a finite base enlargement inside one field, the two integral closures are canonically equivalent. Localizing that equivalence at a primitive element transports etaleness of the literal away map to the normalization o…

Canonical aggregate for EtaleFundamentalGroups.Normalization.IntegralClosure.IntegralBase.ChosenLocalization.

Let A → B be finite, with B Henselian local, and let both rings act on one ambient field L. The integral closures over A and B are the same subring of L; IntegralClosureIntegralBaseEquiv equips that literal A-normalizati…

A bijective map between two ambient fields transports the primitive away property between their normalizations. Selecting a local factor only after that transport then retains the literal composite away map from the orig…

For a finite integral enlargement A → B with B Henselian local, a prime of the common normalization over the closed point exists by integrality. The chosen-localization theorem then makes its localization finite etale ov…

For a finite integral enlargement A → B with B Henselian local, a prime of the common normalization over the closed point exists by lying over. If the normalization is etale over B, localization at that prime is finite e…

An integral enlargement of the base does not change the normalization in a fixed ambient field. This file transports an arbitrary prime through that equivalence and then through localization of the original base. The fin…

Canonical aggregate for EtaleFundamentalGroups.Normalization.IntegralClosure.Localization.

Let M be a finite extension of the fraction field of a domain B. The integral closure C of B in M has fraction field M; localizing C at any prime does not change that fraction field. Consequently the literal FractionRing…

Let M / K be a finite extension of the fraction field of a domain R. The normalization integralClosure R M is integrally closed, and every localization of it at a prime remains integrally closed. This file records that f…

For the integral closure of a normal domain in a finite fraction-field extension, unramifiedness after localization at every base prime implies finite étaleness globally. Domain and faithfulness of each localization are…

Canonical aggregate for EtaleFundamentalGroups.Normalization.Localization.

This file uses the canonical fraction-field factorization from FractionFieldLocalization to relate a prime localization to the normalization in a field extension. The normalization inclusion is obtained by base-changing…

Normalization in a fixed field extension commutes with localization of the base. The resulting square is a pushout, so an etale map on a principal open of the original normalization remains etale after localization at an…

Canonical aggregate for EtaleFundamentalGroups.Normalization.Localization.IntegralClosure.

The standard affine open cover of a relative normalization is built from integral closures. This file turns formal etaleness of the corresponding prime-local algebra maps into finite etaleness of the actual global normal…

An isomorphism from a global normalization to the spectrum of a literal integral closure transports the global stalk map to the canonical prime-local map. This is the bridge used after an affine-chart normalization compa…

For a normalization prime Q over a base prime P, localizing the global normalization at Q agrees canonically with first localizing the base at P, normalizing there, and then localizing at the image of Q. The equivalence…

The stalk map of the affine normalization Spec (integralClosure A L) ⟶ Spec A at a normalization prime is the prime-local map obtained after first localizing the base and then normalizing. This file records the compariso…

This file identifies the localization of a global normalization at the image of a base-prime complement with the normalization after localizing the base. The equivalence is over the localized base itself, so it transport…

Transport only the scalar action along the canonical fraction-field isomorphism. The ambient algebra and its integral closure remain unchanged, and the native dimension comparison preserves the original generic degree.

Canonical aggregate for EtaleFundamentalGroups.Normalization.Primes.

Let q be a prime of the normalization of A in L, and let P be a prime of A containing the contraction of q. Then q is disjoint from the elements inverted in AP. Consequently its image in the normalization over AP is prim…

This file transports a prime of a normalization lying over P to the normalization after localizing the base at P. The construction uses the canonical normalization inclusion from NormalizationLocalization and the general…

A prime of the normalization over AP contracts to a prime of the original normalization. When the localized prime lies over the closed point of AP, that contraction lies over P; localizing it again recovers the original…

This file combines inverse localization with going-up. A chosen local normalization branch over a height-one prime is recovered as a prime of the original normalization, then followed to any prescribed larger prime of th…

If a chosen prime of a normalization lies over p and p \le P, going-up produces a prime over P which still contains the chosen prime. This keeps the same height-one branch factor when it is followed to a codimension-two…

This file isolates the order-sensitive final step used for a retained generic component. A prime over the generic point of an integral base is a minimal prime. Its extension to a larger-prime localization is zero once th…

For an integral scheme and an extension of its function field, lying-over selects a prime of the integral closure of the local ring at a point. The selection is made here once, together with its prime and lying-over inst…

Canonical aggregate for EtaleFundamentalGroups.Normalization.Products.

Stacks Project Tag 0BTF is assembled from the actual global, local-ring, ordinary-henselian, strict-henselian, and scheme-fiber suppliers. Both henselizations are the constructed pointed étale colimits; no finite set of…

The actual generic-fiber square identifies the rank of a finite etale normalization with the degree of the original field extension. Local constancy then gives the same degree on every scheme-theoretic fiber. This proves…

The normalization endomorphism is the actual extension of the original field automorphism. If it fixes any field-valued point, unramified point rigidity makes it the identity. The actual generic-fiber square makes the ma…

An unramified algebra which is a domain faithful over a normal domain is étale. The local structure of unramified algebras presents principal opens as quotients of standard étale algebras. Their dominant domain quotients…

A dominant unramified morphism from an integral scheme to a normal integral scheme is étale. Applied to relative normalization in a field extension of the function field, integrality then supplies finiteness. No Noetheri…

The generic-fibre comparison identifies the finite subfields coming from unramified normalization with the fields fixed by the generic Galois kernel.

Let S be a scheme and denote by FEt S the category of finite étale schemes over S. Then FEt S is a PreGaloisCategory.

The kernel of the natural action on a fiber functor is the intersection of its point stabilizers.

The upstream-derived actions on algebra homomorphisms and field-point morphisms, the comparison with homomorphisms on global sections, and the detection of field automorphisms by finite etale points.

Quotient base change for finite étale algebras over a complete Noetherian local ring is transported across the affine finite étale equivalence. This gives the corresponding equivalence for finite étale covers of affine s…

Local and special-local purity, support, and faithfully flat descent. Canonical aggregate for EtaleFundamentalGroups.Purity.

A finite secondary decomposition has finitely many radical annihilators. Prime avoidance chooses a member of the maximal ideal outside all the nonmaximal ones, together with any prescribed finite set of nonmaximal prime…

For a secondary module, a scalar acts surjectively exactly when it lies outside the radical of the annihilator. That radical is prime: after cancelling a surjective scalar power, a product that kills the module forces th…

Multiplication on a secondary module is either surjective or nilpotent. If an Artinian module fails this condition, the stabilized kernel-range sum for the offending multiplication expresses it as the sum of two proper s…

The submodule killed by the maximal ideal has its canonical residue-field module structure. An Artinian module over this field is finitely generated; restriction of scalars then makes it finite over the original Noetheri…

Choose actual principal Cartier charts. Stalk-localization isomorphisms, normalization under open base change, and the principal complement square transport the given local finite étaleness to the affine normalization. T…

The degree-zero map of the injective Čech contraction is identified with the canonical torsion inclusion using the tensor coefficient comparisons.

The actual principal localization contraction is tensored with the remaining factors. Iteration identifies the Čech complex of an injective module with its ideal-power torsion, concentrated in degree zero.

The natural degree-zero inclusion identifies Čech cohomology with ideal power torsion. This is first checked on injectives using the actual contraction, then descended along an injective presentation by exactness. The co…

Tensoring the two-term principal localization complexes gives a complex whose terms are flat and which ends in the degree given by the length of the list. All signs, summands, and differentials are supplied by the standa…

The antidiagonal indexing the zeroth term has exactly one summand. Its inclusion identifies the zeroth term of each Čech factor with the ring. Tensoring this identification gives the canonical coefficient identification,…

The tensor complex with a coefficient module concentrated in degree zero is naturally identified degreewise with tensoring each original term by that coefficient module. The construction uses the unique nonzero summand i…

When all missing points are closed, at each missing point the open pulls back to the actual stalk puncture. Connectedness of its actual strict-stalk puncture therefore extends a finite etale section to the full stalk. Th…

A point with one-dimensional stalk outside a dense open in a locally Noetherian scheme is a generic point of that open's complement. Indeed, in an affine neighbourhood, every irreducible component meets the dense open. A…

For a dense open and a missing point whose stalk is a DVR, the actual stalk overlap is identified with the spectrum of its fraction field. The induced map from that fraction field to the open preserves the map to the amb…

The finite-length socle of an Artinian maximal-ideal-power torsion module embeds in a finite product of residue-field hulls. Injectivity extends this embedding to the module, and essentialness keeps it injective. The coo…

Chevalley's lemma compares a descending sequence of ideals with zero intersection to the powers of the maximal ideal. The proof uses stable images modulo these powers and lifts compatible representatives directly.

The dual of degree n maximal-support local cohomology of finite coefficients has support dimension at most n. The proof uses the coefficient long exact sequence and the dimension inequality for a scalar quotient. In degr…

Constructing an Artinian injective hull of the residue field shows that any module with a finite-length essential submodule is Artinian. In a maximal-ideal-power torsion module the socle is essential, so it suffices that…

An endomorphism of the hull acts by a scalar on every maximal-ideal power-torsion layer. The scalar classes are compatible because their differences annihilate each smaller layer. Completeness lifts them to one scalar in…

Contracting the maximal-ideal-primary component of a quotient gives the maximal-ideal saturation of its defining ideal. If an ideal lies in a nonmaximal prime of a complete Noetherian local domain, its saturated powers a…

For a prime with quotient of dimension at most one in a complete Noetherian local domain, sufficiently deep symbolic powers lie in any specified ordinary power. Modulo that ordinary power, the symbolic-power images lie i…

The symbolic powers of a prime are the contractions of its powers after localizing at that prime. In a Noetherian domain their intersection is zero. Finite generation also clears the denominators of an entire symbolic po…

Every nonzero scalar acts surjectively on positive top local cohomology of a local domain. Its linear dual is therefore torsion-free. For a complete domain, top nonvanishing and separation by an injective module containi…

Formal smoothness lifts a map from the first infinitesimal quotient to an adically complete target. Adic separatedness and formal unramifiedness make that lift unique. Thus reduction modulo the ideal is bijective on maps…

A connected finite-etale cover of a nonempty quasi-compact open subscheme induces a finite separable extension of the ambient function field. Hence the relative normalization of the ambient scheme in that extension is fi…

The relative normalization attached to a connected finite-etale cover of an open subscheme restricts to that cover. In particular, its restriction to the range of the open immersion is finite etale.

For a connected finite-etale cover on a smooth monomorphism, the relative normalization of the ambient scheme in the cover's function field already has a canonical restriction isomorphism. Thus a proof that this one cano…

Let a finite etale cover of a dense open U already extend to N. At a missing regular point with one-dimensional stalk, its original generic field factors over U still supply the needed DVR model. The canonical fraction-f…

At a generic point of the complement of an open, the actual stalk overlap is the punctured local spectrum. If this local ring is a DVR, its puncture is the spectrum of its fraction field. The unramified field-factor cond…

localCohomology is currently defined using the legacy derived-functor object root.Ext, whereas the depth API uses CategoryTheory.Abelian.Ext. This file records the vanishing comparison needed to pass from the latter to t…

Mathlib's existing localCohomology functor is defined using the legacy left-derived Ext functor. The long exact Ext sequence, on the other hand, is currently available for CategoryTheory.Abelian.Ext. This file names the…

If one generator of the support ideal annihilates the coefficient module, local cohomology vanishes above the number of remaining generators. The proof uses strong induction on that number. Mayer--Vietoris removes one re…

A nonzero element of the maximal ideal of a Noetherian local domain can be completed to a system of parameters. Lift a system of parameters from the quotient by that element; regularity gives the required dimension drop.…

Induction on degree is combined with a prime filtration of the finite coefficient module. Residue-field factors have no positive local cohomology. Every other prime factor has a regular scalar in the maximal ideal, and i…

Degree-zero local cohomology embeds in its finite coefficient module. Noetherianity makes it finite, and its maximal-ideal-power torsion then gives finite length. This is the base of the Artinianness induction.

A scalar annihilating the coefficients annihilates every local-cohomology class, as is seen on its Ext representative. Along a coefficient short exact sequence, an annihilator of the quotient and an annihilator of the mi…

For a short exact complex of coefficient modules, the covariant long exact sequence of derived Ext is natural in the first variable. Applying this to the quotients by all powers of an ideal gives an objectwise exact diag…

Evaluation of degree-zero local cohomology commutes with the second coefficient map. When the middle coefficient module is ideal-power torsion, its evaluation map is surjective. Exactness of the coefficient sequence and…

In degree zero, a representative is a map from a quotient ring to the coefficient module. Evaluation at one is compatible with the quotient transition maps and hence defines a linear map out of local cohomology. Each rep…

For a nonzero nonunit x in a local domain, the extension class of 0 → R → R → R/(x^n) → 0 supplies a class in degree one which survives every transition in the principal ideal-powers diagram.

In a one-dimensional local domain, every nonzero element has principal radical containing the maximal ideal. Consequently, a proper radical ideal different from the maximal ideal contains no nonzero element and is the ze…

The coefficient connecting map is surjective when the middle module is injective, and bijective when its source cohomology degree is positive. These are consequences of the actual coefficient long exact sequence and vani…

The parameter-pair and coefficient-vanishing results are the two-dimensional specializations of the general parameter-list construction and annihilated-coefficient top-degree bound.

The degree-zero base case of Grothendieck nonvanishing is already visible in the ideal-powers Ext diagram. For the zero ideal, every positive power is again zero, and the identity class of R ⧸ (0) survives every later tr…

A nonzero functional on a finite torsion-free module has a nonzero ideal as its image. The kernel has dimension at most that of the ring, whereas the quotient by the image has strictly smaller dimension. The two actual s…

For a finite list in a Noetherian local domain, derived local cohomology supported on the ideal generated by the list vanishes in degrees strictly larger than the list length. If one generator is a unit, the support is t…

A cocycle from R / I^k evaluates at one to an ideal-power torsion cocycle. This respects coboundaries and the transition maps in the Ext-colimit. Conversely every torsion cocycle admits such a representative, and a torsi…

This file constructs the projective-resolution comparison between derived-category Ext and the legacy left-derived Ext used by localCohomology. The comparison is first built in positive degree from the common cocycle quo…

The exact filtered-colimit window in positions two, three, and four of the ideal-quotient derived-Ext sequence has support terms I ⊓ J, I ⊔ J, and the biproduct of the I- and J-support terms. Thus vanishing of the two ou…

The scalar endomorphisms of the additive-group colimit satisfy the module laws. We package this action in an object of ModuleCat R, retaining the original additive group. The module structure is installed only while cons…

The coefficient maps and the connecting maps act on colimit representatives by postcomposition in derived Ext. Bilinearity of composition makes these maps linear for the module structure already constructed on the local-…

Ideals with the same radical define the same torsion submodule. Comparing these submodules before applying a common injective resolution gives an isomorphism on homology that retains its scalar action.

Positive-degree local cohomology vanishes on injective coefficients, because every derived Ext group in its defining diagram vanishes. An ideal-power torsion module over a Noetherian ring has an injective presentation wh…

The coefficient long exact sequence immediately supplies mono/epi criteria when one of its neighboring terms vanishes. The main result of this file is a source-level vanishing theorem: if x annihilates a module M, then d…

For a principal ideal (x), the quotient by its n-th ideal power is canonically the quotient by the submodule x ^ n R. This file records that identification and its compatibility with the standard transition maps between…

Uniform projective-dimension bounds make every object of the derived Ext ideal-powers diagram trivial. This gives the derived-colimit counterpart of the existing vanishing results for Mathlib's legacy local-cohomology ob…

The diagram of powers of an ideal is initial in the diagram of all ideals whose radical contains it. Applying the same cofinality argument as for Mathlib's legacy local cohomology shows that the derived-Ext colimit depen…

Scalars act on each derived-Ext group in the ideal-powers diagram and commute with its transition maps. Their induced colimit endomorphisms describe the scalar action without installing another module structure on the un…

For a scalar regular on the coefficient module, the connecting map from the preceding cohomology of its quotient has image equal to the scalar kernel on the next local-cohomology module. Artinianness of that quotient coh…

For a regular scalar, the coefficient long exact sequence identifies local cohomology of the scalar quotient with the quotient of local cohomology by that scalar whenever the next cohomological degree vanishes.

The ideal-quotient Mayer--Vietoris diagram uses I ^ n ⊓ J ^ n and I ^ n ⊔ J ^ n, whereas local cohomology is defined from powers of a single ideal. The supremum comparison is elementary. For intersections, Artin--Rees sh…

Over a complete Noetherian local ring, a finite module of finite support dimension has nonzero local cohomology in that dimension. In positive dimension the top local-cohomology module is not finitely generated. The two…

Degree induction and a prime filtration reduce finite coefficient modules to prime quotients. Either the support ideal annihilates such a quotient, or it contains a regular scalar in the maximal ideal. Quotienting by tha…

The support of a zero-dimensional finite module over a local ring is the closed point. A power of the maximal ideal therefore annihilates it, and degree-zero local cohomology evaluates isomorphically onto the module.

In a Noetherian local domain of finite Krull dimension d, choose d parameters whose generated ideal has maximal radical. Generator-count vanishing for that ideal, followed by radical invariance, gives vanishing of maxima…

A regular scalar in the maximal ideal lowers the support dimension of finite coefficients. The top cohomology of its quotient vanishes, so the scalar acts surjectively on top cohomology. If that cohomology were finite, N…

The coefficient map for M → M → M / xM agrees with the scalar endomorphism constructed on the ideal-powers colimit. For the ring as coefficients, a nonzero member of the maximal ideal is regular, and its quotient has zer…

The quotient by the maximal-ideal-primary component has zero degree-zero local cohomology: evaluation is injective, and every value is a power-torsion vector in a quotient containing no such nonzero vector. In positive d…

For a finite torsion-free module, quotienting by a nonzero scalar lowers support dimension. The coefficient exact sequence therefore makes that scalar surjective on top local cohomology for every support ideal.

Degree-zero local cohomology has image equal to the primary component of the coefficient module. In a short exact coefficient sequence whose first term is ideal-power torsion, the positive-degree second maps are linear e…

Canonical aggregate for EtaleFundamentalGroups.Purity.Descent.

Integral closedness descends along a faithfully-flat map of domains without any Noetherian hypothesis. For an integral fraction a / b of the base, integral closedness upstairs says that its image belongs to the target do…

Over a Noetherian ring, an essential extension of an ideal-power torsion module is again ideal-power torsion. First, any prime annihilator in the extension contains the ideal: otherwise an element of the ideal acts injec…

A submodule is essential if every submodule disjoint from it is zero. For any submodule N of M, Zorn's lemma gives a maximal submodule P disjoint from N. The image of N in M / P is then essential: the inverse image of a…

Essentiality of N inside S can be tested on the ambient submodules contained in S. Intersecting an arbitrary submodule with S then proves transitivity of essential extensions.

Zorn's lemma applied to essential extensions of a given submodule produces a maximal one inside the chosen ambient module. For a chain, essentiality of the supremum is checked elementwise: an element of a disjoint submod…

Off the principal boundary, normalization recovers the given finite etale cover. At boundary primes of height one, the hypothesis is a property of the actual scheme base change. The canonical function-field comparison tu…

Finite modules over a Noetherian adically complete ring are complete. Hence formal etaleness makes reduction modulo the extended ideal bijective on maps. The tensor-product description of quotient base change then gives…

For a morphism of finite presentation, formal etaleness of every stalk is enough to recover etaleness. Combining this with the finite-presentation consequence of finiteness over a locally Noetherian target gives a bounda…

Over a complete Noetherian local ring, finite-etale algebras lift from every quotient by an ideal in the maximal ideal. For a nilpotent ideal, formal etaleness also lifts every morphism uniquely. Together these statement…

For a complete Noetherian local ring, every finite-etale algebra over a quotient by an ideal in the maximal ideal comes by base change from the original ring. This file packages the algebraic lifting theorem as the canon…

A finite étale algebra over a quotient of a complete Noetherian local ring splits into finitely many local factors. Lifting those factors separately and taking their product gives a finite étale algebra over the original…

Finite étale algebras over a complete local ring need not themselves be local. Their closed fibre is a finite product of fields. The corresponding complete orthogonal idempotents lift through the Henselian closed-fibre m…

A finite generating family of the dual gives finitely many maps that separate the original finite-length module. Their product is an embedding into a finite product of injective hulls. An embedding of an essential submod…

A finite generating set bounds the ideal-power exponents needed to kill individual elements. In the local Noetherian case the module is then finite over an Artinian maximal-ideal-power quotient, so it has finite length.

Localizing a torsion-free module in the fraction field preserves its nonzero vectors. A vector-space functional separates such a vector; clearing the denominators of finitely many generators gives a functional with value…

Tensoring an injection with a flat module is injective. An extension into an injective module along that tensor map can therefore be curried into an extension with values in the linear dual. This supplies the injective t…

At a generic point of an irreducible component of the complement, the actual overlap of the local spectrum with the open is its puncture. Local purity therefore supplies an extending cover, retaining an isomorphism on th…

+# Extending an open section to a generic complement stalk At a generic point of an irreducible component of the missing closed set, the open pulls back to the actual stalk puncture. Connectedness of its actual strict-st…

This file isolates two source-level inputs used at the Hartshorne--Lichtenbaum frontier. First, a colimit of additive groups vanishes when every object admits a later transition whose map is zero. Applied to the ideal-po…

A parameter Čech complex gives a bounded flat model for maximal-support local cohomology. Its dual into the residue-field injective hull is a bounded complex of injectives. Saturated powers remove degree-zero maximal-sup…

Codimension-one intersection arguments naturally descend a generic-fibre linear map before they establish its multiplicative structure. If the descended map becomes an algebra morphism after composition with an injective…

Canonical aggregate for EtaleFundamentalGroups.Purity.HeightOne.

In a positive-dimensional Noetherian local domain, every element of the maximal ideal is contained in a height-one prime. This is the domain case of the general height-one prime existence theorem for Noetherian local rin…

Over a unique factorization domain, a matrix over the fraction field whose entries belong to every prime-element localization has a unique matrix over the original ring. Via the standard bases, this gives existence and u…

An element of the fraction field of a unique factorization domain which lies in the localization at every prime element already lies in the original domain. The proof uses a reduced numerator and denominator and detects…

The inclusion of a module into its injective resolution identifies its power-torsion submodule with the degree-zero torsion cycles. Exactness supplies the preimage of a cycle; injectivity of the inclusion transports its…

The functor takes the submodule of elements killed by a power of an ideal. Its maps are restrictions of the original linear maps, so its inclusion into the identity functor is natural and it is additive. Applying it term…

The primary component of an injective module embeds in an injective power-torsion module. Extending its inclusion into the original module gives a map back whose image remains in the primary component. This is a retracti…

The injective hull of an ideal-power torsion module over a Noetherian ring is again ideal-power torsion because its embedded image is essential. The quotient inherits power torsion from the hull. The inclusion and the qu…

A power-torsion vector defines a map from a quotient of the ring. For an ideal family cofinal with ordinary powers, lifting those quotient maps therefore lifts every power-torsion vector to a power-torsion vector. This p…

The binomial bound (I + J)^(n + m) ≤ I^n + J^m identifies power torsion for a sum with the intersection of the two power-torsion submodules. This also constructs the linear equivalence needed to iterate principal torsion…

An objectwise exact diagram of finite composable sequences determines an exact short complex of functors on every adjacent three-term window. Exact filtered colimits then give the corresponding exact short complex of col…

The middle object in the ideal-quotient Mayer--Vietoris sequence is a Cartesian product of quotient modules. This file identifies its derived-Ext diagram with the pointwise biproduct of the two ideal-power diagrams. Sinc…

The contravariant six-term derived-Ext sequence of a short exact complex is functorial in morphisms of short complexes. Applying that naturality to the power-compatible ideal-quotient Mayer--Vietoris complexes produces t…

The third term in degree n₀ of the finite derived-Ext sequence is the simultaneous-intersection support, and the following term in degree n₁ is the simultaneous-supremum support. Cofinality identifies their filtered coli…

For ideals I and J, the standard sequence 0 → R/(I ∩ J) → R/I ⊕ R/J → R/(I + J) → 0 is short exact. Applying contravariant derived Ext gives its six-term exact sequence. This is the finite-stage algebraic input for a fut…

This file makes the finite-stage ideal-quotient Mayer--Vietoris sequence functorial in inclusions of both ideals. In particular, the sequences for the powers of two fixed ideals form a diagram indexed by ℕᵒᵖ. This is the…

A finite complete orthogonal family e : I → D decomposes a commutative ring into the product of the quotients D / (1 - e i). This file packages the bijectivity statement in CompleteOrthogonalIdempotents.bijectivepi as ri…

The cycle--boundary and boundary--homology short exact sequences are constructed directly from the differentials. Their coefficient sequences allow scalar annihilators to be propagated up the chain.

If the image of a map is the kernel of a scalar endomorphism, the dual map embeds the scalar quotient of the dual into the dual of the source. A functional vanishing on the kernel factors through the scalar image; inject…

Restriction of maps into an injective module is surjective. Together with left exactness of Hom, this gives a short exact sequence dual to a submodule-quotient sequence. The dual of a simple module is identified with the…

The contravariant linear Hom functor with injective values is exact. This is obtained from preadditive Yoneda exactness by the forgetful functor, which reflects finite limits and colimits. Applying the exact functor to a…

Choose a maximal essential extension E of a submodule N inside an injective module M. Quotienting M by a maximal submodule disjoint from E gives an essential extension of E. Injectivity of M extends the inclusion of E to…

Over a Noetherian ring the localization map of an injective module is surjective. Stabilization of the kernels of powers of a denominator makes an appropriate division map well-defined on a principal ideal; injectivity e…

A nonzero element generates a cyclic module whose defining ideal is contained in the maximal ideal. Its quotient onto the residue field, followed by the given embedding, extends to the entire module by injectivity. Thus…

The cocycle constructor for derived-category Ext is linear. Its surjectivity and its explicit coboundary criterion identify the quotient of cocycles by coboundaries with positive-degree Ext over the original scalar ring.

For an injective module containing the residue field, maps to the module separate every quotient. If all its endomorphisms are scalar maps, this separation gives the double-annihilator equality for every submodule. Annih…

The first, torsion-level input to formal gluing is that extension of scalars from a ring to its adic completion does not change a module annihilated by the adic ideal. The proof uses the closed-fibre comparison and is va…

For a finitely generated ideal I, reduction of the I-adic completion modulo the extended ideal is canonically the original quotient R ⧸ I. This is the closed-fibre comparison used by formal gluing along completion.

For a finitely generated ideal I, an element of \hat R \otimesR M annihilated by I ^ n already comes from an I ^ n-annihilated element of M. This is the torsion-reflection calculation used in the mixed completion/localiz…

Canonical aggregate for EtaleFundamentalGroups.Purity.Local.

A quotient of a Noetherian complete local ring by an ideal contained in the maximal ideal is again complete local, hence Henselian. Completeness is first proved for the extended maximal ideal; surjectivity of the quotien…

Regularity supplies both integral closedness and a generating regular system of parameters, giving punctured purity without either as an extra hypothesis.

The actual restriction map on a finite flat scheme over a Noetherian local ring of depth at least two is an isomorphism. A regular pair in the base stays regular in its flat section algebra, so Hartogs extension applies.

At every height-one point of the regular base used in the absolute Abhyankar argument, the local ring is a DVR. A finite torsion-free algebra over that DVR is finite free, hence flat. If the algebra is local, unramifiedn…

A finite étale local algebra over a quotient of a complete Noetherian local ring is the base change of a finite étale algebra over the original ring. The lift is the explicit monogenic lift of the residue-field extension…

Over a noetherian ring, the first syzygy of a finitely presented module is again finitely presented. The contravariant long exact Ext sequence of a finite-free presentation therefore expresses Ext¹ as a cokernel of two H…

For a flat algebra S / R, the canonical map HomR(M, N) → HomS(S ⊗ M, S ⊗ N) is a base-change map when M is finitely presented. The finite-presentation result follows from Module.FinitePresentation.isBaseChangemap; the fi…

For elements f i : R, this file packages the elementary degree-one Koszul relation module {x | f i • x j = f j • x i} / {i ↦ f i • m}. Its key property is that it is annihilated by the ideal generated by the f i. This is…

A finite module over a Noetherian local ring that is complete for the maximal-ideal filtration is complete for every finer ideal-adic filtration. The key point is that the submodules I ^ n • M are closed for the maximal-…

The maximal-adic completion of a Noetherian local ring is flat and local, hence faithfully flat. Once Noetherianity of the completed ring has been produced, going down and the explicit description of its maximal ideal sh…

Let R be a noetherian local ring and let R̂ be its completion at the maximal ideal. For a finitely presented module Q killed by a power of the maximal ideal, the canonical functorial map Ext¹R(Q, N) → Ext¹R̂(R̂ ⊗ Q, R̂ ⊗…

The completion comparison for Ext¹ starts with a finite module killed by a power of the adic ideal. This file records the two elementary facts needed before the flat base-change argument: the same ideal power annihilates…

Bilinear maps are linearized on the tensor product and then descended by the mixed Hom full-faithfulness theorem. Thus a compatible completion component and compatible principal-localization components determine a unique…

For a Noetherian local ring, a module is the fibre product of its maximal-adic completion and its restrictions to the chosen principal cover of the punctured spectrum. The overlap is computed by localizing the completed…

The mixed module equalizer upgrades to full faithfulness on morphisms. A compatible tuple consists of a map after maximal-adic completion and one map on every distinguished principal localization. Compatibility is checke…

Let Rhat be the completion of a Noetherian local ring R at its maximal ideal, and let Ri be the principal localizations associated to a finite generating family of that ideal. This file packages the single affine cover R…

This file packages the degree-zero Cech diagram used in formal gluing. A datum has one completion module, one module on every principal chart, common completion/chart overlap modules, and common chart/chart overlap modul…

This specializes faithfully flat Hom descent to the completion map of a Noetherian local ring. It is the full-faithfulness input for module formal gluing at the closed point.

For a Noetherian local ring of depth at least two, a finite étale cover of the punctured spectrum extends precisely when its actual global-sections algebra is finite étale over the base ring. This proves Stacks Project,…

On a finite étale scheme over a regular local ring of dimension at least two, restriction to the inverse image of the puncture preserves all global sections. The proof uses the actual flat algebra of global sections and…

The completed extension preserves global sections by the prime-pair Hartogs theorem. Flat base change then descends its finite étale section algebra and the open immersion into its affinization. The original cover is rec…

The induction on dimension in local purity cuts a regular local ring by a parameter whose cotangent class is nonzero. This file supplies the local algebra behind that step in arbitrary dimension: quotienting a regular lo…

Successively cut a regular local ring by a nonzero cotangent vector. The quotient is again regular local with dimension one smaller. Lifting its regular system of parameters gives a regular system in the original ring.

A regular local ring of dimension at least two supplies two parameters for the prime-away intersection argument. The nondivisibility is derived from regularity in the quotient by the first parameter.

Local cohomology is defined as a colimit of Ext modules. This file records the categorical passage from pointwise vanishing of the Ext diagram to vanishing of the resulting local-cohomology module.

Local cohomology is a colimit of Ext groups against the quotients by powers of its support ideal. A uniform projective-dimension bound for those quotients therefore gives high-degree vanishing. For a principal ideal gene…

A regular sequence in an ideal annihilates the low positive-degree Ext groups by the Rees theorem. Combining that result with the comparison between the two Ext implementations gives the corresponding local-cohomology va…

A proper ideal with nonmaximal radical lies in a nonmaximal prime. The spectrum of a Noetherian local ring has finite dimension, so a prime of coheight one lies above that prime. The quotient-spectrum order isomorphism i…

On a topologically Noetherian scheme, local purity at all points outside an open implies that every finite étale cover of the open extends globally. At a generic missing point, local purity, spreading, and two-open gluin…

Connected punctured strict stalks give full faithfulness of restriction when every quasi-compact open has finitely many irreducible components. The proof uses the existing finite etale internal Hom representer and the co…

+# Finite etale section extension from punctured strict-stalk connectedness For a scheme whose quasi-compact opens have finitely many irreducible components, a finite etale section on a dense open extends globally when t…

A positive power of the maximal ideal has that same maximal ideal as its only minimal prime. Its quotient is Artinian, and restriction of scalars gives finite length over the original Noetherian local ring.

If every vector is killed by some power of an ideal, the submodule killed by the ideal itself is essential. On a submodule disjoint from it, induction on the annihilating exponent makes each vector zero. The successor st…

The primary component of a finite module over a Noetherian ring has a uniform annihilating ideal power. If a quotient vector is killed by another power, the product of those two powers kills any lift. The lift therefore…

Start with Mathlib's injective presentation of a module and replace the ambient injective module by an injective essential extension of the image. The resulting embedding has essential image and the same universe as the…

For a quasi-compact open immersion, it suffices to prove that the canonical function-field normalization attached to every connected Galois cover is finite etale. The normalization supplies the extension objects, and ope…

If every element of a module is killed by a power of a scalar, the kernel of multiplication by that scalar is essential. On a submodule disjoint from the kernel, induction on the annihilating exponent forces every elemen…

The residue field is annihilated by the maximal ideal. For any other prime quotient of a local ring, an element of the maximal ideal outside the prime acts regularly. These properties transfer along a coefficient linear…

The complex has a coefficient module in degree zero, its localization in degree one, and zero in higher degrees. Its positive cohomology vanishes on injective modules over Noetherian rings, and its terms preserve flatnes…

The localization sequence splits because its kernel is an injective primary component. In particular the localized term is injective. The actual inclusion of the primary component in degree zero is a quasi-isomorphism be…

The usual tensor description of module localization identifies tensoring the ring's principal localization complex with the principal complex of the coefficient module. Compatibility with the differential is checked on p…

The finite source over the principal localization is replaced by its actual affine spectrum. The structure map supplies the algebra structures, and the canonical source-normalization isomorphism preserves every base chan…

For a Noetherian local ring and an equation in its maximal ideal, any open containing the punctured hypersurface has a smaller such neighbourhood on which equality of finite étale morphisms is detected by the hypersurfac…

If every minimal prime not containing the equation has quotient dimension at least two, every connected component of the punctured spectrum meets the hypersurface. Consequently finite étale restriction to its actual pull…

The category of germs is the concrete localization of finite etale models on open neighbourhoods at their cartesian transition arrows. Restriction is the actual base-change functor from this localization to the punctured…

The indices are opens inside the punctured local spectrum that contain its hypersurface. Their order is reversed so that intersections are later stages. The cone vertex is the actual pullback of the hypersurface to the p…

Delete the closed sets of the minimal primes outside V(f) whose quotient dimension is less than two. There are finitely many such primes. None of those closed sets meets the punctured hypersurface: such an intersection w…

Let U be an open neighbourhood of the punctured hypersurface V(f) in the spectrum of a Noetherian local ring. Only minimal primes lying in U and outside V(f) need the quotient-dimension-at-least-two condition. Under that…

The target in Stacks Project, Lemma 58.22.1 is the punctured spectrum of R / (f). The previously constructed neighbourhood cone uses the pullback of Spec (R / (f)) to the puncture of Spec R. The cartesian square of the a…

For a local ring R, the punctured spectrum is the complement of its unique closed point. This file supplies the canonical open immersion and packages local purity as essential surjectivity of finite-étale pullback along…

For a connected finite-etale cover of the punctured spectrum of a positive- dimensional Noetherian normal local domain, its canonical function-field normalization is already finite. This file combines that finiteness wit…

The canonical global relative normalization attached to a connected cover of a punctured local spectrum is already identified with the spectrum of the literal integral closure. Here that global comparison is refined at a…

This file gives the first Cech-level data for the finite principal affine cover of a punctured local spectrum. A pairwise intersection is identified with the spectrum of the localization away from the product of the two…

This file constructs the triple-intersection level of the principal Cech cover. It identifies a triple intersection with the spectrum of both the product localization and the corresponding three-stage localization, expos…

This file converts the ideal-theoretic separation attached to a disconnected punctured hypersurface into the two power containments used by complete-local intersection arguments.

This proves the Grothendieck connectedness input used by the local purity induction from Hartshorne--Lichtenbaum vanishing and top local-cohomology nonvanishing. The Mayer--Vietoris argument applies to every finite list…

This file extracts the consequences of the two radical component ideals produced by a disconnected punctured principal hypersurface. In a domain, the principal element is nonzero. The component ideals also determine two…

Disconnectedness of a punctured principal hypersurface produces two height-one minimal primes whose supremum has maximal radical. This file sharpens the existing height-at-most-one output to exact height one and identifi…

This file generalizes the component-theoretic reduction for a principal hypersurface to an ideal presented by a finite list. Krull's height theorem shows that every minimal prime over the ideal has height at most the num…

Grothendieck connectedness for the literal normalization fibre supplies the connected-cover input in the categorical hypersurface induction theorem. This file packages that passage as a reusable one-step purity theorem.

A local ring map which carries the source maximal ideal onto the target maximal ideal pulls the punctured spectrum back to the target punctured spectrum. This file packages the resulting cartesian square and its finite-e…

This file records the completeness and codimension properties of the finite integral-closure model attached to a connected finite-etale cover of a punctured local spectrum. These are the algebraic inputs preceding the co…

For a connected finite-etale cover of a positive-dimensional punctured normal local spectrum, its function-field normalization over the full spectrum is finite. Pulling that actual finite normalization back to a local qu…

This file isolates the connected part of the normalization construction for a finite-etale cover of a punctured two-dimensional regular local spectrum. The cover supplies a finite separable function-field extension, and…

A finite local integral algebra over a complete Noetherian local ring is complete for its own maximal ideal. This supplies the completeness input for the finite normalization attached to a connected punctured cover.

The punctured closed fibre of the function-field normalization is defined scheme-theoretically by two pullbacks. This file compares those pullbacks with the punctured spectrum of the corresponding quotient of the literal…

For a connected finite-etale cover of the puncture of a positive-dimensional normal Noetherian local domain, the integral closure in the cover's function field is finite over the local domain. No finite-type hypothesis o…

A finite domain algebra over a complete Noetherian local ring is local. The proof passes to the closed fibre: completeness lifts idempotents, so the closed fibre is connected; finite-dimensionality makes it Artinian, hen…

This file compares the normalization in the function field of a connected finite-etale cover with the cover itself. The comparison is constructed from the universal property of relative normalization and checked on affin…

For a Noetherian local ring, the maximal ideal has a finite generating set. The corresponding principal opens cover the complement of the closed point. This file constructs that cover on the actual punctured spectrum, pr…

This file algebraizes connected finite-etale covers of the punctured spectrum by normalizing the full spectrum in their function fields. The normalization is finite etale by the two-dimensional integral-closure theorem,…

The nonempty finite subsets of a chosen finite generating set, ordered by reverse inclusion, index the principal opens obtained by inverting the product of the selected generators. Singleton subsets recover the original…

A cartesian scheme diagram over the directed finite principal-open cover is already effective by relative gluing. This file proves that when its chart maps are finite etale, the resulting glued morphism is finite etale a…

The canonical open immersion identifies the function field of a positive-dimensional local domain with that of its punctured spectrum. In particular, the latter is a fraction field of the original local domain.

This file closes the formal Mayer--Vietoris argument at the Hartshorne--Lichtenbaum frontier. Vanishing in top degree for every radical nonmaximal support, together with nonvanishing for maximal support, forces the punct…

Finite Krull dimension gives an actual natural-number dimension, rather than only a WithBot ENat value. We also record the geometric content of a proper radical support being different from the maximal ideal: its closed…

The component-intersection ideals attached to a separation of a principal hypersurface can be pulled back through the quotient map. This gives two proper ideals of the ambient local ring whose intersection is the radical…

For a Noetherian local domain of dimension at least three, no irreducible component of a principal hypersurface is supported only at the closed point. Equivalently, every irreducible component of the quotient spectrum me…

A clopen separation of a punctured principal hypersurface produces two radical nonmaximal component ideals. Their intersection has the radical of the principal support, while their supremum has maximal radical. Principal…

Disconnectedness of the punctured spectrum gives an honest clopen separation. Because the puncture is itself an ambient open subset, both sides lift to ambient open sets. The component reduction then produces the two pro…

A finite partition of the irreducible components of a principal hypersurface gives two finite families of minimal primes. If every component from one family meets every component from the other only at the closed point,…

The component ideals produced by a separation have radical intersection equal to the principal support and radical sum equal to the maximal ideal. This file turns those equalities into the two support identifications use…

An open separation of the puncture of a principal hypersurface assigns every irreducible component to exactly one side. The resulting two finite, nonempty families of minimal primes have all cross-component intersections…

The derived-to-legacy comparison transports the regular-sequence vanishing supplied by Rees' theorem to derived local cohomology. In particular, a regular pair in the maximal ideal kills degree-one derived local cohomolo…

Let W be a finite-etale scheme over the punctured spectrum of a Noetherian local ring. This file constructs the relative normalization of the full local spectrum in the composite morphism from W. The resulting morphism i…

This file studies the generic fibre of a finite-etale cover of a punctured two-dimensional regular local spectrum. The generic fibre is a finite etale algebra over the function field and hence a finite product of finite…

For a complete Noetherian local ring, finite-etale covers of a quotient lift uniquely to the ambient affine spectrum. If restriction from the ambient puncture to the quotient puncture is fully faithful, purity for the qu…

Punctured purity makes the canonical relative function-field normalization finite etale. The normalization comparison with the spectrum of the literal integral closure then transports this scheme-level conclusion back to…

This file compares the canonical function-field normalization attached to a connected punctured cover with an arbitrary finite-etale extension of that cover. Consequently, categorical punctured purity makes the canonical…

An ideal contained in the maximal ideal of a local ring defines a closed subscheme whose unique closed point maps to the closed point of the ambient spectrum. Hence the quotient morphism restricts canonically to the two…

This file connects the explicit regular system carried by a strict-normal- crossings point to complete-local punctured purity. It also records exactly what survives after maximal-adic completion, before any normality the…

For an arbitrary local ring, connectedness of its actual punctured geometric étale stalk makes restriction to the punctured local spectrum fully faithful on finite étale schemes. The finite étale internal Hom turns a mor…

For a finite module whose maximal ideal is not associated, its finitely many associated primes can be included in the primes avoided by an Artinian parameter. The resulting scalar is regular on the finite module and has…

Regularity along the original boundary supplies regularity at precisely the boundary primes of the spectrum of a stalk. The canonical stalk-localization isomorphism makes this transfer without assuming regularity of the…

The punctured spectrum of a regular strictly Henselian local ring of dimension at least two has trivial étale fundamental group at every geometric point. Local purity extends its finite étale covers over the full local s…

An endomorphism of an injective residue-field hull restricts to scalar multiplication on the elements annihilated by an ideal with finite-length quotient. Finite biduality supplies the scalar as a class in that quotient.…

The residue-field image is killed by the maximal ideal. The general preservation of ideal-power torsion under essential extensions therefore makes every vector in an essential extension of that image power torsion. No in…

In an essential extension of the residue field, the elements killed by the maximal ideal form precisely the given residue-field image. Indeed, the cyclic submodule of any such element meets that image; a coefficient outs…

The finite etale internal Hom turns lifting a morphism into extending a section. The constructed global extension applies exactly to the original hypotheses of Stacks 0BSA: retrocompactness, closed complement points, and…

Every missing point is closed, so the original open pulls back to its actual local puncture. Connectedness of the punctured strict stalk gives a local section; retrocompact compatible spreading gives a neighborhood secti…

The quotient by a saturated ideal is canonically the quotient of the original module by its maximal-ideal-primary component. The first isomorphism theorem identifies these actual quotients before the ideal is specialized…

Canonical aggregate for EtaleFundamentalGroups.Purity.SpecialLocal.

For a finite module over a Noetherian ring, a minimal point of its support is an associated prime. Applying this to the two finite cotangent modules turns a minimal point of the non-etale cotangent support into an associ…

For a finite algebra, the image of each target cotangent support is its support after restriction of scalars to the base. Hence a non-etale algebra has a minimal bad point on the base which is the contraction of an actua…

A minimal point of the base cotangent support of a finite domain algebra cannot have height zero when the algebra is etale at its generic point. Consequently its prime localization has positive Krull dimension. This remo…

Let p be minimal in the base support of the two cotangent obstructions for a finite algebra S over R. After localizing both rings at the complement of p, every target prime away from the fibre over the closed point is et…

A finite algebra over a local ring which is etale at every target prime away from the closed point restricts to a finite-etale cover of the punctured spectrum. Applying this to the localization at a minimal base cotangen…

For a module-finite algebra over a Noetherian ring, both relative Kähler differentials and first cotangent homology are finite over the target. The second assertion does not require projectivity of the differential modul…

Canonical aggregate for EtaleFundamentalGroups.Purity.SpecialLocal.DimensionTwo.

For a finite free algebra, formal unramifiedness is detected by the trace discriminant. Over a Noetherian domain, a nonzero element whose image is a unit at every height-one localization is already a unit: otherwise a mi…

Canonical aggregate for EtaleFundamentalGroups.Purity.SpecialLocal.DimensionTwo.IntegralClosure.

The regular-pair freeness theorem can be made input-free in dimension two. A basis of the cotangent space lifts to a regular pair generating the maximal ideal; trace-dual saturation then transports that pair to the finit…

The full root cover used in the height-two Abhyankar argument, after the selected divisor root has also been adjoined, is a regular local ring of dimension two; it is not presented as a prime localization of a larger reg…

For a normalization over a two-dimensional regular local domain, it is enough to assume unramifiedness at the maximal ideals above every height-one prime. The corresponding localized normalization is finite torsion-free…

A finite module over a Noetherian local ring is free when a pair generating the maximal ideal is a regular sequence on the module. Freeness is lifted twice from the residue-field quotient using Module.freequotSMulTopifff…

A regular pair in a domain is nonzero. For a finite normalization in a finite separable field extension, trace-dual saturation makes the same pair regular on the normalization. If the pair generates the maximal ideal, th…

The localization of an integral closure at its zero prime is its fraction field. Identifying that fraction field with the supplied finite separable extension transports formal etaleness back to the literal localization u…

A hypothetical minimal non-étale point belongs to the specified boundary, because the algebra is étale off that boundary. Generic and height-one étaleness force its height to be at least two. Its regular local ring then…

This file isolates the part of special local purity currently supported by the commutative-algebra API. In a faithfully integral extension of domains over an integrally closed base, going-down and incomparability identif…

The regular system of parameters supplied by a strict-normal-crossings chart is a regular sequence generating the maximal ideal of the local ring. This file feeds that actual sequence into the regular-sequence vanishing…

Multiplication by an element outside a prime is injective on every symbolic-power quotient. For a nonmaximal prime in a local ring, choose such an element in the maximal ideal. Its powers detect the vanishing of maximal-…

If R / P has dimension at most one, adjoining an element outside P to an ordinary power of P gives an Artinian quotient. This supplies the coefficient ring for a finite symbolic-power error killed by that element.

For a prime P with dim (R / P) ≤ 1, the image of P^(n) in R / P^n is an Artinian R-module. A common denominator outside P annihilates this image, as does P^n. The image is therefore a finite module over the Artinian quot…

Tensoring every term of a fixed complex defines a functor in the coefficient module. When all its terms are flat, coefficient short exact sequences remain short exact sequences of complexes. Consequently an injective acy…

Vanishing of degree-zero homology after tensoring with ideal quotients makes every map from those quotients into the degree-zero dual lift to degree one. Cofinality then gives surjectivity of the differential on ideal-po…

The tensor--Hom correspondence is linear and natural in the variable complex. Consequently applying linear Hom from a coefficient module to the dual complex agrees with dualizing the complex after tensoring with that coe…

The maximal-ideal-primary component is supported only at the closed point. Positive support dimension supplies a nonclosed point in the support of the coefficient module; this point survives in the quotient. The quotient…

Base change, tensor, trace, product-coordinate, and unramified-diagonal results. Canonical aggregate for EtaleFundamentalGroups.Ramification.

Canonical aggregate for EtaleFundamentalGroups.Ramification.BaseChange.

Equivalent base and target rings do not change ramification indices. These lemmas package the change of local model needed when one divisorial valuation is represented in different scheme stalks.

Canonical aggregate for EtaleFundamentalGroups.Ramification.HeightTwo.

A normalization prime over a height-one divisor remains a prime after localizing at every larger height-two prime, and that localization preserves its ramification index. Combining this with height-two detection of nonun…

Canonical aggregate for EtaleFundamentalGroups.Ramification.Product.

The maximal prime selected by one coordinate of a product has the same ramification index as the maximal ideal in that coordinate. This is the ideal-theoretic transport needed after a completed finite algebra has been de…

Canonical aggregate for EtaleFundamentalGroups.Ramification.Tensor.

Let S / R be finite and let R' / R be flat. A prime of R' ⊗[R] S has two contractions, one to S and one to R'. If the second contraction is the scheme-theoretic extension of the contraction to R, then the two horizontal…

An affine étale neighborhood of the closed geometric point of a local ring is faithfully flat over that ring. The actual evaluation map to the chosen field shows that the image of the maximal ideal remains proper. Togeth…

Finite-étale chosen factors, fraction fields, and filtered descent over strict Henselizations. Canonical aggregate for EtaleFundamentalGroups.StrictHenselian.

The fraction field of the actual geometric etale stalk maps to the complement of an effective Cartier divisor. Its structure map is injective, whereas the stalk ideal of a Cartier divisor contains a regular element. Norm…

At a boundary point with discrete valuation stalk, the inverse image of the Cartier complement in the actual geometric etale stalk is its generic point. The pullback uses the previously constructed generic morphism and t…

The actual strict generic pullback is compared to the iterated pullback via the local fraction field. Etaleness of its normalization is then transported through the actual Cartier square and the normalization-stalk compa…

A finite etale factor with one closed prime becomes the base over a strictly Henselian filtered colimit. Finite presentation then descends the resulting equivalence, together with its inverse equations, to one finite sta…

For a specified prime over the closed point, separable closedness makes the residue-field map bijective. The pointed Henselian theorem then identifies the corresponding localization with the base. Unlike an existence the…

Henselian reduction identifies finite etale covers with those of the residue field. When this field is separably closed its Galois group is trivial. Base-point comparison gives the result at every geometric point, includ…

For an actual geometric point s : Spec Ω ⟶ S, take the filtered colimit of the rings of global sections on all pointed étale neighborhoods of s. The index category and its filteredness come from Scheme.pointEtaleNeighbor…

The real generic-neighborhood algebras retain their existing Under K scalar maps. Compactness over K first supplies an actual pointed neighborhood. A geometric affine refinement then extends that equivalence along its ac…

The structure maps of the pointed étale neighborhoods commute with the actual geometric-stalk germ maps. Thus the defining ring colimit lifts to the category of algebras under the original ring. Restricting along the sma…

Compose each actual field-valued neighborhood point with the given field embedding. The existing colimit descent constructs the map on stalks. Its evaluation and structure-map equations are proved on the original germ ma…

Represent a nonzero germ on an affine étale neighborhood and localize its sections at the prime selected by the geometric point. The resulting ring is Noetherian, and unramifiedness identifies its maximal ideal with the…

A finite family of germs and a relation among them descend to one pointed étale neighborhood. The filtered-colimit equality criterion makes that relation zero on a further neighborhood. Choose an actual affine open neigh…

The actual geometric stalk is a domain, and its local structure map is faithfully flat and injective. Localizing this injection constructs the map between the actual fraction fields and its compatibility with the origina…

For a normal local domain, the generic tensor of its actual geometric stalk is a localization of a domain at nonzero elements. It is integral over the original fraction field, so every nonzero element is a unit. Thus it…

Base-change the already constructed small pointed-neighborhood diagram from R to its actual fraction field K. Its colimit is K ⊗[R] A, where A is the actual geometric stalk. The existing fraction-tensor comparison identi…

Represent a germ on an actual affine étale neighborhood. After base change to a field, that neighborhood's algebra is formally unramified and of finite type, hence finite as a vector space. Its elements are therefore int…

The field map is induced from the actual injection into the geometric stalk. The generic tensor product over the original fraction field is identified with scalar extension directly from the original ring to the actual s…

The ring in GeometricStalk is the actual filtered colimit over pointed étale neighborhoods. A monic polynomial descends to one neighborhood because it has only finitely many coefficients. A simple root at the geometric p…

The previously constructed generic tensor is integral over the base fraction field and is a fraction ring of the actual stalk. Native algebraicity transfer therefore makes the stalk algebraic over the base. The native al…

An étale algebra map to the strict target gives a pointed affine étale neighborhood by reduction. Uniqueness of the actual pointed Henselian lift identifies its section map with that algebra map. Its germ therefore suppl…

Every pointed étale neighborhood lifts uniquely to the Henselian target, including non-affine neighborhoods. Their actual section maps form a cocone, so the defining presheaf-fiber colimit constructs the ring homomorphis…

An endomorphism of the target that preserves the base map and its residue map fixes every actual pointed-neighborhood lift. Naturality of global sections then fixes their section maps, and the defining presheaf-fiber col…

A finite complete orthogonal family in an arbitrary algebra after base change to the actual geometric stalk descends to one actual pointed étale neighborhood. An affine refinement retains the same idempotents and their l…

On an actual pointed étale neighborhood, take the prime ideal given by the kernel of evaluation in the geometric field. Every section outside this ideal has an invertible germ. The universal property of localization ther…

A monic integral equation and the numerator and denominator of a fraction have representatives on one actual pointed étale neighborhood. Clearing the denominator with Polynomial.scaleRoots gives an equality of sections,…

A zero-product relation between two germs descends to an actual pointed étale neighborhood, then to an affine refinement. Localizing its sections at the prime selected by the geometric point gives a domain, by normality…

The maximal ideal of an arbitrary local base ring generates the maximal ideal of its geometric étale stalk. A nonunit germ is represented on an affine pointed étale neighborhood; after localization at the selected prime,…

If the puncture of the actual geometric étale stalk of a local ring is connected, every finite étale section on the original puncture extends uniquely over the original local spectrum. The extension is first built over t…

Evaluation of the constructed stalk in the geometric field is a local homomorphism, so it induces an embedding of its actual residue field into that field. For a monic separable irreducible residue polynomial, lift its c…

Let the geometric field be a separably closed separable algebraic extension of the residue field of a local ring. Every element of that field is a simple root of its minimal polynomial. Lift the coefficients to the local…

Every residue element is represented by an actual affine pointed étale neighborhood. Its selected prime localization has a finite separable residue extension. The existing local germ map sends that residue element to the…

For a geometric point of Spec R given by a ring map φ : R →+ Ω, use the identity étale neighborhood of Spec R. Its germ map, composed with the canonical identification of the sections of Spec R with R, constructs the str…

The local-ring comparison with a strictly Henselian base implies that every prime over its closed point is maximal. Given a maximal ideal containing the prime, localize there. The two primes then have the same contractio…

An equivalence between finitely presented algebras after scalar extension to the actual geometric stalk descends to an actual affine pointed étale neighborhood. Both inverse equations descend through the small filtered a…

Let H be the actual geometric etale stalk of R, and let T be a strictly Henselian local R-algebra. At any prime of T ⊗[R] H over the closed point of T, the map from T to the local ring is an isomorphism. The proof uses a…

The original definition is phrased using the normalization of the reduction. Its canonical normalization map supplies the integral normal extension used in the proved étale-neighborhood and geometric-stalk irreducibility…

The base local ring need not be normal. An injective integral local map to a normal local domain with purely inseparable residue field gives domain local étale neighborhoods. A zero-product relation between actual geomet…

The base local ring need not be reduced. An integral local map to a normal local domain with purely inseparable residue field and nilpotent kernel elements gives irreducible local étale neighborhoods. A nilpotence relati…

In a Noetherian local ring with principal maximal ideal (π), Krull intersection shows that every nonzero element is a unit times a power of π. If π is also a non-zero-divisor, these factorizations imply that the ring is…

The right map is the actual fraction-field pullback map and the left map is induced by the actual geometric-stalk fraction-field homomorphism. Finite étale covers trivialized by the strict generic field extend by their a…

The actual strict henselization preserves the fiber degree. Its integral base change of the original normalization embeds into the actual generic tensor. Lifting the split fiber's idempotents forces that generic tensor t…

Use the existing ordinary henselization maps into the literal normalization localization and original ambient field. The actual decomposition actions are linear over that henselization by its proved universal rigidity. T…

The actual A-to-H-to-L coefficient triangle identifies the composite ordinary generic point with the canonical original fraction point. The induced fundamental-group map sends every original decomposition element to the…

These equalities retain the existing specialization and closed-residue comparison values before a consumer applies a projection or an inverse. Every local, normal, fraction, and residue structure is supplied from the ori…

The proved fixedness of the actual ordinary fraction-field embedding turns each original decomposition automorphism into the same relative field automorphism. The native generic-point scheme morphism then gives the actua…