Algebraic curves

Algebraic curves, divisors, function fields, differentials and residues. Includes Riemann–Roch, duality and relative geometric constructions used by the Jacobian library.

Once a divisor reaches the Riemann genus bound, every adele is the sum of an adele bounded by that divisor and a principal adele.

Adelic spaces, indices of specialty and Weil differentials. Valuation bounds and global functions define the quotients and genus conditions.

Repartitions and Riemann--Roch spaces defined by valuation bounds. Principal repartitions give the quotient used for the first cohomology space.

Closedness of fibre zeroth-cohomology dimension bounds, using matrix minors on affine charts.

H0 le one

The Euler characteristic of a two-term complex from its field-base-change kernel and cokernel.

Projective kernels of two-term complexes over a reduced ring. Constant fibre-kernel dimension gives projectivity and bijective kernel base change.

Compatibility of Laurent-chart residues with the map induced by a ring homomorphism.

Compatibility of Laurent-chart residues with restriction from the first chart.

Identification of the integral Čech Serre pairing with the curve Serre pairing.

Divisor-bounded functions on two charts and their Cech cohomology. Chart extension maps the first Cech quotient to adelic cohomology.

Pullback and trace on divisor-section Cech cohomology along an integral field embedding.

Cech finiteness for the module presheaf of a locally trivial module sheaf over a proper scheme.

Comparison of two-chart Cech cohomology with the associated ordered affine cover.

Cech finiteness of the structure presheaf of a proper scheme.

Čech cohomology base-change equivalences for locally trivial module presheaves.

one

Representing degree-zero Čech classes of free graded modules by shifted sections.

Vanishing of the Cech cohomology of projective twists in the stated lower degree range.

Vanishing of positive Čech cohomology of projective twists in the stated degree range.

Writing transition functions of a module trivialisation as products of local units.

Refine a Cech trivialisation along a morphism and compare its transition functions with the pullbacks of the original transitions, including coincident and reversed chart indices.

The transition functions of a module trivialisation are units and satisfy the cocycle identity.

Polynomial bounds on Čech section ranks of tensor powers from a projective presentation.

Invertible

Base-change equivalences for two-chart Cech cohomology of locally trivial module sheaves.

Dimensions of base-changed structure-sheaf Cech kernels and cokernels over an algebraically closed field.

The base-changed structure-sheaf Cech kernel has dimension one for a smooth proper integral curve.

Local constancy of the fibre Euler characteristic of two-chart sections of an invertible sheaf.

A morphism to an affine base supplies the base-ring action on module sections. Restriction is linear for this action, and evaluation on two affine opens and their overlap gives the corresponding two-chart Cech section da…

The integral Serre pairing for Čech cochains on a two-chart cover.

Bijectivity of cokernel base change in the finite-presentation construction for a Cech differential.

Bijectivity of kernel base change in the finite-presentation construction for a Cech differential.

Finiteness of the enlarged kernel used in the finite-presentation construction.

Flatness of the enlarged kernel in the finite-presentation construction.

Projectivity of the enlarged kernel in the finite-presentation construction.

Projectivity and base change of a Cech kernel from surjectivity of the fibre kernel comparisons.

Finiteness of matching sections from finite chart modules and localization on the overlap. A projective-line presentation and its kernel section system supply the comparison.

Finiteness of first Cech cohomology from finite sections on a chart. Localization conditions reduce the quotient to finitely many translated generators.

Fibre dimension data for a finite two-term kernel after pullback to a scheme over the base ring.

Finite free two-term models for Cech kernels and their base changes. A lifted presentation of the cokernel yields a model inducing bijections on all kernels.

The dimension of a Cech kernel after base change is unchanged by a field extension.

Closedness of the locus where a fibre kernel has dimension at least a fixed bound.

Local constancy of the fibre kernel-minus-cokernel dimension of a finite flat two-term model.

Injectivity of kernel base change when the base kernel vanishes.

Equivalences between kernel base changes along a tower of fields.

Transfer projective-kernel and base-change conclusions to a Cech kernel. A finite two-term model with bijective kernel comparisons preserves the fibre dimensions.

Bijectivity of the map from divisor-section Cech cohomology to adelic cohomology.

The Riemann--Roch dimension formula from a two-chart section system reaching the genus.

Finiteness and dimensions of structure-sheaf cohomology over an algebraically closed field.

Finiteness of structure-sheaf cohomology of a smooth proper integral curve.

Finite adelic first cohomology from a two-chart Cech system reaching the genus.

Dimensions of sheaf cohomology from chartwise identifications with divisor-bounded function spaces.

The index of specialty is the dimension of first adelic cohomology. The adelic and repartition models are identified by their common bounded families.

Adelic families are precisely repartitions, using a divisor bound for their valuations.

Divisor-bounded repartitions are precisely the bounded adelic families for that divisor.

Equivalences between geometric structure-sheaf cohomology and the two-chart function-field Cech model.

Equivalences between module-sheaf Cech cohomology and divisor-section Cech cohomology.

Identify sheaf Cech cohomology with divisor-section cohomology from chartwise range identifications.

Ring

Trivial

Trivial

This is the pole-control step of the Riemann--Roch proof of Tsen's theorem (Stacks Project, Tag 03RD). Multiplication is supplied by the existing divisor theory.

Dimensions of Riemann--Roch spaces under translation by the divisor of a nonzero function.

A divisor of negative degree has no nonzero Riemann--Roch sections.

Equality of the function-field genus from equality of the Riemann--Roch dimension differences.

Existence of a canonical divisor and the Riemann--Roch genus formula over an algebraically closed field.

For a form of degree d in n > d variables, the number of coefficients of n functions with poles bounded by mD eventually exceeds the dimension of the space containing the evaluated form, even after allowing a fixed divis…

Approximation with a prescribed valuation bound from a place where the Riemann genus is reached.

Existence of a genus and the Riemann index formula for a curve function field.

The Riemann index formula from existence of the Stichtenoth genus. Adelic quotient comparisons and a pole-divisor package control the dimensions.

Vanishing of the index of specialty for sufficiently large multiples of a place divisor.

Find a divisor-bounded chart section realizing the prescribed valuation at a genus-reaching place.

Bounded adelic quotients and the diagonal embedding establish finite dimensionality of each Riemann–Roch space from finite dimensionality of the space for the zero divisor.

Function-field Riemann-Roch over an algebraically closed constant field, using the residue theorem.

Function-field Riemann-Roch for an algebraic curve over an algebraically closed field.

Function-field Riemann-Roch from the residue theorem over algebraically closed constants. Transcendence towers, pole corrections and residue pairings supply the genus and duality arguments.

The function-field genus is invariant under an algebra equivalence. Transport of places and repartitions identifies the defining quotient spaces.

Riemann--Roch supplies a nonzero section of every degree-one divisor. Its effective divisor is a single place. The same dimension calculation proves uniqueness: a function with at most one simple pole must be constant.

Bounded adelic quotients give finite dimensionality and the Riemann–Roch dimension formula for the index of specialty when a divisor reaches the genus bound.

Finiteness of differential-dual spaces from a place where the genus is reached. Adelic quotient and residue-pairing comparisons give the dimension bounds.

The boundary upstairs is the actual union of valuation fibers. Its weighted cardinality is obtained from the finite-extension degree formula. Thus the boundary correction cancels the ramification term for an extension th…

Choose finitely many chart points whose subtraction decreases the Riemann--Roch dimension as prescribed.

The dimension bounds for Riemann–Roch spaces show that every divisor above a divisor reaching the genus bound attains the same value of degree minus dimension.

Existence of the Stichtenoth genus for a curve function field with base-field constants.

A positive-degree homogeneous form with more variables than its degree has a nonzero zero over a finite separable extension of K(x), where K is algebraically closed. The proof uses existing principal-divisor and Riemann-…

Function-field Riemann--Roch and Weil duality statements. The index formula, adelic duality and differential-space dimensions are compared.

Integrally Closed

Local Section of forall subsingleton HSucc

Compatible local two-term models recording the degree-zero fibre dimensions on a scheme.

The small fppf site and its abelian sheaf cohomology.

The structure-sheaf module presheaf associated with a scheme module and its restriction maps.

surjective proj H0Map

Transposition of the identity Leray double complex.

support zero Scheme Ideal eq empty

Base change for Čech cochains of locally trivial sheaves of modules.

support zero Scheme Ideal

Coherence of the module presheaf associated to a locally trivial module sheaf.

Quasicoherence of the section presheaf of a locally trivial scheme module. Quasicoherence of the presheaf associated to a locally trivial module.

Exactness of positive Cech degrees for a quasicoherent module presheaf on an affine cover. An insertion homotopy and localization on basic opens establish the kernel-range inclusion.

Ordered Čech restriction, extension, and pullback identities.

Ordered Čech restriction, extension, and pullback identities.

eq

Independence of degree-one cohomology from the ordered affine cover.

The Euler characteristic change induced by tensoring with the line bundle of a relative Cartier divisor.

Recover an effective relative Cartier divisor and its defining section from the Euler characteristic of an invertible sheaf.

Module tensor and module tensor

tensor pow module tensor eq add sum

tensor eq add mul

sub mul

The Euler characteristic change under tensoring with an invertible ideal inverse module. Chartwise maps and the thickening short exact sequence give the cohomology dimension identity.

Nontrivial degree-zero sections of an invertible sheaf from an Euler characteristic bound.

Vanishing of degree-one cohomology of an invertible sheaf from an Euler characteristic bound.

ker eq

Uniformizer differentials and finite-type valuation-ring models give spanning criteria for the Kähler differential module of a curve function field.

Extension

pullback Along of swap

Find a separable transcendental coordinate when the differential module has rank one.

The differential of a transcendental coordinate is nonzero.

The differential of a transcendental coordinate spans the differential module.

Residue functionals of nonzero Kähler differentials, their canonical-divisor bounds, and the associated residue pairing.

Singleton bases for polynomial and rational-function differentials and their separable field extensions.

Closed

Pullback, trace, and correspondence maps for Kähler differentials along base-field algebra homomorphisms.

Uniformizer differentials, their coefficients, and differential orders at places of a function field.

Local residue data, traced differential residues, and residue functionals on adeles.

Results on Canonical.

Results on Construction.

The compatibility of residue sums over a place fibre with differential pullback and field trace.

Separable extensions with generating coordinate differentials satisfy the fibre residue identity.

The rational-function-field residue theorem and fibre trace identities give the residue theorem over algebraically closed base fields.

Canonical rational-function residues, partial-fraction generators, and coordinate independence establish the residue theorem in every characteristic.

Transfer the residue theorem from its base-field formulation.

A residue theorem for the rational-function field and completed residue-trace compatibility yield the extension residue theorem.

Compare residues, traces and completions.

pullback Along

Agreement between the local Tate residue constructions.

Compare the second Tate residue constructions.

The chain rule for Tate residue constructions.

Compatibility of Tate constructions with finite extensions.

Finite-rank traces and Tate commutators on completions, with residue agreement and completed trace identities.

Compatibility of Tate residues with trace in separable function field extensions.

A chosen uniformizer in each place valuation ring and its order and nonvanishing properties.

Canonical divisors, their divisor classes, and the genus obtained from the order of a nonzero differential.

Places, divisors and divisor class groups of a field extension. The valuation orders define principal divisors and the degree-zero Picard group.

Sending places to their actual valuation extensions transports divisor evaluation through the coefficient embedding. The comparison follows from residue evaluation, including the negative multiplicities in divisors.

Transport of field structures, places, divisors, and degree-zero Picard groups along base-field algebra homomorphisms.

Compute the degree of a divisor as a sum of weighted coefficients.

Compute the degree of a divisor by summing over its support.

Evaluation of a divisor on a sum.

Evaluation of a divisor on a product.

Evaluate the difference of two single-point divisors.

Evaluate integer powers against divisors.

Evaluation of integer multiples of divisors.

Index Along eq one

single

Finite-type valuation-ring charts and separating coordinates produce canonical divisors for curve function fields.

Nonzero functions in a finite separable rational-function-field extension have finitely supported order divisors.

Principal divisors for separable function fields with a transcendental coordinate.

Uniformizer-independent differential orders and rational-function coefficients construct canonical divisors over perfect fields.

Division divisors produce explicit roots by evaluation. The pointed formula retains the basepoint normalization, with no condition on the characteristic.

Restriction of places and residue fields, ramification indices, and divisor pullback and pushforward over field extensions.

Pole-divisor bounds, coordinate towers, and independent bounded function families for function fields.

Extension

Semilinear automorphisms act compatibly on valuation rings, residue fields, and degree-zero divisor classes.

divisible

Abs resultant

Stalk eq

smul D eq

eq

Relate kernel and cokernel dimensions along an exact sequence.

The locus where a linear map is surjective after residue-field base change is open.

The equalizer of the descent maps is the descended submodule. Tensor calculations identify its base change and verify the descent square.

Field le range

Field le range

Fibre localization comparisons reduce finite-presentation flatness to flatness of residue-field tensor fibres.

range

Shows that a finite projective module with one-dimensional fibers is invertible.

Descends invertibility and linear equivalences after base change to a finite stage.

Descend a finitely presented module to a stage of a direct limit.

Descends a linear equivalence of finitely presented modules to a compatible finite stage.

Lifting projective modules across a square-zero quotient using base change.

Lift compatible projective-module identifications across a square-zero quotient.

Compare projective modules after base change across a square-zero quotient.

Field

Change eq

Relates localization and constant stalk rank to finite presentation.

Preserve module rank under a square-zero quotient identification.

Transfers rank one at every prime to dimension one over a field algebra.

Compares ranks at stalks using module equivalences after localization.

Constructs exterior powers of module presheaves and the maps induced by module morphisms.

Finite locally free equivalence relations on rings yield the invariant-ring tensor-square pushout comparison.

Relates tensor products and internal hom constructions for sheaves of modules.

Cancels a tensor factor equipped with a tensor inverse in a braided monoidal category.

Evaluation and curried evaluation are isomorphisms for tensor-invertible objects.

Finite wide pullbacks decompose into binary pullbacks, preserving the required morphism properties.

of forall exists iso pull Functor obj

Detects an isomorphism of sheaves from its components on a basis of open sets.

kaehler Differential eq one

A tensor-product coordinate-relation quotient is identified with a polynomial-ring tensor product for finrank calculations.

Unramified

Localization

Prime of mem non Zero Divisors

Homogeneous prime avoidance constructs a positive-degree homogeneous element outside finitely many prime homogeneous ideals.

Equality of the two tensor-square images is the descent condition for an ideal along a faithfully flat algebra.

Independent

eq

add

A flatness criterion for a tower of local rings and its residue quotient.

of henselian Local Ring

Mem

Spectrum

Subalgebras of finite-dimensional fraction-field extensions of Noetherian domains of Krull dimension at most one are Noetherian and have Krull dimension at most one.

Mem

The dual-number counterexample records why a smoothness hypothesis is needed.

is Local Ring

le one

Deduce flatness from vanishing residue-field Tor for finite modules over local Noetherian rings.

Zero univ

eq map sup span

eq span pair

pair

An intermediate algebra that is finite in the fraction field satisfies the Krull–Akizuki finiteness and dimension bounds. Length estimates for scalar-multiple quotients and finite lattices provide the supporting module a…

Prime

Construct a two-chart Cech Grothendieck complex over a local ring.

MulAction), names suffixed Finsupp 404-412, names suffixed Finsupp GroupWithZero/Action/Basic.lean:89-92 and :104-112, Ring/AddAut.lean:32), lemma names primed Mathlib/Algebra/GroupWithZero/Action/Basic.lean:104-112: the…

range

Separable

Flatness over algebraically closed residue fibres gives non-zero-divisor and quotient flatness criteria.

The fraction field of a scalar-extended affine coordinate ring is generated by the new constants and the image of the old function field. This lemma uses the tensor-product description of the coordinate ring, rather than…

zsmul add

Coordinate level sets of a flat polynomial algebra are finite and free with the prescribed finrank.

Pow

Pow

Closure

This is the dimension-theoretic input to the Riemann--Roch proof of Tsen's theorem. It strengthens the homogeneous case in Stacks Project, Tag 03RB: the equations need only vanish at the origin. https://stacks.math.colum…

This is the coefficient-coordinate step in the Riemann--Roch proof of Tsen's theorem: after bounding the poles of a polynomial expression, its coefficients lie in a finite-dimensional space. Coordinate functionals turn t…

imp

Pow

range

A continuous finite-valued cocycle descends to an actual finite Galois intermediate field. Tsen supplies vanishing of its actual field-unit H² class. The existing Hilbert-90 and Kummer correction gives a continuous mod-p…

A separable algebraic function-field extension satisfies the completed trace-sum identity, using semilocal completions and ramification and inertia degrees.

A place of degree one identifies the constant field with the base field.

A rational place of nonzero degree identifies the constant field with the base field, using the degree of principal divisors.

Function fields of curves over a base field. The curve condition records principal divisors, finite residues and rank-one differentials.

Tsen supplies the norm preimages in the existing actual group-cohomology calculation. This is the finite cyclic step, not a claim about all étale cohomology of a curve.

The function field of an integral scheme locally of finite type over a field is essentially of finite type over that field.

A function outside the image of an algebraically closed base field defines an embedding of the rational function field that sends its variable to that function.

The Sylow fixed fields remain one-variable function fields. Their relative Galois groups are p-groups, so the previously proved vanishing applies. The finite-index trace detects vanishing in the original actual group-coh…

An integral curve locally of finite type over a field has infinitely many closed points.

Rational function fields have finite residue fields at their places and a free module of Kähler differentials of rank one.

A curve function field over a perfect field admits a separating transcendental element, with bases of differentials transported through the generated intermediate field.

A finite separable extension of the field generated by a transcendental element is a curve function field.

The actual algebra norm is represented by a homogeneous form of degree equal to the extension dimension. Tsen applied to N(Y) - a Z^d gives a nonzero point. Anisotropy of the field norm forces Z to be nonzero, so divisio…

A central prime-order subgroup supplies an actual intermediate field. Tsen kills the cyclic upper extension, induction kills the lower extension, and the existing unit H² inflation-restriction exactness kills the origina…

Smoothness, properness, connected fibres and existence of a relative group law over an affine base.

Extend the map (x,y) ↦ q(x/y) from D(y) to the affine plane. Pulling this extension back by (x,y) ↦ (xy,y) agrees with q(x) on D(y), hence everywhere by separatedness. Restriction to y = 0 proves constancy.

The existing morphism G.mulRight f idPoint represents multiplication on every test scheme. Naturality supplies its unit identities and its relation to the actual multiplication-by-an-integer morphisms, over any commutati…

The actual torsion levels of the additive group of algebraic points identify with points of the multiplication kernel. For a proper smooth commutative group scheme over an algebraically closed field of characteristic zer…

Each standard chart is the actual affine line. Their constant values agree at the common rational point with homogeneous coordinates (1,1).

zero

Descend a degree-zero coboundary from the unit pullback using the comparison of sections over the base.

The action on the maximal ideal controls infinitesimal points of a polynomial endomorphism.

Formal unramifiedness and smoothness of the two structure maps imply etaleness. This criterion applies to multiplication maps of a smooth relative group law.

Finite Presentation

Component

The identity component is an irreducible open subgroup of finite index.

one

The genus is defined by the actual function field of the base change to an algebraic closure. It needs neither a rational point nor a chosen affine cover. For a smooth proper geometrically integral curve it equals the di…

A finite extension embeds in an algebraic closure of the original field. Actual Cech cohomology and the function-field isomorphism of the two iterated pullbacks then compare the genera. The auxiliary rational point is on…

If a composite is geometrically connected and its first map is surjective, the second map is geometrically connected.

A flat, universally open, geometrically integral morphism has an integral total scheme when its base is integral.

The public theorem GeometricallyIrreducible.geometricallyConnected is owned by SchemeTheory and remains available through this existing import path.

For a morphism from an integral proper smooth curve to an integral proper smooth scheme over an algebraically closed field of characteristic zero, bijectivity on rational points implies that the original morphism is an i…

Scalar extensions of smooth proper curves, their sections and their basic fibre properties.

Two affine charts cover the curve, with reciprocal coordinates on their intersection. The coordinate maps are finite, and their level sets have the specified common free rank. The associated affine cover and the generic…

A finite-map presentation pulls back along an algebra map with the same exponent, pulled-back charts and pulled-back coordinate functions. Finite local base extensions also preserve the generic etaleness of its level set…

The two coordinate functions in finite-map data glue to a morphism to the projective line. Its chart preimages are the given affine opens and its projective coordinate sections pull back to the original functions.

Finite-map data on a smooth proper curve gives an affine open containing prescribed finitely many points over a fixed affine open of the base.

Localization expresses sections on a basic open using a denominator power. Finite maps on the two affine charts then give finite zeroth and first Cech cohomology for the associated line bundles.

Finite-map data on a smooth proper curve gives finite zeroth and first two-chart cohomology for a module that is locally trivial.

Finite-map data for line bundles on a smooth proper curve imply that sections after base change to an algebra are identified with that algebra by the canonical algebra map.

Closed

The pullback of a smooth proper curve to an algebraically closed field is isomorphic over that field to the scheme of a curve model.

An algebraically closed fibre of a smooth proper curve admits a curve model whose function field has a canonical divisor and satisfies the Riemann--Roch theorem.

Finite map data of arbitrarily large invertible degree.

Finite map data from a two-affine open cover.

Sections of sufficiently large degree disjoint from the marked section.

Space

Data

A smooth proper curve with a two-affine-open cover over a local Noetherian base has one genus that agrees with every Riemann--Roch genus on its algebraically closed fibres.

Sections of an inverse ideal power disjoint from the marked section.

Lifting a section away from the support over a maximal ideal.

Affine Open Cover

pi

A two-affine open cover determined by a section.

A generator of a power of the ideal of a section of a smooth proper curve gives a free quotient of affine sections with the rank prescribed by that power.

Fibrewise Riemann-Roch determines H0 and the vanishing of H1 for sufficiently large powers of the inverse ideal module of a section, after arbitrary field base change.

Connected

An integral scheme locally of finite type over an algebraically closed field is geometrically integral, using the domain property of tensor products of affine sections.

A nontrivial scalar extension of the section ring of an affine open in a geometrically integral scheme to a field is a domain.

span eq top

Square-zero lifts identify tangent points with linear maps from the cotangent space.

Flatness, surjectivity and quasi-compactness are the only hypotheses used. In particular inseparable finite extensions of fields are covered.

The quotient of the actual finite locally free equivalence relation associated with a covering action supplies its descended scheme. Finite presentation is sufficient; no separability of the covering algebra is needed. I…

The descended universal element is retained explicitly. Consequently its classifying equivalence agrees with the fixed local representation, a fact needed to compare group laws rather than merely isomorphism classes of r…

The global classifying equivalence preserves the operations constructed on matching local points. Equality is checked after the actual descent cover using separatedness.

Matching local elements form a subgroup. The actual matching equivalence transports its operations to relative points of the descended scheme.

This identifies points of a descended scheme with the compatible elements of the presheaf represented after base change. The presheaf is not assumed to be a sheaf.

Multiplication tables and their reductions construct a local coboundary near a monogenic fibre.

On an integral curve smooth of relative dimension one over a field, every point other than the generic point has a closed singleton.

An isomorphism of integral schemes over a field induces an algebra equivalence of their function fields.

Places of a function field of a curve have degree at least one. Principal-divisor shifts of Riemann--Roch spaces are implemented by multiplication and division.

Fibrewise algebraic equivalence to zero and its pullback-stable condition on rigidified line bundles.

Algebraically trivial invertible modules are closed under tensor products, inverses and pullback, giving the associated sub-Picard group condition.

Fibrewise section conditions for charts of the relative Picard functor. The conditions combine Riemann--Roch with point removals prescribed by sections.

A Cartesian identification of a fibre transports a two-affine-open cover and induces linear equivalences on the zeroth and first cohomology of the corresponding modules.

This file defines invertible sheaves of modules and line bundles rigidified along a chosen section. Isomorphism classes of rigidified line bundles form a presheaf under base change, with the unit bundle as its distinguis…

Conjugate Cech complexes identify kernels and cokernels. Transport along scheme isomorphisms and constancy in a connected family show that tensoring by an algebraically trivial invertible module preserves the Euler chara…

The pullback square associated with baseChangeSnd along a relative scheme morphism.

Compatibility of section ideals, their powers and associated section twists with scalar- extension pullback.

of is Direct Limit

Scalar extension of Picard conditions and the induced equivalences of rigidified line-bundle classes.

Tensor products and the commutative-group presheaf associated with a group-stable Picard condition.

Presheaves of rigidified line-bundle classes satisfying a pullback-stable Picard condition.

Group laws on test-scheme points over an affine base and their naturality.

Conversions between pointwise relative group laws and group objects over the base.

Adjust an isomorphism of line bundles by a global unit so that it respects the given rigidifications.

Prove uniqueness of rigidified line bundle isomorphisms from universal bijectivity on global sections.

Prove uniqueness of isomorphisms respecting rigidifications when the base-change map on global sections is surjective.

Compatible local isomorphisms of rigidified line bundles descend over an open cover when the structural map has bijective global sections after base change. Chosen fibre products and section pullback isomorphisms track t…

Cocycle

Morphisms between affine scalar-extension stages and their pullback-chart preimages.

Pullback-stable conditions on rigidified line bundles, containing the unit and respecting isomorphism.

The geometric-fibre vanishing and zeroth-cohomology rank of a sufficiently large section twist descend along algebraic closure to every field fibre.

Twisting a fibrewise algebraically trivial rigidified module sufficiently far by the section makes geometric-fibre first cohomology vanish and gives zeroth-cohomology rank from the twist exponent and genus.

This presheaf requires no section of the curve. Choosing a section gives a natural equivalence with the existing rigidified Picard presheaf by normalizing along it. No assertion of the sheaf property is included.

The geometric-fibre condition is invariant under tensoring with a base line bundle. It therefore defines an actual subfunctor of relative classes. At a chosen section, normalization identifies this subfunctor with the ex…

The canonical isomorphism between iterated pullbacks identifies relative classes over an extended base with restriction of the original presheaf. The comparison preserves the actual geometric-fibre condition and requires…

Tensor product and actual tensor inverses give the group structure without a section. Pullback is a group homomorphism.

Forgetting rigidification preserves tensor products on actual representatives. The normalization equivalence is therefore an equivalence of commutative groups.

Immersion of flat of locally Of Finite Presentation

Immersion

Immersion

subsingleton HSucc

Local homogeneous fractions identify shifted graded sections with twisting-module sections.

Projectivity of sections of locally trivial scheme modules on affine open subsets.

Gluing an invertible scheme module from compatible projective chart modules and identifying its sections.

Projectivity, finiteness and fibre rank one for sections of an invertible module on affine charts.

Relative affine spectra and finite-subalgebra descent and equality-detection conditions.

A locally finitely presented morphism admits factorizations and eventual equalities over the affine inverse systems arising from finitely generated subalgebras.

A scheme over an affine base is locally of finite type if every affine test map factors through a finitely generated subalgebra over the base. Basic-open localizations transport these factorizations around a point.

Extend a family of locally finitely presented maps to open immersions covering the total presheaf.

Tensor products at finitely generated subalgebra stages and their directed-limit maps.

The natural cocone of finitely generated subalgebras presents the original algebra as its colimit in the category of commutative rings.

Applying the spectrum functor to the colimit presentation by finitely generated subalgebras gives the canonical limit cone with the spectrum of the original algebra as its vertex.

A closed point of a nonempty scheme locally of finite type has a finite residue field. Its actual residue-field morphism gives a section after base change. No separability or characteristic assumption enters the construc…

Flatness on a finite affine cover descends to finitely generated subalgebras and is combined at a common stage.

The tensor-product description of sections on a base-changed affine open proves that its function field is generated by the new constants and the image of the original function field. Compatibility with germs specifies t…

The germ comparison of the geometric projection forces its action on the original constants. This supplies the scalar tower used by divisor conorm and Weil evaluation without assuming a comparison of coefficient maps.

The image of the section ring of a nonempty affine open in the function field is the intersection of the images of the stalks at points of that open.

Compact

If the first morphism is universally closed and surjective, separatedness of the composite implies separatedness of the second morphism.

A finite, flat, surjective first morphism allows local finite type of its composite to descend to the second morphism over a locally Noetherian base.

The kernel of a coproduct map gives a two-term truncation. When its cokernel is finite, a chosen free presentation and projective lift produce the Mumford truncation maps.

Regularity ascends from a quotient by a regular sequence. The final examples show how this applies to p-adic integers and why regularity of the sequence is necessary.

Rigidified line bundles, their tensor products and tensor inverses, and compatibility with pullback.

Scheme morphisms compatible with chosen structure morphisms form a subtype. This file constructs their identities, composition, and actions on points, and identifies them with morphisms in the over category. It also reco…

Morphisms commuting with their structure maps induce morphisms of the base-changed schemes. Their projections, identities, compositions, and induced module comparisons are compatible.

Field

When the first finite flat morphism has constant rank, the rank of its composite with a second finite flat morphism is the product of that constant and the second rank.

Finiteness, flatness and rank of thickenings of a section cut out by powers of its kernel ideal.

Invertibility of the ideal of a section of a smooth curve and its affine retraction calculations.

exists div

An isomorphism of schemes identifying two closed immersions transports powers of their kernel ideals and the associated inverse ideal modules compatibly.

Local trivializations identify invertible-module sections with rational functions. For a rational point whose ideal power is generated by a section, the corresponding valuation has that power as its order at the point an…

A transcendental section on a nonempty open of an integral smooth curve defines a map to the polynomial spectrum whose point fibres are finite.

For an integral proper curve, the maximal open on which a function is regular maps properly to the polynomial spectrum. The valuative criterion extends points through stalks and compares their specializations.

For a nonempty open of an integral scheme, the image of its section ring in the function field equals the intersection of the images of the stalks at its points.

preimage

Rank-one fibres and finite cohomology identify the base ring with global sections after base change. Localizations compare the algebra map with the corresponding scalar-extended Cech kernel.

Vanishing of the first cohomology in each fibre makes the Cech kernel finite and projective and its base-change map bijective. The adjunction unit on global sections is surjective after a surjective change of the base ri…

Scalar-extension equivalences of affine-chart rings and the induced two-chart Cech kernel and cokernel maps.

After square-zero base change, the two affine chart rings and their overlap are quotients of the corresponding chart rings, compatibly with restriction maps.

An affine open of the base identifies its chart-ring spectrum with the open and gives compatible Cartesian presentations of the curve pullback and chart modules.

apply eq kaehler To Function Field

Compatible lifts of the two chart quotients identify scalar extension to the overlap with overlap sections, compatibly with restrictions and adjunction unit sections.

Global sections of a module identify linearly with zeroth cohomology of the two-chart section complex, by restriction to the two opens.

A scheme isomorphism and a compatible module isomorphism transport a two-affine-open cover and give linear equivalences on its zeroth and first section cohomology.

A locally trivial module has scalar-extension equivalences for sections on the two affine charts and their overlap, compatible with restrictions and adjunction units.

Overlap section equivalences for invertible scheme modules after scalar extension on two affine charts.

LE

For a two-affine-open cover, sections of the unit module and structure-sheaf sections give canonically equivalent zeroth and first Čech groups.

Transport of affine-chart section rings between scalar-extension stages along a tower of algebras.

Compatible scalar-extension equivalences of locally trivial module sections at an affine algebra stage.

For a locally finite type structure morphism, sections on an affine open of its source form a finite type algebra over the base ring with the canonical chart algebra structure.

For a proper scheme over a Noetherian affine base, the zeroth and first cohomology of the structure-sheaf section complex of a two-affine-open cover are finite modules.

Pushing an invertible module forward along a morphism finite over the field gives finite zeroth cohomology, vanishing first cohomology, and the rank formula for the zeroth group.

The base-change equivalences of sections on two affine charts and their overlap identify zeroth-cohomology rank and the vanishing of first cohomology across a field extension.

The unit module on an integral smooth proper curve over an algebraically closed field has zeroth cohomology of rank one and first cohomology of rank equal to the genus.

For a flat scheme over an affine base, the sections on an affine open are flat over the base ring with the algebra structure induced by the scheme morphism.

For an invertible module on a proper scheme with a two-affine-open cover, the base points with vanishing first cohomology on the fibre form an open subset.

Bundle

An isomorphism of invertible scheme modules obtained from compatible linear equivalences of chart sections.

Compatible quotient-ring and section comparisons on a two-affine-open cover identify the pullback of a lifted invertible module with the original module after base change.

For a locally trivial module on a separated scheme, vanishing first cohomology computed on one two-affine-open cover gives vanishing on any such cover.

Global sections identify with degree-zero Cech cohomology for a two-affine open cover. The sheaf condition supplies a ring equivalence with the equalizer of chart restrictions.

Degree-zero Cech cohomology computes global sections and supplies the base-change comparison used in the final statement.

A finite locally free equivalence relation on an affine scheme admits an affine quotient with the expected coequalizer property and finite locally free quotient map.

iff

An integral scheme smooth of relative dimension one over a field has a discrete valuation ring as its stalk at every closed point.

A section of an integral smooth curve over a field determines a closed point whose stalk is a discrete valuation ring.

Kähler differentials and their Čech data on a two-affine-open cover.

Transfer bijectivity of algebra maps on affine base changes to sections of arbitrary base changes.

Dimension one

A morphism from a reduced product over an algebraically closed field that is constant on one slice of a proper integral factor descends to the second factor.

Presentation

Separated

of hom

Finitely many points of a scheme affine over a projective spectrum lie in a common affine open, obtained from a homogeneous basic open of the projective spectrum.

Cut

Dimension one

Restrict pullback snd

snd

Finite

Over an algebraically closed field, a closed point of a scheme locally of finite type is the image of the closed point under a morphism over the field.

The existing public statement is retained as a specialization of the unrestricted Henselian section-lifting theorem in SchemeTheory.

Local trivializations compare section ranks and characterize injectivity of the unit map.

Closed Immersion

Noetherian

Reducedness of étale algebras and local standard-smooth presentations establish reducedness of smooth schemes over a field.

A proper integral scheme smooth of relative dimension one over a field cannot be affine.

The ideal kernels of graphs commute with base change, as do their finite products.

Tensoring an algebraically trivial invertible module with a sufficiently large inverse power of a point ideal gives vanishing first cohomology and the Riemann--Roch rank.

The stalks of an integral scheme smooth of relative dimension one over a field are valuation rings, as shown using local standard-smooth presentations.

Ring

Compatible linear maps on ideals over affine opens admit module operations, composition, and ideal-sheaf ranges.

Constructs the module morphisms associated to an ideal sheaf and its closed subscheme.

The subscheme pullback map induces an ideal-module morphism and its adjoint pullback comparison.

Iterated pullback comparisons determine base change morphisms by adjunction, with compatibility formulas for units, counits, and sections.

Presheaf exterior powers descend through sheafification to exterior-power functors on module sheaves; their objects define the determinant notation.

Identifies internal hom sections with natural linear families and morphisms of restricted modules.

Defines local freeness by trivializations on neighborhoods of every point.

The monoidal pullback comparison and adjunction counit define a projection morphism and its mate under the pullback-pushforward adjunction.

The original public declarations now live in SchemeTheory.Modules.PushforwardRestrict.

Tensor a module with the pullback of the dual of its restriction to a chosen section. Module isomorphisms induce isomorphisms of these rigidifications.

Local coefficients of a module section generate its zero-scheme ideal. This file supplies restriction and pullback operations, coefficient maps, and the associated closed subscheme.

Imports the maintained tensor power constructions for scheme modules.

Compares pullback of an associated module sheaf with extension of scalars.

Exterior-algebra multiplication by a vector induces natural maps on module presheaves and module sheaves through sheafification.

Defines the ideal and module twists of the rigidifying section after base change.

The unit map to the subscheme defined by an ideal power is an epimorphism, with a short exact complex relating the indicated inverse ideal-module powers.

The inverse module of an invertible ideal admits a function-field presentation. The distinguished inverse-module section is nonzero, and its orders compare the representing divisor with local generators of the ideal.

The module of an invertible ideal has a function-field presentation by affine Riemann-Roch spaces. Its inclusion in the unit module fixes a rational multiplier whose orders relate the presenting divisor to local generato…

The unit map for a closed subscheme and tensoring by locally free module sheaves give short exact sequences. Cokernels for successive powers of an invertible ideal yield the exact sequence of thickened restrictions.

Multiplication of ideal sections induces a tensor map into the structure sheaf. This map factors through the module of the product ideal; for invertible ideals the resulting map is an isomorphism. The affine-local argume…

The inverse module is the dual of the module associated to the invertible ideal sheaf.

Constructs local module trivializations from non-zero-divisor generators of an invertible ideal.

For invertible ideal sheaves on both schemes, the pullback module comparison is an isomorphism.

Multiplication by an invertible ideal sheaf can be cancelled from equality of ideal-sheaf products, using local non-zero-divisor generators.

The inverse module of a product of invertible ideal sheaves is identified with the tensor product of their inverse modules.

Constructs the isomorphism between the product ideal module and the tensor product of its invertible factors.

When an ideal sheaf and its inverse image are invertible, their inverse modules are identified by pullback.

Invertibility is preserved by each natural-number power of ideal-sheaf data.

The canonical section of the inverse module of an invertible ideal sheaf has zero-scheme ideal equal to the original ideal sheaf.

Inverse image along a flat surjective scheme morphism is injective on ideal sheaves. The comparison is checked on affine opens and localizations.

is Discrete Valuation Ring

The product of ideal-sheaf data commutes with inverse image along a scheme morphism.

Ideal-sheaf data agree when their pullbacks to every member of an open cover agree.

Ideal sheaves on the members of an open cover glue when their inverse images agree on common refinements. The ideal on each affine open is determined by its restrictions to transported affine opens in the cover.

The inverse image of an ideal sheaf is computed on affine opens by extension of the original ideal along the induced homomorphism on sections.

An ideal sheaf is invertible if its inverse image is invertible under a finite, flat, surjective scheme morphism.

Proves that tensoring the ideal inclusion by a locally free module preserves its monomorphism.

Scheme Ideal

The canonical map from a pulled-back ideal module to the inverse-image ideal module is locally surjective.

On an affine open, the module inclusion is injective and its range is the corresponding ideal of ring sections.

A morphism of module sheaves is an epimorphism precisely when sections locally lift through its components.

A module morphism is an isomorphism when its pullback is an isomorphism on an open neighborhood of each point.

A morphism is an isomorphism if its components are isomorphisms on opens contained in the members of a cover.

Characterizes monomorphisms of scheme modules by injectivity on sections.

A section that is a frame on an open gives an isomorphism between the restricted pullback of the module and the unit module on every smaller open.

The tensor product of two sections that are frames on the same open is again a frame on that open.

The coefficient ideal of a section lies in its zero-scheme ideal. Under a local trivialization, both ideals equal the principal ideal generated by the coefficient.

The zero-scheme ideal of a section of an invertible module pulls back to the zero-scheme ideal of the pulled-back section.

Compatible local generators identify evaluation against the natural-family dual with the structure sheaf. We compare this model with the categorical dual and prove its invertibility.

Local trivializations identify generators and their duals, and restriction compatibility transports the resulting maps to sheaves of modules.

Uniqueness of tensor inverses identifies the dual of a tensor product with the tensor product of the duals of its invertible factors.

Represent endomorphisms of invertible sheaves uniquely as multiplication by a global function.

An invertible module has a local generator whose restrictions form one-element bases of the section modules on smaller opens.

ker eq zero

An invertible module on a smooth integral curve has a compatible presentation in the function field whose affine images are Riemann-Roch spaces. Local generators recover the valuation of the representing divisor.

The dual of an invertible module is identified with the module of its invertible zero-scheme ideal, compatibly with the dual of the original section.

Proper

flat of is Proper

of flat of is Proper

An invertible module admits a section that is a frame on a neighbourhood of each point, obtained from a local trivialization.

An invertible module with an invertible zero-scheme ideal is isomorphic to the inverse ideal module, carrying its section to the canonical section of that inverse module.

flat of surjective

Finite

forall sections linear Equiv

Finite

Two global sections of an invertible module have a ratio on any open disjoint from the support of the zero-scheme ideal of the denominator section.

quotient is Nilpotent

Compatible local generators define a natural-family dual. Evaluation becomes an isomorphism after sheafification and supplies an invertible tensor inverse.

For an invertible module on an integral scheme, the generic point lies outside the support of the zero-scheme ideal of a nonzero section.

A section of an invertible module is a frame on any open disjoint from the support of its zero-scheme ideal.

For an invertible module on a flat locally finite-type scheme, invertibility of the section zero ideal in every geometric fibre implies global invertibility and flatness of the zero subscheme over the base.

An invertible module has invertible internal-Hom evaluation maps and an invertible map obtained by currying the evaluation after the braiding.

For an invertible module, evaluation against its dual is an isomorphism when applied to the unit module.

A locally surjective morphism between invertible module sheaves is an isomorphism, using unit-module maps under local trivializations and a covering criterion.

An invertible scheme module on the spectrum of a field is isomorphic to the tensor unit.

Local trivializations identify generators and their duals, and restriction compatibility transports the resulting maps to sheaves of modules.

An invertible module on an affine scheme is trivial when its pullback to a square-zero quotient is trivial.

Rigidification of an invertible module commutes with pullback along a compatible square of structure morphisms and sections.

Rigidifying the tensor product of an invertible module with a module pulled back from the base yields a module isomorphic to the rigidification of the original module.

An invertible-module section vanishes after pullback to a field-valued point exactly when that point lies in the support of the zero-scheme ideal of the section.

For an invertible source module, the section transposed from a module morphism vanishes after pullback exactly when the pulled-back morphism vanishes.

Uniqueness of a tensor inverse identifies the pullback of the dual with the dual of the pullback of an invertible module.

Rigidification along a section preserves invertibility and identifies the original module with the rigidified module tensored with the pullback of its value along the section.

Restrict local trivializations to their common open subset and tensor them to prove that the tensor product of two invertible modules is invertible.

surjective

Global sections of an invertible module related by multiplication by a unit have the same zero-scheme ideal.

Local trivializations yield compatible bases of section modules on smaller opens contained in a neighborhood of each point.

Pullback to open subschemes identifies the local trivializations used to establish a fixed rank.

Transfers local freeness of a fixed rank along an isomorphism of scheme modules.

Pullback transports local trivializations through the canonical pullback comparison for free module sheaves.

Local frames extend after multiplying by powers of projective coordinate sections.

V2

Section eq zero iff

The module base-change comparison for a composite square agrees with the horizontal composition of the two comparisons, through the canonical pullback and pushforward maps.

The tensor-sections map of quasicoherent modules is bijective on affine opens.

Canonical pullback transitions and their comparison with the prescribed descent data. All scheme maps and module objects retain their original canonical owners.

Sheafification turns a locally surjective morphism of module presheaves into an epimorphism.

Shows that wedging the exterior power of the first map with the middle module is epimorphic when the quotient is invertible.

When the first map is a monomorphism, a section killed by the second map comes from a section under the first map.

Open le

Sections that locally frame the pullback over a residue-field point also locally frame the original module above a basic open neighbourhood of that point.

Local bases of a module give bases after pullback along a point valued in a field.

The rational function relating two function-field presentations of a module on a smooth proper curve also relates their representing divisors by its orders at the places.

Quasicoherent Cech exactness produces local sections whose differences give the cocycle.

Sections of a pullback are identified with pairs whose images in the common target agree.

Two compatible injective function-field presentations of the same module differ by multiplication by a single nonzero rational function on an integral scheme.

Gluing compatible module morphisms from an open cover and their restriction equations.

Krull Dim lt

The determinant of multiplication computes the coefficient of a norm-module frame.

preimage

An isomorphism from the pullback to an open subscheme to its unit module supplies a frame on that open subset, compatible with further restriction.

Limit

Direct Limit

A Cartesian square identifies the two iterated scheme pullbacks and the corresponding pullbacks of modules, compatibly with both projections.

On an affine open and its affine base change, extending the section module gives the sections of the pulled-back locally trivial module.

Local triviality identifies pulled-back sections with scalar extension on affine opens.

A section of the dual determinant vanishes precisely where the pulled-back map is not invertible.

Tensoring the ideal sequence of a closed immersion with a locally free module gives a short exact sequence. Its quotient is identified with the pushforward of the pulled-back module on the closed subscheme.

The unit module embeds in the function field of a smooth integral curve. On each affine open, its image is the Riemann-Roch space for the zero divisor.

Local trivializations on basic opens and a finite affine cover provide finite generation of module sections over an affine open.

Shows that sections of a locally trivial module have rank-one fibers after field base change.

Detects equality of module morphisms from global sections when the affine comparison is invertible.

Degree-zero Cech cohomology computes global sections and supplies the base-change comparison used in the final statement.

The determinant of a locally free module sheaf of fixed rank is invertible.

The isomorphism property of a module base-change comparison is independent of the chosen scheme realizing the same Cartesian square.

The base-change comparison is an isomorphism when it is an isomorphism on compatible Cartesian presentations over neighbourhoods of every point of the new base.

The comparison is an isomorphism for locally trivial modules along an affine morphism.

The module base change comparison for a pullback square with an open immersion is an isomorphism.

The Cech complex of an invertible module compares sections before and after base change. Flatness, finite cohomology, and vanishing of fibre H1 identify the canonical base-change morphism with an isomorphism on global se…

Base change of module sections on affine schemes when the canonical tilde-to-module comparison is an isomorphism.

Characterizes the global-sections comparison by localization on basic open sets.

Localization conditions on restrictions to basic opens identify the module sheaf with the sheaf associated to its global sections on an affine scheme.

Proves that the global-sections comparison is an isomorphism for locally trivial modules. The tilde comparison is an isomorphism for locally trivial modules.

For a scheme with a two-affine-open cover, the pushforward of a locally trivial module is the sheaf associated to its module of global sections on the affine base.

The projection morphism is an isomorphism for a finite free module, using its biproduct presentation and compatibility with module isomorphisms.

Compatibility of the projection morphism with restriction and pullback on an open subscheme.

Identifies modules locally free of rank one with invertible scheme modules.

Pullback charts of the base provide local trivializations that establish the rank of a pushed-forward module sheaf.

Constructs local trivializations of the pushforward from local trivializations on a finite flat cover.

Finite two-chart cohomology, vanishing fibre first cohomology and constant fibre rank give local freeness of the pushforward of a locally trivial module.

Local finite free descriptions of a module over an affine ring give local trivializations of its associated module sheaf.

For function-field presentations of two invertible modules and their tensor product, the tensor-product divisor differs from the sum of the original divisors by a principal divisor.

Exterior powers of a locally free module sheaf vanish in degrees greater than its rank.

Detects a zero module from vanishing pullbacks on a family covering all points.

The left unitor evaluates a tensor of a scalar section with a module section as scalar multiplication.

For a locally free short exact complex with an invertible quotient, the determinant of the middle term is the determinant of the first term tensored with the quotient.

The standard basis determines a top exterior form and an isomorphism from the top exterior power of a free module sheaf to the tensor unit.

Local determinant frames construct the tensor comparison and glue it to an isomorphism.

Restriction commutes with presheaf exterior powers, and sheafification transports this comparison to pullback of module sheaves.

A map to the pushforward along an open immersion induces an isomorphism after pullback when its components are bijective over opens contained in the image.

support

Over the inverse image of an open where a module is trivial, tensoring with its pullback preserves the restricted pullback of the other module up to isomorphism.

For a closed immersion and a locally free module of finite rank, the canonical projection morphism identifies tensoring the pushed-forward unit with pushing forward the pullback.

Evaluating the dual of a module section agrees with the coefficient obtained from the restricted internal-Hom section and the canonical restriction of the tensor unit.

Projection morphisms commute with maps between the module sheaves being pulled back.

Compare pullback composition isomorphisms along pasted commutative squares on sheaves of modules.

The tensor-unit pullback isomorphism on the canonical unit section, via monoidal sheafification.

Sections of a pullback module are locally spanned by images of sections under the adjunction unit.

Pulling back the projection morphism and composing with the counit gives its adjoint mate.

The affine section module of a locally trivial module sheaf has rank one at each stalk, using the localized module on a trivializing basic open.

Local surjectivity of the second map on inverse images of opens ensures that pushforward preserves the short exact complex.

Sectionwise injectivity, local surjectivity, and local lifting of kernel sections establish short exactness of a complex of module sheaves.

A short exact sequence whose kernel is locally trivial remains surjective on affine sections. Local lifts are compared on intersections and glued to a section over the affine open.

Effectivity of descent data for sheaves of scheme modules on an open cover. Compatible local sections form the glued sheaf and recover the prescribed transitions.

Compatible module morphisms on open charts glue uniquely to a morphism on the scheme. The restriction and pullback comparisons identify this gluing with the module pseudofunctor's descent-data map, which is bijective for…

The fpqc sheaf property of functions gives descent of endomorphisms through pullback.

Right whiskering acts on the first factor of a local tensor section.

Postcomposing a module section with an isomorphism preserves its zero-scheme ideal.

The zero-scheme ideal of a postcomposed module section is contained in the zero-scheme ideal of the original section.

The affine pullback comparison sends a module element represented as a section to the section represented by its scalar extension.

Relates the affine pullback comparison isomorphism to the unit of the pullback adjunction.

Constructs the permutation action on a finite fiber power and records symmetric power properties.

eq

is Homogeneous of le of fg