Colimits in categories of presheaves of modules #
In this file, it is shown that under suitable assumptions,
colimits exist in the category PresheafOfModules R
.
def
PresheafOfModules.evaluationJointlyReflectsColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
(c : CategoryTheory.Limits.Cocone F)
(hc : (X : Cᵒᵖ) → CategoryTheory.Limits.IsColimit ((PresheafOfModules.evaluation R X).mapCocone c))
:
A cocone in the category PresheafOfModules R
is colimit if it is so after the application
of the functors evaluation R X
for all X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
PresheafOfModules.instHasColimitModuleCatαRingObjOppositeRingCatCompEvaluationRestrictScalarsMap
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(f : X ⟶ Y)
:
CategoryTheory.Limits.HasColimit
(F.comp ((PresheafOfModules.evaluation R Y).comp (ModuleCat.restrictScalars (R.map f))))
Equations
- ⋯ = ⋯
@[simp]
theorem
PresheafOfModules.colimitPresheafOfModules_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(f : X ⟶ Y)
:
(PresheafOfModules.colimitPresheafOfModules F).map f = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimMap (CategoryTheory.whiskerLeft F (PresheafOfModules.restriction R f)))
(CategoryTheory.preservesColimitIso (ModuleCat.restrictScalars (R.map f))
(F.comp (PresheafOfModules.evaluation R Y))).inv
@[simp]
theorem
PresheafOfModules.colimitPresheafOfModules_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
(X : Cᵒᵖ)
:
(PresheafOfModules.colimitPresheafOfModules F).obj X = CategoryTheory.Limits.colimit (F.comp (PresheafOfModules.evaluation R X))
noncomputable def
PresheafOfModules.colimitPresheafOfModules
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
:
Given F : J ⥤ PresheafOfModules.{v} R
, this is the presheaf of modules obtained by
taking a colimit in the category of modules over R.obj X
for all X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
PresheafOfModules.colimitCocone_ι_app_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
(j : J)
(X : Cᵒᵖ)
:
((PresheafOfModules.colimitCocone F).ι.app j).app X = CategoryTheory.Limits.colimit.ι (F.comp (PresheafOfModules.evaluation R X)) j
@[simp]
theorem
PresheafOfModules.colimitCocone_pt
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
:
noncomputable def
PresheafOfModules.colimitCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
:
The (colimit) cocone for F : J ⥤ PresheafOfModules.{v} R
that is constructed from
the colimit of F ⋙ evaluation R X
for all X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
PresheafOfModules.isColimitColimitCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
:
The cocone colimitCocone F
is colimit for any F : J ⥤ PresheafOfModules.{v} R
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
PresheafOfModules.hasColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
:
Equations
- ⋯ = ⋯
noncomputable instance
PresheafOfModules.evaluationPreservesColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
(X : Cᵒᵖ)
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
PresheafOfModules.toPresheafPreservesColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J (PresheafOfModules R))
[{X Y : Cᵒᵖ} →
(f : X ⟶ Y) →
CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
(ModuleCat.restrictScalars (R.map f))]
[∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
[(X : Cᵒᵖ) →
CategoryTheory.Limits.PreservesColimit F
((PresheafOfModules.evaluation R X).comp (CategoryTheory.forget₂ (ModuleCat ↑(R.obj X)) AddCommGrp))]
:
Equations
- One or more equations did not get rendered due to their size.
instance
PresheafOfModules.hasColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(R : CategoryTheory.Functor Cᵒᵖ RingCat)
(J : Type u₂)
[CategoryTheory.Category.{v₂, u₂} J]
[CategoryTheory.Limits.HasColimitsOfShape J AddCommGrp]
:
Equations
- ⋯ = ⋯
noncomputable instance
PresheafOfModules.evaluationPreservesColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(R : CategoryTheory.Functor Cᵒᵖ RingCat)
(J : Type u₂)
[CategoryTheory.Category.{v₂, u₂} J]
[CategoryTheory.Limits.HasColimitsOfShape J AddCommGrp]
(X : Cᵒᵖ)
:
Equations
- PresheafOfModules.evaluationPreservesColimitsOfShape R J X = { preservesColimit := fun {K : CategoryTheory.Functor J (PresheafOfModules R)} => inferInstance }
noncomputable instance
PresheafOfModules.toPresheafPreservesColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(R : CategoryTheory.Functor Cᵒᵖ RingCat)
(J : Type u₂)
[CategoryTheory.Category.{v₂, u₂} J]
[CategoryTheory.Limits.HasColimitsOfShape J AddCommGrp]
:
Equations
- PresheafOfModules.toPresheafPreservesColimitsOfShape R J = { preservesColimit := fun {K : CategoryTheory.Functor J (PresheafOfModules R)} => inferInstance }
instance
PresheafOfModules.Finite.hasFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(R : CategoryTheory.Functor Cᵒᵖ RingCat)
:
Equations
- ⋯ = ⋯
noncomputable instance
PresheafOfModules.Finite.evaluationPreservesFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(R : CategoryTheory.Functor Cᵒᵖ RingCat)
(X : Cᵒᵖ)
:
Equations
- PresheafOfModules.Finite.evaluationPreservesFiniteColimits R X = { preservesFiniteColimits := inferInstance }
noncomputable instance
PresheafOfModules.Finite.toPresheafPreservesFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(R : CategoryTheory.Functor Cᵒᵖ RingCat)
:
Equations
- PresheafOfModules.Finite.toPresheafPreservesFiniteColimits R = { preservesFiniteColimits := inferInstance }