instance CartierDivisorScheme.instNonemptyIntegralScheme (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : Nonempty ↥X

Every integral scheme has a nonempty underlying topological space (since it is irreducible).

instance CartierDivisorScheme.instNonemptyTop (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : Nonempty ↥↑⊤

The top open set ⊤ of an integral scheme is nonempty.

noncomputable def CartierDivisorScheme.structureUnitsToFunctionFieldUnits (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty ↥↑U] : (↑(X.presheaf.obj (Opposite.op U)))ˣ →* (↑X.functionField)ˣ

The natural map from units of the structure sheaf on U to units of the function field of an integral scheme, induced by the germ-to-function-field morphism.

noncomputable def CartierDivisorScheme.structureUnitsSubgroup (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty ↥↑U] : Subgroup (↑X.functionField)ˣ

The image inside (X.functionField)ˣ of the units of the structure sheaf on U.

noncomputable def CartierDivisorScheme.CartierDivisorPresheafQuotient (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty ↥↑U] : Type u

The Cartier divisor presheaf on U defined as the quotient K(X)ˣ / O(U)ˣ, modelling sections of K*/O*.

structure CartierDivisorScheme.CartierDivisorDatum (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : Type (u + 1)

A Cartier divisor datum on X (Def 31, Lec 15): a cover of X by open sets Uᵢ, rational functions fᵢ ∈ K(X)ˣ, and the compatibility f_j · f_i⁻¹ is a unit of O(U_i ∩ U_j) on overlaps.

• ι : Type u
• cover : self.ι → X.Opens
• cover_eq_top : ⨆ (i : self.ι), self.cover i = ⊤
• f : self.ι → (↑X.functionField)ˣ
• compat (i j : self.ι) (h : Nonempty ↥↑(self.cover i ⊓ self.cover j)) : self.f j * (self.f i)⁻¹ ∈ (structureUnitsToFunctionFieldUnits X (self.cover i ⊓ self.cover j)).range

def CartierDivisorScheme.CartierDivisorGroupScheme (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : Type (u + 1)

The Cartier divisor group on a scheme X, modelled as the type of CartierDivisorDatum.

@[implicit_reducible]

noncomputable instance CartierDivisorScheme.instInhabitedCartierDivisorGroupScheme (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : Inhabited (CartierDivisorGroupScheme X)

The Cartier divisor group of X is inhabited by the trivial datum.

noncomputable def CartierDivisorScheme.CartierDivisorDatum.principal (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (g : (↑X.functionField)ˣ) : CartierDivisorDatum X

The principal Cartier divisor associated to a rational function g ∈ K(X)ˣ, given by the single-chart cover {⊤} with f = g.

noncomputable def CartierDivisorScheme.CartierDivisorDatum.trivialDatum (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : CartierDivisorDatum X

The trivial Cartier divisor datum on X, corresponding to the principal divisor of 1.

noncomputable def CartierDivisorScheme.toDatum (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (g : (↑X.functionField)ˣ) : CartierDivisorDatum X

Convert a rational function g ∈ K(X)ˣ into the associated principal Cartier divisor datum on X.

theorem CartierDivisorScheme.structureUnitsSubgroup_mono (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] {U V : X.Opens} [Nonempty ↥↑U] [Nonempty ↥↑V] (h : V ≤ U) : structureUnitsSubgroup X U ≤ structureUnitsSubgroup X V

The subgroup of K(X)ˣ coming from O(U)ˣ is contained in that coming from O(V)ˣ whenever V ⊆ U, since restrictions are functorial.