Documentation

TauCeti.Algebra.Category.ModuleCat.Sheaf.TensorProduct.Dual

Finite free sheaves of modules are self-dual #

Let R be a sheaf of commutative rings on a small site. In the symmetric monoidal category of sheaves of R-modules, the free sheaf free I on a finite type I is dualizable, with dual free I itself. Writing eᵢ = ιFree i for the basis sections, the evaluation free I ⊗ free I ⟶ R sends eᵢ ⊗ eⱼ to δᵢⱼ, and the coevaluation R ⟶ free I ⊗ free I sends 1 to ∑ i, eᵢ ⊗ eᵢ.

The pairing is obtained from TauCeti.ExactPairing.biproduct: the basic free-sheaf API in TauCeti.Algebra.Category.ModuleCat.Sheaf.Free identifies free I with the biproduct of I copies of the unit R (TauCeti.SheafOfModules.biproductIsoFree), and the unit is canonically self-dual. Finite free sheaves are the local models of finite locally free sheaves, so this is the local input for showing that finite locally free sheaves are dualizable.

Combining the pairing with the closed structure of sheaves of modules identifies the internal Hom out of free I with tensoring by free I, and in particular the dual sheaf 𝓗om(free I, 𝒪) with free I itself. Its basis sections are the dual basis: paired against the basis sections of free I they give δᵢⱼ.

Main declarations #

source
@[instance_reducible]
noncomputable instance TauCeti.SheafOfModules.exactPairingFree {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} (I : Type u) [Finite I] :
CategoryTheory.ExactPairing (SheafOfModules.free I) (SheafOfModules.free I)

The free sheaf of modules on a finite type is self-dual: the evaluation pairs the basis sections ιFree i and ιFree j to δᵢⱼ, and the coevaluation is ∑ i, ιFree i ⊗ ιFree i.

Equations
source
@[simp]
theorem TauCeti.SheafOfModules.ιFree_tensorHom_ιFree_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} {I : Type u} [Finite I] (i : I) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (SheafOfModules.ιFree i)) (ε_ (SheafOfModules.free I) (SheafOfModules.free I)) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)))).hom

The evaluation of the free sheaf on a finite type pairs each basis section with itself to 1.

source
@[simp]
theorem TauCeti.SheafOfModules.ιFree_tensorHom_ιFree_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} {I : Type u} [Finite I] (i : I) {Z : SheafOfModules (ringCatSheaf R)} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)) ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (SheafOfModules.ιFree i)) (CategoryTheory.CategoryStruct.comp (ε_ (SheafOfModules.free I) (SheafOfModules.free I)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)))).hom h

The evaluation of the free sheaf on a finite type pairs each basis section with itself to 1.

source
@[simp]
theorem TauCeti.SheafOfModules.ιFree_tensorHom_ιFree_evaluation_of_ne {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} {I : Type u} [Finite I] {i j : I} (h : i ≠ j) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (SheafOfModules.ιFree j)) (ε_ (SheafOfModules.free I) (SheafOfModules.free I)) = 0

The evaluation of the free sheaf on a finite type pairs distinct basis sections to 0.

source
@[simp]
theorem TauCeti.SheafOfModules.ιFree_tensorHom_ιFree_evaluation_of_ne_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} {I : Type u} [Finite I] {i j : I} (h : i ≠ j) {Z : SheafOfModules (ringCatSheaf R)} (h✝ : CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)) ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (SheafOfModules.ιFree j)) (CategoryTheory.CategoryStruct.comp (ε_ (SheafOfModules.free I) (SheafOfModules.free I)) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

The evaluation of the free sheaf on a finite type pairs distinct basis sections to 0.

source
theorem TauCeti.SheafOfModules.coevaluation_free {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} {I : Type u} [Finite I] [Fintype I] :
η_ (SheafOfModules.free I) (SheafOfModules.free I) = ∑ i : I, CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)))).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (SheafOfModules.ιFree i))

The coevaluation of the free sheaf on a finite type is the sum of the tensor squares of the basis sections.

source
noncomputable def TauCeti.SheafOfModules.ihomFreeIso {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} (I : Type u) [Finite I] (M : SheafOfModules (ringCatSheaf R)) :
(CategoryTheory.ihom (SheafOfModules.free I)).obj M ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (SheafOfModules.free I) M

The internal Hom out of a finite free sheaf of modules is tensoring with that sheaf, since the free sheaf is its own dual.

Equations
Instances For
    source
    noncomputable def TauCeti.SheafOfModules.dualFreeIso {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} (I : Type u) [Finite I] :
    (CategoryTheory.ihom (SheafOfModules.free I)).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R))) ≅ SheafOfModules.free I

    The dual of a finite free sheaf of modules, that is, the internal Hom into the structure sheaf, is free on the same index type. It is TauCeti.SheafOfModules.ihomFreeIso at the structure sheaf, followed by the right unitor.

    Equations
    Instances For
      source
      noncomputable def TauCeti.SheafOfModules.dualFreeι {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} {I : Type u} [Finite I] (i : I) :
      CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)) ⟶ (CategoryTheory.ihom (SheafOfModules.free I)).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)))

      The i-th basis section of the dual of free I, obtained by transporting the corresponding basis section along TauCeti.SheafOfModules.dualFreeIso.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.SheafOfModules.dualFreeι_comp_dualFreeIso_hom {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} {I : Type u} [Finite I] (i : I) :
        CategoryTheory.CategoryStruct.comp (dualFreeι i) (dualFreeIso I).hom = SheafOfModules.ιFree i

        Transporting a dual basis section back along TauCeti.SheafOfModules.dualFreeIso recovers the corresponding basis section of the free sheaf.

        source
        @[simp]
        theorem TauCeti.SheafOfModules.dualFreeι_comp_dualFreeIso_hom_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} {I : Type u} [Finite I] (i : I) {Z : SheafOfModules (ringCatSheaf R)} (h : SheafOfModules.free I ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (dualFreeι i) (CategoryTheory.CategoryStruct.comp (dualFreeIso I).hom h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) h

        Transporting a dual basis section back along TauCeti.SheafOfModules.dualFreeIso recovers the corresponding basis section of the free sheaf.

        source
        @[simp]
        theorem TauCeti.SheafOfModules.ιFree_tensorHom_dualFreeι_comp_ev {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} {I : Type u} [Finite I] (i : I) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (dualFreeι i)) ((CategoryTheory.ihom.ev (SheafOfModules.free I)).app (SheafOfModules.unit (ringCatSheaf R))) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)))).hom

        The basis sections of the dual sheaf are the dual basis: the i-th one evaluates on the i-th basis section of free I to 1.

        source
        theorem TauCeti.SheafOfModules.ιFree_tensorHom_dualFreeι_comp_ev_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} {I : Type u} [Finite I] (i : I) {Z : SheafOfModules (ringCatSheaf R)} (h : SheafOfModules.unit (ringCatSheaf R) ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (dualFreeι i)) ((CategoryTheory.ihom.ev (SheafOfModules.free I)).app (SheafOfModules.unit (ringCatSheaf R)))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)))).hom h

        The basis sections of the dual sheaf are the dual basis: the i-th one evaluates on the i-th basis section of free I to 1.

        source
        @[simp]
        theorem TauCeti.SheafOfModules.ιFree_tensorHom_dualFreeι_comp_ev_of_ne {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} {I : Type u} [Finite I] {i j : I} (h : i ≠ j) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (dualFreeι j)) ((CategoryTheory.ihom.ev (SheafOfModules.free I)).app (SheafOfModules.unit (ringCatSheaf R))) = 0

        The basis sections of the dual sheaf are the dual basis: the j-th one evaluates on the i-th basis section of free I to 0 when i ≠ j.

        source
        theorem TauCeti.SheafOfModules.ιFree_tensorHom_dualFreeι_comp_ev_of_ne_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} {I : Type u} [Finite I] {i j : I} (h : i ≠ j) {Z : SheafOfModules (ringCatSheaf R)} (h✝ : SheafOfModules.unit (ringCatSheaf R) ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (dualFreeι j)) ((CategoryTheory.ihom.ev (SheafOfModules.free I)).app (SheafOfModules.unit (ringCatSheaf R)))) h✝ = CategoryTheory.CategoryStruct.comp 0 h✝

        The basis sections of the dual sheaf are the dual basis: the j-th one evaluates on the i-th basis section of free I to 0 when i ≠ j.

        source
        instance SheafOfModules.isIso_evaluation_dual_freePUnit {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} :
        CategoryTheory.IsIso ((CategoryTheory.ihom.ev (free PUnit.{u + 1})).app (unit (TauCeti.SheafOfModules.ringCatSheaf R)))

        Evaluation of the standard free rank-one sheaf against its dual is an isomorphism.

        source
        theorem SheafOfModules.isIso_evaluation_dual_of_iso_freePUnit {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)) (e : free PUnit.{u + 1} ≅ M) :
        CategoryTheory.IsIso ((CategoryTheory.ihom.ev M).app (unit (TauCeti.SheafOfModules.ringCatSheaf R)))

        Evaluation against the dual is an isomorphism for a sheaf isomorphic to the standard free rank-one sheaf.