Local trivializations of invertible sheaves

An invertible sheaf is locally free on a one-element basis. This file turns the singleton-indexed free presentations in SheafOfModules.IsInvertible into the standard geometric formulation: on every member of a cover, the sheaf is isomorphic to the free sheaf on PUnit.

The structure SheafOfModules.LocalTrivializations M records such a cover and its trivializing isomorphisms. The two formulations are equivalent:

• SheafOfModules.LocalGeneratorsData.IsInvertible.trivializationIso standardizes each rank-one free presentation;
• LocalTrivializations.ofIso transports a local trivialization atlas along an isomorphism;
• LocalTrivializations.isInvertible recovers the local-generator formulation;
• LocalTrivializations.ofIsInvertible constructs local trivializations from an invertible sheaf;
• LocalTrivializations.nonempty_iff_isInvertible characterizes invertibility by the existence of local trivializations.

This supplies the local-triviality interface for TauCetiRoadmap/JacobianChallenge/README.md, Layer A, item "Invertible sheaves on a scheme; the Picard group Pic X under ⊗". It is the form needed to prove that tensor products and duals of invertible sheaves remain invertible. The construction reuses Mathlib's free-sheaf functor and LocalGeneratorsData; no formalization is vendored.

structure TauCeti.SheafOfModules.LocalTrivializations {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) : Type (max (max u (u₁ + 1)) v₁)

A local trivialization atlas for a sheaf of modules. It consists of a cover of the terminal object and, over every member of the cover, an isomorphism from the standard free rank-one sheaf to the restriction of M.

• I : Type u₁

  The indexing type of the trivializing cover.

• X : self.I → C

  The objects of the trivializing cover.

• coversTop : J.CoversTop self.X

  The chosen objects cover the terminal object.

• iso (i : self.I) : SheafOfModules.free PUnit.{u + 1} ≅ M.over (self.X i)

  The isomorphism from the standard free rank-one sheaf to M on each member of the cover.

noncomputable def SheafOfModules.LocalGeneratorsData.IsInvertible.trivializationIso {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} {q : M.LocalGeneratorsData} (hq : q.IsInvertible) (i : q.I) : free PUnit.{u + 1} ≅ M.over (q.X i)

A rank-one free presentation on a member of a cover, standardized to an isomorphism from the free sheaf on PUnit.

Equations

• hq.trivializationIso i = SheafOfModules.freeFunctor.mapIso Equiv.punitOfNonemptyOfSubsingleton.symm.toIso ≪≫ CategoryTheory.asIso (q.generators i).π

@[simp]

theorem SheafOfModules.LocalGeneratorsData.IsInvertible.trivializationIso_hom {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} {q : M.LocalGeneratorsData} (hq : q.IsInvertible) (i : q.I) : (hq.trivializationIso i).hom = CategoryTheory.CategoryStruct.comp (freeFunctor.map Equiv.punitOfNonemptyOfSubsingleton.symm.toIso.hom) (q.generators i).π

The forward map of the standardized trivialization is the relabelling of the free basis, followed by the original local free presentation.

noncomputable def TauCeti.SheafOfModules.LocalTrivializations.ofIso {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 N : SheafOfModules R} (t : LocalTrivializations M) (e : M ≅ N) : LocalTrivializations N

Transport local trivializations along an isomorphism of sheaves of modules.

Equations

• t.ofIso e = { I := t.I, X := t.X, coversTop := ⋯, iso := fun (i : t.I) => t.iso i ≪≫ (SheafOfModules.overFunctor R (t.X i)).mapIso e }

@[simp]

theorem TauCeti.SheafOfModules.LocalTrivializations.ofIso_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 N : SheafOfModules R} (t : LocalTrivializations M) (e : M ≅ N) : (t.ofIso e).I = t.I

Transporting local trivializations preserves the indexing type.

@[simp]

theorem TauCeti.SheafOfModules.LocalTrivializations.ofIso_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 N : SheafOfModules R} (t : LocalTrivializations M) (e : M ≅ N) : (t.ofIso e).X = fun (i : (t.ofIso e).I) => t.X (⋯.mp i)

Transporting local trivializations preserves the covering objects.

@[simp]

theorem TauCeti.SheafOfModules.LocalTrivializations.ofIso_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 N : SheafOfModules R} (t : LocalTrivializations M) (e : M ≅ N) (i : (t.ofIso e).I) : (t.ofIso e).iso i = cast ⋯ (t.iso (⋯.mp i) ≪≫ (SheafOfModules.overFunctor R (t.X (⋯.mp i))).mapIso e)

The transported trivializations are obtained by composing with the restricted isomorphism.

theorem TauCeti.SheafOfModules.LocalTrivializations.isInvertible {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) : IsInvertible M

Local trivializations exhibit a sheaf as invertible.

noncomputable def TauCeti.SheafOfModules.LocalTrivializations.ofIsInvertible {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) [hM : IsInvertible M] : LocalTrivializations M

Every invertible sheaf admits local trivializations by the standard free rank-one sheaf.

Equations

• TauCeti.SheafOfModules.LocalTrivializations.ofIsInvertible M = { I := ⋯.choose.I, X := ⋯.choose.X, coversTop := ⋯, iso := fun (i : ⋯.choose.I) => ⋯.trivializationIso i }

theorem TauCeti.SheafOfModules.LocalTrivializations.nonempty_iff_isInvertible {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} : Nonempty (LocalTrivializations M) ↔ IsInvertible M

A sheaf of modules is invertible exactly when it admits a local trivialization atlas by the standard free rank-one sheaf.