Line-bundle data

This file is the neutral home for a line bundle together with a chosen tensor inverse. The definition belongs with the scheme-level tensor product: it does not depend on divisors, determinants, exterior powers, or the Picard group.

Downstream geometric theories may attach their own interpretations to this common root. For example, Divisors.Determinant constructs Picard-group classes and fixed-rank locally free data, while pullback and projection-formula APIs can use the underlying line-bundle structure directly.

The chosen inverse also makes tensoring by the line bundle an equivalence, with tensoring by the inverse as a specified quasi-inverse. Its adjunction supplies the expected equivalence Hom(L ⊗ M, N) ≃ Hom(M, L⁻¹ ⊗ N). Specializing M to the tensor unit identifies Hom(L, N) with the global sections of L⁻¹ ⊗ N.

These are equivalences of types. Their scalar-linear refinements live in Modules.Tensor.LineBundleLinear, downstream of the monoidal-linear structure on module sheaves. Keeping that dependency separate leaves this file as the neutral categorical root.

structure AlgebraicGeometry.Scheme.Modules.LineBundleData (X : Scheme) : Type (u + 1)

An invertible sheaf together with an explicit tensor inverse.

The two intrinsic invertibility certificates make the underlying sheaves available to generic module-theoretic consumers. The explicit tensor inverse is retained as structure, so downstream Picard and duality constructions do not have to choose it again.

• line : X.Modules
• inverse : X.Modules
• lineIsInvertible : (have this := self.line; this).IsInvertible
• inverseIsInvertible : (have this := self.inverse; this).IsInvertible
• tensorInverseIso : self.line.tensorObj self.inverse ≅ SheafOfModules.unit X.ringCatSheaf

noncomputable def AlgebraicGeometry.Scheme.Modules.unitHomTopEquiv {X : Scheme} (M : X.Modules) : (SheafOfModules.unit X.ringCatSheaf ⟶ M) ≃ ↑(M.presheaf.obj (Opposite.op ⊤))

Maps from the tensor unit are the sections over the top open.

Mathlib first identifies a map from the unit with a compatible family of sections. Since ⊤ is terminal in the category of opens, such a family is equivalent to its component over ⊤.

Equations

• M.unitHomTopEquiv = (have this := M; this).unitHomEquiv.trans ((have this := M; this).val.sectionsEquivOfIsTerminal CategoryTheory.Limits.isTerminalTop)

instance AlgebraicGeometry.Scheme.Modules.LineBundleData.instIsInvertibleOpensCarrierCarrierCommRingCatLine {X : Scheme} (L : LineBundleData X) : (have this := L.line; this).IsInvertible

instance AlgebraicGeometry.Scheme.Modules.LineBundleData.instIsInvertibleOpensCarrierCarrierCommRingCatInverse {X : Scheme} (L : LineBundleData X) : (have this := L.inverse; this).IsInvertible

@[implicit_reducible]

def AlgebraicGeometry.Scheme.Modules.LineBundleData.instCategoryOpens {X : Scheme} : CategoryTheory.Category.{u, u} X.Opens

Equations

• AlgebraicGeometry.Scheme.Modules.LineBundleData.instCategoryOpens = { toCategoryStruct := (Preorder.smallCategory X.Opens).toCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.unit (X : Scheme) : LineBundleData X

The structure sheaf with itself as tensor inverse.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.dual {X : Scheme} (L : LineBundleData X) : LineBundleData X

The inverse line bundle, with the two recorded representatives exchanged.

Equations

• L.dual = { line := L.inverse, inverse := L.line, lineIsInvertible := ⋯, inverseIsInvertible := ⋯, tensorInverseIso := L.inverse.tensorCommIso L.line ≪≫ L.tensorInverseIso }

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.tensorLeftEquivalence {X : Scheme} (L : LineBundleData X) : X.Modules ≌ X.Modules

Tensoring by a line bundle is an equivalence, with tensoring by its recorded inverse as the specified quasi-inverse.

The two composites are reduced to tensoring by L⁻¹ ⊗ L and L ⊗ L⁻¹ using the associator, then to the identity using the two tensor-inverse isomorphisms and the left unitor. Equivalence.mk performs the standard normalization needed for the triangle identity; no rigid or closed monoidal structure is assumed.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.tensorLeftHomEquiv {X : Scheme} (L : LineBundleData X) (M N : X.Modules) : (L.line.tensorObj M ⟶ N) ≃ (M ⟶ L.inverse.tensorObj N)

Moving a line-bundle factor across a Hom uses the recorded tensor inverse.

This is the Hom equivalence of tensorLeftEquivalence; in particular it is natural in M and N through the adjunction API.

Equations

• L.tensorLeftHomEquiv M N = L.tensorLeftEquivalence.toAdjunction.homEquiv M N

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.tensorLeftHomEquiv_apply {X : Scheme} (L : LineBundleData X) (M N : X.Modules) (f : L.line.tensorObj M ⟶ N) : (L.tensorLeftHomEquiv M N) f = CategoryTheory.CategoryStruct.comp (L.tensorLeftEquivalence.unit.app M) (tensorHom (CategoryTheory.CategoryStruct.id L.inverse) f)

The forward Hom equivalence is the adjunction unit followed by tensoring the morphism with the identity of the inverse line bundle.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.tensorLeftHomEquiv_symm_apply {X : Scheme} (L : LineBundleData X) (M N : X.Modules) (f : M ⟶ L.inverse.tensorObj N) : (L.tensorLeftHomEquiv M N).symm f = CategoryTheory.CategoryStruct.comp (tensorHom (CategoryTheory.CategoryStruct.id L.line) f) (L.tensorLeftEquivalence.counit.app N)

The inverse Hom equivalence tensors the morphism with the identity of the line bundle and then applies the adjunction counit.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.lineHomTopEquiv {X : Scheme} (L : LineBundleData X) (N : X.Modules) : (L.line ⟶ N) ≃ ↑((L.inverse.tensorObj N).presheaf.obj (Opposite.op ⊤))

The line-bundle Hom/sections comparison: Hom(L, N) ≃ Γ(X, L⁻¹ ⊗ N).

This is the reusable categorical reduction behind the usual proof that Hom spaces between coherent sheaves on a projective variety are finite-dimensional. Its scalar-linear refinement is lineHomTopLinearEquivOver; the remaining geometric input is coherence of L⁻¹ ⊗ N, after which projective Serre finiteness applies.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.tensor {X : Scheme} (L M : LineBundleData X) : LineBundleData X

Tensor product of explicitly invertible line bundles.

Equations

• One or more equations did not get rendered due to their size.