Documentation

TauCeti.Algebra.Category.ModuleCat.Sheaf.Dualizable

Finite locally free sheaves of modules are dualizable #

Let M be a locally free sheaf of modules of finite type. Its dual-tensor comparison 𝓗om(M, 𝒪) ⊗ N ⟶ 𝓗om(M, N) is an isomorphism for every N (SheafOfModules.isIso_dualTensorIhom_of_isLocallyFree). By the dual-basis criterion TauCeti.exactPairingOfIsIsoDualTensorIhom, 𝓗om(M, 𝒪) is therefore a left dual of M, with evaluation the evaluation of the internal Hom.

Whether a morphism of sheaves is invertible can be checked on a cover (SheafOfModules.isIso_of_coversTop). Take a cover by charts on which M is finite free; there the dual-tensor comparison is invertible (SheafOfModules.IsLocallyFree.exists_isLocallyFreeData_isFiniteType_isIso_dualTensorIhom). Restriction to a chart is strong monoidal and commutes with internal Hom (SheafOfModules.isIso_overIhomComparison), so it carries the global comparison to the local one (CategoryTheory.Functor.isIso_map_dualTensorIhom_app).

The same charts show that the dual 𝓗om(M, 𝒪) is again finite locally free (SheafOfModules.isFiniteLocallyFree_ihom_unit), and hence so is 𝓗om(M, N) ≅ 𝓗om(M, 𝒪) ⊗ N for finite locally free M and N (SheafOfModules.isFiniteLocallyFree_ihom).

source
@[instance_reducible]
noncomputable def TauCeti.SheafOfModules.instMonoidalCategorySheafOfModulesOverOverRingCatRingCatSheaf_2 {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), (J.over X).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} (X : C) :
CategoryTheory.MonoidalCategory (SheafOfModules ((ringCatSheaf R).over X))

The monoidal structure on sheaves of modules over the restriction of R to X.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable def TauCeti.SheafOfModules.instMonoidalClosedSheafOfModulesOverOverRingCatRingCatSheaf_1 {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), (J.over X).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} (X : C) :
    CategoryTheory.MonoidalClosed (SheafOfModules ((ringCatSheaf R).over X))

    The closed monoidal structure on sheaves of modules over the restriction of R to X.

    Equations
    Instances For
      source
      instance SheafOfModules.isIso_dualTensorIhom_of_isLocallyFree {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasPullbacks C] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [M.IsLocallyFree] [M.IsFiniteType] :
      CategoryTheory.IsIso (TauCeti.dualTensorIhom M)

      The dual-tensor comparison 𝓗om(M, 𝒪) ⊗ N ⟶ 𝓗om(M, N) of a locally free sheaf of modules of finite type is an isomorphism. By TauCeti.exactPairingOfIsIsoDualTensorIhom, 𝓗om(M, 𝒪) is then a left dual of M.

      source
      theorem SheafOfModules.isFiniteLocallyFree_ihom_unit {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasPullbacks C] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] [M.IsLocallyFree] [M.IsFiniteType] :
      isFiniteLocallyFree (TauCeti.SheafOfModules.ringCatSheaf R) (M ⟹ CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)))

      The dual 𝓗om(M, 𝒪) of a locally free sheaf of modules of finite type is finite locally free.

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

      The internal Hom between finite locally free sheaves of modules is finite locally free.