The Hom complex of two curved duplexes

For duplexes with the same curvature, the even and odd pairs of component maps form a two-periodic complex. Its differential is the graded commutator with the duplex differentials. The curvature terms cancel in its square. Degree-zero cycles are the closed even morphisms of duplexes, and degree-zero boundaries are their null-homotopic morphisms.

The sign convention follows Frenkel, Khovanov, and Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compositio Mathematica 141 (2005), Sections 2–3.

@[reducible, inline]

abbrev TauCeti.CurvedDuplex.EvenCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : Type v

The degree-zero component of the Hom complex: pairs of maps preserving parity.

Equations

• X.EvenCochain Y = ((X.X₀ ⟶ Y.X₀) × (X.X₁ ⟶ Y.X₁))

@[reducible, inline]

abbrev TauCeti.CurvedDuplex.OddCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : Type v

The degree-one component of the Hom complex: pairs of maps reversing parity.

Equations

• X.OddCochain Y = ((X.X₀ ⟶ Y.X₁) × (X.X₁ ⟶ Y.X₀))

def TauCeti.CurvedDuplex.evenDifferential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : X.EvenCochain Y →ₗ[R] X.OddCochain Y

The graded commutator on even maps.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.CurvedDuplex.oddDifferential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : X.OddCochain Y →ₗ[R] X.EvenCochain Y

The graded commutator on odd maps. Its plus signs reflect that odd maps have degree one modulo two.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CurvedDuplex.evenDifferential_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) (f : X.EvenCochain Y) : (X.evenDifferential Y) f = (CategoryTheory.CategoryStruct.comp f.1 Y.d₀ - CategoryTheory.CategoryStruct.comp X.d₀ f.2, CategoryTheory.CategoryStruct.comp f.2 Y.d₁ - CategoryTheory.CategoryStruct.comp X.d₁ f.1)

@[simp]

theorem TauCeti.CurvedDuplex.oddDifferential_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) (h : X.OddCochain Y) : (X.oddDifferential Y) h = (CategoryTheory.CategoryStruct.comp X.d₀ h.2 + CategoryTheory.CategoryStruct.comp h.1 Y.d₁, CategoryTheory.CategoryStruct.comp X.d₁ h.1 + CategoryTheory.CategoryStruct.comp h.2 Y.d₀)

@[simp]

theorem TauCeti.CurvedDuplex.oddDifferential_comp_evenDifferential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : X.oddDifferential Y ∘ₗ X.evenDifferential Y = 0

The even-to-odd differential followed by the odd-to-even differential vanishes.

@[simp]

theorem TauCeti.CurvedDuplex.evenDifferential_comp_oddDifferential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : X.evenDifferential Y ∘ₗ X.oddDifferential Y = 0

The odd-to-even differential followed by the even-to-odd differential vanishes.

def TauCeti.CurvedDuplex.homComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : CurvedDuplex (ModuleCat R) 0

The two-periodic Hom complex of curved duplexes with a common curvature.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CurvedDuplex.homComplex_X₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.homComplex Y).X₀ = ↧(X.EvenCochain Y)

@[simp]

theorem TauCeti.CurvedDuplex.homComplex_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.homComplex Y).X₁ = ↧(X.OddCochain Y)

@[simp]

theorem TauCeti.CurvedDuplex.homComplex_d₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.homComplex Y).d₀ = ModuleCat.ofHom (X.evenDifferential Y)

@[simp]

theorem TauCeti.CurvedDuplex.homComplex_d₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X.homComplex Y).d₁ = ModuleCat.ofHom (X.oddDifferential Y)

theorem TauCeti.CurvedDuplex.evenDifferential_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) (f : X.EvenCochain Y) : (X.evenDifferential Y) f = 0 ↔ CategoryTheory.CategoryStruct.comp f.1 Y.d₀ = CategoryTheory.CategoryStruct.comp X.d₀ f.2 ∧ CategoryTheory.CategoryStruct.comp f.2 Y.d₁ = CategoryTheory.CategoryStruct.comp X.d₁ f.1

An even pair is a degree-zero cycle exactly when it defines a closed duplex map.

@[simp]

theorem TauCeti.CurvedDuplex.evenDifferential_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) (f : X ⟶ Y) : (CategoryTheory.CategoryStruct.comp f.f₀ Y.d₀ - CategoryTheory.CategoryStruct.comp X.d₀ f.f₁, CategoryTheory.CategoryStruct.comp f.f₁ Y.d₁ - CategoryTheory.CategoryStruct.comp X.d₁ f.f₀) = 0

A closed even map gives a cycle in the Hom complex.

def TauCeti.CurvedDuplex.homEquivCycles {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) : (X ⟶ Y) ≃ₗ[R] ↥(X.evenDifferential Y).ker

Degree-zero cycles in the Hom complex are precisely closed even maps of duplexes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CurvedDuplex.homEquivCycles_apply_val {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) (f : X ⟶ Y) : ↑((X.homEquivCycles Y) f) = (f.f₀, f.f₁)

@[simp]

theorem TauCeti.CurvedDuplex.homEquivCycles_symm_f₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) (z : ↥(X.evenDifferential Y).ker) : ((X.homEquivCycles Y).symm z).f₀ = (↑z).1

@[simp]

theorem TauCeti.CurvedDuplex.homEquivCycles_symm_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) (z : ↥(X.evenDifferential Y).ker) : ((X.homEquivCycles Y).symm z).f₁ = (↑z).2

theorem TauCeti.CurvedDuplex.oddDifferential_eq_nullHomotopicMap_components {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) (h : X.OddCochain Y) : (X.oddDifferential Y) h = ((nullHomotopicMap h.1 h.2).f₀, (nullHomotopicMap h.1 h.2).f₁)

An odd boundary is the pair of components of the null-homotopic map it defines.

theorem TauCeti.CurvedDuplex.mem_nullHomotopic_iff_exists_oddDifferential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [CommRing R] [CategoryTheory.Linear R C] {w₀ : R} (X Y : CurvedDuplex C w₀) (f : X ⟶ Y) : f ∈ (nullHomotopic C w₀).hom X Y ↔ ∃ (h : X.OddCochain Y), (X.oddDifferential Y) h = (f.f₀, f.f₁)

A closed map is null-homotopic exactly when its cycle is an odd boundary.