Rigidity of the rigidified Picard functor

Let f : X ⟶ S be a morphism of schemes with a section x₀, and let T be a scheme over S. The objects of the rigidified Picard functor of (X, x₀) at T are line bundles on X_T = T ×_S X rigidified along the base-changed section x₀_T. A rigidified line bundle has no automorphisms other than the identity once every global function on X_T is pulled back from T. This holds when f is quasi-compact and quasi-separated with f_* 𝒪_X = 𝒪_S and T is flat over S, because f_* 𝒪_X = 𝒪_S is stable under flat base change (TauCeti.AlgebraicGeometry.isIso_app_pullback_fst_of_flat).

Over a field every scheme is flat, so for a proper integral scheme X over a field K with a K-rational point x₀, line bundles on X_T rigidified along x₀_T have no nontrivial automorphisms for every scheme T over K. This is the setting of the Jacobian of a curve, where it means that an isomorphism between two objects of the rigidified Picard functor is unique when it exists.

Main results

• TauCeti.AlgebraicGeometry.RigidifiedLineBundle.autSubgroup_eq_bot_of_flat: rigidity over a flat base change, when f is quasi-compact and quasi-separated with f_* 𝒪_X = 𝒪_S;
• TauCeti.AlgebraicGeometry.RigidifiedLineBundle.autSubgroup_eq_bot_of_universallyClosed: rigidity over every base change, for a proper (more generally, universally closed and quasi-separated) integral scheme over a field with a rational point.

References

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

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.autSubgroup_eq_bot_of_flat {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f] (hf : ∀ (V : ↑S.affineOpens), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.app f ↑V)) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : CategoryTheory.Over S) [AlgebraicGeometry.Flat T.hom] (P : RigidifiedLineBundle (baseChangeSection f x₀ hx₀ T)) : P.autSubgroup = ⊥

Rigidity over a flat base change. Let f : X ⟶ S be quasi-compact and quasi-separated with f_* 𝒪_X = 𝒪_S, and let x₀ be a section of f. For every scheme T flat over S, a line bundle on T ×_S X rigidified along the base-changed section has no automorphisms other than the identity.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.autSubgroup_eq_bot_of_universallyClosed {K : Type u} [Field K] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧K) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.UniversallyClosed f] [AlgebraicGeometry.QuasiSeparated f] (x₀ : AlgebraicGeometry.Spec ↧K ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧K)) (T : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) (P : RigidifiedLineBundle (baseChangeSection f x₀ hx₀ T)) : P.autSubgroup = ⊥

Rigidity for a proper integral scheme with a rational point. Let X be integral, universally closed and quasi-separated over a field K (for instance proper), with a K-rational point x₀. For every scheme T over K, a line bundle on T ×_K X rigidified along the base-changed point has no automorphisms other than the identity.