Restricting local trivializations

A local trivialization of a sheaf of modules over an object X remains a trivialization after restriction along a morphism f : Y ⟶ X. This file packages that elementary but necessary step for the local-triviality formulation of invertible sheaves.

Main declarations

• SheafOfModules.overMapFreePUnitIso identifies the restriction of the standard free rank-one sheaf over X with the standard free rank-one sheaf over Y;
• SheafOfModules.LocalTrivializations.isoOver restricts one chosen trivialization in an atlas along a morphism into its covering object;
• SheafOfModules.LocalTrivializations.ofRefinement transports an entire atlas to any cover equipped with refinement arrows into the original cover.

The common refinement of two atlases can therefore carry both sets of trivializations on the same cover. Together with compatibility of tensor products with restriction, this is the final local-triviality input for closure of invertible sheaves under tensor product. That closure is needed for the Picard group in TauCetiRoadmap/JacobianChallenge/README.md, Layer A, item "Invertible sheaves on a scheme; the Picard group Pic X under ⊗".

No formalization is vendored. The construction reuses Mathlib's SheafOfModules.overMap, SheafOfModules.overFunctorMap, and SheafOfModules.overMapUnitIso, and the standard free-rank-one/tensor-unit comparison already in Tau Ceti.

noncomputable def TauCeti.SheafOfModules.overMapFreePUnitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {X Y : C} (f : Y ⟶ X) : (SheafOfModules.overMap R f).obj (SheafOfModules.free PUnit.{u + 1}) ≅ SheafOfModules.free PUnit.{u + 1}

Restriction along f : Y ⟶ X carries the standard free rank-one sheaf over X to the standard free rank-one sheaf over Y.

For one generator this follows directly by identifying both free sheaves with their tensor units and using Mathlib's canonical comparison for restriction of the unit.

Equations

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

noncomputable def TauCeti.SheafOfModules.LocalTrivializations.isoOver {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (t : LocalTrivializations M) (i : t.I) {Y : C} (f : Y ⟶ t.X i) : SheafOfModules.free PUnit.{u + 1} ≅ M.over Y

Restrict one member of a local trivialization atlas along a morphism into its covering object. The resulting isomorphism trivializes M over the source of that morphism.

Equations

• t.isoOver i f = (TauCeti.SheafOfModules.overMapFreePUnitIso f).symm ≪≫ (SheafOfModules.overMap R f).mapIso (t.iso i) ≪≫ (SheafOfModules.overFunctorMap R f).app M

noncomputable def TauCeti.SheafOfModules.LocalTrivializations.ofRefinement {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (t : LocalTrivializations M) {I : Type u₁} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → t.I) (map : (j : I) → Y j ⟶ t.X (index j)) : LocalTrivializations M

Replace the cover of a local trivialization atlas by a refining cover.

Each object Y j of the new cover is equipped with a chosen arrow into an object of the old cover. Restricting the corresponding old trivialization along that arrow supplies the new one.

Equations

• t.ofRefinement Y coversTop index map = { I := I, X := Y, coversTop := coversTop, iso := fun (j : I) => t.isoOver (index j) (map j) }

@[simp]

theorem TauCeti.SheafOfModules.LocalTrivializations.ofRefinement_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (t : LocalTrivializations M) {I : Type u₁} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → t.I) (map : (j : I) → Y j ⟶ t.X (index j)) : (t.ofRefinement Y coversTop index map).I = I

Refining a local trivialization atlas uses the indexing type of the refining cover.

@[simp]

theorem TauCeti.SheafOfModules.LocalTrivializations.ofRefinement_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (t : LocalTrivializations M) {I : Type u₁} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → t.I) (map : (j : I) → Y j ⟶ t.X (index j)) : (t.ofRefinement Y coversTop index map).X = fun (j : (t.ofRefinement Y coversTop index map).I) => Y (⋯.mp j)

The covering objects of a refined local trivialization atlas are the specified refining objects.

@[simp]

theorem TauCeti.SheafOfModules.LocalTrivializations.ofRefinement_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (t : LocalTrivializations M) {I : Type u₁} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → t.I) (map : (j : I) → Y j ⟶ t.X (index j)) (j : (t.ofRefinement Y coversTop index map).I) : (t.ofRefinement Y coversTop index map).iso j = cast ⋯ (t.isoOver (index (⋯.mp j)) (map (⋯.mp j)))

The trivializations of a refined atlas are obtained by restricting the chosen old trivializations along the refinement arrows.