Linear Hom comparisons for line bundles

The categorical line-bundle equivalences in LineBundle.lean are compatible with scalar actions. Over an arbitrary scheme the scalars are global functions; over a field they are restricted along the structure morphism.

This file supplies only the linear algebra bridge. In particular it does not assert that L⁻¹ ⊗ N is coherent or that its global sections are finite-dimensional.

Main results

• unitHomTopLinearEquiv upgrades maps from the tensor unit to a linear sections comparison;
• LineBundleData.tensorLeftHomLinearEquiv upgrades the tensor adjunction;
• LineBundleData.lineHomTopLinearEquivOver identifies Hom(L, N) with the global sections of L⁻¹ ⊗ N as vector spaces over the base field.

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

Maps from the tensor unit to M are linearly equivalent to the global sections of M.

Equations

• M.unitHomTopLinearEquiv = { toFun := M.unitHomTopEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := M.unitHomTopEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.Modules.unitHomTopLinearEquivOver {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (M : Y.Modules) : (SheafOfModules.unit Y.ringCatSheaf ⟶ M) ≃ₗ[k] ↑(Cohomology.linearGlobalSectionsObj Y M)

The tensor-unit Hom/sections comparison is linear over the base field.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.tensorLeftHomLinearEquiv {X : Scheme} (R : Type w) [Semiring R] [CategoryTheory.Linear R X.Modules] [CategoryTheory.MonoidalPreadditive X.Modules] [CategoryTheory.MonoidalLinear R X.Modules] (L : LineBundleData X) (M N : X.Modules) : (L.line.tensorObj M ⟶ N) ≃ₗ[R] M ⟶ L.inverse.tensorObj N

The tensor-Hom adjunction of a line bundle is linear over every compatible scalar ring.

Equations

• AlgebraicGeometry.Scheme.Modules.LineBundleData.tensorLeftHomLinearEquiv R L M N = L.tensorLeftEquivalence.toAdjunction.homLinearEquiv M N

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

The line-bundle Hom/sections comparison is linear over global functions.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.lineHomTopLinearEquivOver {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] (L : LineBundleData Y) (N : Y.Modules) : (L.line ⟶ N) ≃ₗ[k] ↑(Cohomology.linearGlobalSectionsObj Y (L.inverse.tensorObj N))

The line-bundle Hom/sections comparison is linear over the base field.

Equations

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