Local duality of finite locally free sheaves

A finite basis of a sheaf of modules gives an exact self-pairing, transported from the standard pairing on a finite free sheaf, and makes its dual-tensor comparison invertible. A finite locally free sheaf admits such bases on a cover. The pairing depends on the chosen basis; global duality uses the canonical internal Hom into the unit instead.

@[instance_reducible]

noncomputable def TauCeti.SheafOfModules.localMonoidalCategory {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

• TauCeti.SheafOfModules.localMonoidalCategory X = TauCeti.SheafOfModules.monoidalCategory (R.over X)

@[instance_reducible]

noncomputable def TauCeti.SheafOfModules.localMonoidalClosed {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

• TauCeti.SheafOfModules.localMonoidalClosed X = TauCeti.SheafOfModules.monoidalClosed (R.over X)

@[instance_reducible]

noncomputable def SheafOfModules.GeneratingSections.exactPairing {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (σ : M.GeneratingSections) [CategoryTheory.IsIso σ.π] [Finite σ.I] : CategoryTheory.ExactPairing M M

A finite basis gives an exact self-pairing, transported from the standard finite free pairing. The pairing depends on the chosen basis.

Equations

• σ.exactPairing = CategoryTheory.exactPairingCongr (CategoryTheory.asIso σ.π).symm (CategoryTheory.asIso σ.π).symm

theorem SheafOfModules.GeneratingSections.exactPairing_evaluation {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (σ : M.GeneratingSections) [CategoryTheory.IsIso σ.π] [Finite σ.I] : ε_ M M = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.asIso σ.π).symm.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.asIso σ.π).symm.hom (free σ.I)) (ε_ (free σ.I) (free σ.I)))

Evaluation in a finite basis is the standard finite free pairing transported along the inverse of its basis isomorphism.

theorem SheafOfModules.GeneratingSections.exactPairing_evaluation_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (σ : M.GeneratingSections) [CategoryTheory.IsIso σ.π] [Finite σ.I] {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ε_ M M) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.asIso σ.π).symm.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.asIso σ.π).symm.hom (free σ.I)) (CategoryTheory.CategoryStruct.comp (ε_ (free σ.I) (free σ.I)) h))

Evaluation in a finite basis is the standard finite free pairing transported along the inverse of its basis isomorphism.

theorem SheafOfModules.GeneratingSections.exactPairing_coevaluation {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (σ : M.GeneratingSections) [CategoryTheory.IsIso σ.π] [Finite σ.I] : η_ M M = CategoryTheory.CategoryStruct.comp (η_ (free σ.I) (free σ.I)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (free σ.I) (CategoryTheory.asIso σ.π).symm.inv) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.asIso σ.π).symm.inv M))

Coevaluation in a finite basis is the standard finite free coevaluation transported along its basis isomorphism.

theorem SheafOfModules.GeneratingSections.exactPairing_coevaluation_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (σ : M.GeneratingSections) [CategoryTheory.IsIso σ.π] [Finite σ.I] {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp (η_ M M) h = CategoryTheory.CategoryStruct.comp (η_ (free σ.I) (free σ.I)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (free σ.I) (CategoryTheory.asIso σ.π).symm.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.asIso σ.π).symm.inv M) h))

Coevaluation in a finite basis is the standard finite free coevaluation transported along its basis isomorphism.

theorem SheafOfModules.GeneratingSections.isIso_dualTensorIhom {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (σ : M.GeneratingSections) [CategoryTheory.IsIso σ.π] [Finite σ.I] : CategoryTheory.IsIso (TauCeti.dualTensorIhom M)

A finite basis makes the dual-tensor comparison invertible.

theorem SheafOfModules.IsLocallyFree.exists_isLocallyFreeData_isFiniteType_isIso_dualTensorIhom {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} {M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} [CategoryTheory.Limits.HasPullbacks C] [M.IsLocallyFree] [M.IsFiniteType] : ∃ (q : M.LocalGeneratorsData), q.IsLocallyFreeData ∧ q.IsFiniteType ∧ ∀ (i : q.I), CategoryTheory.IsIso (TauCeti.dualTensorIhom (M.over (q.X i)))

A finite locally free sheaf has a cover of finite free charts, each equipped with the local dual-tensor comparison isomorphism.