Rigidified line bundles

Let s : T ⟶ Y be a morphism of schemes. A line bundle on Y rigidified along s is a line bundle L on Y together with a trivialization s^* L ≅ 𝒪_T of its pullback along s. Two rigidified line bundles are isomorphic when some isomorphism of the underlying line bundles carries one trivialization to the other.

Rigidified line bundles pull back along commutative squares

T' --s'--> Y'
|          |
g          h
v          v
T  --s-->  Y

by pulling the line bundle back along h and the trivialization back along g. On isomorphism classes this pullback is compatible with identity squares and with stacking squares. Taking for s the base changes of a section of a morphism X ⟶ S to the schemes over S, the classes therefore form a functor of the scheme over S: the rigidified Picard functor (TauCeti.AlgebraicGeometry.rigidifiedPicardFunctor).

Unlike isomorphism classes of line bundles, isomorphism classes of rigidified line bundles remember the trivialization up to the automorphisms of L; an automorphism of L given by a unit u of Γ(Y, 𝒪_Y) rescales the trivialization by the pullback of u along s.

Main declarations

• TauCeti.AlgebraicGeometry.RigidifiedLineBundle s: line bundles on Y rigidified along s;
• RigidifiedLineBundle.trivial: the canonically rigidified structure sheaf;
• TauCeti.AlgebraicGeometry.RigidifiedLineBundle.pullback: pullback along a commutative square;
• TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass s: isomorphism classes of rigidified line bundles, with RigidifiedLineBundleClass.mk_eq_mk_iff characterizing equality of classes;
• TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.pullback, with the functoriality statements RigidifiedLineBundleClass.pullback_id, RigidifiedLineBundleClass.pullback_comp, and RigidifiedLineBundleClass.pullback_trivial;
• TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.toLineBundleClass: forgetting the trivialization, compatibly with pullback (toLineBundleClass_pullback).

References

• S. Bosch, W. Lütkebohmert, M. Raynaud, Néron Models, Section 8.1 (rigidified line bundles).
• S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Section 9.2.

structure TauCeti.AlgebraicGeometry.RigidifiedLineBundle {T Y : AlgebraicGeometry.Scheme} (s : T ⟶ Y) : Type (u + 1)

A line bundle on Y rigidified along a morphism s : T ⟶ Y: a line bundle L on Y together with a trivialization s^* L ≅ 𝒪_T of its pullback along s.

• lineBundle : InvertibleSheaf Y

  The underlying line bundle on Y.

• rigidification : (AlgebraicGeometry.Scheme.Modules.pullback s).obj self.lineBundle.obj ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules

  The trivialization of the pullback of the line bundle along s.

noncomputable def TauCeti.AlgebraicGeometry.RigidifiedLineBundle.trivial {T Y : AlgebraicGeometry.Scheme} (s : T ⟶ Y) : RigidifiedLineBundle s

The structure sheaf, with its canonical rigidification along s.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.trivial_lineBundle_obj {T Y : AlgebraicGeometry.Scheme} (s : T ⟶ Y) : (trivial s).lineBundle.obj = CategoryTheory.MonoidalCategoryStruct.tensorUnit Y.Modules

The underlying sheaf of the canonical rigidified line bundle is the structure sheaf.

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.trivial_rigidification {T Y : AlgebraicGeometry.Scheme} (s : T ⟶ Y) : (trivial s).rigidification = AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso s

The rigidification of the trivial line bundle is the canonical pullback isomorphism.

def TauCeti.AlgebraicGeometry.RigidifiedLineBundle.setoid {T Y : AlgebraicGeometry.Scheme} (s : T ⟶ Y) : Setoid (RigidifiedLineBundle s)

Isomorphism of rigidified line bundles: an isomorphism of the underlying line bundles whose pullback along s carries the first trivialization to the second.

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.RigidifiedLineBundle.pullbackRigidification {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) (L : Y.Modules) (α : (AlgebraicGeometry.Scheme.Modules.pullback s).obj L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules) : (AlgebraicGeometry.Scheme.Modules.pullback s').obj ((AlgebraicGeometry.Scheme.Modules.pullback h).obj L) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit T'.Modules

For a commutative square s' ≫ h = g ≫ s, the trivialization s'^* h^* L ≅ 𝒪_{T'} obtained from a trivialization α : s^* L ≅ 𝒪_T: identify s'^* h^* L with g^* s^* L through the composition isomorphisms of pullback, and pull α back along g.

Equations

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

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.pullbackRigidification_naturality {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) {L M : Y.Modules} (e : L ⟶ M) (α : (AlgebraicGeometry.Scheme.Modules.pullback s).obj L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules) (β : (AlgebraicGeometry.Scheme.Modules.pullback s).obj M ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules) (he : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback s).map e) β.hom = α.hom) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback s').map ((AlgebraicGeometry.Scheme.Modules.pullback h).map e)) (pullbackRigidification w M β).hom = (pullbackRigidification w L α).hom

The trivializations obtained by pullback are natural in the line bundle: a morphism e carrying α to β pulls back to a morphism carrying the pulled-back trivializations to each other.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.pullbackRigidification_id {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (w : CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id T) s) (L : Y.Modules) (α : (AlgebraicGeometry.Scheme.Modules.pullback s).obj L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback s).map ((AlgebraicGeometry.Scheme.Modules.pullbackId Y).hom.app L)) α.hom = (pullbackRigidification w L α).hom

Pulling a trivialization back along the identity square recovers it, through the identity isomorphism 𝟙^* L ≅ L.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.pullbackRigidification_comp {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} {T'' Y'' : AlgebraicGeometry.Scheme} {s'' : T'' ⟶ Y''} {h' : Y'' ⟶ Y'} {g' : T'' ⟶ T'} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) (w' : CategoryTheory.CategoryStruct.comp s'' h' = CategoryTheory.CategoryStruct.comp g' s') (w'' : CategoryTheory.CategoryStruct.comp s'' (CategoryTheory.CategoryStruct.comp h' h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g' g) s) (L : Y.Modules) (α : (AlgebraicGeometry.Scheme.Modules.pullback s).obj L ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback s'').map ((AlgebraicGeometry.Scheme.Modules.pullbackComp h' h).hom.app L)) (pullbackRigidification w'' L α).hom = (pullbackRigidification w' ((AlgebraicGeometry.Scheme.Modules.pullback h).obj L) (pullbackRigidification w L α)).hom

Pulling a trivialization back along two stacked squares agrees with pulling it back along the composite square, through the composition isomorphism h'^* h^* L ≅ (h' ≫ h)^* L.

noncomputable def TauCeti.AlgebraicGeometry.RigidifiedLineBundle.pullback {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) (P : RigidifiedLineBundle s) : RigidifiedLineBundle s'

The pullback of a rigidified line bundle along a commutative square s' ≫ h = g ≫ s: the line bundle is pulled back along h, and its trivialization along g.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.pullback_lineBundle {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) (P : RigidifiedLineBundle s) : (pullback w P).lineBundle = (InvertibleSheaf.pullback h).obj P.lineBundle

The line bundle of a pulled-back rigidified line bundle is the pulled-back line bundle.

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.pullback_rigidification {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) (P : RigidifiedLineBundle s) : (pullback w P).rigidification = pullbackRigidification w P.lineBundle.obj P.rigidification

The trivialization of a pulled-back rigidified line bundle is pullbackRigidification.

def TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass {T Y : AlgebraicGeometry.Scheme} (s : T ⟶ Y) : Type (u + 1)

Isomorphism classes of line bundles on Y rigidified along s : T ⟶ Y.

Equations

• TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass s = Quotient (TauCeti.AlgebraicGeometry.RigidifiedLineBundle.setoid s)

def TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.mk {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (P : RigidifiedLineBundle s) : RigidifiedLineBundleClass s

The isomorphism class of a rigidified line bundle.

Equations

• TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.mk P = ⟦P⟧

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.mk_surjective {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} : Function.Surjective mk

Every class of rigidified line bundles is the class of a rigidified line bundle.

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.mk_eq_mk_iff {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {P Q : RigidifiedLineBundle s} : mk P = mk Q ↔ ∃ (e : P.lineBundle.obj ≅ Q.lineBundle.obj), CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback s).map e.hom) Q.rigidification.hom = P.rigidification.hom

Two rigidified line bundles have the same class exactly when an isomorphism of their line bundles carries one trivialization to the other.

def TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.lift {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {α : Sort v} (f : RigidifiedLineBundle s → α) (hf : ∀ (P Q : RigidifiedLineBundle s), (∃ (e : P.lineBundle.obj ≅ Q.lineBundle.obj), CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback s).map e.hom) Q.rigidification.hom = P.rigidification.hom) → f P = f Q) : RigidifiedLineBundleClass s → α

Descend a function on rigidified line bundles that respects rigidified isomorphisms to their isomorphism classes.

Equations

• TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.lift f hf = Quotient.lift f ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.lift_mk {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {α : Sort v} {f : RigidifiedLineBundle s → α} {hf : ∀ (P Q : RigidifiedLineBundle s), (∃ (e : P.lineBundle.obj ≅ Q.lineBundle.obj), CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback s).map e.hom) Q.rigidification.hom = P.rigidification.hom) → f P = f Q} (P : RigidifiedLineBundle s) : lift f hf (mk P) = f P

Applying lift to a representative returns the original function.

noncomputable def TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.pullback {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) : RigidifiedLineBundleClass s → RigidifiedLineBundleClass s'

Pullback of classes of rigidified line bundles along a commutative square s' ≫ h = g ≫ s.

Equations

• TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.pullback w = Quotient.map (TauCeti.AlgebraicGeometry.RigidifiedLineBundle.pullback w) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.pullback_mk {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) (P : RigidifiedLineBundle s) : pullback w (mk P) = mk (RigidifiedLineBundle.pullback w P)

Pullback of the class of a rigidified line bundle is the class of its pullback.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.pullback_trivial {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) : pullback w (mk (RigidifiedLineBundle.trivial s)) = mk (RigidifiedLineBundle.trivial s')

Base change preserves the canonically rigidified trivial line bundle.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.pullback_id {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {h : Y ⟶ Y} {g : T ⟶ T} (hh : h = CategoryTheory.CategoryStruct.id Y) (hg : g = CategoryTheory.CategoryStruct.id T) (w : CategoryTheory.CategoryStruct.comp s h = CategoryTheory.CategoryStruct.comp g s) (a : RigidifiedLineBundleClass s) : pullback w a = a

Pullback along a square whose vertical morphisms are identities is the identity on classes of rigidified line bundles.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.pullback_comp {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} {T'' Y'' : AlgebraicGeometry.Scheme} {s'' : T'' ⟶ Y''} {h' : Y'' ⟶ Y'} {g' : T'' ⟶ T'} {h'' : Y'' ⟶ Y} {g'' : T'' ⟶ T} (hh : CategoryTheory.CategoryStruct.comp h' h = h'') (hg : CategoryTheory.CategoryStruct.comp g' g = g'') (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) (w' : CategoryTheory.CategoryStruct.comp s'' h' = CategoryTheory.CategoryStruct.comp g' s') (w'' : CategoryTheory.CategoryStruct.comp s'' h'' = CategoryTheory.CategoryStruct.comp g'' s) (a : RigidifiedLineBundleClass s) : pullback w' (pullback w a) = pullback w'' a

Pullback of classes of rigidified line bundles along two stacked squares is pullback along the composite square.

def TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.toLineBundleClass {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} : RigidifiedLineBundleClass s → LineBundleClass Y

The class of the underlying line bundle of a rigidified line bundle, forgetting the trivialization.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.toLineBundleClass_mk {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (P : RigidifiedLineBundle s) : (mk P).toLineBundleClass = LineBundleClass.mk P.lineBundle

Forgetting the trivialization of the class of P gives the class of its line bundle.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.toLineBundleClass_trivial {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} : (mk (RigidifiedLineBundle.trivial s)).toLineBundleClass = 1

Forgetting the rigidification of the canonical class gives the identity of the Picard monoid.

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.toLineBundleClass_pullback {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {T' Y' : AlgebraicGeometry.Scheme} {s' : T' ⟶ Y'} {h : Y' ⟶ Y} {g : T' ⟶ T} (w : CategoryTheory.CategoryStruct.comp s' h = CategoryTheory.CategoryStruct.comp g s) (a : RigidifiedLineBundleClass s) : (pullback w a).toLineBundleClass = LineBundleClass.pullback h a.toLineBundleClass

Forgetting the trivialization commutes with pullback.