Mapping cones of curved duplexes #
For a closed even map f : X ⟶ Y of curved duplexes with the same curvature, its cone has
components X₁ ⊞ Y₀ and X₀ ⊞ Y₁. The differential is the block matrix with diagonal
entries -d_X and d_Y and lower-left entry f. Its square remains multiplication by the
curvature: the off-diagonal terms cancel because f commutes with the differentials.
The canonical inclusion of Y and projection to the parity shift of X give the sequence
Y ⟶ cone(f) ⟶ X[1] used to form cone triangles in the homotopy category. The cone behaves
like a cofibre of f: the composite X ⟶ Y ⟶ cone(f) is null-homotopic, and the cone of an
isomorphism is contractible.
The parity shift is the only shift curved duplexes carry, so its compatibility with the cone is
recorded here too: the parity shift of cone(f) is the cone of the parity shift of f, the two
differing only by the sign on the summand coming from Y.
This is the curved analogue of the ordinary mapping cone; see Frenkel, Khovanov and Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compositio Mathematica 141 (2005), Sections 2–3.
noncomputable def
TauCeti.CurvedDuplex.coneD₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
The first differential of the cone, from X₁ ⊞ Y₀ to X₀ ⊞ Y₁.
Equations
Instances For
noncomputable def
TauCeti.CurvedDuplex.coneD₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
The second differential of the cone, from X₀ ⊞ Y₁ to X₁ ⊞ Y₀.
Equations
Instances For
@[implicit_reducible]
noncomputable def
TauCeti.CurvedDuplex.cone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
CurvedDuplex C w
The mapping cone of a closed even map of curved duplexes. Both squares of its differential
are multiplication by the original curvature w.
Equations
- TauCeti.CurvedDuplex.cone f = { X₀ := X.X₁ ⊞ Y.X₀, X₁ := X.X₀ ⊞ Y.X₁, d₀ := TauCeti.CurvedDuplex.coneD₀ f, d₁ := TauCeti.CurvedDuplex.coneD₁ f, d₀_comp_d₁ := ⋯, d₁_comp_d₀ := ⋯ }
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.cone_X₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.cone_X₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.cone_d₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.cone_d₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.biprod_inl_comp_coneD₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.biprod_inr_comp_coneD₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.biprod_inl_comp_coneD₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.biprod_inr_comp_coneD₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
noncomputable def
TauCeti.CurvedDuplex.coneInclusion
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
The canonical inclusion of the codomain into the cone.
Equations
- TauCeti.CurvedDuplex.coneInclusion f = { f₀ := CategoryTheory.Limits.biprod.inr, f₁ := CategoryTheory.Limits.biprod.inr, comm₀ := ⋯, comm₁ := ⋯ }
Instances For
noncomputable def
TauCeti.CurvedDuplex.coneProjection
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
The canonical projection from the cone onto the parity shift of the domain.
Equations
- TauCeti.CurvedDuplex.coneProjection f = { f₀ := CategoryTheory.Limits.biprod.fst, f₁ := CategoryTheory.Limits.biprod.fst, comm₀ := ⋯, comm₁ := ⋯ }
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.coneInclusion_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneInclusion_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneProjection_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneProjection_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneInclusion_comp_coneProjection
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
The inclusion followed by the projection vanishes.
@[simp]
theorem
TauCeti.CurvedDuplex.coneInclusion_comp_coneProjection_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
{Z : CurvedDuplex C w}
(h : (parityShift C w).obj X ⟶ Z)
:
The inclusion followed by the projection vanishes.
theorem
TauCeti.CurvedDuplex.comp_coneInclusion
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
The composite X ⟶ Y ⟶ cone(f) is null-homotopic: it is d h + h d for the odd map given
by the two biproduct inclusions.
@[simp]
theorem
TauCeti.CurvedDuplex.quotientFunctor_map_comp_coneInclusion
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp ((nullHomotopic C w).quotientFunctor.map f)
((nullHomotopic C w).quotientFunctor.map (coneInclusion f)) = 0
The composite X ⟶ Y ⟶ cone(f) vanishes in the homotopy category.
theorem
TauCeti.CurvedDuplex.nullHomotopicMap_cone_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
:
nullHomotopicMap
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd
(CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f).f₀ CategoryTheory.Limits.biprod.inl))
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd
(CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f).f₁ CategoryTheory.Limits.biprod.inl)) = CategoryTheory.CategoryStruct.id (cone f)
The cone of an isomorphism is contractible. The odd contracting map applies the inverse to the second summand and sends the result into the first summand.
theorem
TauCeti.CurvedDuplex.isZero_quotientFunctor_obj_cone_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
:
CategoryTheory.Limits.IsZero ((nullHomotopic C w).quotientFunctor.obj (cone f))
The cone of an isomorphism becomes a zero object in the homotopy category.
noncomputable def
TauCeti.CurvedDuplex.coneParityShiftIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
The parity shift of the cone of f is the cone of the parity shift of f. Both curved
duplexes have the same components; the isomorphism negates the summand coming from the codomain
of f, which is where the sign of the parity shift and the sign of the cone differ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.coneParityShiftIso_hom_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneParityShiftIso_hom_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneParityShiftIso_inv_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.coneParityShiftIso_inv_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
noncomputable def
TauCeti.CurvedDuplex.coneMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X' Y' : CurvedDuplex C w}
(f : X ⟶ Y)
(g : X' ⟶ Y')
(a : X ⟶ X')
(b : Y ⟶ Y')
(h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g)
:
A commutative square of closed even maps induces a map of their cones, componentwise given by the biproducts of its vertical maps.
Equations
- TauCeti.CurvedDuplex.coneMap f g a b h = { f₀ := CategoryTheory.Limits.biprod.map a.f₁ b.f₀, f₁ := CategoryTheory.Limits.biprod.map a.f₀ b.f₁, comm₀ := ⋯, comm₁ := ⋯ }
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.coneMap_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X' Y' : CurvedDuplex C w}
(f : X ⟶ Y)
(g : X' ⟶ Y')
(a : X ⟶ X')
(b : Y ⟶ Y')
(h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g)
:
The even component of the map induced on cones.
@[simp]
theorem
TauCeti.CurvedDuplex.coneMap_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X' Y' : CurvedDuplex C w}
(f : X ⟶ Y)
(g : X' ⟶ Y')
(a : X ⟶ X')
(b : Y ⟶ Y')
(h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g)
:
The odd component of the map induced on cones.
@[simp]
theorem
TauCeti.CurvedDuplex.coneInclusion_comp_coneMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X' Y' : CurvedDuplex C w}
(f : X ⟶ Y)
(g : X' ⟶ Y')
(a : X ⟶ X')
(b : Y ⟶ Y')
(h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g)
:
CategoryTheory.CategoryStruct.comp (coneInclusion f) (coneMap f g a b h) = CategoryTheory.CategoryStruct.comp b (coneInclusion g)
Cone maps commute with the inclusions of their codomains.
@[simp]
theorem
TauCeti.CurvedDuplex.coneInclusion_comp_coneMap_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X' Y' : CurvedDuplex C w}
(f : X ⟶ Y)
(g : X' ⟶ Y')
(a : X ⟶ X')
(b : Y ⟶ Y')
(h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g)
{Z : CurvedDuplex C w}
(h✝ : cone g ⟶ Z)
:
Cone maps commute with the inclusions of their codomains.
@[simp]
theorem
TauCeti.CurvedDuplex.coneMap_comp_coneProjection
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X' Y' : CurvedDuplex C w}
(f : X ⟶ Y)
(g : X' ⟶ Y')
(a : X ⟶ X')
(b : Y ⟶ Y')
(h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g)
:
CategoryTheory.CategoryStruct.comp (coneMap f g a b h) (coneProjection g) = CategoryTheory.CategoryStruct.comp (coneProjection f) ((parityShift C w).map a)
Cone maps commute with the projections to the shifted domains.
@[simp]
theorem
TauCeti.CurvedDuplex.coneMap_comp_coneProjection_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X' Y' : CurvedDuplex C w}
(f : X ⟶ Y)
(g : X' ⟶ Y')
(a : X ⟶ X')
(b : Y ⟶ Y')
(h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g)
{Z : CurvedDuplex C w}
(h✝ : (parityShift C w).obj X' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (coneMap f g a b h) (CategoryTheory.CategoryStruct.comp (coneProjection g) h✝) = CategoryTheory.CategoryStruct.comp (coneProjection f)
(CategoryTheory.CategoryStruct.comp ((parityShift C w).map a) h✝)
Cone maps commute with the projections to the shifted domains.
@[simp]
theorem
TauCeti.CurvedDuplex.coneMap_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
(f : X ⟶ Y)
:
The identity square induces the identity on the cone.
theorem
TauCeti.CurvedDuplex.coneMap_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X' Y' X'' Y'' : CurvedDuplex C w}
(f : X ⟶ Y)
(g : X' ⟶ Y')
(k : X'' ⟶ Y'')
(a : X ⟶ X')
(b : Y ⟶ Y')
(a' : X' ⟶ X'')
(b' : Y' ⟶ Y'')
(h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g)
(h' : CategoryTheory.CategoryStruct.comp g b' = CategoryTheory.CategoryStruct.comp a' k)
:
coneMap f k (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b') ⋯ = CategoryTheory.CategoryStruct.comp (coneMap f g a b h) (coneMap g k a' b' h')
Composing commutative squares composes their induced cone maps.
instance
TauCeti.CurvedDuplex.isIso_coneMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X' Y' : CurvedDuplex C w}
(f : X ⟶ Y)
(g : X' ⟶ Y')
(a : X ⟶ X')
(b : Y ⟶ Y')
(h : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a g)
[CategoryTheory.IsIso a]
[CategoryTheory.IsIso b]
:
CategoryTheory.IsIso (coneMap f g a b h)
A square whose two vertical maps are isomorphisms induces an isomorphism of cones.