Null-homotopic maps factor through elementary disks #
For curved duplexes of the same curvature, the boundary of an odd map factors through the direct sum of a disk and a parity-shifted disk. Conversely, this direct sum is contractible, so every morphism factoring through it is null-homotopic. In particular, a contractible duplex is a retract of the disk sum on its two components. This gives the concrete factorization needed to compare the homotopy quotient with a stable quotient of a split exact category.
The disk sum is functorial (diskSumMap), and the projection diskSumToParityShift from the
disk sum onto the parity shift kills the inclusion toDiskSum. The resulting sequence
X ⟶ diskSum X ⟶ X[1] splits in both components; it presents the stable suspension of X as
its parity shift.
The disk construction and its role in the homotopy category follow Frenkel, Khovanov and Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Sections 2–3.
noncomputable def
TauCeti.CurvedDuplex.diskSum
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
CurvedDuplex C w
The two elementary disks associated to the components of a duplex, with the disk on the even component shifted in parity.
Equations
- X.diskSum = (TauCeti.CurvedDuplex.disk w X.X₁).biprod ((TauCeti.CurvedDuplex.parityShift C w).obj (TauCeti.CurvedDuplex.disk w X.X₀))
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.diskSum_X₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
@[simp]
theorem
TauCeti.CurvedDuplex.diskSum_X₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
@[simp]
theorem
TauCeti.CurvedDuplex.diskSum_d₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
@[simp]
theorem
TauCeti.CurvedDuplex.diskSum_d₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
def
TauCeti.CurvedDuplex.toOddDisk
{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 canonical map from a duplex to the disk on its odd component.
Equations
Instances For
def
TauCeti.CurvedDuplex.toEvenShiftedDisk
{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 canonical map from a duplex to the shifted disk on its even component.
Equations
- X.toEvenShiftedDisk = { f₀ := CategoryTheory.CategoryStruct.id X.X₀, f₁ := -X.d₁, comm₀ := ⋯, comm₁ := ⋯ }
Instances For
def
TauCeti.CurvedDuplex.fromOddDisk
{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}
(h₁ : X.X₁ ⟶ Y.X₀)
:
The map out of the odd disk determined by the odd-to-even part of a homotopy.
Equations
Instances For
def
TauCeti.CurvedDuplex.fromEvenShiftedDisk
{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}
(h₀ : X.X₀ ⟶ Y.X₁)
:
The map out of the shifted even disk determined by the even-to-odd part of a homotopy.
Equations
- TauCeti.CurvedDuplex.fromEvenShiftedDisk h₀ = { f₀ := CategoryTheory.CategoryStruct.comp h₀ Y.d₁, f₁ := -h₀, comm₀ := ⋯, comm₁ := ⋯ }
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.toOddDisk_f₀
{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)
:
@[simp]
theorem
TauCeti.CurvedDuplex.toOddDisk_f₁
{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)
:
@[simp]
theorem
TauCeti.CurvedDuplex.toEvenShiftedDisk_f₀
{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)
:
@[simp]
theorem
TauCeti.CurvedDuplex.toEvenShiftedDisk_f₁
{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)
:
@[simp]
theorem
TauCeti.CurvedDuplex.fromOddDisk_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}
(h₁ : X.X₁ ⟶ Y.X₀)
:
@[simp]
theorem
TauCeti.CurvedDuplex.fromOddDisk_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}
(h₁ : X.X₁ ⟶ Y.X₀)
:
@[simp]
theorem
TauCeti.CurvedDuplex.fromEvenShiftedDisk_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}
(h₀ : X.X₀ ⟶ Y.X₁)
:
@[simp]
theorem
TauCeti.CurvedDuplex.fromEvenShiftedDisk_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}
(h₀ : X.X₀ ⟶ Y.X₁)
:
noncomputable def
TauCeti.CurvedDuplex.toDiskSum
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
The map into the two disks determined by the source duplex.
Equations
Instances For
noncomputable def
TauCeti.CurvedDuplex.fromDiskSum
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(h₀ : X.X₀ ⟶ Y.X₁)
(h₁ : X.X₁ ⟶ Y.X₀)
:
The map out of the two disks determined by an odd homotopy.
Equations
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.toDiskSum_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
@[simp]
theorem
TauCeti.CurvedDuplex.toDiskSum_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
@[simp]
theorem
TauCeti.CurvedDuplex.fromDiskSum_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(h₀ : X.X₀ ⟶ Y.X₁)
(h₁ : X.X₁ ⟶ Y.X₀)
:
(fromDiskSum h₀ h₁).f₀ = CategoryTheory.Limits.biprod.desc h₁ (CategoryTheory.CategoryStruct.comp h₀ Y.d₁)
@[simp]
theorem
TauCeti.CurvedDuplex.fromDiskSum_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(h₀ : X.X₀ ⟶ Y.X₁)
(h₁ : X.X₁ ⟶ Y.X₀)
:
(fromDiskSum h₀ h₁).f₁ = CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.comp h₁ Y.d₀) (-h₀)
@[simp]
theorem
TauCeti.CurvedDuplex.toDiskSum_comp_fromDiskSum
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(h₀ : X.X₀ ⟶ Y.X₁)
(h₁ : X.X₁ ⟶ Y.X₀)
:
A homotopy boundary factors through the direct sum of two elementary disks.
noncomputable def
TauCeti.CurvedDuplex.diskSumToParityShift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
The map from the disk sum on the components of X onto the parity shift of X. Together with
toDiskSum X it forms a short complex X ⟶ diskSum X ⟶ X[1] which splits in both components.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.diskSumToParityShift_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
@[simp]
theorem
TauCeti.CurvedDuplex.diskSumToParityShift_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
@[simp]
theorem
TauCeti.CurvedDuplex.toDiskSum_comp_diskSumToParityShift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
The inclusion of a duplex into its disk sum, followed by the projection onto its parity shift, vanishes.
@[simp]
theorem
TauCeti.CurvedDuplex.toDiskSum_comp_diskSumToParityShift_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
{Z : CurvedDuplex C w}
(h : (parityShift C w).obj X ⟶ Z)
:
The inclusion of a duplex into its disk sum, followed by the projection onto its parity shift, vanishes.
noncomputable def
TauCeti.CurvedDuplex.diskSumMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(f : X ⟶ Y)
:
The map induced on disk sums by a morphism of curved duplexes.
Equations
- TauCeti.CurvedDuplex.diskSumMap f = { f₀ := CategoryTheory.Limits.biprod.map f.f₁ f.f₀, f₁ := CategoryTheory.Limits.biprod.map f.f₁ f.f₀, comm₀ := ⋯, comm₁ := ⋯ }
Instances For
@[simp]
theorem
TauCeti.CurvedDuplex.diskSumMap_f₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.diskSumMap_f₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(f : X ⟶ Y)
:
@[simp]
theorem
TauCeti.CurvedDuplex.toDiskSum_comp_diskSumMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(f : X ⟶ Y)
:
The inclusion into the disk sum is natural.
@[simp]
theorem
TauCeti.CurvedDuplex.toDiskSum_comp_diskSumMap_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(f : X ⟶ Y)
{Z : CurvedDuplex C w}
(h : Y.diskSum ⟶ Z)
:
The inclusion into the disk sum is natural.
@[simp]
theorem
TauCeti.CurvedDuplex.diskSumToParityShift_comp_parityShift_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(f : X ⟶ Y)
:
The projection from the disk sum onto the parity shift is natural.
@[simp]
theorem
TauCeti.CurvedDuplex.diskSumToParityShift_comp_parityShift_map_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(f : X ⟶ Y)
{Z : CurvedDuplex C w}
(h : (parityShift C w).obj Y ⟶ Z)
:
The projection from the disk sum onto the parity shift is natural.
theorem
TauCeti.CurvedDuplex.id_diskSum_mem_nullHomotopic
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
:
The disk sum itself is contractible.
theorem
TauCeti.CurvedDuplex.mem_nullHomotopic_iff_factors_diskSum
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
{X Y : CurvedDuplex C w}
(f : X ⟶ Y)
:
f ∈ (nullHomotopic C w).hom X Y ↔ ∃ (a : X ⟶ X.diskSum) (b : X.diskSum ⟶ Y), CategoryTheory.CategoryStruct.comp a b = f
A map is null-homotopic exactly when it factors through the disk sum on its source.
noncomputable def
TauCeti.CurvedDuplex.retractDiskSum
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{R : Type w'}
[Semiring R]
[CategoryTheory.Linear R C]
{w : R}
(X : CurvedDuplex C w)
(h : CategoryTheory.CategoryStruct.id X ∈ (nullHomotopic C w).hom X X)
:
A contractible duplex is a retract of the direct sum of the disks on its components.
Equations
- X.retractDiskSum h = { i := Classical.choose ⋯, r := Classical.choose ⋯, retract := ⋯ }