Local generator data transported along functors on slices

Local generator data for M on a covering family X is transported to local generator data for N on a covering family Y of another ringed site, given on each member a colimit preserving functor F i between the slice categories that fixes the structure sheaf and an identification (F i).obj (M.over (X i)) ≅ N.over (Y i): the generators on Y i are Mathlib's GeneratingSections.map along F i, pushed along the identification. Locally free data is transported to locally free data, with the same index types.

The construction is stated on general ringed sites because its instance is proved by reducing projections of the structure, and that reduction does not terminate in the default heartbeat budget once the sites carry scheme-level instances; Modules/Pullback/LocallyFree.lean applies it to pullback on the slices of a scheme.

Main definitions

• SheafOfModules.LocalGeneratorsData.transport: the transported local generator data.

Main results

• SheafOfModules.LocalGeneratorsData.isLocallyFreeData_transport: locally free data is transported to locally free data;
• SheafOfModules.LocalGeneratorsData.transport_generators_I: the index types are unchanged.

noncomputable def SheafOfModules.LocalGeneratorsData.transport {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {R' : CategoryTheory.Sheaf J' RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C'), CategoryTheory.HasSheafify (J'.over X) AddCommGrpCat] [∀ (X : C'), (J'.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {N : SheafOfModules R'} (q : M.LocalGeneratorsData) (Y : q.I → C') (hY : J'.CoversTop Y) (F : (i : q.I) → CategoryTheory.Functor (SheafOfModules (R.over (q.X i))) (SheafOfModules (R'.over (Y i)))) [∀ (i : q.I), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (F i)] (η : (i : q.I) → unit (R'.over (Y i)) ≅ (F i).obj (unit (R.over (q.X i)))) (e : (i : q.I) → (F i).obj (M.over (q.X i)) ≅ N.over (Y i)) : N.LocalGeneratorsData

Transport local generator data along colimit-preserving functors on slices that fix the structure sheaf: on Y i the generators are GeneratingSections.map along F i, pushed along e i.

Equations

• q.transport Y hY F η e = { I := q.I, X := Y, coversTop := hY, generators := fun (i : q.I) => ((q.generators i).map (F i) (η i)).ofEpi (e i).hom }

@[simp]

theorem SheafOfModules.LocalGeneratorsData.transport_generators_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {R' : CategoryTheory.Sheaf J' RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C'), CategoryTheory.HasSheafify (J'.over X) AddCommGrpCat] [∀ (X : C'), (J'.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {N : SheafOfModules R'} (q : M.LocalGeneratorsData) (Y : q.I → C') (hY : J'.CoversTop Y) (F : (i : q.I) → CategoryTheory.Functor (SheafOfModules (R.over (q.X i))) (SheafOfModules (R'.over (Y i)))) [∀ (i : q.I), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (F i)] (η : (i : q.I) → unit (R'.over (Y i)) ≅ (F i).obj (unit (R.over (q.X i)))) (e : (i : q.I) → (F i).obj (M.over (q.X i)) ≅ N.over (Y i)) (i : q.I) : ((q.transport Y hY F η e).generators i).I = (q.generators i).I

Neither GeneratingSections.map nor ofEpi changes the index type of the generators, so a fixed-rank atlas is transported with its rank.

instance SheafOfModules.LocalGeneratorsData.isLocallyFreeData_transport {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {R' : CategoryTheory.Sheaf J' RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C'), CategoryTheory.HasSheafify (J'.over X) AddCommGrpCat] [∀ (X : C'), (J'.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {N : SheafOfModules R'} (q : M.LocalGeneratorsData) (Y : q.I → C') (hY : J'.CoversTop Y) (F : (i : q.I) → CategoryTheory.Functor (SheafOfModules (R.over (q.X i))) (SheafOfModules (R'.over (Y i)))) [∀ (i : q.I), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (F i)] (η : (i : q.I) → unit (R'.over (Y i)) ≅ (F i).obj (unit (R.over (q.X i)))) (e : (i : q.I) → (F i).obj (M.over (q.X i)) ≅ N.over (Y i)) [q.IsLocallyFreeData] : (q.transport Y hY F η e).IsLocallyFreeData

Locally free data is transported to locally free data: GeneratingSections.map sends an isomorphism π to an isomorphism, and so does pushing along e i.