The distinguished point of the rigidified Picard functor

The trivial line bundle has a canonical trivialization along every section. Its rigidified isomorphism class is preserved by base change, giving the rigidified Picard functor a natural distinguished point. This is the identity used by the tensor-product group law on rigidified classes.

Reference

• S. Bosch, W. Lütkebohmert, M. Raynaud, Néron Models, Section 8.1.

noncomputable def TauCeti.AlgebraicGeometry.rigidifiedPicardPoint {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : (CategoryTheory.Over S)ᵒᵖ) : (rigidifiedPicardFunctor f x₀ hx₀).obj T

The class of the canonically rigidified trivial line bundle over a base change of X.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.rigidifiedPicardPoint_eq {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : (CategoryTheory.Over S)ᵒᵖ) : rigidifiedPicardPoint f x₀ hx₀ T = RigidifiedLineBundleClass.mk (RigidifiedLineBundle.trivial (baseChangeSection f x₀ hx₀ (Opposite.unop T)))

The distinguished point is represented by the canonically rigidified structure sheaf.

theorem TauCeti.AlgebraicGeometry.toLineBundleClass_rigidifiedPicardPoint {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : (CategoryTheory.Over S)ᵒᵖ) : RigidifiedLineBundleClass.toLineBundleClass (rigidifiedPicardPoint f x₀ hx₀ T) = 1

Forgetting the distinguished rigidification gives the identity line-bundle class.

theorem TauCeti.AlgebraicGeometry.rigidifiedPicardPoint_map {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') : (CategoryTheory.ConcreteCategory.hom ((rigidifiedPicardFunctor f x₀ hx₀).map φ)) (rigidifiedPicardPoint f x₀ hx₀ T) = rigidifiedPicardPoint f x₀ hx₀ T'

Pullback along a morphism over S preserves the distinguished rigidified class.