Associated sheaves of Cartier divisors

For an integral scheme X and a Cartier divisor D, this umbrella exports the construction of O_X(D) and its comparison with the Picard group. It is owned by three modules:

• AssociatedSheaf.RationalSections -- the presheaf of rational functions on an integral scheme, as a presheaf of modules over the structure presheaf;
• AssociatedSheaf.Construction -- local equations, the fractional subpresheaf generated by their inverses, the associated sheaf as its module sheafification, its invertibility, and the tensor comparison;
• AssociatedSheaf.PicardMap -- the zero, principal, and inverse identifications, and the additive map to the Picard group factoring through the divisor class group.

The construction is intrinsic: the fractional presheaf is generated by every local equation. For two equations on the same open, equationTransitionIso gives the canonical change of trivialization, and equationTransitionIso_trans records its cocycle law.

No unconditional pullback theorem is stated. CartierPullbackData supplies a justified function-field pullback for divisors, but a comparison with pullback of module sheaves would also need compatibility between that data, rational sections, and module sheafification. That extra compatibility is not part of the current Mathlib API.

Importing this module is equivalent to the former single-file surface; new code should prefer the narrowest owning module above.

The heavier bridge from associatedSheaf D to explicit LineBundleData lives separately in Divisors.CartierLineBundle. It is intentionally absent from this umbrella so effective-divisor consumers do not acquire the determinant/dual dependency merely by importing the associated-sheaf API.