Scheme theory

Canonical aggregate generated by the reviewed rehome.

Canonical aggregate generated by the reviewed rehome.

This file packages the SGA 1 inertia-group argument prime by prime. The base DVR is neither assumed complete nor henselian. All maximal ideals of the normalization in the compositum are quantified, and the conclusion rec…

Canonical aggregate for EtaleFundamentalGroups.TameRamification.Abhyankar.CyclicInertia.

This file records the finite-level equivariance of the residue-unit inertia character under the decomposition group. In residue characteristic zero the character is faithful, so an element whose residue action inverts th…

The production inertia character embeds tame inertia into the residue field after coprimality kills the wild ramification kernel. This file contains that character argument and the comparison with ideal inertia.

This file constructs the rational cyclotomic automorphism with character -1, transports it to a separable closure of a regular characteristic-zero field, and connects its residue lift to conjugation on finite tame inerti…

An automorphism of a separable closure which inverts roots of unity restricts to every normal separable subextension. The subextension is first embedded in the separable closure and the restricted automorphism is then tr…

For a discrete valuation base, the residue field is the function field of the corresponding prime divisor. This file identifies that field with the intrinsic decomposition residue field of a prime in a finite Galois norm…

This file is the field-valued entry point for the DVR cyclicity theorem. A discrete production ExponentialValuation supplies a discrete valuation ring, so cyclicity follows directly from the valuation-subring theorem in…

The normal residue extension attached to a decomposition group is embedded in a genuine separable closure. Cyclotomic inversion restricts to that normal extension and the residue exact sequence lifts it back to the decom…

For a discrete valuation ring, the value-class source of the production inertia character is cyclic and every decomposition automorphism acts trivially on that source. The lightweight character core then turns coprimalit…

The residue field of a base prime is canonically identified with the intrinsic decomposition residue field after localization. Consequently, geometric integrality stated on the base-prime residue field supplies the finit…

Localization identifies ideal-theoretic inertia in a Dedekind normalization with inertia for the corresponding discrete valuation subring. Finite-level cyclotomic inversion therefore gives conjugacy to inversion directly…

This file contains the orbit-sum argument controlling the wild ramification group. The same field calculation supplies both branches needed by tame inertia: the ramification group is trivial in residue characteristic zer…

Canonical aggregate for EtaleFundamentalGroups.TameRamification.Abhyankar.GroupTheory.

The inertia group of a compositum embeds in the product of the inertia groups of the two factors. This file records the elementary consequence needed to propagate tameness to the compositum.

This file isolates the finite-group calculation in the proof of SGA 1, Expose X, Lemma 3.6. A cyclic group embedded in a product of two cyclic groups has order dividing the order of the second factor when the order of th…

Canonical aggregate for EtaleFundamentalGroups.TameRamification.Abhyankar.Inertia.

An automorphism of a field generated by two intermediate fields is determined by its restrictions to the two fields. This gives the injective map from the inertia group of a compositum to the product of the two lower ine…

This file isolates the group-theoretic tower map used in the proof of SGA 1, Expose X, Lemma 3.6. A valuation subring A of a field E restricts to a valuation subring of every intermediate field M. When M / K is normal, r…

This file combines the ideal-theoretic restriction map with the cyclic group calculation in Abhyankar's lemma. The field-specific construction of the two restriction homomorphisms is deliberately kept separate.

This file compares the ideal-theoretic inertia subgroup attached to a nonzero maximal ideal of a Dedekind normalization with the inertia group of the corresponding valuation subring of the fraction field. The valuation s…

This file compares the decomposition group and residue action attached to a prime of a normalization with the corresponding objects for the localized valuation subring. The comparison is canonical and retains the base-pr…

This file gives the source-level inertia restriction map for a tower of normalizations. It is formulated for equivariant actions on a tower of rings, so it can be instantiated by the integral closures occurring in SGA 1,…

For a finite Galois extension of Dedekind domains, cardinality one of the ideal inertia group forces both ramification index one and separability of the residue extension. Thus it gives mathlib's Algebra.IsUnramifiedAt w…

Canonical aggregate for EtaleFundamentalGroups.TameRamification.Abhyankar.Normalization.

This file combines the two restriction maps from a compositum with the ideal-theoretic cyclic projection argument. The resulting relative inertia group is trivial, and hence the right normalization is unramified in the t…

For a DVR the contraction of every maximal prime in a finite normalization is the unique maximal ideal of the base. Consequently, all residue fields in a normalization tower have the same exponential characteristic as th…

This file instantiates the ideal-theoretic inertia tower for the integral closures of a Dedekind domain in a finite Galois tower of fields.

This file specializes the tame-inertia residue criterion to the integral closures of a Dedekind domain in a finite Galois tower. It supplies the two residue-separability inputs used by the normalization form of Abhyankar…

The inertia group at a prime of a compositum embeds in the product of the two factor inertia groups. Consequently, prime-to-residue-characteristic tameness of both factors propagates to the compositum, prime by prime.

Canonical aggregate for EtaleFundamentalGroups.TameRamification.Abhyankar.Residue.

This file supplies the residue-field step in the SGA 1 form of Abhyankar's lemma. It works at an arbitrary nonzero maximal ideal of a finite Galois extension of Dedekind domains; no completeness or Henselian hypothesis i…

This file records the local commutative-algebra bridge used in the SGA 1 form of Abhyankar's lemma. For a nonzero prime of a Dedekind domain, unramifiedness is exactly separability of the residue-field extension together…

Canonical aggregate generated by the reviewed rehome.

Suppose that the residue characteristic p = char(kappa) is positive. An algebraic valued extension L/K is tamely ramified when its residue extension is separable and [L : T] is prime to p, where T/K is the maximal unrami…

This file develops the primary-reduction calculation used in the trace argument: a monic polynomial whose reduction admits no nontrivial coprime factorization and has a residue root is a pure power of the corresponding l…

For a finite extension of a Henselian valued field, the norm formula says that the extension degree times the value of an element is the value of its norm. Thus the order of every value-group coset divides the field degr…

For a finite tamely ramified extension, the radical-generation theorem describes the extension over its maximal unramified subfield by finitely many radicals of orders prime to the residue characteristic. The definitions…

This file carries out the second concrete step in the tame-generation proof. A representative of each actual value-group coset is corrected first by a base element and then by a principal-unit root. The result has the sa…

This file proves the root-of-unity descent used in the converse and degree calculation for a single prime-to-residue-characteristic radical.

The corrected representatives of all value-group cosets generate an intermediate field with the same value group and residue field as the target. The immediate prime-to-p lemma then identifies that field with the target.

The ramification index is the cardinality of the actual value-group quotient. This file records its multiplicativity in a tower and then applies the one-radical calculation successively.

Canonical aggregate generated by the reviewed rehome.

This file defines tame ramification directly for the ambient valued extension base / target. No proof-irrelevant extension record is introduced: complete and Henselian discretely valued fields use the same definitions th…

Canonical aggregate for TameRamification.Book.

This file constructs the maximal-unramified inclusion and transported radical presentation used by finite tame base change. All dependencies are production CFT and SchemeTheory APIs.

The radical presentation used in the proof of Corollary 7.8 uses the same chosen roots before and after base change. Combining that presentation with the finite-radical value-group theorem identifies the value group of t…

The value group of a nontrivial discrete book exponential valuation is an infinite cyclic additive group. In an infinite cyclic group, two subgroups which generate the whole group have coprime indices. This file records…

This file supplies the finite maximal-unramified and degree identities needed to compare the exponential-valuation presentation with the canonical DVF presentation. It is stated entirely in the production AlgebraicNumber…

The value subgroup of the actual compositum is generated by the two lower value subgroups. Since the target value group is discrete cyclic, the two upper subgroup indices are coprime. Multiplicativity in the two towers t…

The declarations here complete the production radical API: a finite family of prime-to-residue-characteristic radicals over the maximal unramified subextension gives a finite tame extension.

This file lifts the one-radical value-group calculation to the finite radical presentation supplied by Proposition 7.7.

This file supplies the value-group generation source needed for the classical ramification-index form of Abhyankar's lemma. It starts with the group-theory comparison between the order of one value coset and the relative…

This module is an umbrella for the valued-compositum layer. The implementation uses the shared record-free compositum facts and the canonical common-top square arguments. The former one-sided wrapper layers duplicated th…

This module is an umbrella for common-top valued-compositum arguments.

This file contains the ramification-index square, branch divisibility statements, and lower-branch lcm product used by the Abhyankar step. All invariants belong directly to the chosen valued fields; there are no extensio…

Field-degree coprimality supplies the lower ramification-index coprimality used by the common-top branch theorems.

Total tameness converts field-degree coprimality into the lower-index coprimality consumed by the common-top endpoints.

This file exposes the common-top index-one, unramified, and tame endpoints whose inputs are total tameness of the two lower valued extensions.

Prime divisors of a nontrivial common primitive quotient obstruct coprimality of the two upper ramification indices.

The tame Abhyankar lemma is ultimately about the valued extension L K' / K'. Before adding valuation data to that extension, this file records the field-theoretic facts about the compositum L ⊔ K' inside a common ambient…

This is the finite tame-base-change corollary used on the way to Abhyankar's lemma. Starting only with compatibility of the book and CompleteDVF presentations at the original base, it constructs the valuation on the actu…

The geometric input of tame Abhyankar is a source theorem bounding the ramification index after base change by e / gcd e e'. This file proves the arithmetic consequences of that bound. It deliberately does not assert the…

This aggregate collects integer-valued and local-field value groups, norm constructions, and transport of value-group data.

This aggregate collects the common constructions and image of field norms used in the value-group theory of tame ramification.

This file supplies the common-image containments used by the value-group frontier from the concrete tower transitivity of field norms.

This file turns the common-top field-norm lcm divisibility from elementwise form into the subgroup-image form needed by the ramification-image comparison.

The tame Abhyankar value-group step reduces to lcm arithmetic in a rank-one integer value group. This file isolates that arithmetic without assuming any field-theoretic ramification comparison.

This is the umbrella module for the Neu1999 specialization of the tame Abhyankar value-group frontier. The implementation is split into: NAField.Valuation: the normalized integer valuation and norm formula; NAField.Invar…

This file supplies concrete elements of field-norm subgroups coming from base units. It is an element-level source for later ramification-image comparisons.

This file specializes the generic field-norm image lemmas to Neu1999 local fields. It keeps the arbitrary subgroup and generator forms close to the frontier where the actual ramification-image subgroup will be constructe…

This aggregate collects norm-down calculations, primitive and least common multiple cases, and Galois ramification over nonarchimedean local fields.

This file studies the image obtained by applying N{L/K} to the powered embedded-base-unit ramification image. It keeps the common-top norm containment and its valuation generator in a separate source layer.

This file keeps the Galois residue-degree lcm subgroup comparisons for the norm-down ramification image separate from the construction of that image.

This file contains the arithmetic cancellation layer on top of NAField.GaloisNormDown: once the norm-down construction has supplied an lcm divisor, these lemmas extract the primitive residue-degree factor by cancelling t…

This umbrella keeps the Galois ramification image source layer available under the original import path. The implementation is split into: GaloisRamification.Basic: embedded-base-unit subgroups, tower transport, powered…

This file contains the subgroup constructions used by the Neu1999 Galois ramification source: embedded base units, their tower transport, their [M : L]-powered lower image, and the norm-down image in the base field.

This file records the lower local-top residue-degree consequences forced by the powered embedded-base-unit image inside a field-norm subgroup.

This file identifies the exact value images generated by embedded base units and their [M : L]-powered lower-branch images using Neu1999 Galois valuation data.

This file records the field-degree identities for finite Galois extensions whose canonical valuations form an extension. These identities keep the later ramification-image comparison tied to the actual ramification index…

This file exposes the elementary divisibility consequences of the canonical ramification identity e f = [L : K] for finite separable nonarchimedean local-field extensions.

This file extracts concrete residue-degree divisibility from the Neu1999 field-norm value-image comparison.

This file packages the normalized integer valuation from IsNonarchimedeanLocalField as the MultiplicativeIntegerValuation used by the tame Abhyankar value-group layer, and rewrites the Neu1999 norm formula for the field-…

This aggregate collects the common norm constructions for value groups in tame ramification.

This file generates the two lower value-step inclusions used by the transport layer from concrete ValuedNorm.normSubgroup containments.

The common-top value-group comparison needs one transport step: the actual ramification image is a subgroup of a larger common image, while the two lower value-step inclusions are naturally proved for that larger common…

This aggregate collects canonical valued extensions, their residue characteristic, and tower constructions.

For a finite separable extension of complete discretely valued fields, the ambient valued extension is defectless. Consequently tameness is controlled directly by residue separability and the ramification index; no auxil…

This file records the elementary residue-characteristic facts needed for tower and base-change forms of the tame Abhyankar lemma. The key point is that the residue characteristic is unchanged along a valued-field extensi…

Tameness and total tameness propagate through a finite valued tower. The statements use the canonical invariants of ValuedExtension directly, so the same declarations apply to complete and Henselian discretely valued fie…

The actual affinization square commutes with flat affine base change. An open immersion after an affine fpqc base change therefore descends.

This facade collects affine-over-base colimits, affine morphism properties, flat minimal-prime control, and geometric irreducibility of affine schemes.

The local-ring isomorphism induced by the open chart identifies its literal prime localization map with the canonical map from the original stalk.

A disconnection of a scheme produces a nontrivial idempotent global section by gluing the constant sections zero and one. Consequently, a scheme whose ring of global sections is a domain is connected. In particular, a sc…

The two flat global-section pushouts give the actual pushout square for the map of sections induced by a morphism over the base. Surjectivity then descends along the faithfully flat map of section rings.

The qcqs theorem on sections gives an actual pushout square of global sections. Applying Spec and cancelling the affine base square proves that the canonical affinization map commutes with the given base change.

The actual maps on sections form a pushout for a qcqs source and a flat base change. The tensor comparison retains those maps as its scalar owners. The four section rings retain their canonical bundled ring structures. T…

Going down sends a minimal prime of a flat algebra to a minimal prime of the base. Over a domain the base has only the zero minimal prime, so every irreducible component of the affine source dominates the base.

A prescribed point of a localized stalk in an étale chart admits a geometric point over any chosen algebraically closed residue-field extension downstairs. The construction uses the actual residue map of the chart and th…

If a qcqs scheme over a field has exactly the base field as its global sections through the actual structure map, it is geometrically connected. Every extension of the base field is flat, so flat base change preserves th…

An idempotent section is locally zero or one. Its two open pieces transport through a homeomorphism and the constant sections glue there. In particular, an idempotent on a closed fibre lifts to every infinitesimal thicke…

A section on a quasi-compact, quasi-separated open containing a principal open has a global numerator after multiplication by a power of its regular defining section. Two prime parameters then give a global section uniqu…

Two regular parameters suffice to extend sections across their common zero locus. The parameters need not be prime, and the ring need not be a domain.

A non-zero-divisor on an affine scheme remains a non-zero-divisor on the sections of every open subset. This follows by testing at the actual localized stalks and is valid without reducedness or Noetherianity.

The scalar maps here are the actual maps from the rings defining the two affine bases. This comparison is used for residue-field coefficients in proper-family cohomology, where the original field actions must agree.

The ΓSpec conversion is performed in this generic owner. The exported constructor and its equations keep that intermediate section ring out of callers that use the resulting morphism.

For a qcqs morphism whose structure-sheaf map is an isomorphism, flat base change to the spectrum of a target stalk preserves the global-section map as an isomorphism. The section pushout is computed on an affine neighbo…

The canonical map from the spectrum of an arbitrary model of a localization has isomorphic stalk maps. Mathlib contains this for the quotient-type Localization M; the statement below removes that representation choice.

This applies native stability of surjective ring maps to the actual categorical pushout, retaining all four supplied maps.

Canonical aggregate for SchemeTheory.Affine.WeilRestriction.

For a finite free commutative R-algebra A and a finitely presented commutative R-algebra B, this file constructs explicitly an R-algebra representing C ↦ HomR(B, C ⊗[R] A). This is the affine algebra input for the finite…

This file proves that the affine corepresenter constructed in SchemeTheory.Affine.WeilRestriction.Basic is compatible with arbitrary base change and is finite étale when both input algebras are finite étale. These are th…

For finite free A/R and finitely presented B/R, the algebraic Weil restriction represents the relative internal Hom on every scheme over Spec R. The proof extends the affine comparison along the cover-dense affine subsit…

For finite free A/R and finitely presented B/R, the explicit spectrum representing the relative internal Hom commutes with arbitrary affine base change. The comparison is an isomorphism over Spec S, obtained from the alg…

For finite étale R-algebras A and B, with A free as an R-module, the relative internal Hom from Spec A to Spec B is represented by a finite étale scheme over Spec R. The representing equivalence applies to every scheme o…

For finite étale R-algebras A and B, refine the principal open cover carrying local internal Hom representers to a locally directed open cover. Pulling back the local representers gives representations of the restriction…

For finite étale R-algebras A and B, the locally constructed internal Hom schemes glue to a finite étale scheme representing the internal Hom on all schemes over Spec R. The sheaf condition supplies the global representi…

This file promotes the algebraic affine Weil restriction from SchemeTheory.Affine.WeilRestriction.Basic to the corresponding geometric representability statement for affine schemes over Spec R. For finite free A/R and fi…

A finite projective module becomes free after localizing at a suitable element outside any prescribed prime. We express this freeness using tensor products, so that the finite free Weil restriction construction applies.…

For finite étale R-algebras A and B, we construct an open cover of Spec R by spectra of principal localizations. On each member of the cover, the restriction of the fixed global internal Hom presheaf is represented by an…

The local tensor-product construction represents the restriction of one fixed presheaf on schemes over Spec R. The comparison combines geometric base change with the spectrum of a tensor product. This provides the local…

Foundations for algebraic geometry: schemes and morphisms, descent, normalization, finite étale covers, sheaves and cohomology. Includes commutative algebra and Abhyankar's lemma.

This aggregate exposes descent comparisons, module tensor extensions, over-category pullback, and total presheaves over a base.

The coefficient maps are the native maps stored by the commutative algebra objects. The categorical morphism is constructed only after its actual RingHom coefficient square has been proved. No new algebra action is used.

Transport the coherence of actual descent morphisms along component equations, project the existing base-change isomorphism, and compare pullback overlaps using commuting squares. The coherence comes from DescentData.Hom…

Compares native scalar extension with algebra tensors using the given ring homomorphism.

The left-projection pullback functor on over categories is defined together with its object and morphism formulas. A natural isomorphism compares it with the usual over-category pullback functor.

A presheaf on the slice over S determines a presheaf on the original category by collecting its values over all arrows to S. Fibrewise transport relates their representations, and the total presheaf is a sheaf when the s…

Constructs transformations and adjunctions from the corresponding indexing functors and compatible morphisms of ring presheaves.

General scheme-theoretic foundations and their direct child modules.

General scheme-theoretic foundations and their direct child modules.

Finiteness of Cech cohomology is invariant under a cochain equivalence commuting with differentials.

Cech finiteness of the left term of an affine short exact sequence from the other two terms.

Cech finiteness of the middle term of an affine short exact sequence from the other two terms.

Cech finiteness of the right term of an affine short exact sequence from the other two terms.

Cech finiteness by devissage through powers of the vanishing ideal of a supporting closed subset.

Cech finiteness from the corresponding assertion on integral closed subschemes of the support.

Cech finiteness of coherent, quasicoherent module presheaves over a proper scheme.

Cech finiteness for a pushforward is equivalent to finiteness on the preimage cover.

Finiteness of pushforward Cech cohomology by induction on the integral support.

Finiteness of unit-presheaf Cech cohomology for a closed immersion into projective space.

Cech finiteness of the structure presheaf of an integral proper scheme by induction.

Finite ordered affine covers index increasing tuples of charts and their intersections. For a presheaf of modules over the structure sheaf, this file constructs cochains and the alternating restriction differential, and…

An ordered affine cover of an open has increasing-index Cech cochains, alternating restriction differentials, and an augmentation from sections of the structure sheaf.

Cech sections and cohomology of graded modules for projective space. Fraction sections, presentations and maps supply the coordinate-chart complexes.

Monomial sections and Cech cohomology of twists on projective space.

Finiteness of graded-module Cech cohomology from a presentation short exact sequence.

Finite generation of the kernel of a graded module presentation over a noetherian base.

The square of the graded-module Cech differential is zero.

Finite Cech cohomology of a shifted free graded module on projective space.

Finite Cech cohomology of a finitely generated graded module over a noetherian ring.

Finite Cech cohomology of a finite product of shifted free graded modules.

Equivalence between twist Cech cohomology and cohomology of the corresponding shifted free module.

Cech cohomology of a finite product of graded modules is the product of their cohomologies.

The square of the Cech differential for a twist on projective space is zero.

Finiteness of twist cohomology on projective space through the monomial Cech complex.

The augmentation from sections on an open into the degree-zero Cech cochains of its ordered affine cover is injective.

For a separated structure morphism and an affine open, the positive-degree Cech complex of an ordered affine cover of the open is exact.

Sections on an open are exactly the degree-zero cochains whose Cech differential vanishes. The increasing-index construction is compared with the finite-subset description.

Two affine charts with affine intersection, their section-ring cover and its scalar extension.

This file defines algebraic chart covers and their section modules, the Cech difference, its kernel and cokernel, and their comparison maps under scalar extension. It also defines two-term models whose kernel and cokerne…

General scheme-theoretic foundations and their direct child modules.

Finite free two-term complexes, their fibre dimensions and the canonical kernel base-change map.

Double complexes, their two spectral-sequence pages and bounded convergence data.

Basic constructions on module presheaves, including kernels, cokernels, products and restrictions.

Morphisms of module presheaves, their affine sections and short exact sequences.

Filtration of a module presheaf by powers of an ideal and the resulting quotient presheaves.

The Leray bicomplex of a module presheaf for two ordered affine covers.

The double-complex structure, augmentations and total cohomology of the Leray bicomplex.

The vertical differential vanishes on the bicomplex augmentation.

A short exact sequence from the Chow devissage construction for a module presheaf.

A morphism from the degree-zero relative cohomology presheaf to the total-cohomology presheaf.

Coherence of the relative cohomology presheaf in the Chow construction.

Quasicoherence of the relative cohomology presheaf in the Chow construction.

Identification of the first Leray spectral-sequence page with Cech cohomology of relative cohomology.

Identification of Leray total cohomology with cohomology on the preimage cover.

Identification of relative cohomology sections on an affine open with fibre-cover Cech cohomology.

Exactness of the Leray bicomplex rows for a quasicoherent module presheaf.

Support of the relative cohomology presheaf arising from the Chow construction.

The composite of successive Cech differentials is zero for a module presheaf.

Generic freeness of quasicoherent module-presheaf sections on an integral scheme.

The Rees algebra and proper Čech finiteness give a uniform loss of ideal power when replacing a zero-cochain by one with the same coboundary.

A sufficiently high ideal power annihilates a coherent module presheaf supported on its vanishing locus.

Devissage of coherent quasicoherent module presheaves supported on a closed subset.

Coherence of the cokernel of a morphism of module presheaves.

Coherence of quotients of a coherent module presheaf by ideal powers.

Quasicoherence of the cokernel of a morphism of quasicoherent module presheaves.

Quasicoherence of quotients of a quasicoherent module presheaf by ideal powers.

Support of a module-presheaf quotient by an ideal power.

An action of the cover groupoid on a scheme over the cover gives an actual isomorphism between the two overlap pullbacks. Its inverse is obtained by exchanging the two cover coordinates and applying the same action. The…

We transport an action across the equality between a composite structure map and its affine coordinate map. The resulting overlap isomorphism, its two base coordinates, and its diagonal restriction are expressed in tenso…

The two affine overlap schemes have coordinate rings C ⊗[R] B and B ⊗[R] C. An isomorphism between them over Spec (B ⊗[R] B) determines an actual algebra equivalence by the full faithfulness of Spec. Its linearity follow…

+# Compatible stalk spreading through an affine chart We base-change the actual target to a finite-component affine neighborhood, transport the given section through the chart's actual stalk map, and apply affine compati…

The geometric action law is an equality of maps from an actual iterated pullback. Tensor-product coordinates identify it with coassociativity. Together with the overlap square over the tensor-square base, this supplies t…

Apply the native Spec limit-preservation theorem to the actual small finite-FP ring-model colimit. The resulting scheme diagram has its genuine maps to the original affine base, with finite and locally finitely presented…

A finite collection of recovered identities holds at one common tail stage. The source and target models may vary with the equation. This is the finite equation supplier needed for the inverse and triple-cocycle identiti…

For a cofiltered diagram of qcqs schemes with affine transition maps, a morphism between two base-changed models descends to an actual stage. The source model is qcqs over the base and the target is locally of finite pre…

First descend each map, then project its target to the fixed original model. Transport these projected maps along a finite cofiltered cone and reconstruct the maps between stage pullbacks. This retains every original rec…

A global section descends to a stage, and its idempotency equation holds at a further stage. Both the section and the equation are actually constructed.

A map into the vertex of a scheme cone gives compatible scheme-theoretic images at every stage. The image transition maps are constructed by the closed-immersion kernel factorization, and preserve affine transitions.

Sections on affine preimages descend to an actual ambient stage. This detects the kernel of a quasi-compact morphism from its stage kernels and supplies the universal property of the corresponding scheme-theoretic image…

The comparison is built from the chosen scheme pullbacks. Its components preserve both projections, and their naturality is proved by those projections. No limiting or cofilteredness hypothesis is needed.

The diagonal and triple objects used in scheme gluing are finite etale over compact overlaps, rather than over the whole ambient stage. Their structural maps to that stage are quasi-compact and locally of finite type. Th…

The real qcqs/LFP scheme Hom supplier is transported through pullback symmetry. Recovery uses the native cone comparison, with both projection equations proved from the chosen pullbacks. This applies to raw gluing overla…

An overlap isomorphism is written as C ⊗[R] B ≃ₐ[B] B ⊗[R] C. Its diagonal normalization is an equality after the two multiplication maps. Its triple cocycle compares two explicit maps from C ⊗[R] (B ⊗[R] B) to B ⊗[R] (B…

A concrete scalar-extension equivalence gives a concrete coaction. Its two laws follow from the pure-tensor formula for the canonical coaction. These are the upper coactions used when descending a finite radicial local m…

The algebra equalizer is constructed from the actual Amitsur module equalizer. A map into a scalar extension descends when its values are fixed by the canonical coaction. If its scalar extension is bijective, faithful fl…

+# Spreading a stalk section compatibly with an existing open section For a separated etale target over an affine scheme with finitely many irreducible components, a stalk section which agrees with an existing open secti…

Ordinary tensor descent data give an actual invariant subalgebra. Its spectrum is the descended scheme: the original scheme is its pullback along the cover, and finite étaleness descends to this scheme. The comparison us…

This Nyll lemma computes the forward map of pi1's equalizer scalar comparison. The comparison itself and its upstream notices remain in the imported Pi1 module.

The actual map from the scalar extension of the invariant subalgebra intertwines the canonical scalar-extension coaction and the given coaction. This identity already holds without flatness or the coaction laws. For genu…

Finitely generated subalgebras, their inclusion diagram and its affine inverse-limit construction.

For a faithfully flat ring map, an algebra coaction satisfying the usual counit and coassociativity equations descends to its equalizer subalgebra. The actual map from the base change of that subalgebra is an isomorphism…

An fpqc cover detects whether a morphism of schemes is a coequalizer, provided the asserted coequalizer property holds both over every member of the cover and over every pairwise overlap. This is Stacks Project, Tag 0BMN…

Suppose an actual algebra coaction over a faithfully flat cover becomes the transported canonical coaction of an actual upper algebra after extending scalars. The invariant algebra then has that upper algebra as its scal…

A ring map to a local ring factors through localization at the contracted maximal ideal. The residue fiber of a scheme over the stage is unchanged by this localization. These actual maps compare sections lifted at the lo…

A closed subscheme of the base change of a proper scheme over a Noetherian ring is recovered as the limit of its actual images over finitely generated subalgebras. Every image is proper over its actual Noetherian stage r…

An idempotent on the original fiber descends to an actual Noetherian image stage. Localizing that stage at the contracted closed point permits the Noetherian proper-section theorem to lift it. Pullback of that section gi…

The fibers of the actual stage images over the contracted primes form an inverse system. Its limit is the actual fiber of the original closed subscheme. The three limits used here are supplied by the image construction,…

A specified isomorphism of finite étale covers over the part of an actual local spectrum lying in a retrocompact open descends to the intersection with an actual open neighborhood. The original local isomorphism is retai…

Base change the actual stalk inverse system by a retrocompact open. Its stages are quasi-compact and quasi-separated. Finite-presentation Hom descent then spreads the given morphism to the overlap with an actual neighbor…

An actual model over an étale covering algebra acquires its canonical upper coaction from its scalar-extension equivalence. Universal-homeomorphism invariance of algebra maps descends this map. The same injectivity detec…

We base-change the actual target to a chosen affine neighborhood, transport the given section through the chart's actual stalk map, and apply affine compatible spreading. The resulting section and its overlap equation ar…

The disagreement locus is clopen in the overlap with an affine neighborhood. Retrocompactness of the original open makes that locus compact. Stalk compatibility excludes every generization of the chosen point from this c…

+# Spreading a stalk morphism with finitely presented target The actual stalk is the colimit of the rings of sections over its open neighborhoods. Applying Spec gives an affine inverse system. A morphism from this limit…

The actual affine-neighborhood stalk is identified by its canonical stalk isomorphism. Finite-presentation spreading on that affine neighborhood then produces a morphism on an actual open of the original scheme, with the…

The generator of the ideal on an affine chart identifies the actual inverse image of the support complement with a principal open. The resulting map from the principal localization forms a pullback square with that compl…

Canonical aggregate for scheme-theoretic divisors.

This file records the scheme-theoretic data used to state boundary conditions over an integral base, directly on the closed subschemes defined by irreducible components. The condition uses local Noetherianity rather than…

This file develops the finite-etale stability of the arithmetic boundary conditions. It first records the topological fact that a closed generalizing map sends every irreducible component onto an irreducible component. A…

This file supplies scheme-theoretic boundary data using Scheme.IdealSheafData. The stalk ideal is constructed canonically as the supremum of the images of the ideal on affine neighbourhoods. Effective Cartier and normal-…

The pullback ideal of a locally principal non-zero-divisor remains locally principal and is generated by the image of that non-zero-divisor. Flatness preserves its regularity.

The generic point of an irreducible boundary component specializes to each point on that component. Pulling the closed prime of the generic stalk back along the corresponding generization map gives the canonical branch p…

The complement of an effective Cartier divisor is dense, without a reducedness hypothesis. A dense open subset of a connected space is connected if every point of its complement admits an irreducible open neighborhood. F…

Pulling back a reduced component of the base produces an actual finite étale cover. A component of the original source lifts to a closed component in that pullback. Domain stalks make this lifted component open, which pr…

Domain stalks make irreducible components open on a locally Noetherian scheme. For a reduced scheme, the reduced closed component then coincides with that open subscheme. In particular its inclusion is both finite and ét…

This file proves that regularity of local rings ascends along the local ring maps induced by etale morphisms. Consequently, regularity along the support of an ideal sheaf is preserved after etale pullback.

Every irreducible component of the pullback of a horizontal boundary maps onto an irreducible component downstairs. Consequently its composite with the structural morphism has dense range. The statement is made directly…

This file constructs the induced morphism between the reduced closed subschemes carried by irreducible components. It also supplies the reverse component-lifting statement for surjective closed generalizing maps.

This file identifies the complement of the support of an ideal sheaf near a scheme point. If the stalk ideal becomes principal after localizing at a prime, the resulting open subscheme is canonically the spectrum of the…

This file relates the support of an ideal sheaf near a scheme point to prime ideals of its local ring. It contains the point-level bridge used when a codimension-two localization is selected inside a local ramification a…

The height-two strict-normal-crossings geometric input. Canonical aggregate for SchemeTheory.Divisors.NormalCrossings.

This file fixes the lightweight local-algebra data used by the one-point inertia theorem. The chart is a proposition, not a typeclass or a structure, so merely carrying it does not enlarge instance search. The boundary c…

A height-one prime containing a split normal-crossings equation is exactly one of the labelled branch ideals. This identifies a geometric divisorial prime with the branch index required by the local Kummer theorem.

Canonical aggregate for SchemeTheory.Divisors.NormalCrossings.HeightTwo.

At a height-two point containing a selected branch, at most one further labelled branch can pass through the point. Every other boundary parameter becomes a unit after localization. Consequently the localized boundary eq…

If a height-two prime contains two distinct labelled branches of a split strict-normal-crossings chart, those two branch equations form a regular system of parameters after localization at that prime. The proof first mov…

A height-two prime contains at most two members of a regular system of parameters. Applied to the labelled part of a split strict-normal-crossings chart, this gives the exact dichotomy needed by the local Abhyankar const…

A branch of a strict normal crossings divisor stays a regular parameter after localization at every height-two point on that branch. The key input is the scheme-level regularity of the branch quotient. Quotienting after…

The explicit local chart is invariant under a change of ring model by an isomorphism. This is used to pass between a scheme stalk and the canonical prime-localization model of the same local ring.

An ideal sheaf is radical exactly when its associated closed subscheme is reduced. This is checked on the canonical affine cover by the quotients Spec (Γ(X, U) / I(U)).

The closed subscheme of a pulled-back ideal sheaf is the corresponding scheme-theoretic fibre product. An etale morphism over a locally Noetherian reduced base has reduced source, so radical boundary ideals remain radica…

The reduced closed subscheme carried by an irreducible component is integral. Its generic point maps to the canonical generic point of the chosen component. These facts let later local-chart constructions select the corr…

A regular effective Cartier divisor in a locally Noetherian scheme forces the ambient local rings along its support to be regular. The proof uses the actual quotient description of the divisor's stalk and the regularity…

The vanishing ideal of an irreducible closed set defines an integral subscheme with that closed set as its support.

The local normality theorem for smooth morphisms supplies the domain stalks needed to identify reduced irreducible components as finite étale covers.

This is the one-localization counterpart of LocalComplement: the actual spectrum of the stalk localized away from a generator maps to the global support complement, and the canonical maps form a pullback square.

The kernel of the stalk map of a closed immersion is the stalk ideal of its defining ideal sheaf. Thus the actual local ring of a closed subscheme is the quotient of the ambient local ring by its stalk ideal. The compari…

This file distinguishes surjectivity of every boundary component from the weaker condition that every component merely dominates the base. Over the integer base, componentwise surjectivity supplies a point of every prime…

The canonical tensor-product spectrum isomorphism identifies the structure map, so properties of the scheme pullback give properties of the tensor algebra with its canonical scalar action. Prime localization then gives e…

Start with the original integral morphism and its existing local lifts. On an affine base chart, its actual map on sections supplies the integral algebra. The literal source section spectrum maps to the actual pullback t…

An affine étale scheme over a closed subscheme of an affine scheme lifts to an affine étale scheme over the ambient scheme. We apply the shared algebraic lifting theorem to the actual maps on global sections and use the…

The integral refinement of a surjective étale cover over an affine base has an affine source. Its actual isoSpec and the native Spec.preimage map supply the integral algebra to which finite-FP local-factor descent applie…

The existing affine finite-presentation descent produces a finite stage with an actual map to the original integral algebra. Taking that map's image produces a finite subalgebra of the original algebra. Its spectrum inhe…

For an étale map between spectra, one natural number bounds the actual carrier of every pullback to the spectrum of a separably closed field. The field and its map to the base are chosen after the bound. The proof uses t…

A Zariski-local factorization of the actual integral affine limit map through a locally finitely presented morphism descends to one of its finite-FP stages. The finite affine cover and its local maps are descended using…

The canonical Scheme.Spec.residueFieldIso intertwines the scheme residue map of Spec.map f with Ideal.ResidueField.map. This allows the purely inseparable residue extensions constructed at tensor-product primes to be use…

Realize the separable closure of the base residue field inside the selected residue field in an étale neighborhood. Evaluation into the selected residue field defines a prime of the tensor product. The induced residue ma…

The closed fibre after a local base change is the base change of the original closed fibre along the canonical residue-field map. When the extended maximal ideal is the new maximal ideal, it is also the base change of th…

Two maps from a closed subscheme into an unramified scheme, equal at a chosen point, become equal after an étale refinement of the ambient scheme through which the point lifts. We pull back the open diagonal to form thei…

Choose an affine open in the ambient scheme containing the image of the point, then an affine open in the restricted étale neighborhood. The affine lifting theorem supplies an ambient étale scheme; the pullback pasting i…

An étale cover of a quasi-compact scheme has a finite affine refinement by open subschemes of its members. Collapsing this finite cover to its disjoint union gives a single surjective étale morphism with affine source. T…

An algebraically closed geometric fiber of a finite morphism is Artinian. The correspondence between rational points and closed points therefore constructs every geometric lift and proves that the set of lifts is finite.…

A neighborhood containing a fiber of a closed morphism contains the inverse image of a neighborhood on the base. Applied to the isomorphism neighborhood of a finite étale morphism, this constructs a section over a neighb…

The chosen-residue-extension construction supplies pure inseparability over the bottom ring, rather than over the intervening finite radicial algebra. The residue-field tower transfers this property to the étale morphism…

First choose an étale extension of the bottom ring that removes the separable part of the selected residue extension. The quasi-finite structure theorem then constructs a finite open factor with singleton fiber. Its actu…

Choose a splitting étale neighborhood upstairs using the finite étale algebra splitting theorem. The finite radicial section theorem constructs a map to that neighborhood after an étale base change downstairs. An affine…

The pointwise splitting neighborhoods over the lower ring form an open cover of its spectrum. Compactness selects finitely many of them. Their product is faithfully flat over the lower ring, and the finite powers of the…

Start with the original surjective étale morphism. Its integral refinement supplies both the actual integral cover and its local factorizations. On finitely many affine base charts, finite subalgebras inside its actual d…

An étale morphism with quasi-compact source has a uniform finite bound on all actual geometric fibers. The target is arbitrary. The proof uses the native affine refinement of the pullback of an affine target cover, then…

For a separated étale morphism, a finite set of distinct points in one geometric fiber gives equally many distinct points in every nearby geometric fiber. The conclusion is an actual injection; no finiteness or cardinali…

An arbitrary field-valued point over the closed point of a strictly local spectrum extends uniquely to an étale section. The residue-field point lifts by Henselianity. Its section is an open immersion; its image contains…

A rational point of the closed fiber of an arbitrary étale scheme over a Henselian local ring lifts to a section. An affine open neighborhood of the point reduces this statement to étale algebra section lifting over a He…

This file proves the integral-refinement assertion of Stacks Project, Tag 09Z0, by induction on the actual uniform geometric-fiber bound. The recursive refinement is produced by the strict degree decrease of the normaliz…

The rank-one locus of a finite flat finitely presented morphism is open, and the restriction to it is an isomorphism. For an étale morphism, a singleton fiber with unchanged residue field is an isomorphism: the residue-f…

Pull back the existing neighborhoods and their actual lifts, then use the native pullback universal property. In particular the original integral refinement's local factorizations remain available on every affine chart o…

Local lifts through a base-changed target map to lifts through the original target by the pullback projection. Local lifts on open-cover charts become local lifts on the glued source by taking their actual open images. N…

A finite separable extension of the residue field of a Noetherian local ring is realized by localizing an actual etale neighborhood at its supplied prime. The resulting ring is Noetherian and faithfully flat over the ori…

+# The largest open extension of an etale section A section over a dense open into a separated etale target has a largest open domain of extension. We glue all local sections that agree with the given section on their ov…

For a quasi-compact separated étale morphism f : U ⟶ X, Zariski's main theorem embeds U as an open subscheme of its relative normalization Y. The graph of this embedding in U ×[X] Y is both open and closed. Its complemen…

A supplied uniform finite bound on the geometric fibers of a separated quasi-compact étale morphism strictly decreases on its actual normalization remainder. Over the dense normalization image the residual fiber omits th…

Canonical aggregate for SchemeTheory.Etale.OverField.

This file supplies the coproduct-fiber step used internally for Stacks Project, Tag 03QR. A morphism from a connected scheme to a coproduct factors through a unique summand, so its morphism set is the dependent sum of th…

This file proves the geometric decomposition used in the first half of Stacks Project, Tag 02GL: a scheme étale over a field is a coproduct of spectra of finite separable field extensions.

For a universally closed scheme over a local spectrum, an étale morphism is surjective exactly when its base change to the closed fiber is surjective. The open image of the étale morphism contains the entire closed fiber…

The finite factor is constructed by the quasi-finite local structure theorem. Its selected tensor prime inherits pure inseparability under base change, and localization induces an isomorphism on the selected residue fiel…

For an actual prime of a tensor product, pure inseparability at its image in the original algebra implies pure inseparability over the new base. The proof uses the uniqueness of field embeddings and the two generators of…

A common denominator rescales a primitive element so that its minimal polynomial lifts to a monic polynomial over the original ring. Inverting its derivative gives a standard étale algebra. The kernel of evaluation at th…

When the extended maximal ideal is the maximal ideal of the target, the actual square of the ring map and the two residue maps is a pushout. The universal factorization is the quotient lift of the given map from the targ…

A section of the base-changed étale morphism is an open immersion. The homeomorphism on the total spaces carries its image to an open subscheme of the original étale scheme. The projection of this open subscheme is étale…

Canonical aggregate for scheme-theoretic fiber comparisons.

The inclusion of a scheme-theoretic fibre is surjective on stalks and hence does not change residue fields. For a dominant morphism of integral schemes, the generic point of the generic fibre maps to the generic point of…

This file identifies finite étale covers of an affine scheme with finite étale algebras. Under this identification, the contravariance of Spec accounts for the opposite category on the scheme side.

A nil ideal defines a Henselian pair. Thus finite étale covers are unchanged by its quotient. Factoring a surjective ring map through its kernel quotient, and an affine closed immersion through a quotient spectrum, gives…

The inverse images of an affine open at an original stage form an actual affine inverse system. Descend each finite-etale chart cover through its global-sections colimit, then use a finite cofiltered wide cospan to put a…

Starting with one cover of the inverse limit, restrict it to a finite affine stage cover and construct all local finite-etale models at one later stage. The restricted cone maps are proved cartesian, so the recovery maps…

The global-sections cocone of the actual affine limit is colimiting. Descend the cover through that ring cocone and transfer it back with isoSpec and the canonical pullback-composition isomorphisms. Recovery is along the…

Restrict a recovered local model to any smaller base open. The literal inclusions commute with the restricted cone maps, so native pullback composition transports its given recovery to the restriction of the same origina…

The constructed finite étale algebra model gives essential surjectivity of the actual tensor-product functor. The affine comparison carries this result to scheme pullback. Together with universal-homeomorphism full faith…

An actual finite subalgebra model for a finite étale algebra over an integral extension also retains surjectivity and universal injectivity of the base map. The larger integral algebra surjects onto this intermediate spe…

A finite étale cover of an open subscheme is the restriction of its affinization once that affinization is an open immersion and its section algebra is finite étale. Density of the canonical affinization and properness o…

The differentials vanish after every maximal localization of the base, because the actual tensor algebra there is étale. Localization detects vanishing, and finite projectivity supplies flatness and finite presentation.

For a surjective map R₀ → R and an étale R-algebra S, we construct an étale R₀-algebra whose base change is S. The construction uses mathlib's relative-dimension-zero submersive presentation, lifts its polynomial coeffic…

An algebra map from an étale algebra to a quotient of the base factors canonically through reduction by the extended ideal. The resulting map is surjective and induces an open immersion on spectra. Thus it supplies an ac…

A finite etale algebra splits over an etale neighbourhood of a prescribed prime.

The equalizer algebra constructed by faithfully flat descent is itself finite étale when the algebra carrying the coaction is finite étale. The comparison with its scalar extension is the actual invariant-subalgebra map,…

First construct a finite étale model over a finitely generated coefficient ring. This ring is finitely presented over the initial ring, so its actual map to the colimit factors through a stage. Scalar extension of the mo…

Finitely many monic equations over an arbitrary scalar extension use only finitely many coefficients. Flatness ensures that those equations already hold after adjoining their coefficients. In particular, this constructio…

A maximal quotient of the actual finite faithfully flat splitting algebra is a finite separable field extension and still splits the original algebra. The construction also applies to the zero algebra.

A finite étale algebra over R ⊗[k] L, for an algebraic extension L/k, descends to R ⊗[k] F for an actual finite intermediate field F. We reuse the integral finite-model construction and ValuedFieldTheory's finite-coeffic…

The geometric-fibre algebra in the proper-family argument is finite étale: after extending the field to an algebraic closure it is a finite product of fields, and étaleness descends along the field extension.

The lower spectrum has an actual finite affine étale splitting cover. The product of its split local models has a concrete scalar-extension comparison with the given upper algebra. Its transported coaction descends uniqu…

The coordinate idempotents of a finite split algebra form a basis. If their preimages and the scalar coefficient preimages exist, every element has an explicitly constructed preimage. For proper H⁰, the idempotents are l…

An actual étale model is supplied by Mathlib's Noetherian descent theorem. Its coefficient ring is enlarged by the monic equations needed for module finiteness. Both properties therefore hold on the same model, with the…

Formal smoothness gives existence of lifts across nilpotent ideals, while formal unramifiedness gives uniqueness. This file combines the two halves for formally étale algebras and records the resulting rigidity of two ni…

Reduction is faithful by unramified rigidity, full by lifting the idempotent of a graph, and essentially surjective by extracting a finite factor of an étale lift. These constructions prove the equivalence for the canoni…

An étale algebra over A need not be an algebra over the target S. Base change to S and the native AlgHom.liftEquiv reduce existence to the existing Henselian section theorem. The existing Jacobson rigidity theorem suppli…

A section over the quotient selects an integral idempotent factor of the étale algebra. This factor is finite étale, and its special fiber is generated by the base. The section makes its structural map injective on the s…

A map on the special fiber defines a section of the tensor product over the target algebra. The kernel of its reduction is generated by an idempotent. Lifting the complementary idempotent over the original Henselian base…

First lift the étale presentation. Its finite special fiber selects a factor of the integral closure on a principal neighborhood. Lift the corresponding idempotent using the Henselian pair, and transport its factor throu…

The quotient imposing e = 1 for an idempotent e is localization at e. Consequently, an idempotent factor of an étale algebra is again étale over the original base, with the canonical quotient algebra structure.

An étale algebra has a model over a finitely generated subalgebra of its base. When the base is integral and the original algebra is finite, the model is finite too: flatness embeds it into the scalar extension, where in…

The upper algebra first descends to an actual finite intermediate universal homeomorphism. Finite radicial descent then constructs its model over the original ring. The tensor-product associator supplies the comparison w…

An integral algebra carries an ideal in the base Jacobson radical into its own Jacobson radical. Unramified rigidity then makes reduction injective on algebra maps. Transporting through the quotient/tensor comparison pro…

Reduction modulo an ideal in the Jacobson radical reflects isomorphisms of finite étale algebras. Nakayama first gives surjectivity. The kernel is then a finitely generated idempotent ideal in the Jacobson radical, so it…

The separability element of an essentially finite type unramified algebra annihilates the difference between two algebra maps. If the maps agree modulo an ideal in the Jacobson radical, the image of that element is a uni…

A finite étale algebra with a section over a Jacobson quotient is the base algebra if its reduction is generated by base scalars. The section makes the reduced scalar map injective, and finite étale conservativity lifts…

Étaleness on the closed fibre kills the residue-field extension of the finite module of differentials. Nakayama kills the original differentials. Finite projectivity supplies flatness and finite presentation.

Formal etaleness makes morphisms lift uniquely across nilpotent thickenings. Using the canonical identification (R ⧸ I) ⊗[R] B ≃ B ⧸ I B, this gives full faithfulness of finite-etale base change along a nilpotent quotien…

For an integral algebra over the base, every point in a normal local ring's fraction field has a unique factorization through that ring. This uses its normal self-integral-closure structure, not integrality of the local…

Maps out of an essentially finite type unramified algebra into a local ring are determined by congruence modulo its maximal ideal. Localizing a domain at a prime applies that criterion to endomorphisms agreeing modulo th…

The interchange map identifies the two concrete orders of scalar extension. Its formulas retain the actual coefficient maps used for descent.

An algebra section of a finite étale algebra cuts out an idempotent factor isomorphic to the base. The complementary factor is an actual quotient by the complementary idempotent, and remains finite étale. The product iso…

For an étale algebra A and an arbitrary algebra B, every map from A to the scalar extension of B descends uniquely through an affine universal homeomorphism. The source spectrum for this lifting problem is arbitrary; in…

This facade collects affine Weil restriction, fpqc descent for finite étale algebras, exactness of the forgetful functor, and étale schemes over a field.

The chosen Tag factor and the root-refined normalization factor are related by an algebra equivalence. This file records the formal transport needed to keep the literal Away map while changing between those two carriers.…

Canonical aggregate for SchemeTheory.FiniteEtale.Away.

If the distinguished element is already a unit in the target, the target Away localization is isomorphic to the original target. This file records the corresponding descent of etaleness and its target-local application.

The boundary Away property is stable under a genuinely etale extension of the target. This elementary map-level statement is useful after a Tag/ETag comparison has produced the primitive Away map on one local factor and…

The complement hypothesis on a finite normalization is stated using the literal map between two away localizations. This file transports that map through a pushout. The proof pastes the original pushout with the four can…

These scheme-level formulas are shared by geometric descent and pointed fundamental-group comparison. They retain the actual chosen pullbacks.

The identity comparison uses the first projection of the chosen pullback. Its compatibility with a cone leg is proved by those actual projections.

For a point of a scheme-theoretic pullback, the pullback carrier API gives a canonical map from the tensor product of the two residue fields to the residue field of the point. When that tensor product is Artinian, this m…

If one projected residue field is finite over the common residue field, its tensor product with the other projected residue field is finite-dimensional over that other field. The categorical tensor in the pullback-carrie…

This file replaces the categorical pushout in the pullback-carrier API by the ordinary tensor product and records the two factor maps. The resulting map is surjective as soon as the categorical residue tensor is Artinian…

A clopen subset is represented by its characteristic section of the trivial cover with two sheets. Fullness descends that section, without any hypothesis that arbitrary finite étale covers descend. Lifting inclusions of…

A clopen subscheme is a subterminal finite étale scheme. An equivalence on finite étale schemes lifts this object and detects its subterminality, so its lift is again a clopen subscheme. Fullness also detects containment…

The actual descent of finite etale sections supplies fullness through the finite etale internal Hom. Surjectivity of a geometrically connected map supplies faithfulness. Neither source nor target is assumed connected.

An open surjection with connected fibres descends every clopen subset. Applied to the image of a section of a finite etale cover after base change, this constructs a clopen subscheme of the original cover. Its degree is…

Let R be a discrete valuation ring with fraction field K. For an arbitrary finite étale cover of Spec K, take the finite étale coordinate algebra supplied by the affine equivalence. If all its actual field factors are un…

Finite étale morphisms are open, so the projection from their pullback along a dominant map is still dominant. Two arrows between finite étale schemes which agree on that pullback agree globally: their relative equalizer…

The actual finite-etale algebra model over a stage is transferred across the existing affine equivalence. Its native base-change comparison yields recovery along the literal Spec map of the given cocone component.

Canonical aggregate for SchemeTheory.FiniteEtale.Forget.

This file proves the coequalizer-preservation part of Stacks Project, Tag 0BNA, for the canonical forgetful functors from finite étale schemes.

This file proves the finite-coproduct part of Stacks Project, Tag 0BNA, directly for the canonical forgetful functor from finite étale schemes.

This file records the limit-preservation part of Stacks Project, Tag 0BNA, directly for the canonical forgetful functor from finite étale schemes.

The actual finite etale internal Hom represents a morphism after base change by a section. Descending that section and evaluating it gives the original morphism. This supplies a shared proof for geometric and Henselian s…

Canonical aggregate for SchemeTheory.FiniteEtale.Henselian.

Canonical aggregate for SchemeTheory.FiniteEtale.Henselian.ChosenFactor.

Tag 00UJ isolates a finite idempotent factor with a unique prime over the chosen closed point. Once local purity has made that factor étale, the uniqueness makes the factor local. Faithful flatness is then produced from…

A finite etale factor with a unique closed prime over a strictly Henselian base is canonically the base ring. The induced equivalence of fraction fields is therefore the existing scalar map from the fraction field of the…

The strict-Henselian chosen-factor argument does not depend on the base and factor carriers living in the same universe. This file records the universe-polymorphic form needed when the factor is a localization of an inte…

A prime-local factor of an etale algebra over a Henselian local ring is finite over the base. The proof uses the finite idempotent factor furnished by Tag 00UJ and trivializes its pointed etale neighbourhood by Hensel's…

An arbitrary localization of an etale algebra need not be finite over the original base. For the localization at a prime over the closed point of a Henselian local ring, Tag 00UJ supplies finiteness. Flatness then makes…

An etale neighborhood of a Henselian local ring is trivial at a chosen point when that point has the same residue field as the base. The algebra need not be module-finite: standard-etale structure near the point supplies…

A finite etale local algebra over a Henselian local ring is the base ring as soon as its residue-field map is bijective. This is the pointed form of the usual strict-Henselian splitting argument: instead of assuming that…

The connected splitting step in the strict-Henselian part of Abhyankar's lemma reduces to the following affine statement: a finite étale local algebra over a Henselian local ring with separably closed residue field is th…

Equality after pullback to the actual inverse limit is detected by a genuine later stage. The maps in the conclusion are the native finite-etale pullback maps, so the result applies directly to inverse and cocycle equati…

Choose a finite affine cover of one quasi-compact original stage and descend the restrictions of the given finite-etale cover of the limit. This produces all chart models and their recovery isomorphisms at one common sta…

Recovered chart maps prove the diagonal and triple equations after the actual limit projection. Eventual equality then proves all of these relations at one common original stage. Limit projections need not be faithful, f…

Translate the actual scheme Hom descent through pullback symmetry and retain the canonical pullback-composition comparison. The output is a morphism in the native finite-etale category with its categorical recovery equat…

An isomorphism between the pullbacks of two finite-etale models descends to an actual isomorphism at a later stage. The comparison with the given map is retained under the literal native pullback-composition isomorphism.

Combine actual Hom descent, eventual invertibility, and pullback-composition coherence. The resulting isomorphism recovers the originally supplied map.

Native Hom descent supplies an inverse map, and native eventual equality makes both inverse equations hold at a common actual stage. No projection is assumed faithfully flat, surjective, or faithful on finite-etale cover…

Starting with the original finite-etale object over an actual inverse limit, construct a finite affine stage cover and recovered local models. Actual morphism descent and eventual gluing equations then give a global fini…

Compact stage opens, including pairwise and triple intersections of affine charts in a quasi-separated scheme, give actual quasi-compact restricted inverse systems. A finite family of equations over different such opens…

For a finite collection of compact opens, isomorphisms between limit pullbacks of finite-etale models all descend to the same original stage. Each overlap is treated over its own restricted inverse system; no cover of an…

The finite affine chart models already constructed from the original cover are transported through their proved cartesian chart squares to the literal Over.pullback charts. This supplies exactly the recovery data consume…

The finite family of recovered overlap transitions descends by the real qcqs scheme Hom theorem. The descended local models retain their literal cartesian overlaps and their covering maps into the original object. Eventu…

All finiteness properties and gluing relations are proved from finite-etale local models and their actual recovered chart overlaps. The resulting scheme is finite etale over an original later stage, and its literal nativ…

Canonical aggregate for SchemeTheory.FiniteEtale.Local.

For an algebra of finite presentation, formal etaleness at every prime of the target is equivalent to global etaleness. This file records that implication in forms convenient for literal ring maps: it is enough to check…

Every finite étale morphism becomes a finite disjoint union of copies of the base on an étale cover. The cover is constructed from the local algebraic splitting theorem, first on affine schemes and then on an affine open…

The ascending chain condition on opens gives a maximal open over which a given finite étale cover extends. This is maximal among extensions, without assuming uniqueness of extensions or compatibility between unrelated on…

The canonical affine presentation and the native spectrum algebra-hom equivalence identify points with algebra maps on sections over any base ring. The comparison is natural and respects actual point automorphisms.

Over any local ring, finite étale morphisms on a proper scheme are determined by their restriction to the closed fibre. The proof uses the actual relative equalizer, which is open and closed, and the existing proper clos…

The clopen image of a section on the closed fibre lifts to a clopen subscheme of the finite etale cover. Its projection is an isomorphism because it is an isomorphism on the closed fibre. The original FLT section constru…

Over a locally Noetherian reduced base, morphisms between finite-etale covers are determined after pullback along a quasi-compact scheme-theoretically dominant morphism. The proof uses reducedness of the source cover, se…

Postcomposition with a monomorphism is fully faithful on slice categories. The unit of its pullback adjunction is therefore invertible. Restricting a representation of T ↦ Hom(i⁎ T, V) to the smaller slice recovers V by…

The threefold fiber product is viewed as two copies of X ×[Y] X with their first coordinates identified. Its small diagonal is the composite of two diagonals. Both are surjective closed immersions for a separated univers…

The diagonal of a separated universally injective morphism is a surjective closed immersion. Its fully faithful pullback therefore lifts the canonical comparison between the two iterated pullbacks to a unique natural iso…

The local models are finite etale over affine charts. Their raw overlaps are open subschemes of affine models, and are compact because the original base is quasi-separated. Their ambient maps are locally finitely present…

The range and open-immersion lifting arguments below adapt Christian Merten's RelativeGluingData.preimagetoBaseeqrangeι and RelativeGluingData.isPullbacknatTransιtoBase from Mathlib: https://github.com/leanprover-communi…

Finite-etale models over compact open charts have compact pairwise and triple overlap objects. Their maps to the ambient quasi-separated base are quasi-compact and locally of finite type; they are not asserted to be fini…

The gluing relations proved at a later inverse-system stage give actual scheme gluing data. Its local structure morphisms are base changes of the original finite-etale maps; their cartesian overlap squares construct a fi…

The book's condition S = R[z] is recorded by the existence of a power basis. The Galois condition is stated for the induced extension of fraction fields.

The algebra of global sections descends as an actual finite étale algebra when it is finite étale after faithfully flat affine base change. The comparison is the pushout of the four actual maps on sections.

A morphism from a nonempty connected scheme into a finite étale scheme over a strictly Henselian local ring factors uniquely through a global section. In particular a section on a connected punctured spectrum extends uni…

Affine lifting supplies local maps on the directed cover by affine opens. Affine uniqueness makes these maps compatible, so they glue to a unique global map. In particular, pullback along any surjective closed immersion…

Local finite étale lifts represent the same presheaf of maps after pullback. Their universal elements therefore supply compatible transition maps and cartesian squares on the directed affine cover. Gluing these local rep…

An isomorphism over the actual intersection glues two finite étale covers. The glued scheme is the pushout of their open overlap; the Cartesian squares over the two base opens prove that its structural morphism is finite…

Étale sections descend along integral, universally injective, surjective morphisms. Applying section descent after pullback by the source object gives fullness. Relative maps into a separated unramified scheme are determ…

This facade collects functoriality for dominant morphisms, function-field transcendence, valuation-theoretic prime divisors and their counting theorems, together with ring covers of domains.

A field tensor product with the algebraic closure of the rationals makes the corresponding base change of the generic point integral. Scheme-theoretic dominance transports this to the whole scheme. Smoothness and field d…

A morphism with dense image between integral schemes sends the generic point to the generic point. Its map on local rings therefore gives the canonical embedding of function fields.

This file proves that passing from a geometrically integral domain over a field to its fraction field preserves geometric integrality. It then applies this ring-theoretic fact to the function field of an integral scheme.

The integer base of a scheme in universe u is represented by Spec (ULift.{u} ℤ). This file identifies its generic residue field with ULift.{u} ℚ, and hence with ℚ. All auxiliary algebra structures are local to the defini…

This aggregate exposes centered prime divisors, degree and counting comparisons, integral-closure primes, divisors at infinity, and transport across function-field maps.

This file introduces the model-independent form of a prime divisor used in Fried--Jarden, Chapter 6. The underlying discrete K-valuation of F is represented by a valuation subring of F which is a discrete valuation ring,…

This file supplies the monic-projection form of Fried--Jarden, Lemma 6.2.2(b).

Coordinate-ring equivalences transport rational points and centered prime divisors. Applied to the monic representative of a plane equation, this removes the literal monicity assumption from the separable-projection form…

A prime divisor finite on a Dedekind model has a nonzero prime center, and that center determines the divisor. Thus prime divisors whose centers lie over a fixed base prime inject into the set of primes over that base pr…

This file identifies a prime divisor of a fraction field which is finite on a Dedekind model with the height-one prime at its center. In particular, the center is automatically nonzero and determines the valuation subrin…

This file formalizes Fried--Jarden, Lemma 6.2.2(c), for an arbitrary map from an affine plane-curve coordinate ring into a function field. Finiteness at a prime divisor gives a residue map on the coordinate ring. When th…

This file develops the valuation-theoretic input for Fried--Jarden, Lemma 6.2.2(d). If t is a transcendental function, a prime divisor which is not finite on K[t] is finite on K[t⁻¹], and its center there is the unique c…

The normalization-finiteness theorem used in the separable proofs of Fried--Jarden 6.2.2(b),(d) need only be applied to the maximal separable subextension. A valuation subring of the full field is determined by its restr…

A valuation ring is integrally closed in its fraction field. Consequently, if a prime divisor is finite on a model A, it is finite on the integral closure of A in the ambient field. This is the bridge from an affine coor…

The fundamental equality between ramification indices, inertia degrees, and the rank of a finite flat extension immediately bounds the number of primes above a fixed prime. This file records that consequence in a form co…

A K-algebra equivalence of function fields transports valuation subrings, discrete K-valuations, residue fields, and hence Fried--Jarden prime divisors. This is the model-independent bridge needed to replace a plane equa…

Canonical aggregate for field-theoretic constructions.

A field extension K / k is regular in the geometric sense when Spec K → Spec k is geometrically integral. This file derives the linear disjointness with a separable closure directly from that geometric condition, then ob…

For a tower of fields k ⊆ K ⊆ Ω, every K-automorphism of Ω restricts to the separable closure of k inside Ω. When Ω is a separable closure of K, this restriction map is surjective provided that K and the separable closur…

An injective map out of an integral scheme's stalk gives a dominant morphism from the spectrum of its target back to the scheme. The induced function-field map restricts to the original ring map on that stalk.

The canonical map on function fields commutes with every stalk map, not only with global sections. For an open immersion it therefore identifies the actual local-ring subrings. This supplies the local equations needed wh…

This aggregate exposes the valuation comparisons for purely inseparable function-field extensions.

Let E / F be a purely inseparable extension of fields. Membership in a valuation subring of E can be tested after raising an element to a positive power. A sufficiently large exponential-characteristic power of every ele…

General scheme gluing and recovery.

Changing the base-change functor along a specified natural isomorphism preserves the recovered open cover, its cartesian structure squares, and the actual pairwise recovery equations.

The actual overlap isomorphism and its compatibility with the functor comparison transport both projections of the recovered cartesian square.

Actual recovered local charts and overlap maps after arbitrary base change.

The canonical recovered transition identifies the two chart overlaps inside the original recovered scheme. The cartesian assertion follows from the already proved chart squares and transition projection equations.

Local comparison maps that cover the target and identify pairwise overlaps produce the comparison isomorphism from the glued scheme.

Base change of local models and their actual overlaps retains the chart structure morphisms, finite-etaleness, and cartesian overlap squares. Any transition morphism over the new base then preserves the second chart stru…

Actual cartesian pairwise overlaps produce triple transition maps. After an arbitrary base change, monic recovered chart maps prove the diagonal and triple equations. No faithfulness or surjectivity of the base change is…

Once the diagonal and triple relations have been proved after a base change, the transported cartesian overlap maps form actual scheme gluing data. The triple comparison construction adapts GlueData.mapGlueData: https://…

The native pullback of the glued model and the original scheme have the same recovered charts and actual overlaps. Common-cover recovery therefore produces an isomorphism over the limit base, retaining the actual structu…

General scheme-theoretic foundations and their direct child modules.

Finiteness in the zero row of the second page of a convergent double complex.

The bounded spectral sequence and its filtration for a double complex.

Canonical aggregate for SchemeTheory.LocalGeometry.

Every generization of a missing point, other than that point itself, lies in the original open. Its pullback to the actual local spectrum is therefore the punctured spectrum, without finiteness assumptions on X.

The proof takes a finite constructible-open cover of the compact open set by complements of compact open neighborhoods of the specified point.

On a locally Noetherian scheme with domain stalks, irreducible components are open and closed. Connectedness therefore forces one component to be the whole scheme, and reducedness follows directly from the stalks.

An etale morphism induces a formally etale, essentially finite type map on stalks. These properties persist after localizing the target stalk at an arbitrary prime. The resulting map need not be etale: prime localization…

+# The stalk puncture at a generic point of an open complement At a generic point of an irreducible component of the complement of an open subscheme, the pullback of the open to the actual stalk spectrum is exactly the p…

This aggregate exposes boundary-prime dichotomies, localizations, normal local discrete valuation rings, and principal DVR comparisons.

If a boundary equation is associated to a prime parameter, every height-one prime either is that parameter divisor or lies on its complement. If the boundary is associated to a prime parameter times a power of a second p…

This file supplies the commutative-algebra entry point needed to apply the existing DVR form of Abhyankar's lemma to a boundary component. The hypotheses describe geometric source data: a regular affine domain and a codi…

A height-one localization of a Noetherian integrally closed domain is a one-dimensional normal Noetherian local domain, hence a DVR. This is the form needed for height-one primes in finite normalizations; no regularity o…

A local domain of Krull dimension at most one whose nonzero maximal ideal is principal is a discrete valuation ring. The usual DVR TFAE in mathlib assumes Noetherianity. Here Noetherianity is a conclusion rather than an…

This aggregate exposes nonunit localizations, regular parameters, and residue-characteristic comparisons at height two.

Let t generate a prime divisor in a Noetherian local domain. If a positive integer e is nonzero but noninvertible modulo t, then a minimal prime over (t, e) has height exactly two. At that prime, e remains a nonunit. Thi…

In a two-dimensional regular local ring, an element whose cotangent class is nonzero can be completed to a minimal pair of generators of the maximal ideal. If the prescribed element is prime, the resulting pair is a regu…

An integer which is a nonunit in a prime localization vanishes in its residue field. For a prime integer this determines the residue characteristic. We also record the canonical map from a localized branch quotient to th…

Representable open charts for a sheaf determine scheme gluing data. The glued scheme represents the sheaf through the universe-lifted Yoneda functor, with the chart maps giving the local comparison and the induced Yoneda…

A representable restriction supplies a chart of the total presheaf. Its pointwise factorization and pullback properties make this chart a relative open immersion.

The fraction field of a DVR is its localization away from any uniformizer. Consequently its spectrum is the actual open complement of the closed point. The resulting scheme isomorphism retains the canonical map to the fu…

This module supplies the canonical open complement of the closed point and its basic nonemptiness criterion.

The inverse image of a nonempty punctured local spectrum is dense under any flat morphism. For a point over the closed point, flat going-down lifts the generalization from a chosen puncture point. Every remaining point i…

Canonical aggregate for SchemeTheory.LocalGeometry.RegularLocal.

In dimension one every nonzero prime of a local domain is maximal. Thus a one-dimensional regular local domain is regular at all of its primes without using the missing general theorem that arbitrary regular local rings…

This file supplies the algebraic fact needed by finite local root covers: a Noetherian local ring admitting a regular sequence which generates its maximal ideal is a domain, and every member of that regular system is pri…

For a smooth morphism to an affine scheme whose global section ring is a domain and integrally closed, every source stalk has these properties. The proof uses the smooth algebra on an affine source chart and its prime lo…

+# A neighborhood dominated by the actual local spectrum When a scheme has finitely many irreducible components, deleting the components which miss a given point gives an open neighborhood dominated by its actual stalk s…

This extracts the finite-cover kernel bound and compact-open gluing argument from the attributed source above. The same induction now uses powers of a natural endomorphism of an abelian sheaf. Scalar multiplication is su…

The canonical spectrum of the affine chart supplies finite extraction on the compact overlap. Its actual inclusion is transported back along the affine isomorphism and extended by the kernel of the quotient direct image.…

A submodule of the affine global-section module gives an actual morphism from its tilde sheaf to the ambient module by the native tilde--Gamma adjunction. Its native image is a sheaf submodule. The unit identity proves t…

Starting with an actual quasicoherent native submodule, extract finitely many global numerator sections using the existing finite localization theorem. Their actual affine tilde morphism has full range on the specified p…

An actual quasicoherent submodule which is finite type on a quasi-compact open contains a globally finite-type quasicoherent submodule with the same restriction to that open. Compactness supplies finitely many principal…

Tensor base change for sections over affine opens.

Surjectivity on global sections of a morphism into a quasicoherent module over a spectrum implies that the actual sheaf morphism is epimorphic. The proof uses the native tilde--Gamma counit and preservation of epimorphis…

Surjectivity on an affine open gives an epimorphism on its native slice site when the target is quasicoherent. The proof first uses the actual canonical spectrum of the affine open, then transports through restriction an…

The original quasicoherent restriction map identifies the canonical localized module with the actual sections on a principal open. The canonical localization ring is identified with its actual section ring. These proved…

For an affine open with affine inverse image, extending sections of an invertible module gives the sections of its pullback, with the prescribed unit formula.

For an actual affine morphism, pull back the base's affine locally directed cover. The pullback charts are identified with the literal spectra of the sections on the inverse-image opens. Their natural isomorphism transpo…

Naturality and the tilde--Gamma unit identify the concrete section map with localization of the original submodule inclusion. The existing localization-of-ranges theorem then computes its actual range on every principal…

Canonical aggregate for SchemeTheory.Modules.

The ring sheaf is the native pushforward of the structure sheaf and its structure morphism is the original morphism's sheaf map. Its underlying module is identified with the native direct image of the unit module, using…

The unit sheaf is the one-generator free sheaf. Affine pushforward preserves its quasicoherence, and the actual direct-image algebra/module comparison identifies the resulting module with the algebra's underlying module.

For each selected affine open, finitely many actual section generators are included in the actual quotient-kernel extension of their finite free image. The proved finite-type extension theorem replaces this by a global f…

The literal finite free sheaf epimorphism becomes a map from a finite free module under the fully faithful tilde functor. The actual quasicoherent counit isomorphism identifies its target with the original global section…

The finite free image on an open subscheme is inserted into the actual quotient-kernel construction. Its restriction is the original image, so the extension is finite type on that open and contains the original specified…

The original sections on an open are transported to the top of that open subscheme by the native restriction comparison. The finite free image construction produces an actual quasicoherent finite-type local submodule, an…

The native sheaf-lattice join is identified with the actual image of the map from the coproduct. The proof uses the least-submodule property of the image and both original inclusions. No pointwise-sum description of the…

The input is an actual sheaf of commutative rings and its structure map from the structure sheaf. Its underlying module is obtained by the existing restriction-of-scalars functor. Quasicoherence of that native module sup…

A family of actual global sections defines a morphism from the free sheaf through freeHomEquiv. Its native image contains the given sections. For a finite family the source is finite type and quasicoherent, so the image…

The compact-open induction adds one affine chart at a time. Its invariant is an actual global quasicoherent submodule, finite type on the prescribed open together with all charts already added, and unchanged on that pres…

The two actual submodules are glued on the union of their prescribed opens. The native quasicoherent extension construction then produces a global representative with both exact restrictions and finite type on the union.…

The actual local finite generators restrict to every subordinate affine open. Their free epimorphisms yield finite section modules there. Basic opens subordinate to the given generator cover span the unit ideal of an aff…

The product of the two original local generating covers is again a cover. On each product chart both finite generating families restrict, and their disjoint union generates the actual categorical coproduct.

The actual equivalence between an iterated slice and the slice over its underlying object transports the local finite generating families. All site, ring and module structures here use the native slice projections. The c…

The finite-type hypothesis concerns the original module restricted to the given open. The proved site-equivalence transport puts it on that actual open subscheme. Its affine-section finiteness is transported back with th…

The native finite-type condition is preserved under isomorphisms and can be checked on a covering family. The proof composes the actual covers and transports the actual finite families of generating sections through the…

Cover lifting and the actual maps of generating sections transport finite type through continuous and cocontinuous functors. This supplies the iterated-slice and subopen restrictions needed for gluing on a union. The cov…

The original local generating covers are retained. Restriction to a slice is a left adjoint, so the actual restricted morphisms are epimorphisms; their images of the original finite generators generate the quotient.

The covering of a restriction consists of objects mapping both to the chosen slice object and to a member of the original generating cover. Each finite family is transported along the actual restriction functor.

The native site-equivalence coefficient isomorphisms transport the actual finite local generating families in both directions. These comparisons connect slice-site finite type with the geometric restriction functor.

Restriction to a smaller open is obtained within the larger slice site, then transported by the actual equivalence of iterated slice sites.

Choose actual finite module generators, and use the native tilde presentation with exactly this generating set. Its relation module is allowed to be infinite. Restricting the finite family of generators to the slice site…

The singleton family consisting of the top open covers every open. The existing finite-type locality theorem therefore recovers global finite type from the actual top-slice module used by the open induction.

Flat base change for sections via finite affine covers and their overlaps.

A frame of an invertible module sheaf descends to an open neighborhood when its pullback is a frame at a point.

A trivialization on an open subscheme gives compatible local generators and a section that is a frame on that open.

Multiplication by a fixed global section is bijective on every open when it is bijective on a suitable neighbourhood of each point.

Local frames for scheme modules and their restrictions.

An inclusion of an actual chart subalgebra into the generated section ring gives its literal Spec map. The map commutes with the actual coefficient maps, so the subalgebra's local lifts pull back to the generated chart.…

Both input module restrictions are the actual sheaf restriction maps. Their quasicoherence supplies their localizations. The generated-algebra localization theorem then establishes the affine diagram's cartesian property…

Given an actual sheaf of commutative algebras and a submodule of its underlying module presheaf, generate the section subring from the structure coefficients and the given submodule sections. Restriction is the literal a…

The inclusion of the actual generated section rings induces a map of the literal spectrum diagrams. The previously proved colimit with vertex the original affine-morphism source gives the scheme morphism. Its composite w…

The section algebra is generated inside the given integral ambient algebra. Finitely generated module sections therefore give finite section algebras. The native cartesian affine charts of the previously constructed glui…

Transports the section-localization results through the existing global coefficient modules.

The image is the native kernel submodule of the actual cokernel projection. Its comparison with the abelian image gives an epimorphic corestriction, and the categorical image universal property gives its least-submodule…

If a morphism into a prescribed native submodule becomes epimorphic on an open, the image of its composite into the ambient sheaf restricts to that exact prescribed submodule. The reverse inclusion is constructed by the…

Natural linear families are identified with a subpresheaf of the ordinary presheaf Hom. When the target module presheaf is a sheaf, this description proves that the internal-Hom module presheaf is also a sheaf.

Invertible scheme modules and the canonical pullback of the unit module.

The kernel is the native submodule consisting, on each object, of the sections killed by the actual component morphism. Membership is local by separatedness of the target sheaf. Evaluation identifies its kernel fork with…

The native kernel submodule and the geometric kernel have the same actual inclusion. Transporting that comparison along open restriction gives the embedded geometric restriction isomorphism needed for affine extraction a…

The native sectionwise kernel subsheaf is transported through the identity-action equivalence with the category of scheme modules. The comparison with the actual categorical kernel respects the inclusion into the origina…

Constructs localization from the actual invertibility, fraction and kernel criteria.

Preserves the actual localized-module property under the prescribed coefficient ring map.

Local trivializations transfer scalar localization to module sections. A finite basic-open refinement then glues numerators and annihilates restriction kernels.

Module sheafification transfers the tensor product and its unit from module presheaves to module sheaves. The reflective adjunction supplies the monoidal closed structure. The file also defines the resulting tensor, dual…

Keeps section opens, rings and modules in their existing categorical objects.

Uses the existing section rings and modules to represent their actual restriction maps.

The unit is bijective on sections over opens contained in the image of the immersion.

The internal Hom is constructed from families of linear maps compatible with restriction. Currying and uncurrying give the tensor-left adjunction, and hence the monoidal closed structure on module presheaves over a presh…

Restriction of scalars, free module presheaves, and free representables provide the tensor and unit comparisons for module-presheaf pullback. Preservation of finite products on the base category makes these pullback comp…

A projective presentation describes a module as a quotient of a finite sum of twists of the structure sheaf. Pullbacks and tensor powers of twists retain these presentations.

Base change of a projective presentation by pulling back its presenting sections and morphism. The chart ratios and pullback square give the compatibility of the resulting presentation.

Faithfully flat descent of projective presentations.

Pullback preserves the property that multiplication by a section gives a bijection on sections over every open subset of a prescribed open.

The adjunction unit pulls sections back to inverse-image opens, compatibly with module operations, restriction maps, morphisms, and the counit.

Pullback on module presheaves descends through module sheafification to a monoidal functor on module sheaves. Its tensor and unit comparison isomorphisms identify pullbacks of tensor products and structure modules with t…

The unit for a composite scheme morphism agrees with the successive units after the canonical pullback composition comparison.

Constructs the prescribed coefficient maps to global and local sections and compares them.

Proves localization of pushforward sections for a quasicoherent module along a quasi-compact open immersion into an affine scheme. This gives quasicoherence of the direct image.

The comparison uses the actual preimage-open equality and native scheme restriction maps. The former AlgebraicCurves owner reexports this shared owner.

Compares the existing section modules through the prescribed coefficient and restriction maps.

Relates the actual basic-open restriction maps to their elementwise localization clauses.

On an affine scheme, the actual morphism is transported through its canonical tilde isomorphisms. The existing tilde adjunction preserves its cokernel. Restriction and the shared affine-presentation criterion then give t…

On each affine chart the tilde adjunction carries the coproduct of the two section modules to the actual sheaf coproduct. Restriction preserves this coproduct, so the affine criterion gives global quasicoherence.

For a monomorphism φ : G ⟶ F|U, the extension is the actual kernel of F ⟶ jcoker φ. The restriction adjunction identifies this kernel over U with G, and the identification respects the given inclusion in F|U. This is the…

The identity-action equivalence transports the actual kernel and cokernel theorems for scheme modules to native sheaves. The native image is then the actual kernel of the actual cokernel projection.

The section functor preserves the actual categorical kernel. Its canonical comparison with the ordinary linear-map kernel commutes with restrictions. Localization of kernels therefore proves quasicoherence, without assum…

Restriction preserves the actual categorical kernel. Affine kernel quasicoherence supplies the hypotheses of the shared affine-presentation criterion, which constructs the global quasicoherent data.

The affine tilde presentation is transported to the open subscheme and then through the native equivalence with the slice site. These genuine local presentations form quasicoherent data on the canonical affine open cover…

The affine-target theorem is transported from the actual Spec theorem through isoSpec. The arbitrary-target theorem uses the actual open-restriction comparison on each affine target open, then the native affine-cover cri…

The input and restriction use the actual sectionwise submodules on the slice site. The kernel of the map to the direct image of the quotient extends the input, and the embedded restriction isomorphism gives equality of t…

Uses abelian-presheaf gluing to prove localization for the actual module restrictions.

The graded section-ring condition identifies degree n with global sections of the nth tensor power. The direct-sum construction in SectionRingConstruction satisfies these compatibilities without an assumed section-ring w…

The direct sum of tensor-power global sections is embedded into products of polynomial rings using local frames. The injective coefficient map supplies the ring laws, and the natural summand ranges supply the grading. No…

The structure-presheaf map and section algebra induced by a morphism to an affine scheme.

SectionsGluing for scheme modules.

Glue compatible local numerators and bound the powers that annihilate restriction kernels to obtain localization on an affine open from a finite basic-open cover.

For a locally bijective morphism of ring presheaves, the module-presheaf morphisms whose underlying additive presheaf maps are sheafification equivalences form a monoidal morphism property. The proof uses the internal-Ho…

SpanningFrameDescent for scheme modules.

Containment of the actual restricted submodules is local on an open cover. The proof uses the native membership locality axiom on the intersections of each test open with the cover. This turns the finite principal-open e…

An actual morphism commuting with the native inclusions gives pointwise containment. An actual isomorphism commuting with the inclusions therefore gives equality of the original native submodules. In particular, the embe…

The construction imposes membership in a given native submodule only on objects mapping to a specified object of the site. Intersecting two such submodules glues their prescribed local values when those values agree on t…

Actual finite-type submodules on the two covering slice sites glue to a finite-type submodule. The finite-type proof uses only their generating families; it imposes no finite-presentation or Noetherian hypothesis.

Restriction of a native submodule to the slice site is computed on its actual section submodules. The local section equalities of glueOn thus identify its restrictions with the two given quasicoherent modules. The native…

The two actual opens cover their union in its slice site. Consequently, the actual glued submodule restricts to a finite-type quasicoherent module on that union whenever the prescribed local submodules have those propert…

Equality on a slice gives equality of every actual section submodule below that slice. It is therefore inherited by smaller slices, and the native gluing has the exact prescribed restrictions on both opens.

The top-section restriction comparison is natural in the actual module. A lift through the restricted inclusion therefore gives an element of the original native section submodule. This supplies the containment step afte…

The comparison is built from the actual sectionwise restriction of the submodule and the canonical slice-to-open equivalence. Its inclusion identity lets geometric restriction isomorphisms give literal equality of the na…

The module of the top submodule is canonically the ambient module. If an actual native submodule equals the whole module on a slice, the geometric restriction of its inclusion is an isomorphism: each actual section map i…

The presheaf tensor comparison carries tensor products of generators to frames.

Tensor powers add under tensor product, transport along an isomorphism, and commute with pullback. Each comparison is constructed recursively from the monoidal structure.

Tensor powers start at the unit, adjoin one tensor factor at a time, and carry the canonical degree-one comparison.

The formula is proved through the monoidal sheafification adjunction and naturality.

The components of a tensor product of module morphisms act separately on the two factors of a local tensor section.

The monoidal sheafification comparison carries the tensor of two unit images to the unit image of their presheaf tensor.

Local tensor sections and their iterated powers are compatible with restrictions and module operations; frames characterize sections freely generating smaller opens.

For a qcqs morphism to an affine scheme, an isomorphism on global sections extends to an isomorphism of the structure sheaf with its pushforward. Flat base change supplies the assertion on affine opens, and the sheaf bas…

This facade collects the finite, flat, smooth, rank, reduced-etale, and closed-immersion lemmas used by the finite étale and fundamental-group developments.

Segre embeddings and projective Chow data for proper schemes.

Construction of Chow data from finite affine covers of proper integral schemes.

Set-theoretic containment suffices: the pullback is a surjective closed immersion into the reduced source, hence an isomorphism. In particular this applies to points valued in any field, without an algebraic closure hypo…

The range of a pullback projection is the inverse image of the range of the other morphism. Since an open map pulls dense sets back to dense sets, base change along an open morphism preserves dominance.

If the second map of a factorization is etale, its graph is an open immersion into the base change of the composite. Flatness, local finite presentation, and geometric reducedness of the composite therefore hold for the…

The diagonal of an étale morphism is an open immersion. Universal injectivity makes it surjective and hence an isomorphism. The morphism is therefore a monomorphism, and the flat finite-presentation criterion makes it an…

An etale algebra over a field is reduced, because it is essentially of finite type and formally unramified. Applying this on an affine cover after an arbitrary field-valued base change shows that every etale morphism is…

For finite flat morphisms, the literal scheme-theoretic fiber has the rank of the original morphism at the chosen point. Over an integral base, finite presentation makes this rank equal to the rank on any specified actua…

If a separated étale morphism becomes integral after precomposition with a surjective morphism, it is universally closed. It is consequently proper and locally quasi-finite, hence finite by Zariski's main theorem.

A finite etale morphism has reduced fibres after every field extension. A finite etale cover of a geometrically reduced family of finite type is therefore geometrically reduced over the original base. No Noetherian condi…

The relative normalization of a universally closed qcqs morphism agrees with affinization over an affine base. The flat base-change theorem for sections therefore gives the cartesian square for the native normalization m…

This file records a descent criterion for geometric integrality over a field. The morphism used for descent need not be flat: quasicompact scheme-theoretic dominance is enough, since it remains scheme-theoretically domin…

Geometric integrality is recovered from a pullback over a field extension. The argument combines faithful flat descent of reducedness with the geometric irreducibility comparison.

A geometrically irreducible morphism has connected fibres after every field base change.

An irreducible scheme over an algebraically closed field remains irreducible after extension of the base field. Affine algebra arguments and local affine charts supply the comparison.

Over a Noetherian ring, every idempotent section on a closed base change of a proper scheme is the restriction of an actual global section. The lift need not be idempotent. Its existence follows from the already construc…

For a quasi-finite separated morphism of finite type, Zariski's main theorem embeds its source into its relative normalization. After arbitrary base change, an open subscheme finite over the new base is both open and clo…

For a universally closed qcqs morphism, the native normalization comparison is an isomorphism after flat base change between affine bases. The proof compares the two actual pushout squares on global sections, using the s…

The section isomorphisms above affine opens of the original base imply the full structure-sheaf pushforward assertion for the native relative normalization, with no affine or Noetherian hypothesis on the base.

An open immersion restricts to an isomorphism over any open contained in its image. For spectra, the canonical comparison with principal localization then proves bijectivity of the actual localized ring map. This applies…

The literal map R / I → S / I S is the base change of a ring map R → S. Its pushout square is obtained from the tensor-product pushout and the canonical quotient/tensor-product equivalence. Consequently its spectrum is a…

The scheme-theoretic closed fibre is identified with its actual closed subset in the proper total space. The spectral closed-restriction theorem then lifts each clopen subset. No Noetherian hypothesis is required.

For every irreducible closed subset, its actual reduced induced subscheme is integral and proper over the base. Applying connectedness to that scheme supplies the point-closure condition in Stacks 09ZG. The existing spec…

Every sheaf of sets on the underlying space of an arbitrary proper scheme over a henselian local ring has the same global sections on its actual closed fiber. The map is the unit of the topological inverse-image adjuncti…

The actual integral projective Chow cover embeds in the base change of projective space over the integers. Its closed-fiber idempotents descend to the actual Noetherian image stages and lift to global sections. The globa…

Universal closedness makes the actual global-section algebra integral over the base. When the total space is integral and the base is henselian local, the section ring is therefore henselian local, without a finiteness o…

The canonical relative normalization of a universally closed qcqs morphism has the same sections as the source above every affine open of the base. Over an affine base this identifies the actual normalization with the sp…

A formally unramified morphism locally of finite type is locally quasi-finite.

The map between the two diagonal objects induced by a surjective morphism is surjective. Thus surjectivity of the diagonal of a composite implies surjectivity of the diagonal of its second factor.

If a scheme endomorphism fixes a point and its induced residue-field map is the canonical identification at that same point, naturality identifies its composite with the actual canonical residue-field point morphism. Con…

For an arbitrary small family of morphisms, the square formed by a component and the corresponding coproduct inclusions is cartesian. The proof uses the open cover of a coproduct and the equality criterion for points in…

After an arbitrary field-valued base change, smoothness supplies domain stalks and local Noetherianity. Geometric connectedness supplies connectedness, so the resulting scheme is integral.

The equalizer of two relative morphisms into an unramified scheme is an open subscheme. If the target is also separated, the equalizer is closed. Thus agreement after a dominant morphism forces the equalizer to be the en…

The relative equalizer of maps to a separated unramified scheme is both open and closed. Agreement after a map from a nonempty scheme makes this equalizer nonempty. A preconnected source therefore forces the maps equal.

Affine local lifts and ideal-power control of Čech coboundaries produce global sections after restricting from a sufficiently thick closed base change.

This facade collects the linear and power-triangular constructions for generator-sensitive Noether normalization.

The linear normalization theorem produces algebraically independent elements in the linear span of a prescribed generating tuple. This file develops the finite-dimensional exchange argument which completes those elements…

This file packages the first induction step in the infinite-field form of Fried--Jarden, Proposition 6.2.1. Starting from a nonzero relation among n + 1 generators, the triangular change from LinearNormalization produces…

This file carries out the generator-reducing induction over an arbitrary field. In a dependent step, the power-triangular coordinates from PowerNormalization replace n + 1 generators by n generators. The induction rememb…

This file turns the unit-leading-coefficient relation produced by the triangular change of variables into an actual monic relation over the algebra generated by the remaining coordinates.

This file formalizes the triangular linear substitution used in Fried--Jarden, Lemma 22.5.1. It fixes the first variable and sends each remaining variable Xᵢ to Xᵢ + cᵢ X₀.

This file supplies the nonvanishing step used in the constructive proof of Fried--Jarden, Lemma 22.5.1, and hence in the linear refinement of Proposition 6.2.1. The second theorem says that dehomogenizing a nonzero homog…

This file exposes the power-triangular change of variables used in Nagata's proof of Noether normalization. The degree-coding argument is adapted from Mathlib.RingTheory.NoetherNormalization (Apache-2.0; authors Riccardo…

This file connects mathlib's Noether normalization theorem with the transcendence degree of the quotient field. This is the first source-producing step toward the full generator-sensitive statement in Fried--Jarden.

The relative normalization of Spec B → Spec R is canonically isomorphic to Spec (integralClosure R B). The comparison intertwines the canonical map into the normalization with the map induced by the inclusion of the inte…

The canonical affine normalization isomorphism intertwines the actual structure map with the algebra map into the integral closure. This gives the ring criterion for finite etaleness of that actual normalization map.

This facade collects normalization finiteness, conductor-quotient, and prime-separation results.

Constructs the action of ambient field automorphisms on the normalization by restriction of scalars and integral-closure functoriality. The induced ring maps commute with the inclusion into the ambient field.

Suppose L → Ω is compatible with a base change A → B. Every element of the normalization of A in L maps to an element integral over B, hence into the normalization of B in Ω. This file constructs the actual normalization…

Fried--Jarden, Lemma 6.3.1 states that, for an affine integral curve R = K[x, y] with function field F and normalization S in F, the quotient S / R is finite-dimensional over K. This file develops the conductor and finit…

Let U ⟶ X be an open immersion and let W ⟶ U be finite etale. The relative normalization of X in the composite W ⟶ X, restricted back to U, is canonically isomorphic to W. This comparison does not assert that the normali…

This generalizes the affine integral-closure argument used for finite étale covers to any finite morphism with normal integral source. It applies at ramified boundary points as well. The resulting isomorphism is over the…

This file records the scheme-level form of the trace-dual finiteness theorem: over a locally Noetherian normal integral scheme, normalization in a finite separable extension of the function field is finite.

Canonical aggregate for EtaleFundamentalGroups.Normalization.GenericFiber.

Let R be a normal domain with fraction field K, and let S / R be smooth. Every element of S ⊗[R] K which is integral over S already comes from S. This is the elementwise form of smooth base change for integral closure. I…

Normalization selects an idempotent in the special fiber. Its integral closure is integral over the original Henselian base, so this idempotent lifts there. The resulting factor is integral and étale over the new base, a…

The section first selects a finite factor in the special fiber of the integral closure. A principal neighborhood identifies the integral closure with the étale algebra. The cyclic idempotent of this factor lifts by the H…

This aggregate exposes finite-product integral closures, intersections of localizations, regular pairs, integral bases, and comparisons between two integral bases.

Suppose x is prime and does not divide the nonzero element y of an integrally closed domain A. For an algebraic extension of the fraction field of A, integrality over both A[1/x] and A[1/y] implies integrality over A. Th…

Completion of a finite separable field extension splits its generic fibre as a finite product of completed fields. To aggregate local normalization statements one needs the corresponding integral closure to split coordin…

This aggregate exposes the equivalence comparing integral closures over the specified integral base.

If A → B is integral and both rings act compatibly on the same ambient ring L, an element of L is integral over A exactly when it is integral over B. Thus the two literal integral-closure types are canonically equivalent…

Let A be a domain with fraction field K. If x is prime and does not divide the nonzero element y, then the images of A[1/x] and A[1/y] inside K intersect in the image of A. This is the small codimension-two intersection…

Canonical aggregate for EtaleFundamentalGroups.Normalization.IntegralClosure.RegularPair.

Let A be an integrally closed domain with fraction field K, let L / K be algebraic, and let B be the integral closure of A in L. If x is prime and x, y are relatively prime nonzero elements of A, then the equality y b =…

This file develops the trace-dual argument which avoids factoriality and normality assumptions on the base. For a finite separable extension L / K and the finite normalization B of a Noetherian domain A, the trace dual o…

Let B and C be integral A-algebras embedded compatibly in one ambient ring L. Both integralClosure B L and integralClosure C L are the same subring of L, although their literal Lean types differ. This file gives the cano…

Bundles restriction of algebra automorphisms to the integral closure as a group homomorphism.

Proves that the algebra automorphism group of the integral closure in a finite Galois extension forms a Galois group over the integrally closed base domain.

Let p : Z ⟶ V be integral and j : V ⟶ Y a quasi-compact open immersion. The relative normalization of Y in p ≫ j restricts over V to Z. The canonical normalization map embeds Z as exactly the inverse image of the origina…

This aggregate exposes the equivalence between localization away from an element and the corresponding integral-closure construction.

The normalization of an away localization is the localization of the original normalization. This file records the comparison as an algebra equivalence over the localized base and transports étaleness back to the literal…

Defines the underlying ring maps of coefficient and Galois automorphisms, together with the inclusion of the normalization into its ambient algebra.

Proves faithfulness and lies-over properties for subalgebra normalizations. For faithful algebras over a discrete valuation ring, the contracted maximal prime is nonzero.

Restricts an algebra homomorphism to a ring homomorphism between integral closures, using preservation of integral elements.

This file provides a focused normality interface for integral schemes. The definition is phrased on affine charts, and the basic stalk consequence is recorded here so that normalization and divisor developments can share…

Defines the coefficient automorphism group as a group object and the induced group morphism obtained by restriction to the normalization.

Proves that every algebra automorphism of the integral closure in a finite field extension extends to an automorphism over the base fraction field. Coefficient-square lemmas identify the extension and its restriction.

Every intrinsic coefficient automorphism is induced by an automorphism of the finite fraction-field extension.

This file formalizes the weak-approximation argument in Fried--Jarden, Lemma 6.3.2(b). Pairwise distinct primes above a fixed maximal ideal are separated by the Chinese remainder theorem. The resulting elements are the s…

This aggregate exposes DVR primes below product coordinates and local-ring factor comparisons.

In a product of local rings, fix the maximal prime selected by one coordinate. If that coordinate is a DVR, the only strictly smaller prime is the kernel of coordinate evaluation. This identifies a selected generic compo…

For a family of local rings A, the inverse image of the maximal ideal of A i under evaluation at i is a maximal ideal of the product. Localization of the product at this ideal canonically recovers A i. The construction d…

For a quasi-finite algebra of finite type, a finite open factor of a quotient fiber is a factor of the corresponding quotient of the integral closure. The factor's unit has a representative in the integral closure whose…

Bundles algebra automorphisms as group objects and constructs the group morphism that restricts their scalars along an algebra tower.

Constructs the ring map between normalizations of nested subalgebras. It proves compatibility with the ambient inclusion and injectivity of the tower map.

Proves compatibility of the normalization tower map with base coefficients and multiplicativity of ramification indices for the resulting tower.

The normalization objects and their preimage are constructed from the native carriers and inherited actions. Their ring maps and coefficient equations are established before any fraction-field, Galois, or inertia data ap…

Finite separable intermediate fields control tensor-product elements and minimal primes. The resulting irreducibility statements compare separable and algebraic closures.

Scalar restriction and tensor-product comparisons identify equalizers after flat base change, using the original algebra homomorphisms.

Scalar restriction and tensor-product comparisons identify equalizers after flat base change, using the original algebra homomorphisms.

Étaleness is characterized by local standard smoothness of relative dimension zero, including the degenerate subsingleton algebra case.

The finite etale property combines etaleness with module finiteness. The accompanying lemmas transport this property across algebra equivalences and localizations.

An algebra whose tensor product with a faithfully flat base algebra is finite etale is itself finite etale, by descending etaleness and module finiteness separately.

Equalizers of maps between finite products are described by function coequalizers. Localization provides covers on which finite étale maps have these split presentations.

Finite étale algebras admit split presentations on étale neighborhoods. These presentations and faithfully flat descent compare tensor products with algebra equalizers.

We say a morphism is finite étale if it is finite and étale. The category FiniteEtale X is the category of finite etale schemes over X.

This module contains the scheme-theoretic and over-field results used by the finite étale category, independently of fundamental groups and Galois objects.

Finite algebra generation gives finite field generation, and algebraic finitely generated field extensions are finite. The file also records smoothness of polynomial fraction fields.

Finite morphisms satisfy cancellation after postcomposition by a finite morphism.

Flat ring maps of finite presentation induce open maps on prime spectra. Flat scheme morphisms with the stated finiteness, surjectivity, or monomorphism hypotheses give isomorphisms and open immersions.

Smoothness satisfies the localization-span criterion. Bijective algebra maps give formally smooth algebras, and fraction fields of multivariate polynomial algebras are formally smooth.

The canonical equivalence from a quotient by the infimum of pairwise coprime ideals sends a quotient representative to its family of representatives in the individual quotients.

This facade collects coordinate rings, rational points, monic projections, and the equivalence between simple and normal points on affine plane curves.

For a finite ground field, a generic linear projection need not be defined over the ground field itself. Fried--Jarden therefore first passes to a suitable finite constant extension. This file develops that missing const…

This file supplies the affine-coordinate-ring foundations used in Fried--Jarden, Section 6.2. A bivariate equation f defines the quotient of K[X, Y] by the principal ideal (f). A K-rational zero of f gives an evaluation…

This file derives the one-dimensionality needed in Fried--Jarden, Section 6.2, directly from an irreducible bivariate equation. The proof uses the correspondence between primes of a quotient and primes above its kernel,…

This file starts the source-producing infrastructure for Section 6.1: scalar extension to an algebraic closure and the zero sets of multivariate polynomials.

This file connects the linear normalization developed for Fried--Jarden, Proposition 6.2.1, with the monic projection model. Over an infinite field, an invertible linear change of the two affine coordinates makes the lea…

This file isolates the finite-degree input used in Fried--Jarden, Lemma 6.2.2(b),(d). If the equation of a plane curve is monic in Y, its coordinate ring is a finite free algebra over the polynomial ring in X. After pass…

This file proves the difficult implication in Fried--Jarden, Lemma 6.2.3: a normal rational point of an irreducible affine plane curve has a nonzero partial derivative. The proof follows the valuation-theoretic argument.…

For an irreducible affine plane curve and a rational point at which the local ring is normal, the point local ring is a discrete valuation ring. This file realizes that local ring as its canonical valuation subring in th…

This file develops the first-order polynomial decomposition used in Fried--Jarden, Lemma 6.2.3. Besides writing a polynomial minus its value at a point as a combination of the two translated coordinates, the construction…

Every K-algebra map from an affine plane-curve coordinate ring to K comes from a unique rational point. Consequently, coordinate-ring equivalences transport rational points and their maximal ideals.

This file proves the simple-to-normal direction of Fried--Jarden, Lemma 6.2.3. At a point where one partial derivative is nonzero, the first-order decomposition of the curve equation eliminates the corresponding translat…

Canonical aggregate for SchemeTheory.ProjectiveSpace.

The morphism of projective spaces induced by an algebra map is a pullback of the structural morphism. Polynomial scalar extension identifies the affine charts and their overlaps.

Projective space is constructed from graded polynomial rings together with its standard affine charts, maps and fibre products. Chow data records the resulting projective compactification constructions.

The coordinate basic opens give an ordered affine cover of projective space and affine pullback covers for affine morphisms into projective space.

The inverse image of a coordinate basic open under the base-change map of projective spaces is the corresponding coordinate basic open over the new ring.

This aggregate exposes completion of coprime products, algebra structures for integral extensions, and localization-at-prime comparisons.

The Chinese remainder theorem decomposes every finite quotient by a power of a product of pairwise coprime ideals. This file proves that these finite-level decompositions are compatible with the transition maps, and henc…

The Chinese-remainder decomposition of a completed finite integral extension is compatible with the canonical maps from the extension ring.

For a maximal ideal Q of a commutative ring S, localization at Q identifies every finite quotient S ⧸ Q ^ n with the corresponding quotient of Localization.AtPrime Q by the n-th power of its maximal ideal. We prove that…

This aggregate exposes adic completions, generic fibres, henselian factorizations, flatness and descent, normalization, and ramification modules.

The predicate records equality of the Krull dimension and the depth of the ring with a specified natural number. Its two projections recover the dimension and depth equalities.

If the maximal ideal of a noetherian local ring is not an associated prime of either finite module, it contains an element whose scalar multiplication is injective on both modules.

Suppose an element of a finite algebra reduces to an idempotent whose factor is generated by that idempotent over the base. A finite generating family beginning with this element makes its multiplication matrix diagonal…

If multiplication by the reduction of e has cyclic image, imposing e = 1 makes the resulting special fiber generated by its unit over the quotient base. Thus its canonical algebra map from the quotient base is surjective…

Every nonzero denominator divides a power of any fixed nonzero nonunit: a uniformizer divides that nonunit, while each denominator is associated to a power of the uniformizer. Thus localization at that nonunit already in…

This aggregate exposes module and algebra equalizers, homomorphism descent, prime-away gluing, finite etale neighborhoods, and descent of finite type and finite presentation.

Only the local rings on the principal boundary need to be normal. An integral element of the localization has no pole there: normality proves local divisibility of its numerator, and divisibility descends from the locali…

Integral elements in the generic fibre of a smooth algebra descend to the original algebra. These comparisons yield the domain and integral-closure properties of an etale algebra localized at a prime.

The algebraic input is an actual injective integral local map into a normal local domain, with purely inseparable residue field extension. Base change of that extension along a local étale neighborhood is local. It is al…

The same actual normal base change used in the domain theorem also handles nonreduced local rings. Flatness carries a nilpotent kernel to a nilpotent kernel; embedding modulo that kernel into the constructed normal domai…

Only the local ring of the base at the contracted prime is assumed normal. Localizing the etale algebra over that ring and then at the lifted prime gives the original local ring, through the actual localization compariso…

For R → S → T with S → T and R → T étale, every prime of S in the actual image of Spec T has a principal neighborhood étale over R. The open image supplies its defining ideal. Localizing at an element of that ideal makes…

The prime-local comparison is extracted from EtaleFundamentalGroups.Purity.SpecialLocal.BaseMinimalPrimePuncturedPurity. It uses the actual iterated-localization isomorphism and requires no normality, finiteness, or glob…

For a tower R → A → B, faithful flatness of A → B reflects the ideal injectivity criterion for flatness. The existing iterated-base-change identity supplies the comparison, without any new tensor construction. If both R…

The equalizer subalgebra of a compatible algebra descent datum recovers the upstairs algebra after base change. The proof obtains its underlying module isomorphism from Module.FaithfullyFlat.isBaseChangeeqLocusofdescentD…

The degree-preserving hypothesis makes every homogeneous component of an invariant upstairs element invariant. The ungraded bijectivity statement is reused directly; its proof is not duplicated in this file.

The invariant submodule of an arbitrary compatible tensor descent datum base-changes back to the given module. This differs from the canonical Amitsur equalizer of an already descended module. Public assumptions and conc…

This file develops the degree-zero part of faithfully flat descent for modules. The first step is the split case: if an algebra admits an algebra section, then the usual Amitsur pair remains exact after tensoring with an…

The usual Amitsur equalizer for a target module also gives the Hom-level full-faithfulness statement. An S-linear map between two extended modules comes from the base precisely when its values on the canonical generators…

An integral domain is integrally closed when a faithfully flat domain extension is integrally closed. The proof descends an integral element through the original algebra map.

The spectral image of a flat finitely presented algebra is represented by an ideal. A base change on which this ideal becomes the unit ideal makes the tensor-product algebra faithfully flat.

The complement of the etale locus has closed image under an integral map. A fiber contained in the etale locus therefore has an entire principal neighborhood contained in that locus.

The model is a genuine subalgebra of the original algebra on D(d). It recovers that algebra after inverting d, and agrees with the integral closure at the selected prime. Its generators come from the two actual localizat…

A finite model becomes etale after shrinking the base. Normality of the original base along the boundary then makes the model's boundary local rings normal. Integral closure across that boundary identifies the model with…

Finiteness at a point first produces an actual finite subalgebra model. Its etale locus spreads around the whole fiber, and boundary normality identifies that model with the integral closure on this neighborhood. The res…

Finite generation of the kernel of a polynomial presentation descends through faithfully flat base change. Combined with finite-type descent, this proves descent of finite presentation.

For an integral algebra, finitely many numerators generate a finite subalgebra. If two localizations are finite, the numerators of their module generators can be chosen together. The resulting subalgebra has exactly the…

Finite generation of an algebra descends along a faithfully flat finitely presented extension. Polynomial presentations and finite subalgebra models supply the generators over the original base.

The unramified locus of a finite type algebra is open without a finite presentation assumption. Its closed complement has closed image under an integral map, so unramifiedness of one entire fiber spreads to a principal n…

The inverse is defined on each homogeneous component and extended through the direct sum.

The grading is the inverse image of the upstairs homogeneous pieces. Its direct-sum retractions compare scalar extension degree by degree; this is a concrete construction, independent of how the subalgebra was obtained.

If T is integral over a localization of R, its integral closure over R recovers T after inverting the original denominators. This is an application of Mathlib's integral-closure localization theorem, transported along th…

An integral fraction has locally divisible numerator at each maximal ideal. At a maximal ideal meeting the denominator submonoid, normality gives that divisibility in the prime localization. At the other maximal ideals t…

Maps between tensor extensions are determined on elements 1 ⊗ m, and maps between localized modules are determined on fractions with denominator one. These are the two componentwise extensionality lemmas used by mixed fo…

Flat Hartogs extension preserves the multiplicative structure: the algebra identities can be checked after the two principal localizations. These are the maps used to extend the actual completion-overlap isomorphism.

Two relatively prime principal localizations of a domain intersect in the base ring when one parameter is prime. Flat tensor products preserve this equalizer. This supplies the scalar extension step on completion overlap…

A map from a flat module is an isomorphism if it becomes an isomorphism at two prime-away localizations and the first parameter acts injectively on the target. The source's flat Hartogs equalizer constructs preimages.

Finitely many elements of a fraction field lie in a single principal localization of the original domain. Use the existing common-denominator construction and the actual localization subalgebra of the fraction field. App…

A smooth algebra localized at a prime over an integrally closed domain is a domain and is integrally closed. The proof first treats polynomial algebras and then the etale local presentation.

The comparison of two given tensor-product identifications respects scalars and homogeneous pieces, and identifies its invariant elements with the original equalizer.

A diagonal action on a finite generating family modulo an ideal gives a monic annihilating polynomial whose reduction is the product of the diagonal linear factors. The generating family need not be a basis.

Maps from a standard étale algebra to a field inject into the roots of its defining monic polynomial. The existing standard-étale hom equivalence and root-cardinality theorem therefore give actual finiteness and a numeri…

Compactness of the actual prime spectrum gives a finite family of the previously constructed bounded principal charts. A map to a field has a prime kernel, so one chart element maps to a unit and the map extends by the e…

If an affine open subscheme is finite over a common base, its map into any intermediate affine scheme is finite. An open immersion is a monomorphism, so the corresponding finite ring epimorphism is surjective. Together w…

Suppose a finite relation ideal vanishes under an algebra map after inverting one element. Multiplying its finitely many generators by suitable powers of that element gives a smaller finitely generated ideal in the actua…

Two maps from a finitely generated algebra into a finite, finitely presented stage which agree in the target can be coequalized by an actual finite, finitely presented quotient of that stage. Its defining ideal is genera…

A finite family of domain algebras over a Dedekind domain gives a faithfully flat product when the structure maps are injective and their spectra cover the base. This applies to finite affine covers of arithmetic schemes…

Every maximal ideal of a finite algebra above the closed point can be represented over the same chosen algebraic closure of the base residue field. The resulting ring map has the given kernel and the canonical base map.

This aggregate exposes local flatness criteria, generic flatness, openness of the flat locus, and finite-subalgebra models.

Flatness descends to a finitely generated subalgebra containing any chosen finite set. The proof first treats the noetherian case and then descends a finite presentation model.

Finite-subalgebra localization and tensor-kernel generation give finite algebraic models for flat modules.

A finite module over a finite-type algebra over a noetherian domain becomes flat after localizing at a suitable nonzero base element. The proof controls tensor kernels and passes to the localized module.

Flatness of the kernel of a surjection between flat modules.

Local flatness criteria.

Tensor-kernel torsion criteria characterize flatness at a prime and its behavior under specialization. For the stated noetherian and finite-presentation hypotheses, the locus of flat prime localizations is open.

The tensor functor retains independent base-ring, tensor-factor and source universes. Its right exactness follows from an explicitly constructed tensor-Hom adjunction in the larger module universe and a proved natural co…

Exactness of tensoring with a flat algebra represents every element killed by base change using elements of the original kernel. Their images are nilpotent, so the resulting finite sum is nilpotent as well.

For any subalgebra B of the fraction field K of a domain R, the actual multiplication map K tensor B to K is an isomorphism. Flatness preserves the inclusion B to K, and each element of K is the image of k tensor 1. Cons…

A flat algebra over an arbitrary base embeds in its tensor product with a faithful algebra. If that tensor product is a domain, localizing the original algebra to its fraction field preserves this property. Over the inte…

Scalar multiplication by a ring element is injective on a nontrivial free module exactly when multiplication by that element is injective on the ring.

Weak regularity of a sequence on a nontrivial free module is equivalent to weak regularity on the ring. The public statement uses the free-module comparison proved in the auxiliary module.

Weak regularity of a sequence on a nontrivial free module is equivalent to weak regularity on the ring. This auxiliary proof compares quotient modules and proceeds by induction on the sequence length.

This aggregate exposes finite generic fibres, fraction-ring comparisons, primes lying over fraction rings, and chosen components of DVR products.

Let K be a fraction field of R, let U be an R-algebra, and let m be a maximal ideal of the generic fibre K ⊗[R] U. The quotient by m is canonically a fraction field of U modulo the contraction of m. The construction keep…

For a generic fibre of a product of DVRs, a maximal ideal whose contraction lies strictly below a specified coordinate maximal prime selects the fraction field of that same coordinate. The kernel identification is produc…

For a finite extension of domains C / R, extending scalars from R to a fraction field K identifies the generic fibre K ⊗[R] C with a fraction field E of C, provided the two fraction-field embeddings are compatible. The p…

An equivalence between the generic fibre K ⊗[R] C and a field E canonically embeds C in E. When C is a domain, this embedding makes E a fraction field of C.

Let D / S be a finite extension of domains, and let q lie over p. This file fixes all canonical algebra structures between the two prime localizations and the fraction field of D. It also transports finite dimensionality…

Mathlib's pushout cancellation identifies (K ⊗[R] S) ⊗[K] B with S ⊗[R] B as S-algebras, using the canonical S action on the right factor of K ⊗[R] S. A supplied splitting then gives an actual splitting into copies of S…

The definition uses the normalization of the reduction in its total fraction ring. It requires the reduction to be a domain, its normalization to be local, and the resulting residue field extension to be purely inseparab…

The determinant trick gives an annihilator reducing to (X - 1) X ^ d. Hensel's lemma lifts the simple root 1. Dividing out this root and evaluating the remaining factor constructs the desired idempotent in the finite alg…

The universal coprime factorization ring is étale over the coefficient ring. Its section supplied by a factorization over the quotient therefore lifts over a Henselian pair. Naturality of its representing equivalence giv…

The special fiber is an Artinian algebra. Two distinct maximal ideals would be separated by an idempotent in that fiber. Henselian lifting produces an idempotent in the domain, which must be zero or one, a contradiction.

A doubled generating family gives an annihilator reducing to powers of X - 1 and X. The Henselian factorization theorem lifts these coprime factors, and evaluation of a Bézout identity gives the required idempotent.

Quotient idempotence uses only finitely many coefficients of the integral algebra. A finite subalgebra containing these coefficients retains the quotient idempotent. The finite-algebra theorem lifts it, and the canonical…

For a monic polynomial with an approximate simple root, the standard étale algebra obtained by inverting its derivative has a section over the quotient. The integral-base section theorem lifts that section and hence the…

The integral closure of a Henselian local ring in a field is local. Inside a normal local ring with that fraction field, the integral closure embeds by the native integral-element constructor. Its map is local because it…

A finite subalgebra can retain a quotient idempotent and its principal localization. Cyclicity descends through that localization comparison, so the finite-algebra lifting theorem applies. Mapping the resulting idempoten…

Each element belongs to a finite simple subalgebra. That subalgebra is a domain and is local by the existing finite-domain Henselian theorem. Its unit alternative maps into the original integral domain.

of module Finite

For a polynomial with an approximate simple root modulo a nil ideal, its initial error generates a nilpotent principal ideal. The adic filtration for this smaller ideal terminates, so completeness supplies a root whose c…

The actual bijection on quotient idempotents of an integral algebra lifts each member of a finite family. Uniqueness lifts orthogonality and the equation that their sum is one. The algebra need not be finite or finite ty…

Positive-degree spanning suffices for the irrelevant-ideal containment needed by Proj.

An element of a finite algebra that becomes idempotent modulo an extended ideal admits a monic annihilator reducing to (X - 1) ^ n X ^ n, with positive n. Splitting a finite generating family into its multiples by b and…

Imposing e = 1 commutes with reducing by an extended base ideal. The comparison is obtained from the canonical interchange of two quotient rings. It also identifies a reduced factor with a specified factor of a product.

A Bézout identity for two coprime factors of an annihilating polynomial gives an idempotent after evaluation. If the factors reduce to positive powers of X - 1 and X, this idempotent lifts the given quotient idempotent.

If the basic open of an idempotent in a quotient ring lies over an open subset of the original spectrum, it has a lift whose basic open is contained in that subset. The lift is obtained from a positive power and need not…

A bijection on principal localizations identifies ideals extended from the base ring. Clearing the resulting denominator gives an ideal-membership statement in the source. For a quotient idempotent, multiplication by one…

For a surjective algebra map inducing an open immersion on spectra, the kernel is generated by an idempotent. The complementary idempotent gives a concrete product decomposition, with its first projection equal to the or…

A splitting over a pointed étale neighborhood gives a split product in a localization by non-zero-divisors. Local normality of that étale neighborhood shows it is integrally closed in that localization. Smooth base chang…

If the base ring is integrally closed in an ambient algebra, its integral closure in a finite product of copies of that algebra is the same finite product of the base ring. Coordinate evaluation supplies every integral c…

The actual small model cocone is jointly surjective for an integral target, by the finite-subset model construction. Equality of two elements in one stage is detected later by coequalizing the two polynomial evaluation m…

The objects use the existing FGAlgCatSkeleton, whose presentation data already lies in the base universe. Each object is an actual finite, finitely presented algebra equipped with a map to the target algebra. Morphisms a…

Each finite subset of an integral algebra is contained in the image of an actual finite, finitely presented algebra over the original base. The model is constructed by successively adjoining roots of the elements' monic…

If a principal localization of an integral algebra is of finite type, finitely many numerators of algebra generators already generate that localization. They can be adjoined together with any prescribed finite set before…

Ideal membership uses only finitely many coefficients. Including those coefficients in a finite subalgebra makes a quotient idempotent descend to that subalgebra. A finite-type principal localization can also be preserve…

If an integral map of local rings induces a purely inseparable residue field extension, its tensor product with any local algebra is local. The proof constructs the map to the tensor product of the two residue fields. Ev…

A presubmersive presentation has an injective assignment of relations to variables, without any assumption that its Jacobian is invertible. Composing with the presentation of the localization at that Jacobian gives a sub…

In an integral algebra over a Jacobson pair, an element congruent to the unit of a factor becomes a unit on that factor. The factor is the actual quotient by the complementary element, and its algebra structure comes fro…

An idempotent in the Jacobson radical vanishes, since its complement is a unit annihilating it. Applying this to the two complementary products shows that reduction modulo a Jacobson ideal is injective on idempotents.

An ideal contained in the Jacobson radical remains so after extension to an integral algebra, because maximal ideals contract to maximal ideals.

A local ring is adic when its maximal ideal defines its topology. Topological finite generation means that finitely many algebra generators form a dense subalgebra. Module depth is the supremum of the lengths of weakly r…

Canonical aggregate for SchemeTheory.RingTheory.Localization.

An algebra equivalence carries the complement of a prime ideal onto the complement of its image. Hence it induces an algebra equivalence between the corresponding local rings. The explicit formula on elements from the ba…

Bundles localization away from an element as a commutative algebra over the coefficient ring and proves its localization witness.

The source is the actual native principal localization. The target and its coefficient map are the existing native prime-localization owners. The single localization proof below closes the coefficient equation in an R/C-…

The objects retain their existing native commutative algebra structures. The maps are the already proved native RingHoms. The contracted ideal is computed before its membership condition is used, so the public map and co…

Proves that localization of a Dedekind domain at a nonzero prime is a discrete valuation ring.

Canonical aggregate for SchemeTheory.RingTheory.Localization.Fraction.

This file fixes the canonical algebra maps from a prime localization into an arbitrary chosen fraction field and then into a field extension. The latter map is defined by composition through the fraction field, so the tw…

An application may use an arbitrary chosen fraction field K of a domain V, while a generic construction is formulated over the literal quotient type FractionRing V. This file fixes the canonical composite algebra on an e…

Proves that an injective ring map into a domain induces an injective map on localizations at a prime and its contraction.

Proves that a commuting square of ring maps induces a commuting square on prime localizations when the relevant primes are preserved.

The transition is the existing native principal map from Rf to R(fd). Its etaleness is proved through the actual second principal localization of Rf. The product-localization equivalence and its coefficient equation are…

The ring objects are the actual native prime localizations. Their coefficient maps are the native algebra maps, retained as RingHoms. The localization map is Localization.localRingHom; its native coefficient equation is…

If a map becomes bijective after inverting b, it identifies the factors on which an idempotent is 1, provided b is already a unit in the source factor. The comparison is the actual map induced on the two quotient rings.…

For an algebra over a localization of the base ring, first extending the localization and then extending that algebra gives the same tensor product as extending the algebra directly. The comparison remains linear over th…

If a submodule becomes the whole canonical localized module, it also becomes the whole of any actual localization. The proof transfers actual fraction representatives along the localized identity map. This is the compari…

The depth of a nontrivial finite module over a Noetherian local ring is bounded by the Krull dimension of its support and hence by the Krull dimension of the ring.

For a finite module over a Noetherian local ring, quotienting by a scalar in the maximal ideal that is regular on the module lowers its depth by one. The supporting arguments compare regular sequences, associated primes,…

When a submodule is finitely generated on finitely many principal opens, choose numerator representatives for all those local generators. Their finite span is a submodule of the original module and has exactly the same l…

The native localization theorem identifies the kernel of the universal localized arrow with the localization of the original kernel. Here the lower arrow is the one supplied by an actual commutative square. Its universal…

Deduce module finiteness from a kernel contained in a range over a Noetherian ring.

Stacks Project, Section 58.32, defines NF by considering every ordered finite algebra-generating family, taking its longest integral prefix, and minimizing the number of remaining generators. This file constructs that li…

The determinant of the actual multiplication matrix gives a homogeneous polynomial of degree equal to the extension dimension. Its evaluation is the actual algebra norm. This construction is shared input for norm equatio…

A finite open factor of a closed fiber of an affine open immersion is an actual factor of the target closed fiber. Its defining idempotent has a representative whose principal open lies in the image of the immersion. Loc…

Nonzero orthogonal idempotents are linearly independent. If their number is at least the dimension of the algebra, the explicit sum of scalar multiples is a bijective algebra map from a product of copies of the base fiel…

This file proves the local-ring prime-existence statement of Stacks Project Tag 0BJG. A prime chain selects a positive-dimensional component of a hypersurface, and localization decreases the positive height.

A principal hypersurface in a Noetherian local ring of dimension at least two contains a prime different from the maximal ideal. The same construction on a prime quotient produces a point on a specified irreducible compo…

The map between the quotients by the extended base ideal is an algebra map over the quotient base. The quotient/tensor equivalences identify it with the canonical tensor-product base change.

This aggregate exposes the flat-base-change comparisons for ramification invariants.

If both vertical maps in a commutative square are faithfully flat and the chosen primes are exactly the extensions of the original primes, then the ramification index is unchanged across the square. The proof compares th…

Proves the commuting square for conjugating a ring automorphism through a ring equivalence. It also transports a compatible ambient coefficient square to the conjugated automorphism.

Canonical aggregate for EtaleFundamentalGroups.Ramification.Etale.

This file records the ramification-index comparison needed after choosing an étale factor as in Stacks Project, Tag 00UJ. The contraction equality supplied by that construction is the only prime-comparison input: residue…

Suppose a ring in the upper-right corner is etale over the upper-left corner, while the lower-right corner is etale over the lower-left corner. For one prime in the lower-right corner and its contraction to the lower-lef…

The native quotient action is first constructed on the fixed subring before introducing a coefficient algebra. Its literal carrier is then the existing fixed subalgebra over the original base. The finite uniform-lift the…

The finite characteristic-polynomial theorem proves preservation of the actual coefficient image. The native first isomorphism theorem transports the resulting image automorphism to the quotient by the kernel. The native…

A ring automorphism of a domain preserves the image of a finite invariant ring extension whenever it fixes the composite coefficient map. Only native ring homomorphisms are used on the target. In particular, the argument…

The stage at a finite Galois intermediate field is the preimage of the upper inertia-fixed subalgebra under the literal normalization inclusion. Transition maps are restrictions of the existing intermediate-field inclusi…

The canonical action on the actual integral closure is continuous for the Krull topology and the discrete ring topology. The subgroup fixing an actual intermediate field has that field's integral closure as its invariant…

Every stage is localized at the literal contraction of the chosen upper prime. The maps are the existing Localization.localAlgHom; their composition and values on fractions use the existing local-ring homomorphism identi…

Every finite family of elements in the actual integral closure fixed by its prime inertia comes from one finite Galois intermediate field. The returned elements are integral over the original base and fixed by the inerti…

The original ring action supplies the subgroup. Its coefficient stabilizers give a continuous action on the discrete ring, and inertia is the intersection of the closed coefficient-difference conditions.

Proves that a prime-localization automorphism, viewed through the canonical valuation-ring equivalence, agrees with a compatible ambient field action on coefficients.

Transports a prime-localization automorphism acting by principal-unit multipliers to the corresponding valuation ring. The transported automorphism retains its compatible ambient field action.

Constructs the canonical ring equivalence between a Dedekind prime localization and its valuation-ring model in the fraction field. Computation lemmas identify its values on the original coefficients.

Proves that the inertia difference condition descends to a contracted ideal along a commuting square of coefficient maps.

For an element of the ambient Galois field fixed by normalization inertia, the native integral-multiple theorem supplies a nonzero base denominator. Scalar preservation and the existing literal coefficient square prove t…

The native inertia-to-stabilizer theorem supplies preservation of the prime, then the native local-ring equivalence extends the original automorphism. Its coefficient formula proves compatibility with the original base m…

Transports CharP and characteristic-zero instances between residue fields of isomorphic local rings.

Identifies the residue automorphism of a localization as the conjugate of the quotient automorphism through the canonical maximal-quotient residue equivalence.

Proves that the canonical equivalence from a maximal-ideal quotient to the localization residue field intertwines the maps induced by a prime-preserving ring automorphism.

Defines ring equivalences and coefficient maps underlying algebra residue automorphisms. It proves that these coefficient maps determine the automorphisms and computes the residue morphism on coefficients.

The coefficient map and its action are those stored in the native algebra object. Coefficient fixedness, fixed-element descent, and open stabilizers supply the actual compact residue-lift theorem. Its surjectivity proves…

Identifies the algebra residue morphism with the quotient automorphism of its coefficient action. The canonical maximal-quotient equivalence then relates it to the localization residue map.

The coefficient residue field is the native local-ring quotient. At a maximal ideal, the canonical quotient-to-prime-residue map is bijective; its actual map defines the equivalence below and preserves the original quoti…

The source and target are the existing stabilizer and quotient-algebra automorphism groups. The map is exactly Ideal.Quotient.stabilizerHom. Its surjectivity is obtained from the constructed global residue equations, and…

The prescribed normalization action is invariant over the original normal base. Field fixedness gives a fraction-field preimage. The integral-closure subtype supplies its integrality, and normality descends it to the bas…

The groups and homomorphism below are the native stabilizer and the literal quotient-algebra automorphism group of the actual integral closure. The possibly infinite Galois action has the prescribed normalization action.…

The finite invariant-kernel argument extends to a compact totally disconnected kernel acting continuously on the discrete ring. The two substantial inputs are the existing profinite prime-orbit theorem and the existing s…

For each open normal subgroup N, take the actual elements of G whose residue equations hold on every N-fixed original coefficient. These sets are closed, nonempty by the finite quotient lift, and directed downward by int…

The diagram stores ordinary ring/group/action/map/topology data only. In particular it stores no equivariance, invariance, surjectivity, contraction, stabilizer-image, or inertia-image proof. These facts must be proved f…

An injective equivariant ring map and the proved full inertia image give the equality between the actual upper-fixed preimage and the actual lower fixed ring. The proof stays in the existing ring-action restriction owner…

Proves that a power of a ring automorphism is the identity whenever the same power of a compatible extension is the identity and the coefficient map is injective.

Constructs the action of a prime stabilizer on the prime localization and computes it on coefficients. It identifies localization inertia with the original ideal inertia inside the stabilizer.

Proves that the inertia group of the stabilizer action on a prime localization has the same cardinality as the original ideal inertia group.

Constructs a multiplicative equivalence between inertia for the stabilizer action on a prime localization and the original ideal inertia group.

Canonical aggregate for EtaleFundamentalGroups.Ramification.Trace.

This file develops the linear-algebra input for the dimension-two branch-locus argument. For a finite free commutative algebra, the trace pairing is onto the module dual exactly when the discriminant of a basis is a unit…

Canonical aggregate for EtaleFundamentalGroups.Ramification.Unramified.

A finite étale algebra over a fraction field is a product of its actual maximal-ideal quotient fields. The normalization in that algebra therefore splits as the product of the normalizations in those fields. Over a DVR,…

For a finite separable extension of a DVR's fraction field, unramifiedness means that every maximal prime of the integral closure has ramification index one and separable residue extension. This is the unramified case of…

For a finite formally unramified R-algebra S, the canonical separability element Algebra.FormallyUnramified.elem R S cuts out the diagonal component of S \otimesR S. After inverting this element, multiplication identifie…

Let f be a nonzerodivisor in a Noetherian ring A, with A / (f) reduced. At every minimal prime over (f), the local ring of A is a DVR and the image of f generates its maximal ideal. The ambient ring need not be a domain,…

The depth of a regular local ring equals its Krull dimension. Regular sequences and quotients by regular parameters supply the supporting induction and lifting arguments.

A finite module over a regular local ring is free when its depth equals the Krull dimension of the ring. Regular parameters reduce the dimension, and bases lifted from regular quotients finish the induction.

Regularity supplies the domain structure and identifies the dimension of the cotangent space with Krull dimension. The one-dimensional local-domain criterion then produces the discrete valuation ring structure. No domain…

Avoiding minimal primes produces regular elements that lower the dimension. Induction on the dimension then proves the domain property for regular local rings.

The depth argument and the resolution construction are extracted from the attributed source above, independently of its subsequent localization and unique factorization argument. The ring hypothesis here is only regular…

If a Noetherian local ring modulo a nonzerodivisor is regular, then the original ring is regular. A minimal generating set of the quotient maximal ideal lifts, together with the nonzerodivisor, to a generating set of the…

A finite free resolution expresses the trace after flat field extension as an alternating sum of traces of finite free modules. We use only the finite free resolution theorem for a regular local ring from the imported so…

If every element separable over the base in one field lies in the base image, that field is linearly disjoint from a separable extension. Their tensor product is therefore a field.

The sign group is the concrete group ℤˣ = {1, -1}. Its action is kept as explicit data, so no competing action on the polynomial ring is registered. This is the action occurring in Stacks Project, Tag 0BTE.

A nonempty set of variables makes the sign action faithful. The existing finite-group invariant-field theorem then gives ring rank two, and the canonical fraction-field extension has the same degree. No algebraic closure…

The polynomial ring is finite over its concrete quadratic subalgebra. The invariant-ring input is the proved calculation for simultaneous sign change, with the action explicitly selected. These statements allow zero vari…

Over every field of characteristic different from two, the invariants of simultaneous sign change are exactly the subalgebra generated by X i X j. There is no restriction on the number of variables in this algebraic stat…

This supplies the concrete monomial factorization needed by Stacks Project, Tag 0BTE, including the case of zero variables.

Normality descends because a polynomial quotient of two invariant polynomials is itself invariant. The polynomial ring is the integral closure of the quadratic subalgebra in its own fraction field, using its original inc…

The etale generic-fiber argument and local standard-etale presentations prove reducedness directly. This is the reusable ring part of the pinned FLT proof previously maintained in AlgebraicCurves.

Lift the closed fiber's complete orthogonal family in an arbitrary integral algebra, map it through the actual embedding into a finite-dimensional algebra, and use the generic degree bound to obtain a split algebra.

A finite domain over a Henselian local ring is local. When the base residue field is separably closed, its finite residue extension is purely inseparable. Thus every automorphism of the finite algebra fixes every closed…

The prescribed local map to an algebraically closed field induces the scalar map on the base residue field. The finite residue extension embeds over that scalar map into the same field. Composing with the residue map con…

For an exhaustive directed family of subalgebras, contraction of one prime of the ambient ring gives a diagram of actual residue fields. Its canonical cocone has the ambient residue field as its colimit: every fraction h…

The algebra generated by a submodule commutes with actual localization. The comparison is proved inside the given localized ambient algebra, and the actual restriction of its algebra map is a localization of modules. An…

The lower submodule is given by the actual restriction map, as with sections of a quasicoherent subsheaf. Its identification with the native localized submodule follows from denominators of its own sections. The previous…

Two prime ideals of algebras over the same ring lift simultaneously to the tensor product when their contractions agree. The point is constructed in the scheme fiber product and transported through its affine tensor-prod…

Canonical aggregate for sheaves of modules on schemes.

Compares restriction to open subschemes with the corresponding pullback constructions.

Topological results used by scheme theory.

On a space with a generic point, the skyscraper at that point is the actual sheafification of a constant presheaf. The comparison is locally bijective because every nonempty open contains the generic point. Pushing this…

Precomposition restricts continuous functions on a support to its inverse image. Its adjoint is a morphism from the actual sheaf pullback. At every point of the support it agrees with the actual stalk evaluation maps. Th…

On the closed support the actual comparison identifies stalk evaluations. Outside the support its source stalk is terminal, so its stalk map is automatically a monomorphism. Stalks then detect that the actual sheaf compa…

The actual sheaf of continuous functions into a discrete value space has stalk equal to that value space, by evaluation. Constant functions give surjectivity, while open fibers give injectivity. Pushing forward from a su…

The open complement of the support has exactly the empty function as section, even for an empty value type. Every germ at a point outside the support restricts to this section, so the actual stalk is terminal. The Lean p…

For a finite set S of compact opens, the space Space S consists of the membership patterns actually realized by points of X. It has the upper-set topology for inclusion of patterns. Forgetting coordinates gives continuou…

The actual sheafifications of the free representables on compact opens form a strong generator on a prespectral space. Their maps into a sheaf are its sections on those opens. Compact-open neighbourhoods therefore detect…

Maps from the actual sheafified one-generator free representable are sections over the corresponding open. For a compact open, the naturality of this correspondence transfers preservation of filtered colimits from the se…

The colimit of topological sheaves is the sheafification of their presheaf colimit. Over a compact open in a prespectral, quasi-separated space, the sheafification unit is bijective. Comparing the evaluated presheaf coli…

Compact open neighbourhoods and quasi-separatedness replace Hausdorff separation in the description of connected components as intersections of clopen neighbourhoods.

For compact prespectral quasi-separated spaces, a continuous map inducing a bijection on clopen subsets induces a homeomorphism on connected components. Surjectivity is proved by the finite intersection property in the s…

The connected-component quotient of a compact quasi-separated prespectral space is Hausdorff, even when the original space is not Hausdorff.

The constant presheaf maps to the existing sheaf of continuous functions into a discrete space. This map is locally injective by evaluation and locally surjective because each continuous function is constant on the open…

If global restriction is surjective at every stage of a filtered diagram, then it is surjective for any colimit cocone. Only the restriction domain needs to be compact, prespectral, and quasi-separated: its global-sectio…

The presheaf colimit of a filtered diagram of sheaves satisfies descent for every finite open covering. The proof uses the actual finite pairwise intersection diagram, whose limit expresses the sheaf condition. Compactne…

The germ map from a principal Alexandrov neighborhood is an isomorphism: that neighborhood is a terminal object in the opposite neighborhood category defining the actual stalk. A singleton compact-open model recovers its…

For a prespectral space, the actual counits q⁻¹qF → F form a colimit cocone. On each stalk the diagram is the explicitly constructed diagram of principal-neighborhood sections. Its germ cocone is a colimit. Stalks preser…

Finite families of compact opens form a filtered index category. Their realized membership spaces and coordinate-forgetting maps give the actual approximations q⁻¹qF, with transition maps adjoint to the finer unit. The a…

For a continuous map q, the approximation to a sheaf F is the actual inverse image of its direct image, with its adjunction counit to F. Factoring a map through a finer space gives a map between these actual approximatio…

Sections over the inverse images of finite-model principal opens form an actual filtered diagram. Its germ cocone is a colimit at the actual stalk. Every germ has a compact-open representative, and equality of germs is w…

The stalk of q⁻¹qF is identified with sections of F on the inverse image of the finite model's principal neighborhood. The comparison uses the actual principal-open germ and the actual inverse-image stalk isomorphism, so…

Global restriction through the actual inverse-image adjunction is surjective for a finite product whenever it is surjective for each factor. The proof uses actual sheaf product projections, preservation of finite product…

The units of the stalk-skyscraper adjunction give a monomorphism from a sheaf into the product of its stalk skyscrapers. The proof uses the adjunction triangle to split every stalk map, then the conservativity of stalks…

Mapping the components of the actual stalk-skyscraper embedding gives a morphism from the inverse image of a sheaf to the product of the inverse images of its stalk skyscrapers. For a finite target space, this is a monom…

For an arbitrary continuous map, the inverse image of a skyscraper is the direct image of discrete-valued continuous functions on the inverse image of its closed support. The comparison is the actual adjoint of the const…

The inverse-image stalk comparison identifies approximation counits with direct-image stalk maps. Refinement acts on germs by restriction between inverse images of open neighborhoods. Taking the neighborhoods to be princ…

The stalk comparison for the chosen sheaf pullback intertwines germs with the unit of its actual pullback-pushforward adjunction. The Lean proofs are original.

The chosen left adjoint defining topological sheaf pullback is compared with sheafification of presheaf pullback. The adjunction units are related using uniqueness of the left adjoint and the unit formula for restricting…

For a continuous map whose image contains a specialization of every point, global restriction through the actual inverse-image adjunction is injective. Surjectivity of this restriction passes to subsheaves. In particular…

Suppose every point specializes to a point of a subset Z. Equality of global sections is detected by their germs on Z. A global section of a sheaf lies in a subsheaf if its germs on Z lie in the subsheaf stalks. The latt…

The actual restriction of supported continuous functions is surjective on global sections under the original hypotheses of Stacks 09ZG. The proof applies the locally constant extension theorem on the closed support; the…

If every point closure meets a closed subset in a connected nonempty set, every clopen partition of the closed subset extends uniquely to the whole space. This proves the topological partition step of Stacks Project, tag…

Let Z be closed in a spectral space X, and suppose every point closure meets Z in a connected nonempty set. The actual inverse-image unit gives a bijection from sections of any sheaf on X to its sections on Z. The proof…

Closed subspaces of spectral spaces are spectral. The connected point-closure intersection condition restricts to each closed subspace, because the closure of any point of that subspace remains in it. Thus the locally co…

The global sections of a finite étale scheme over an affine base form a finite étale algebra. The naturality square of isoSpec identifies the original relative scheme with the pullback of the spectrum of this algebra. Pu…

Canonical aggregate for SchemeTheory.WeilRestriction.

Restriction from schemes over S to schemes over S' identifies the relative internal Hom with the internal Hom of the two pullbacks. The comparison is obtained from pullback pasting and the adjunction between composition…

Isomorphisms of the source and target induce a natural isomorphism of relative internal Hom presheaves. This identifies geometric pullbacks with their affine tensor-product presentations when constructing local represent…

The common lower indices of a locally directed open cover give a cover of each pairwise intersection. They therefore define a 1-hypercover, also in the category of schemes over a fixed base. The relative construction acc…

Given an open cover of a scheme, consider every open subset contained in the image of some member of that cover. These open subsets form a basis, and their inclusion ordering makes the associated open cover locally direc…

Restrict two finite étale schemes to the directed cover by all affine opens of the base. The affine internal Hom representers represent the restrictions of a single sheaf, by the base change comparison. Their canonical t…

The cartesian squares of relative gluing identify each local representer with the pullback of the glued scheme. The resulting hom-set equivalence has an explicit inverse: compose a local map with its gluing inclusion.

The universal section constructed from the local universal elements induces a map from the Yoneda presheaf of the glued scheme. Its restriction to each cover member is a bijection, by the cartesian gluing square and the…

The canonical transitions between local representers preserve their universal elements. These elements therefore form a compatible family on the locally directed cover of the glued scheme. The sheaf condition supplies a…

Local representations of one presheaf on Over S determine relative gluing data on a locally directed open cover. The transition maps and cartesian squares are constructed from universal elements, using the iterated slice…

A representation on schemes over U, obtained by composition along U ⟶ S, also gives a representation on the slice of Over S over U ⟶ S. This is the form needed to glue local representers within the category Over S.

A morphism of sheaves on schemes over S is an isomorphism if its components are bijective on every scheme over a member of an open cover of S. Pulling that cover back to each test scheme supplies the covering sieves need…

Representers of restrictions of a fixed presheaf form a diagram over the base diagram. Its transition maps come from the representing equivalences, so their identity, composition, and pullback properties are consequences…

Restrict a presheaf on C to the slice over each object of C. Given representing objects on two slices, a morphism between the bases determines a canonical morphism between the representing objects. The universal elements…

If a presheaf on schemes over S is represented after restriction to schemes over X, then its restriction along Y ⟶ X ⟶ S is represented by the pullback of that local representer to Y. This transfers local representers to…

For schemes U and V over S, the relative internal Hom presheaf sends T to morphisms over S from T ×ₛ U to V. It is a sheaf for the topology induced on Over S by any subcanonical topology on schemes. The key observation i…