Limits and colimits of curved duplexes #
Limits and colimits of curved duplexes are computed componentwise. If a diagram
F : J ⥤ CurvedDuplex C w has a limit after evaluation at both components, then the two
componentwise limits, with the differentials induced by those of the duplexes in the diagram,
form a curved duplex of curvature w, and this is a limit of F preserved by both evaluation
functors. The same holds for colimits.
The curvature equations of the componentwise limit hold because the curvature acts through the
linear structure, hence commutes with the limit projections. No limits are assumed in C; this is
what lets an exact structure on C induce a componentwise exact structure on curved duplexes,
whose kernels, cokernels, pushouts and pullbacks exist only for the diagrams the axioms need.
The construction follows Joël Riou's Mathlib.Algebra.Homology.HomologicalComplexLimits for
homological complexes.
Main definitions #
TauCeti.CurvedDuplex.d₀NatTransandTauCeti.CurvedDuplex.d₁NatTrans: the differentials as natural transformations between the evaluation functors.TauCeti.CurvedDuplex.isLimitOfEvalandTauCeti.CurvedDuplex.isColimitOfEval: a cone (resp. cocone) whose evaluations at both components are limits (resp. colimits) is a limit (resp. colimit).TauCeti.CurvedDuplex.coneOfHasLimitEvalandTauCeti.CurvedDuplex.coconeOfHasColimitEval: the componentwise limit cone and colimit cocone.
Main results #
- The instances
HasLimit FandHasColimit Fwhen the evaluated diagrams have limits (resp. colimits), withPreservesLimit F (eval₀ C w)and its variants for the other evaluation functor and for colimits. TauCeti.CurvedDuplex.hasColimit_span_comp_eval₀andTauCeti.CurvedDuplex.hasLimit_cospan_comp_eval₀, with their odd variants: a span (resp. cospan) of curved duplexes with a pushout (resp. pullback) in a component has a colimit (resp. limit) after evaluation at that component.
def
TauCeti.CurvedDuplex.d₀NatTrans
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
(w : R)
:
The even differentials of curved duplexes, as a natural transformation between the evaluation functors.
Equations
- TauCeti.CurvedDuplex.d₀NatTrans C w = { app := fun (X : TauCeti.CurvedDuplex C w) => X.d₀, naturality := ⋯ }
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.d₀NatTrans_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
The components of d₀NatTrans are the even differentials.
def
TauCeti.CurvedDuplex.d₁NatTrans
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
(w : R)
:
The odd differentials of curved duplexes, as a natural transformation between the evaluation functors.
Equations
- TauCeti.CurvedDuplex.d₁NatTrans C w = { app := fun (X : TauCeti.CurvedDuplex C w) => X.d₁, naturality := ⋯ }
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.d₁NatTrans_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
The components of d₁NatTrans are the odd differentials.
Limits #
def
TauCeti.CurvedDuplex.isLimitOfEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
(s : CategoryTheory.Limits.Cone F)
(h₀ : CategoryTheory.Limits.IsLimit ((eval₀ C w).mapCone s))
(h₁ : CategoryTheory.Limits.IsLimit ((eval₁ C w).mapCone s))
:
A cone of curved duplexes is a limit if its evaluations at the even and the odd components are limits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TauCeti.CurvedDuplex.coneOfHasLimitEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
The componentwise limit of a diagram of curved duplexes, with the differentials induced by the differentials of the duplexes in the diagram.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.coneOfHasLimitEval_pt_X₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneOfHasLimitEval_pt_X₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneOfHasLimitEval_pt_d₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneOfHasLimitEval_π_app_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
(j : J)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneOfHasLimitEval_π_app_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
(j : J)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneOfHasLimitEval_pt_d₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
noncomputable def
TauCeti.CurvedDuplex.isLimitEval₀ConeOfHasLimitEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
CategoryTheory.Limits.IsLimit ((eval₀ C w).mapCone (coneOfHasLimitEval F))
The even component of the componentwise limit cone is a limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TauCeti.CurvedDuplex.isLimitEval₁ConeOfHasLimitEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
CategoryTheory.Limits.IsLimit ((eval₁ C w).mapCone (coneOfHasLimitEval F))
The odd component of the componentwise limit cone is a limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TauCeti.CurvedDuplex.isLimitConeOfHasLimitEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
The componentwise limit cone is a limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
TauCeti.CurvedDuplex.instHasLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
instance
TauCeti.CurvedDuplex.instPreservesLimitEval₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
instance
TauCeti.CurvedDuplex.instPreservesLimitEval₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasLimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasLimit (F.comp (eval₁ C w))]
:
Colimits #
def
TauCeti.CurvedDuplex.isColimitOfEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
(s : CategoryTheory.Limits.Cocone F)
(h₀ : CategoryTheory.Limits.IsColimit ((eval₀ C w).mapCocone s))
(h₁ : CategoryTheory.Limits.IsColimit ((eval₁ C w).mapCocone s))
:
A cocone of curved duplexes is a colimit if its evaluations at the even and the odd components are colimits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TauCeti.CurvedDuplex.coconeOfHasColimitEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
The componentwise colimit of a diagram of curved duplexes, with the differentials induced by the differentials of the duplexes in the diagram.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.coconeOfHasColimitEval_pt_d₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
@[simp]
theorem
TauCeti.CurvedDuplex.coconeOfHasColimitEval_ι_app_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
(j : J)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coconeOfHasColimitEval_pt_X₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
@[simp]
theorem
TauCeti.CurvedDuplex.coconeOfHasColimitEval_pt_d₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
@[simp]
theorem
TauCeti.CurvedDuplex.coconeOfHasColimitEval_ι_app_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
(j : J)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coconeOfHasColimitEval_pt_X₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
noncomputable def
TauCeti.CurvedDuplex.isColimitEval₀CoconeOfHasColimitEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
The even component of the componentwise colimit cocone is a colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TauCeti.CurvedDuplex.isColimitEval₁CoconeOfHasColimitEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
The odd component of the componentwise colimit cocone is a colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TauCeti.CurvedDuplex.isColimitCoconeOfHasColimitEval
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
The componentwise colimit cocone is a colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
TauCeti.CurvedDuplex.instHasColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
instance
TauCeti.CurvedDuplex.instPreservesColimitEval₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
instance
TauCeti.CurvedDuplex.instPreservesColimitEval₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{J : Type u'}
[CategoryTheory.Category.{v', u'} J]
(F : CategoryTheory.Functor J (CurvedDuplex C w))
[CategoryTheory.Limits.HasColimit (F.comp (eval₀ C w))]
[CategoryTheory.Limits.HasColimit (F.comp (eval₁ C w))]
:
Pushouts and pullbacks #
theorem
TauCeti.CurvedDuplex.hasColimit_span_comp_eval₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y Z : CurvedDuplex C w}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f.f₀ g.f₀]
:
CategoryTheory.Limits.HasColimit ((CategoryTheory.Limits.span f g).comp (eval₀ C w))
If a span of curved duplexes has a pushout in the even component, then its composite with the even evaluation functor has a colimit.
theorem
TauCeti.CurvedDuplex.hasColimit_span_comp_eval₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y Z : CurvedDuplex C w}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f.f₁ g.f₁]
:
CategoryTheory.Limits.HasColimit ((CategoryTheory.Limits.span f g).comp (eval₁ C w))
If a span of curved duplexes has a pushout in the odd component, then its composite with the odd evaluation functor has a colimit.
theorem
TauCeti.CurvedDuplex.hasLimit_cospan_comp_eval₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y Z : CurvedDuplex C w}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f.f₀ g.f₀]
:
CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan f g).comp (eval₀ C w))
If a cospan of curved duplexes has a pullback in the even component, then its composite with the even evaluation functor has a limit.
theorem
TauCeti.CurvedDuplex.hasLimit_cospan_comp_eval₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y Z : CurvedDuplex C w}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f.f₁ g.f₁]
:
CategoryTheory.Limits.HasLimit ((CategoryTheory.Limits.cospan f g).comp (eval₁ C w))
If a cospan of curved duplexes has a pullback in the odd component, then its composite with the odd evaluation functor has a limit.