Transition units for Cartier divisors

Local equations for a Cartier divisor differ by regular units on overlaps. This file packages that unit and exposes the restriction compatibility needed to glue the local copies of the structure sheaf:

• CartierDivisor.transitionUnit chooses the unique unit between two local equations;
• transitionUnit_spec exposes the defining equation for the chosen unit.

This prepares the exact descent datum used in the Cartier-divisor-to-line-bundle construction in Layer A of TauCetiRoadmap/JacobianChallenge/README.md; no smoothness or Noetherian hypothesis is needed for this part. The construction follows Hartshorne, Algebraic Geometry, II.6, and the Stacks Project, Divisors, Tag 02AR. It reuses the local equation and uniqueness theorem from TauCeti.AlgebraicGeometry.CartierDivisor.LocalEquations.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.transitionUnit {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) {U V : X.Opens} (f : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op U)))ˣ) (g : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op V)))ˣ) (hf : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op U))) f = TopCat.Presheaf.restrictOpen D U ⋯) (hg : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op V))) g = TopCat.Presheaf.restrictOpen D V ⋯) : Additive (↑(X.presheaf.obj (Opposite.op (U ⊓ V))))ˣ

The regular unit relating two chosen local equations of a Cartier divisor.

Equations

• D.transitionUnit f g hf hg = Exists.choose ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.transitionUnit_spec {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) {U V : X.Opens} (f : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op U)))ˣ) (g : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op V)))ˣ) (hf : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op U))) f = TopCat.Presheaf.restrictOpen D U ⋯) (hg : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op V))) g = TopCat.Presheaf.restrictOpen D V ⋯) : (AddCommGrpCat.Hom.hom ((toRationalUnitSheaf X).hom.app (Opposite.op (U ⊓ V)))) (D.transitionUnit f g hf hg) = TopCat.Presheaf.restrictOpen f (U ⊓ V) ⋯ - TopCat.Presheaf.restrictOpen g (U ⊓ V) ⋯

The defining equation for transitionUnit.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.transitionUnit_eq_of_spec {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) {U V : X.Opens} (f : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op U)))ˣ) (g : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op V)))ˣ) (hf : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op U))) f = TopCat.Presheaf.restrictOpen D U ⋯) (hg : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op V))) g = TopCat.Presheaf.restrictOpen D V ⋯) {r : Additive (↑(X.presheaf.obj (Opposite.op (U ⊓ V))))ˣ} (hr : (AddCommGrpCat.Hom.hom ((toRationalUnitSheaf X).hom.app (Opposite.op (U ⊓ V)))) r = TopCat.Presheaf.restrictOpen f (U ⊓ V) ⋯ - TopCat.Presheaf.restrictOpen g (U ⊓ V) ⋯) : r = D.transitionUnit f g hf hg

The transition unit is uniquely determined by its defining equation.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.transitionUnit_restrict_spec {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) {U V W : X.Opens} (f : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op U)))ˣ) (g : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op V)))ˣ) (hf : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op U))) f = TopCat.Presheaf.restrictOpen D U ⋯) (hg : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op V))) g = TopCat.Presheaf.restrictOpen D V ⋯) (hW : W ≤ U ⊓ V) : (AddCommGrpCat.Hom.hom ((toRationalUnitSheaf X).hom.app (Opposite.op W))) (TopCat.Presheaf.restrictOpen (D.transitionUnit f g hf hg) W hW) = TopCat.Presheaf.restrictOpen f W ⋯ - TopCat.Presheaf.restrictOpen g W ⋯

The defining equation for transitionUnit remains valid after restriction to a refinement.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.transitionUnit_self {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) {U : X.Opens} (f : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op U)))ˣ) (hf : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op U))) f = TopCat.Presheaf.restrictOpen D U ⋯) : D.transitionUnit f f hf hf = 0

A local equation has trivial transition unit with itself.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.transitionUnit_symm_restrict {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) {U V W : X.Opens} (f : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op U)))ˣ) (g : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op V)))ˣ) (hf : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op U))) f = TopCat.Presheaf.restrictOpen D U ⋯) (hg : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op V))) g = TopCat.Presheaf.restrictOpen D V ⋯) (hW : W ≤ U ⊓ V) : TopCat.Presheaf.restrictOpen (D.transitionUnit g f hg hf) W ⋯ = -TopCat.Presheaf.restrictOpen (D.transitionUnit f g hf hg) W hW

Reversing two local equations inverts their transition unit on every common refinement.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.transitionUnit_cocycle {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) {U V W T : X.Opens} (f : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op U)))ˣ) (g : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op V)))ˣ) (h : Additive (↑((rationalFunctionsRing X).presheaf.obj (Opposite.op W)))ˣ) (hf : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op U))) f = TopCat.Presheaf.restrictOpen D U ⋯) (hg : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op V))) g = TopCat.Presheaf.restrictOpen D V ⋯) (hh : (AddCommGrpCat.Hom.hom ((toCartierDivisorSheaf X).hom.app (Opposite.op W))) h = TopCat.Presheaf.restrictOpen D W ⋯) (hT : T ≤ U ⊓ V ⊓ W) : TopCat.Presheaf.restrictOpen (D.transitionUnit f h hf hh) T ⋯ = TopCat.Presheaf.restrictOpen (D.transitionUnit f g hf hg) T ⋯ + TopCat.Presheaf.restrictOpen (D.transitionUnit g h hg hh) T ⋯

Transition units satisfy the cocycle identity on every triple overlap.