Internal Hom from a finite free sheaf

The internal Hom from a finite free sheaf into a finite locally free sheaf is finite locally free. The finite free sheaf is self-dual, so this internal Hom is its tensor product with the target. This is the local calculation behind duals and internal Homs of algebraic vector bundles.

The closure gives an endofunctor of the full category of finite locally free sheaves. Its underlying object and morphism are the usual internal Hom object and map.

On each finite free chart of a source sheaf, the same calculation shows that internal Hom from its restriction preserves finite local freeness. This is the local input for descent from a finite locally free source.

theorem TauCeti.isFiniteLocallyFree_ihom_free {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasSheafify J AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] (N : SheafOfModules (SheafOfModules.ringCatSheaf R)) (hN : SheafOfModules.isFiniteLocallyFree (SheafOfModules.ringCatSheaf R) N) : SheafOfModules.isFiniteLocallyFree (SheafOfModules.ringCatSheaf R) (SheafOfModules.free I ⟹ N)

Internal Hom out of a finite free sheaf preserves finite local freeness.

theorem TauCeti.isFiniteLocallyFree_ihom_of_iso_free {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasSheafify J AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] (M N : SheafOfModules (SheafOfModules.ringCatSheaf R)) (e : SheafOfModules.free I ≅ M) (hN : SheafOfModules.isFiniteLocallyFree (SheafOfModules.ringCatSheaf R) N) : SheafOfModules.isFiniteLocallyFree (SheafOfModules.ringCatSheaf R) (M ⟹ N)

Internal Hom from a sheaf isomorphic to a finite free sheaf preserves finite local freeness.

theorem TauCeti.isFiniteLocallyFree_ihom_chart {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M : SheafOfModules (SheafOfModules.ringCatSheaf R)} {q : M.LocalGeneratorsData} (i : q.I) [CategoryTheory.IsIso (q.generators i).π] [(q.generators i).IsFiniteType] (N : SheafOfModules ((SheafOfModules.ringCatSheaf R).over (q.X i))) (hN : SheafOfModules.isFiniteLocallyFree ((SheafOfModules.ringCatSheaf R).over (q.X i)) N) : SheafOfModules.isFiniteLocallyFree ((SheafOfModules.ringCatSheaf R).over (q.X i)) (M.over (q.X i) ⟹ N)

On a finite free chart of M, internal Hom from the restriction of M preserves finite local freeness. This is the chartwise input for descending internal Homs from a finite locally free source.

noncomputable def TauCeti.ihomFree {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasSheafify J AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] : CategoryTheory.Functor (SheafOfModules.isFiniteLocallyFree (SheafOfModules.ringCatSheaf R)).FullSubcategory (SheafOfModules.isFiniteLocallyFree (SheafOfModules.ringCatSheaf R)).FullSubcategory

Internal Hom out of a finite free sheaf as an endofunctor of finite locally free sheaves.

Equations

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

@[simp]

theorem TauCeti.ihomFree_obj_obj {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasSheafify J AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] (N : (SheafOfModules.isFiniteLocallyFree (SheafOfModules.ringCatSheaf R)).FullSubcategory) : ((ihomFree I).obj N).obj = (SheafOfModules.free I ⟹ N.obj)

The underlying sheaf of the finite free internal Hom is the ordinary internal Hom.

@[simp]

theorem TauCeti.ihomFree_map_hom {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasSheafify J AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (I : Type u) [Finite I] {M N : (SheafOfModules.isFiniteLocallyFree (SheafOfModules.ringCatSheaf R)).FullSubcategory} (f : M ⟶ N) : ((ihomFree I).map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom (SheafOfModules.free I)).map f.hom) (CategoryTheory.eqToHom ⋯))

On morphisms, the finite free internal Hom is the ordinary internal Hom map.