Documentation

TauCeti.Algebra.Category.ModuleCat.Sheaf.Quasicoherent.Biprod

Direct sums of quasi-coherent and locally free sheaves of modules #

Let R be a sheaf of rings on a site with pullbacks. This file shows that the binary biproduct (direct sum) M ⊞ N of two sheaves of R-modules is quasi-coherent, of finite type, finitely presented, or locally free as soon as M and N are. In particular, direct sums of finite locally free sheaves (locally free and finitely presented) are finite locally free.

The local input is that generating sections, and presentations, of M and N give generating sections, and a presentation, of M ⊞ N: the free sheaf on I ⊕ I' is free I ⊞ free I' (SheafOfModules.freeBiprodIso), and the biproduct of two cokernels is a cokernel (CategoryTheory.Limits.CokernelCofork.isColimitBiprod). Restriction to a slice site is additive, so it commutes with direct sums (SheafOfModules.overBiprodIso), and the local data of M and N are compared on a common refinement of their covers.

The common-refinement construction follows the tensor-product closure formalization in SheafOfModules.QuasicoherentData.tensor.

Main declarations #

source
noncomputable def TauCeti.SheafOfModules.freeBiprodIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I I' : Type u) :
SheafOfModules.free I ⊞ SheafOfModules.free I' ≅ SheafOfModules.free (I ⊕ I')

The direct sum of the free sheaves of modules on I and on I' is the free sheaf of modules on I ⊕ I'.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.SheafOfModules.inl_freeBiprodIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I I' : Type u) :
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (freeBiprodIso I I').hom = SheafOfModules.freeMap Sum.inl
    source
    @[simp]
    theorem TauCeti.SheafOfModules.inl_freeBiprodIso_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I I' : Type u) {Z : SheafOfModules R} (h : SheafOfModules.free (I ⊕ I') ⟶ Z) :
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (freeBiprodIso I I').hom h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inl) h
    source
    @[simp]
    theorem TauCeti.SheafOfModules.inr_freeBiprodIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I I' : Type u) :
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (freeBiprodIso I I').hom = SheafOfModules.freeMap Sum.inr
    source
    @[simp]
    theorem TauCeti.SheafOfModules.inr_freeBiprodIso_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I I' : Type u) {Z : SheafOfModules R} (h : SheafOfModules.free (I ⊕ I') ⟶ Z) :
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (freeBiprodIso I I').hom h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inr) h
    source
    @[simp]
    theorem TauCeti.SheafOfModules.freeMap_inl_freeBiprodIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I I' : Type u) :
    CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inl) (freeBiprodIso I I').inv = CategoryTheory.Limits.biprod.inl
    source
    @[simp]
    theorem TauCeti.SheafOfModules.freeMap_inl_freeBiprodIso_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I I' : Type u) {Z : SheafOfModules R} (h : SheafOfModules.free I ⊞ SheafOfModules.free I' ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inl) (CategoryTheory.CategoryStruct.comp (freeBiprodIso I I').inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h
    source
    @[simp]
    theorem TauCeti.SheafOfModules.freeMap_inr_freeBiprodIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I I' : Type u) :
    CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inr) (freeBiprodIso I I').inv = CategoryTheory.Limits.biprod.inr
    source
    @[simp]
    theorem TauCeti.SheafOfModules.freeMap_inr_freeBiprodIso_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I I' : Type u) {Z : SheafOfModules R} (h : SheafOfModules.free I ⊞ SheafOfModules.free I' ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inr) (CategoryTheory.CategoryStruct.comp (freeBiprodIso I I').inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h
    source
    noncomputable def SheafOfModules.GeneratingSections.biprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (G : M.GeneratingSections) (H : N.GeneratingSections) :
    (M ⊞ N).GeneratingSections

    Generating sections of M and of N give generating sections of M ⊞ N, indexed by the disjoint union of the two index types.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem SheafOfModules.GeneratingSections.biprod_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (G : M.GeneratingSections) (H : N.GeneratingSections) :
      (G.biprod H).I = (G.I ⊕ H.I)
      source
      @[simp]
      theorem SheafOfModules.GeneratingSections.biprod_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (G : M.GeneratingSections) (H : N.GeneratingSections) :
      (G.biprod H).π = CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.freeBiprodIso G.I H.I).inv (CategoryTheory.Limits.biprod.map G.π H.π)

      The generating morphism of G.biprod H is the direct sum of the generating morphisms, read through freeBiprodIso.

      source
      instance SheafOfModules.GeneratingSections.isFiniteType_biprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (G : M.GeneratingSections) (H : N.GeneratingSections) [hG : G.IsFiniteType] [hH : H.IsFiniteType] :
      (G.biprod H).IsFiniteType
      source
      instance SheafOfModules.GeneratingSections.isIso_biprod_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (G : M.GeneratingSections) (H : N.GeneratingSections) [hG : CategoryTheory.IsIso G.π] [hH : CategoryTheory.IsIso H.π] :
      CategoryTheory.IsIso (G.biprod H).π
      source
      noncomputable def SheafOfModules.Presentation.biprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (P : M.Presentation) (Q : N.Presentation) :
      (M ⊞ N).Presentation

      Presentations of M and of N give a presentation of M ⊞ N: its generators and its relations are indexed by the disjoint unions of those of M and N.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem SheafOfModules.Presentation.biprod_generators {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (P : M.Presentation) (Q : N.Presentation) :
        (P.biprod Q).generators = P.generators.biprod Q.generators
        source
        @[simp]
        theorem SheafOfModules.Presentation.biprod_relations_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (P : M.Presentation) (Q : N.Presentation) :
        (P.biprod Q).relations.I = (P.relations.I ⊕ Q.relations.I)
        source
        @[simp]
        theorem SheafOfModules.Presentation.biprod_relations_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (P : M.Presentation) (Q : N.Presentation) :
        CategoryTheory.CategoryStruct.comp (P.biprod Q).relations.π (CategoryTheory.Limits.kernel.ι (P.biprod Q).generators.π) = CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.freeBiprodIso P.relations.I Q.relations.I).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.comp P.relations.π (CategoryTheory.Limits.kernel.ι P.generators.π)) (CategoryTheory.CategoryStruct.comp Q.relations.π (CategoryTheory.Limits.kernel.ι Q.generators.π))) (TauCeti.SheafOfModules.freeBiprodIso P.generators.I Q.generators.I).hom)

        The relation morphism of the direct-sum presentation is the direct sum of the two relation morphisms, read through the free-sheaf biproduct isomorphisms.

        source
        instance TauCeti.SheafOfModules.instIsFiniteBiprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (P : M.Presentation) (Q : N.Presentation) [P.IsFinite] [Q.IsFinite] :
        (P.biprod Q).IsFinite

        The direct sum of two finite presentations is finite.

        source
        noncomputable def SheafOfModules.overBiprodIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M N : SheafOfModules R) (X : C) :
        (M ⊞ N).over X ≅ M.over X ⊞ N.over X

        Restriction to a slice site commutes with direct sums.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.SheafOfModules.inl_overBiprodIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (X : C) :
          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (M.overBiprodIso N X).inv = SheafOfModules.Hom.over CategoryTheory.Limits.biprod.inl X
          source
          @[simp]
          theorem TauCeti.SheafOfModules.inl_overBiprodIso_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (X : C) {Z : SheafOfModules (R.over X)} (h : (M ⊞ N).over X ⟶ Z) :
          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (M.overBiprodIso N X).inv h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.Hom.over CategoryTheory.Limits.biprod.inl X) h
          source
          @[simp]
          theorem TauCeti.SheafOfModules.inr_overBiprodIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (X : C) :
          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (M.overBiprodIso N X).inv = SheafOfModules.Hom.over CategoryTheory.Limits.biprod.inr X
          source
          @[simp]
          theorem TauCeti.SheafOfModules.inr_overBiprodIso_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (X : C) {Z : SheafOfModules (R.over X)} (h : (M ⊞ N).over X ⟶ Z) :
          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (M.overBiprodIso N X).inv h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.Hom.over CategoryTheory.Limits.biprod.inr X) h
          source
          @[simp]
          theorem TauCeti.SheafOfModules.overBiprodIso_hom_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (X : C) :
          CategoryTheory.CategoryStruct.comp (M.overBiprodIso N X).hom CategoryTheory.Limits.biprod.fst = SheafOfModules.Hom.over CategoryTheory.Limits.biprod.fst X
          source
          @[simp]
          theorem TauCeti.SheafOfModules.overBiprodIso_hom_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (X : C) {Z : SheafOfModules (R.over X)} (h : M.over X ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (M.overBiprodIso N X).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.Hom.over CategoryTheory.Limits.biprod.fst X) h
          source
          @[simp]
          theorem TauCeti.SheafOfModules.overBiprodIso_hom_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (X : C) :
          CategoryTheory.CategoryStruct.comp (M.overBiprodIso N X).hom CategoryTheory.Limits.biprod.snd = SheafOfModules.Hom.over CategoryTheory.Limits.biprod.snd X
          source
          @[simp]
          theorem TauCeti.SheafOfModules.overBiprodIso_hom_snd_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (X : C) {Z : SheafOfModules (R.over X)} (h : N.over X ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (M.overBiprodIso N X).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.Hom.over CategoryTheory.Limits.biprod.snd X) h
          source
          noncomputable def SheafOfModules.LocalGeneratorsData.biprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.LocalGeneratorsData) (qN : N.LocalGeneratorsData) :
          (M ⊞ N).LocalGeneratorsData

          Local generators of M and of N give local generators of M ⊞ N. Its cover is the common refinement of the two covers, and over each of its members the generators are the direct sum of the restricted generators of M and N.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem SheafOfModules.LocalGeneratorsData.biprod_generators {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.LocalGeneratorsData) (qN : N.LocalGeneratorsData) (i : (⋯.commonRefinement ⋯).I) :
            (qM.biprod qN).generators i = (GeneratingSections.equivOfIso (M.overBiprodIso N ((⋯.commonRefinement ⋯).X i)).symm) (((qM.ofRefinement (⋯.commonRefinement ⋯).X ⋯ (⋯.commonRefinement ⋯).leftIndex (⋯.commonRefinement ⋯).left).generators i).biprod ((qN.ofRefinement (⋯.commonRefinement ⋯).X ⋯ (⋯.commonRefinement ⋯).rightIndex (⋯.commonRefinement ⋯).right).generators i))
            source
            @[simp]
            theorem SheafOfModules.LocalGeneratorsData.biprod_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.LocalGeneratorsData) (qN : N.LocalGeneratorsData) :
            (qM.biprod qN).I = (⋯.commonRefinement ⋯).I
            source
            @[simp]
            theorem SheafOfModules.LocalGeneratorsData.biprod_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.LocalGeneratorsData) (qN : N.LocalGeneratorsData) (a✝ : (⋯.commonRefinement ⋯).I) :
            (qM.biprod qN).X a✝ = (⋯.commonRefinement ⋯).X a✝
            source
            instance TauCeti.SheafOfModules.instIsLocallyFreeDataBiprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.LocalGeneratorsData) (qN : N.LocalGeneratorsData) [qM.IsLocallyFreeData] [qN.IsLocallyFreeData] :
            (qM.biprod qN).IsLocallyFreeData

            The direct sum of locally free data is locally free data.

            source
            instance TauCeti.SheafOfModules.instIsFiniteTypeBiprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.LocalGeneratorsData) (qN : N.LocalGeneratorsData) [qM.IsFiniteType] [qN.IsFiniteType] :
            (qM.biprod qN).IsFiniteType

            The direct sum of local generators of finite type is of finite type.

            source
            noncomputable def SheafOfModules.QuasicoherentData.biprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) :
            (M ⊞ N).QuasicoherentData

            Quasi-coherent data for M and for N give quasi-coherent data for M ⊞ N. Its cover is the common refinement of the two covers, and over each of its members the presentation is the direct sum of the restricted presentations of M and N.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem SheafOfModules.QuasicoherentData.biprod_presentation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) (i : (⋯.commonRefinement ⋯).I) :
              (qM.biprod qN).presentation i = Presentation.ofIsIso (M.overBiprodIso N ((⋯.commonRefinement ⋯).X i)).inv (((qM.ofRefinement (⋯.commonRefinement ⋯).X ⋯ (⋯.commonRefinement ⋯).leftIndex (⋯.commonRefinement ⋯).left).presentation i).biprod ((qN.ofRefinement (⋯.commonRefinement ⋯).X ⋯ (⋯.commonRefinement ⋯).rightIndex (⋯.commonRefinement ⋯).right).presentation i))
              source
              @[simp]
              theorem SheafOfModules.QuasicoherentData.biprod_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) (a✝ : (⋯.commonRefinement ⋯).I) :
              (qM.biprod qN).X a✝ = (⋯.commonRefinement ⋯).X a✝
              source
              @[simp]
              theorem SheafOfModules.QuasicoherentData.biprod_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) :
              (qM.biprod qN).I = (⋯.commonRefinement ⋯).I
              source
              instance TauCeti.SheafOfModules.instIsFinitePresentationBiprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) [qM.IsFinitePresentation] [qN.IsFinitePresentation] :
              (qM.biprod qN).IsFinitePresentation

              The direct sum of finite quasi-coherent data is finite.

              source
              instance TauCeti.SheafOfModules.isLocallyFree_biprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] [M.IsLocallyFree] [N.IsLocallyFree] :
              (M ⊞ N).IsLocallyFree

              The direct sum of two locally free sheaves of modules is locally free.

              source
              instance TauCeti.SheafOfModules.isFiniteType_biprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] [M.IsFiniteType] [N.IsFiniteType] :
              (M ⊞ N).IsFiniteType

              The direct sum of two sheaves of modules of finite type is of finite type.

              source
              instance TauCeti.SheafOfModules.isQuasicoherent_biprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] [M.IsQuasicoherent] [N.IsQuasicoherent] :
              (M ⊞ N).IsQuasicoherent

              The direct sum of two quasi-coherent sheaves of modules is quasi-coherent.

              source
              instance TauCeti.SheafOfModules.isFinitePresentation_biprod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} [CategoryTheory.Limits.HasPullbacks C] [M.IsFinitePresentation] [N.IsFinitePresentation] :
              (M ⊞ N).IsFinitePresentation

              The direct sum of two finitely presented sheaves of modules is finitely presented.