Automorphisms and rescalings of rigidified line bundles

Let s : T ⟶ Y be a morphism of schemes and P a line bundle L on Y rigidified along s, with trivialization α : s^* L ≅ 𝒪_T. The automorphisms of L are the global units Γ(Y, 𝒪_Y)ˣ (Scheme.Modules.unitsGlobalSectionsMulEquivAut), and the automorphism given by a unit u respects the rigidification exactly when the pullback s^♯ u of u is 1. So the automorphism group of the rigidified line bundle is the kernel of Γ(Y, 𝒪_Y)ˣ → Γ(T, 𝒪_T)ˣ, and the rigidified line bundle has no automorphisms other than the identity exactly when this map is injective, for instance when s is a section of a morphism f : Y ⟶ T with f_* 𝒪_Y = 𝒪_T. This rigidity removes the automorphisms from the moduli problem: an isomorphism of rigidified line bundles is then unique when it exists, so the isomorphism classes of rigidified line bundles form a set-valued functor with no automorphism ambiguity, the rigidified Picard functor.

The trivializations of a fixed line bundle L along s are permuted by the global units Γ(T, 𝒪_T)ˣ, acting through the automorphisms of 𝒪_T. This action descends to isomorphism classes of rigidified line bundles. There it is transitive on the classes with a given underlying line bundle, and the stabilizer of every class is the image of Γ(Y, 𝒪_Y)ˣ → Γ(T, 𝒪_T)ˣ. Consequently, forgetting the rigidification is injective on classes exactly when Γ(Y, 𝒪_Y)ˣ → Γ(T, 𝒪_T)ˣ is surjective, as it is when s is a section of a morphism Y ⟶ T, and its image consists of the classes of the line bundles whose pullback along s is trivial.

Main declarations

• TauCeti.AlgebraicGeometry.RigidifiedLineBundle.autSubgroup: the automorphisms of the underlying line bundle respecting the rigidification, identified with the kernel of Γ(Y, 𝒪_Y)ˣ → Γ(T, 𝒪_T)ˣ by RigidifiedLineBundle.unitsGlobalSectionsMulEquivAut_mem_autSubgroup_iff;
• RigidifiedLineBundle.autSubgroup_eq_bot_iff: rigidity, a rigidified line bundle has only the identity automorphism exactly when Γ(Y, 𝒪_Y)ˣ → Γ(T, 𝒪_T)ˣ is injective, and RigidifiedLineBundle.autSubgroup_eq_bot_of_comp_eq_id the case where s is a section of a morphism p : Y ⟶ T with Γ(T, 𝒪_T) → Γ(Y, 𝒪_Y) surjective;
• the actions of Γ(T, 𝒪_T)ˣ on RigidifiedLineBundle s and on RigidifiedLineBundleClass s by rescaling the trivialization;
• RigidifiedLineBundleClass.mk_mk_eq_mk_mk_iff: two rigidifications of the same line bundle give the same class exactly when they differ by the pullback of a global unit of Y;
• RigidifiedLineBundleClass.exists_smul_eq_of_toLineBundleClass_eq and RigidifiedLineBundleClass.stabilizer_eq_range: rescaling is transitive on the classes over a fixed line bundle, with stabilizer the image of Γ(Y, 𝒪_Y)ˣ;
• RigidifiedLineBundleClass.toLineBundleClass_injective_iff and RigidifiedLineBundleClass.mem_range_toLineBundleClass_iff: the fibres and the image of forgetting the rigidification;
• RigidifiedLineBundleClass.toLineBundleClass_injective_of_comp_eq_id: forgetting the rigidification is injective when s is a section of a morphism Y ⟶ T, and RigidifiedLineBundleClass.range_toLineBundleClass describes its image as the line-bundle classes whose pullback along s is trivial;
• RigidifiedLineBundleClass.mk_toLineBundleClass_bijective: for a section s of p : Y ⟶ T, forgetting the rigidification identifies the classes of line bundles rigidified along s with Pic(Y) / p^* Pic(T).

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.

def TauCeti.AlgebraicGeometry.RigidifiedLineBundle.autSubgroup {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (P : RigidifiedLineBundle s) : Subgroup (CategoryTheory.Aut P.lineBundle.obj)

The automorphisms of the line bundle underlying a rigidified line bundle P that respect its rigidification: those whose pullback along s carries the trivialization to itself.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.mem_autSubgroup_iff {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (P : RigidifiedLineBundle s) (e : CategoryTheory.Aut P.lineBundle.obj) : e ∈ P.autSubgroup ↔ CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback s).map e.hom) P.rigidification.hom = P.rigidification.hom

An automorphism of the line bundle respects the rigidification when its pullback along s carries the trivialization to itself.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.unitsGlobalSectionsMulEquivAut_mem_autSubgroup_iff {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (P : RigidifiedLineBundle s) (u : (↑(Y.presheaf.obj (Opposite.op ⊤)))ˣ) : P.lineBundle.obj.unitsGlobalSectionsMulEquivAut u ∈ P.autSubgroup ↔ (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop s)) ↑u = 1

The automorphism of the line bundle given by a global unit u of Y respects the rigidification exactly when u pulls back to 1 along s.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.autSubgroup_eq_bot_iff {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (P : RigidifiedLineBundle s) : P.autSubgroup = ⊥ ↔ Function.Injective ⇑(Units.map ↑(CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop s)))

Rigidity of rigidified line bundles. A rigidified line bundle has no automorphisms other than the identity exactly when the pullback of global units along s is injective.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.autSubgroup_eq_bot_of_comp_eq_id {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (P : RigidifiedLineBundle s) {p : Y ⟶ T} (h : CategoryTheory.CategoryStruct.comp s p = CategoryTheory.CategoryStruct.id T) (hp : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop p))) : P.autSubgroup = ⊥

If s is a section of a morphism p : Y ⟶ T along which every global function on Y is pulled back from T, as when p_* 𝒪_Y = 𝒪_T, then a line bundle rigidified along s has no automorphisms other than the identity.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.RigidifiedLineBundle.instSMulUnitsCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} : SMul (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ (RigidifiedLineBundle s)

Global units of T act on line bundles rigidified along s : T ⟶ Y by rescaling the trivialization through multiplication by the unit on 𝒪_T.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.smul_lineBundle {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (v : (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ) (P : RigidifiedLineBundle s) : (v • P).lineBundle = P.lineBundle

Rescaling the trivialization does not change the underlying line bundle.

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundle.smul_rigidification {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (v : (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ) (P : RigidifiedLineBundle s) : (v • P).rigidification = P.rigidification ≪≫ CategoryTheory.asIso ((CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules).globalSectionsSmul ↑v)

The trivialization of a rescaled rigidified line bundle is the original trivialization followed by multiplication by the unit.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.RigidifiedLineBundle.instMulActionUnitsCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} : MulAction (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ (RigidifiedLineBundle s)

Rescaling the trivialization is an action of the global units of T.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.instSMulUnitsCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} : SMul (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ (RigidifiedLineBundleClass s)

Rescaling the trivialization by a global unit of T descends to isomorphism classes of rigidified line bundles.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.smul_mk {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (v : (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ) (P : RigidifiedLineBundle s) : v • mk P = mk (v • P)

Rescaling the class of a rigidified line bundle is the class of its rescaling.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.instMulActionUnitsCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} : MulAction (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ (RigidifiedLineBundleClass s)

Rescaling the trivialization is an action of the global units of T on classes.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.toLineBundleClass_smul {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (v : (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ) (a : RigidifiedLineBundleClass s) : (v • a).toLineBundleClass = a.toLineBundleClass

Rescaling the trivialization does not change the underlying line-bundle class.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.mk_mk_eq_mk_mk_iff {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (L : InvertibleSheaf Y) (α β : (AlgebraicGeometry.Scheme.Modules.pullback s).obj L.obj ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules) : mk { lineBundle := L, rigidification := α } = mk { lineBundle := L, rigidification := β } ↔ ∃ (u : (↑(Y.presheaf.obj (Opposite.op ⊤)))ˣ), α.hom = CategoryTheory.CategoryStruct.comp β.hom ((CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules).globalSectionsSmul ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop s)) ↑u))

Two rigidifications α, β of the same line bundle L give the same class of rigidified line bundles exactly when they differ by the pullback along s of a global unit of Y.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.exists_smul_eq_of_toLineBundleClass_eq {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {a b : RigidifiedLineBundleClass s} (h : a.toLineBundleClass = b.toLineBundleClass) : ∃ (v : (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ), v • a = b

Two classes of rigidified line bundles with the same underlying line-bundle class differ by rescaling the trivialization by a global unit of T.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.stabilizer_eq_range {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (a : RigidifiedLineBundleClass s) : MulAction.stabilizer (↑(T.presheaf.obj (Opposite.op ⊤)))ˣ a = (Units.map ↑(CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop s))).range

The stabilizer of a class of rigidified line bundles under rescaling by the global units of T is the image of the global units of Y.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.toLineBundleClass_injective_iff {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} : Function.Injective toLineBundleClass ↔ Function.Surjective ⇑(Units.map ↑(CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop s)))

Forgetting the rigidification is injective on classes exactly when every global unit of T is the pullback of a global unit of Y.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.toLineBundleClass_injective_of_comp_eq_id {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {p : Y ⟶ T} (h : CategoryTheory.CategoryStruct.comp s p = CategoryTheory.CategoryStruct.id T) : Function.Injective toLineBundleClass

If s is a section of a morphism p : Y ⟶ T, then forgetting the rigidification is injective on classes: every global unit of T is the pullback along s of its pullback along p.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.mem_range_toLineBundleClass_iff {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} (L : InvertibleSheaf Y) : LineBundleClass.mk L ∈ Set.range toLineBundleClass ↔ Nonempty ((AlgebraicGeometry.Scheme.Modules.pullback s).obj L.obj ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.Modules)

A line-bundle class is the class of a rigidified line bundle exactly when its pullback along s is trivial.

@[simp]

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.range_toLineBundleClass {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} : Set.range toLineBundleClass = {a : LineBundleClass Y | LineBundleClass.pullback s a = 1}

The line-bundle classes underlying classes of rigidified line bundles are exactly those whose pullback along s is trivial.

theorem TauCeti.AlgebraicGeometry.RigidifiedLineBundleClass.mk_toLineBundleClass_bijective {T Y : AlgebraicGeometry.Scheme} {s : T ⟶ Y} {p : Y ⟶ T} (h : CategoryTheory.CategoryStruct.comp s p = CategoryTheory.CategoryStruct.id T) : Function.Bijective fun (a : RigidifiedLineBundleClass s) => ↑a.toLineBundleClass

If s is a section of p : Y ⟶ T, then forgetting the rigidification and passing to the quotient by the line-bundle classes pulled back along p is a bijection from the classes of line bundles rigidified along s onto Pic(Y) / p^* Pic(T).