Curved duplexes and their homotopy category

Let C be an R-linear category and w : R. A curved duplex of curvature w in C is a pair of objects with maps in both directions

X₀ --d₀--> X₁ --d₁--> X₀

whose two composites are both w • 𝟙. Since w acts through the linear structure, it commutes with every morphism of C; this is the central, parity-graded case of a curved module, in which the square of the differential is multiplication by the curvature. For C = ModuleCat S over a commutative ring S, a curved duplex whose two components are finitely generated projective is a matrix factorization of w. For w = 0 the two equations say that both composites vanish: a curved duplex of curvature zero is a genuine two-periodic complex. For w ≠ 0 a curved duplex has no homology in general, so homotopy is its primitive notion of equivalence.

This file sets up

• the category CurvedDuplex C w of curved duplexes and even closed morphisms (pairs of maps commuting with both differentials), which is preadditive and R-linear, with the two evaluation functors to C;
• the parity shift CurvedDuplex.parityShift, which swaps the two components and negates both differentials, and the natural isomorphism exhibiting it as an involution;
• the null-homotopic morphisms d h + h d for odd maps h = (h₀, h₁), which form a two-sided ideal CurvedDuplex.nullHomotopic because source and target have the same curvature;
• the homotopy category CurvedDuplex.HomotopyCategory C w, the quotient by that ideal, which is preadditive and R-linear, together with the parity shift it inherits;
• the elementary disk A --𝟙--> A --w•𝟙--> A on an object A, whose morphisms to a duplex are the morphisms from A to its even component, and which is contractible and therefore zero in the homotopy category.

Main definitions

• TauCeti.CurvedDuplex C w: curved duplexes of curvature w in the linear category C.
• TauCeti.CurvedDuplex.parityShift: the parity shift, and TauCeti.CurvedDuplex.parityShiftEquivalence the resulting self-equivalence.
• TauCeti.CurvedDuplex.nullHomotopicMap: the morphism d h + h d of an odd map (h₀, h₁).
• TauCeti.CurvedDuplex.nullHomotopic: the ideal of null-homotopic morphisms.
• TauCeti.CurvedDuplex.HomotopyCategory: the homotopy category of curved duplexes.
• TauCeti.CurvedDuplex.disk: the elementary disk on an object.

Main results

• TauCeti.CurvedDuplex.quotientFunctor_map_eq_quotientFunctor_map_iff: two morphisms become equal in the homotopy category exactly when their difference is d h + h d for an odd map h.
• TauCeti.CurvedDuplex.diskHomEquiv: morphisms out of the disk on A correspond to morphisms from A to the even component.
• TauCeti.CurvedDuplex.isZero_quotientFunctor_obj_disk: the disk is zero in the homotopy category.

References

• D. Eisenbud, Homological algebra on a complete intersection, with an application to group representations, Trans. Amer. Math. Soc. 260 (1980), 35–64, Section 5.
• I. Frenkel, M. Khovanov, O. Schiffmann, Homological realization of Nakajima varieties and Weyl group actions, Compos. Math. 141 (2005), 1479–1503, Sections 2–3 (curved complexes and duplexes and their homotopy categories).
• The category structure follows Joël Riou's CategoryTheory.ShortComplex in Mathlib.Algebra.Homology.ShortComplex.Basic.

structure TauCeti.CurvedDuplex (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : Type (max u v)

A curved duplex of curvature w in an R-linear category C: objects X₀ and X₁ with maps d₀ : X₀ ⟶ X₁ and d₁ : X₁ ⟶ X₀ whose composites d₀ ≫ d₁ and d₁ ≫ d₀ are both w • 𝟙. At w = 0 this is a two-periodic complex.

• X₀ : C

  The even component.

• X₁ : C

  The odd component.

• d₀ : self.X₀ ⟶ self.X₁

  The differential from the even to the odd component.

• d₁ : self.X₁ ⟶ self.X₀

  The differential from the odd to the even component.

• d₀_comp_d₁ : CategoryTheory.CategoryStruct.comp self.d₀ self.d₁ = w • CategoryTheory.CategoryStruct.id self.X₀

  The square of the differential on the even component is the curvature.

• d₁_comp_d₀ : CategoryTheory.CategoryStruct.comp self.d₁ self.d₀ = w • CategoryTheory.CategoryStruct.id self.X₁

  The square of the differential on the odd component is the curvature.

@[simp]

theorem TauCeti.CurvedDuplex.d₁_comp_d₀_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (self : CurvedDuplex C w) {Z : C} (h : self.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.d₁ (CategoryTheory.CategoryStruct.comp self.d₀ h) = CategoryTheory.CategoryStruct.comp (w • CategoryTheory.CategoryStruct.id self.X₁) h

The square of the differential on the odd component is the curvature.

@[simp]

theorem TauCeti.CurvedDuplex.d₀_comp_d₁_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (self : CurvedDuplex C w) {Z : C} (h : self.X₀ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.d₀ (CategoryTheory.CategoryStruct.comp self.d₁ h) = CategoryTheory.CategoryStruct.comp (w • CategoryTheory.CategoryStruct.id self.X₀) h

The square of the differential on the even component is the curvature.

structure TauCeti.CurvedDuplex.Hom {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) : Type v

A morphism of curved duplexes: an even closed map, that is a pair of maps between the components commuting with both differentials.

• f₀ : X.X₀ ⟶ Y.X₀

  The component on the even objects.

• f₁ : X.X₁ ⟶ Y.X₁

  The component on the odd objects.

• comm₀ : CategoryTheory.CategoryStruct.comp self.f₀ Y.d₀ = CategoryTheory.CategoryStruct.comp X.d₀ self.f₁

  The morphism commutes with the even differentials.

• comm₁ : CategoryTheory.CategoryStruct.comp self.f₁ Y.d₁ = CategoryTheory.CategoryStruct.comp X.d₁ self.f₀

  The morphism commutes with the odd differentials.

theorem TauCeti.CurvedDuplex.Hom.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {R : Type w'} {inst✝² : Semiring R} {inst✝³ : CategoryTheory.Linear R C} {w : R} {X Y : CurvedDuplex C w} {x y : X.Hom Y} (f₀ : x.f₀ = y.f₀) (f₁ : x.f₁ = y.f₁) : x = y

theorem TauCeti.CurvedDuplex.Hom.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {R : Type w'} {inst✝² : Semiring R} {inst✝³ : CategoryTheory.Linear R C} {w : R} {X Y : CurvedDuplex C w} {x y : X.Hom Y} : x = y ↔ x.f₀ = y.f₀ ∧ x.f₁ = y.f₁

theorem TauCeti.CurvedDuplex.Hom.comm₁_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} (self : X.Hom Y) {Z : C} (h : Y.X₀ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.f₁ (CategoryTheory.CategoryStruct.comp Y.d₁ h) = CategoryTheory.CategoryStruct.comp X.d₁ (CategoryTheory.CategoryStruct.comp self.f₀ h)

The morphism commutes with the odd differentials.

theorem TauCeti.CurvedDuplex.Hom.comm₀_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} (self : X.Hom Y) {Z : C} (h : Y.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.f₀ (CategoryTheory.CategoryStruct.comp Y.d₀ h) = CategoryTheory.CategoryStruct.comp X.d₀ (CategoryTheory.CategoryStruct.comp self.f₁ h)

The morphism commutes with the even differentials.

def TauCeti.CurvedDuplex.Hom.id {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) : X.Hom X

The identity morphism of a curved duplex.

Equations

• TauCeti.CurvedDuplex.Hom.id X = { f₀ := CategoryTheory.CategoryStruct.id X.X₀, f₁ := CategoryTheory.CategoryStruct.id X.X₁, comm₀ := ⋯, comm₁ := ⋯ }

@[simp]

theorem TauCeti.CurvedDuplex.Hom.id_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) : (id X).f₁ = CategoryTheory.CategoryStruct.id X.X₁

@[simp]

theorem TauCeti.CurvedDuplex.Hom.id_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) : (id X).f₀ = CategoryTheory.CategoryStruct.id X.X₀

def TauCeti.CurvedDuplex.Hom.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 Z : CurvedDuplex C w} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

The composition of morphisms of curved duplexes.

Equations

• f.comp g = { f₀ := CategoryTheory.CategoryStruct.comp f.f₀ g.f₀, f₁ := CategoryTheory.CategoryStruct.comp f.f₁ g.f₁, comm₀ := ⋯, comm₁ := ⋯ }

@[simp]

theorem TauCeti.CurvedDuplex.Hom.comp_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 Z : CurvedDuplex C w} (f : X.Hom Y) (g : Y.Hom Z) : (f.comp g).f₀ = CategoryTheory.CategoryStruct.comp f.f₀ g.f₀

@[simp]

theorem TauCeti.CurvedDuplex.Hom.comp_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 Z : CurvedDuplex C w} (f : X.Hom Y) (g : Y.Hom Z) : (f.comp g).f₁ = CategoryTheory.CategoryStruct.comp f.f₁ g.f₁

@[instance_reducible]

instance TauCeti.CurvedDuplex.instCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : CategoryTheory.Category.{v, max u v} (CurvedDuplex C w)

Equations

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

theorem TauCeti.CurvedDuplex.hom_ext {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} {f g : X ⟶ Y} (h₀ : f.f₀ = g.f₀) (h₁ : f.f₁ = g.f₁) : f = g

theorem TauCeti.CurvedDuplex.hom_ext_iff {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} {f g : X ⟶ Y} : f = g ↔ f.f₀ = g.f₀ ∧ f.f₁ = g.f₁

@[simp]

theorem TauCeti.CurvedDuplex.id_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) : (CategoryTheory.CategoryStruct.id X).f₀ = CategoryTheory.CategoryStruct.id X.X₀

@[simp]

theorem TauCeti.CurvedDuplex.id_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) : (CategoryTheory.CategoryStruct.id X).f₁ = CategoryTheory.CategoryStruct.id X.X₁

@[simp]

theorem TauCeti.CurvedDuplex.comp_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 Z : CurvedDuplex C w} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).f₀ = CategoryTheory.CategoryStruct.comp f.f₀ g.f₀

theorem TauCeti.CurvedDuplex.comp_f₀_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 Z : CurvedDuplex C w} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.X₀ ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₀ h = CategoryTheory.CategoryStruct.comp f.f₀ (CategoryTheory.CategoryStruct.comp g.f₀ h)

@[simp]

theorem TauCeti.CurvedDuplex.comp_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 Z : CurvedDuplex C w} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).f₁ = CategoryTheory.CategoryStruct.comp f.f₁ g.f₁

theorem TauCeti.CurvedDuplex.comp_f₁_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 Z : CurvedDuplex C w} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.X₁ ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₁ h = CategoryTheory.CategoryStruct.comp f.f₁ (CategoryTheory.CategoryStruct.comp g.f₁ h)

def TauCeti.CurvedDuplex.homMk {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} (f₀ : X.X₀ ⟶ Y.X₀) (f₁ : X.X₁ ⟶ Y.X₁) (comm₀ : CategoryTheory.CategoryStruct.comp f₀ Y.d₀ = CategoryTheory.CategoryStruct.comp X.d₀ f₁) (comm₁ : CategoryTheory.CategoryStruct.comp f₁ Y.d₁ = CategoryTheory.CategoryStruct.comp X.d₁ f₀) : X ⟶ Y

A constructor for morphisms of curved duplexes when the commutativity conditions are not obvious.

Equations

• TauCeti.CurvedDuplex.homMk f₀ f₁ comm₀ comm₁ = { f₀ := f₀, f₁ := f₁, comm₀ := comm₀, comm₁ := comm₁ }

@[simp]

theorem TauCeti.CurvedDuplex.homMk_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} (f₀ : X.X₀ ⟶ Y.X₀) (f₁ : X.X₁ ⟶ Y.X₁) (comm₀ : CategoryTheory.CategoryStruct.comp f₀ Y.d₀ = CategoryTheory.CategoryStruct.comp X.d₀ f₁) (comm₁ : CategoryTheory.CategoryStruct.comp f₁ Y.d₁ = CategoryTheory.CategoryStruct.comp X.d₁ f₀) : (homMk f₀ f₁ comm₀ comm₁).f₀ = f₀

@[simp]

theorem TauCeti.CurvedDuplex.homMk_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} (f₀ : X.X₀ ⟶ Y.X₀) (f₁ : X.X₁ ⟶ Y.X₁) (comm₀ : CategoryTheory.CategoryStruct.comp f₀ Y.d₀ = CategoryTheory.CategoryStruct.comp X.d₀ f₁) (comm₁ : CategoryTheory.CategoryStruct.comp f₁ Y.d₁ = CategoryTheory.CategoryStruct.comp X.d₁ f₀) : (homMk f₀ f₁ comm₀ comm₁).f₁ = f₁

@[instance_reducible]

instance TauCeti.CurvedDuplex.instAddHom {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} : Add (X ⟶ Y)

Equations

• TauCeti.CurvedDuplex.instAddHom = { add := fun (f g : X ⟶ Y) => { f₀ := f.f₀ + g.f₀, f₁ := f.f₁ + g.f₁, comm₀ := ⋯, comm₁ := ⋯ } }

@[instance_reducible]

instance TauCeti.CurvedDuplex.instSubHom {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} : Sub (X ⟶ Y)

Equations

• TauCeti.CurvedDuplex.instSubHom = { sub := fun (f g : X ⟶ Y) => { f₀ := f.f₀ - g.f₀, f₁ := f.f₁ - g.f₁, comm₀ := ⋯, comm₁ := ⋯ } }

@[instance_reducible]

instance TauCeti.CurvedDuplex.instNegHom {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} : Neg (X ⟶ Y)

Equations

• TauCeti.CurvedDuplex.instNegHom = { neg := fun (f : X ⟶ Y) => { f₀ := -f.f₀, f₁ := -f.f₁, comm₀ := ⋯, comm₁ := ⋯ } }

@[instance_reducible]

instance TauCeti.CurvedDuplex.instZeroHom {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} : Zero (X ⟶ Y)

Equations

• TauCeti.CurvedDuplex.instZeroHom = { zero := { f₀ := 0, f₁ := 0, comm₀ := ⋯, comm₁ := ⋯ } }

@[simp]

theorem TauCeti.CurvedDuplex.add_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} (f g : X ⟶ Y) : (f + g).f₀ = f.f₀ + g.f₀

@[simp]

theorem TauCeti.CurvedDuplex.add_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} (f g : X ⟶ Y) : (f + g).f₁ = f.f₁ + g.f₁

@[simp]

theorem TauCeti.CurvedDuplex.sub_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} (f g : X ⟶ Y) : (f - g).f₀ = f.f₀ - g.f₀

@[simp]

theorem TauCeti.CurvedDuplex.sub_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} (f g : X ⟶ Y) : (f - g).f₁ = f.f₁ - g.f₁

@[simp]

theorem TauCeti.CurvedDuplex.neg_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} (f : X ⟶ Y) : (-f).f₀ = -f.f₀

@[simp]

theorem TauCeti.CurvedDuplex.neg_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} (f : X ⟶ Y) : (-f).f₁ = -f.f₁

@[simp]

theorem TauCeti.CurvedDuplex.zero_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} : Hom.f₀ 0 = 0

@[simp]

theorem TauCeti.CurvedDuplex.zero_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} : Hom.f₁ 0 = 0

@[instance_reducible]

instance TauCeti.CurvedDuplex.instAddCommGroupHom {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} : AddCommGroup (X ⟶ Y)

Equations

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

@[instance_reducible]

instance TauCeti.CurvedDuplex.instPreadditive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : CategoryTheory.Preadditive (CurvedDuplex C w)

Equations

• TauCeti.CurvedDuplex.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

@[instance_reducible]

instance TauCeti.CurvedDuplex.instSMulHom {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} : SMul R (X ⟶ Y)

Equations

• TauCeti.CurvedDuplex.instSMulHom = { smul := fun (a : R) (f : X ⟶ Y) => { f₀ := a • f.f₀, f₁ := a • f.f₁, comm₀ := ⋯, comm₁ := ⋯ } }

@[simp]

theorem TauCeti.CurvedDuplex.smul_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} (a : R) (f : X ⟶ Y) : (a • f).f₀ = a • f.f₀

@[simp]

theorem TauCeti.CurvedDuplex.smul_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} (a : R) (f : X ⟶ Y) : (a • f).f₁ = a • f.f₁

@[instance_reducible]

instance TauCeti.CurvedDuplex.instModuleHom {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} : Module R (X ⟶ Y)

Equations

• TauCeti.CurvedDuplex.instModuleHom = { toSMul := TauCeti.CurvedDuplex.instSMulHom, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

instance TauCeti.CurvedDuplex.instLinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : CategoryTheory.Linear R (CurvedDuplex C w)

Equations

• TauCeti.CurvedDuplex.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

Evaluation functors

def TauCeti.CurvedDuplex.eval₀ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CategoryTheory.Functor (CurvedDuplex C w) C

The functor sending a curved duplex to its even component.

Equations

• TauCeti.CurvedDuplex.eval₀ C w = { obj := fun (X : TauCeti.CurvedDuplex C w) => X.X₀, map := fun {X Y : TauCeti.CurvedDuplex C w} (f : X ⟶ Y) => f.f₀, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem TauCeti.CurvedDuplex.eval₀_map (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} (f : X✝ ⟶ Y✝) : (eval₀ C w).map f = f.f₀

@[simp]

theorem TauCeti.CurvedDuplex.eval₀_obj (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) : (eval₀ C w).obj X = X.X₀

def TauCeti.CurvedDuplex.eval₁ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CategoryTheory.Functor (CurvedDuplex C w) C

The functor sending a curved duplex to its odd component.

Equations

• TauCeti.CurvedDuplex.eval₁ C w = { obj := fun (X : TauCeti.CurvedDuplex C w) => X.X₁, map := fun {X Y : TauCeti.CurvedDuplex C w} (f : X ⟶ Y) => f.f₁, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem TauCeti.CurvedDuplex.eval₁_obj (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) : (eval₁ C w).obj X = X.X₁

@[simp]

theorem TauCeti.CurvedDuplex.eval₁_map (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} (f : X✝ ⟶ Y✝) : (eval₁ C w).map f = f.f₁

instance TauCeti.CurvedDuplex.instAdditiveEval₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : (eval₀ C w).Additive

instance TauCeti.CurvedDuplex.instAdditiveEval₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : (eval₁ C w).Additive

instance TauCeti.CurvedDuplex.instLinearEval₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : CategoryTheory.Functor.Linear R (eval₀ C w)

instance TauCeti.CurvedDuplex.instLinearEval₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : CategoryTheory.Functor.Linear R (eval₁ C w)

instance TauCeti.CurvedDuplex.instIsIsoF₀ {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} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.f₀

instance TauCeti.CurvedDuplex.instIsIsoF₁ {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} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.f₁

def TauCeti.CurvedDuplex.isoMk {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} (e₀ : X.X₀ ≅ Y.X₀) (e₁ : X.X₁ ≅ Y.X₁) (comm₀ : CategoryTheory.CategoryStruct.comp e₀.hom Y.d₀ = CategoryTheory.CategoryStruct.comp X.d₀ e₁.hom) (comm₁ : CategoryTheory.CategoryStruct.comp e₁.hom Y.d₁ = CategoryTheory.CategoryStruct.comp X.d₁ e₀.hom) : X ≅ Y

A constructor for isomorphisms of curved duplexes from isomorphisms of their components commuting with the differentials.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.isoMk_inv {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} (e₀ : X.X₀ ≅ Y.X₀) (e₁ : X.X₁ ≅ Y.X₁) (comm₀ : CategoryTheory.CategoryStruct.comp e₀.hom Y.d₀ = CategoryTheory.CategoryStruct.comp X.d₀ e₁.hom) (comm₁ : CategoryTheory.CategoryStruct.comp e₁.hom Y.d₁ = CategoryTheory.CategoryStruct.comp X.d₁ e₀.hom) : (isoMk e₀ e₁ comm₀ comm₁).inv = homMk e₀.inv e₁.inv ⋯ ⋯

@[simp]

theorem TauCeti.CurvedDuplex.isoMk_hom {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} (e₀ : X.X₀ ≅ Y.X₀) (e₁ : X.X₁ ≅ Y.X₁) (comm₀ : CategoryTheory.CategoryStruct.comp e₀.hom Y.d₀ = CategoryTheory.CategoryStruct.comp X.d₀ e₁.hom) (comm₁ : CategoryTheory.CategoryStruct.comp e₁.hom Y.d₁ = CategoryTheory.CategoryStruct.comp X.d₁ e₀.hom) : (isoMk e₀ e₁ comm₀ comm₁).hom = homMk e₀.hom e₁.hom comm₀ comm₁

theorem TauCeti.CurvedDuplex.isIso_iff {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} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.f₀ ∧ CategoryTheory.IsIso f.f₁

A morphism of curved duplexes is an isomorphism exactly when both of its components are.

The parity shift

@[implicit_reducible]

def TauCeti.CurvedDuplex.parityShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CategoryTheory.Functor (CurvedDuplex C w) (CurvedDuplex C w)

The parity shift of curved duplexes: it swaps the even and odd components and negates both differentials, (X₁ --(-d₁)--> X₀ --(-d₀)--> X₁).

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.parityShift_obj_d₁ (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) : ((parityShift C w).obj X).d₁ = -X.d₀

@[simp]

theorem TauCeti.CurvedDuplex.parityShift_obj_d₀ (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) : ((parityShift C w).obj X).d₀ = -X.d₁

@[simp]

theorem TauCeti.CurvedDuplex.parityShift_map_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} (f : X✝ ⟶ Y✝) : ((parityShift C w).map f).f₀ = f.f₁

@[simp]

theorem TauCeti.CurvedDuplex.parityShift_obj_X₀ (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) : ((parityShift C w).obj X).X₀ = X.X₁

@[simp]

theorem TauCeti.CurvedDuplex.parityShift_obj_X₁ (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) : ((parityShift C w).obj X).X₁ = X.X₀

@[simp]

theorem TauCeti.CurvedDuplex.parityShift_map_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} (f : X✝ ⟶ Y✝) : ((parityShift C w).map f).f₁ = f.f₀

instance TauCeti.CurvedDuplex.instAdditiveParityShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : (parityShift C w).Additive

instance TauCeti.CurvedDuplex.instLinearParityShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : CategoryTheory.Functor.Linear R (parityShift C w)

def TauCeti.CurvedDuplex.parityShiftCompParityShiftIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (parityShift C w).comp (parityShift C w) ≅ CategoryTheory.Functor.id (CurvedDuplex C w)

Applying the parity shift twice gives back the original duplex: the components are the same, and the differentials are negated twice.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftCompParityShiftIso_hom_app_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) : ((parityShiftCompParityShiftIso C w).hom.app X).f₁ = CategoryTheory.CategoryStruct.id X.X₁

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftCompParityShiftIso_hom_app_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) : ((parityShiftCompParityShiftIso C w).hom.app X).f₀ = CategoryTheory.CategoryStruct.id X.X₀

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftCompParityShiftIso_inv_app_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) : ((parityShiftCompParityShiftIso C w).inv.app X).f₀ = CategoryTheory.CategoryStruct.id X.X₀

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftCompParityShiftIso_inv_app_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) : ((parityShiftCompParityShiftIso C w).inv.app X).f₁ = CategoryTheory.CategoryStruct.id X.X₁

@[implicit_reducible]

def TauCeti.CurvedDuplex.parityShiftEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : CurvedDuplex C w ≌ CurvedDuplex C w

The parity shift is a self-equivalence of the category of curved duplexes.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftEquivalence_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (parityShiftEquivalence C w).inverse = parityShift C w

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftEquivalence_unitIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (parityShiftEquivalence C w).unitIso = (parityShiftCompParityShiftIso C w).symm

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftEquivalence_functor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (parityShiftEquivalence C w).functor = parityShift C w

@[simp]

theorem TauCeti.CurvedDuplex.parityShiftEquivalence_counitIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : (parityShiftEquivalence C w).counitIso = parityShiftCompParityShiftIso C w

instance TauCeti.CurvedDuplex.instAdditiveFunctorParityShiftEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : (parityShiftEquivalence C w).functor.Additive

Null-homotopic morphisms

def TauCeti.CurvedDuplex.nullHomotopicMap {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₁) (h₁ : X.X₁ ⟶ Y.X₀) : X ⟶ Y

The null-homotopic morphism d h + h d attached to an odd map h = (h₀, h₁) from X to Y. It commutes with the differentials because X and Y have the same curvature.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.nullHomotopicMap_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₁) (h₁ : X.X₁ ⟶ Y.X₀) : (nullHomotopicMap h₀ h₁).f₀ = CategoryTheory.CategoryStruct.comp X.d₀ h₁ + CategoryTheory.CategoryStruct.comp h₀ Y.d₁

@[simp]

theorem TauCeti.CurvedDuplex.nullHomotopicMap_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₁) (h₁ : X.X₁ ⟶ Y.X₀) : (nullHomotopicMap h₀ h₁).f₁ = CategoryTheory.CategoryStruct.comp X.d₁ h₀ + CategoryTheory.CategoryStruct.comp h₁ Y.d₀

@[simp]

theorem TauCeti.CurvedDuplex.nullHomotopicMap_zero {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} : nullHomotopicMap 0 0 = 0

theorem TauCeti.CurvedDuplex.nullHomotopicMap_add {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₀ h₀' : X.X₀ ⟶ Y.X₁) (h₁ h₁' : X.X₁ ⟶ Y.X₀) : nullHomotopicMap (h₀ + h₀') (h₁ + h₁') = nullHomotopicMap h₀ h₁ + nullHomotopicMap h₀' h₁'

theorem TauCeti.CurvedDuplex.nullHomotopicMap_neg {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₁) (h₁ : X.X₁ ⟶ Y.X₀) : nullHomotopicMap (-h₀) (-h₁) = -nullHomotopicMap h₀ h₁

theorem TauCeti.CurvedDuplex.comp_nullHomotopicMap {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) (h₀ : Y.X₀ ⟶ Z.X₁) (h₁ : Y.X₁ ⟶ Z.X₀) : CategoryTheory.CategoryStruct.comp f (nullHomotopicMap h₀ h₁) = nullHomotopicMap (CategoryTheory.CategoryStruct.comp f.f₀ h₀) (CategoryTheory.CategoryStruct.comp f.f₁ h₁)

theorem TauCeti.CurvedDuplex.comp_nullHomotopicMap_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 Z : CurvedDuplex C w} (f : X ⟶ Y) (h₀ : Y.X₀ ⟶ Z.X₁) (h₁ : Y.X₁ ⟶ Z.X₀) {Z✝ : CurvedDuplex C w} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (nullHomotopicMap h₀ h₁) h) = CategoryTheory.CategoryStruct.comp (nullHomotopicMap (CategoryTheory.CategoryStruct.comp f.f₀ h₀) (CategoryTheory.CategoryStruct.comp f.f₁ h₁)) h

theorem TauCeti.CurvedDuplex.nullHomotopicMap_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 Z : CurvedDuplex C w} (h₀ : X.X₀ ⟶ Y.X₁) (h₁ : X.X₁ ⟶ Y.X₀) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (nullHomotopicMap h₀ h₁) g = nullHomotopicMap (CategoryTheory.CategoryStruct.comp h₀ g.f₁) (CategoryTheory.CategoryStruct.comp h₁ g.f₀)

theorem TauCeti.CurvedDuplex.nullHomotopicMap_comp_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 Z : CurvedDuplex C w} (h₀ : X.X₀ ⟶ Y.X₁) (h₁ : X.X₁ ⟶ Y.X₀) (g : Y ⟶ Z) {Z✝ : CurvedDuplex C w} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (nullHomotopicMap h₀ h₁) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (nullHomotopicMap (CategoryTheory.CategoryStruct.comp h₀ g.f₁) (CategoryTheory.CategoryStruct.comp h₁ g.f₀)) h

@[simp]

theorem TauCeti.CurvedDuplex.parityShift_map_nullHomotopicMap {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₁) (h₁ : X.X₁ ⟶ Y.X₀) : (parityShift C w).map (nullHomotopicMap h₀ h₁) = nullHomotopicMap (-h₁) (-h₀)

def TauCeti.CurvedDuplex.nullHomotopic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : MorphismIdeal (CurvedDuplex C w)

The two-sided ideal of null-homotopic morphisms of curved duplexes: those of the form d h + h d for an odd map h.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.mem_nullHomotopic_iff {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} {f : X ⟶ Y} : f ∈ (nullHomotopic C w).hom X Y ↔ ∃ (h₀ : X.X₀ ⟶ Y.X₁) (h₁ : X.X₁ ⟶ Y.X₀), nullHomotopicMap h₀ h₁ = f

theorem TauCeti.CurvedDuplex.nullHomotopicMap_mem_nullHomotopic {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₁) (h₁ : X.X₁ ⟶ Y.X₀) : nullHomotopicMap h₀ h₁ ∈ (nullHomotopic C w).hom X Y

theorem TauCeti.CurvedDuplex.comap_parityShift_nullHomotopic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : (nullHomotopic C w).comap (parityShift C w) = nullHomotopic C w

The null-homotopic morphisms are exactly those whose parity shift is null-homotopic.

Elementary disks

@[implicit_reducible]

def TauCeti.CurvedDuplex.disk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) (A : C) : CurvedDuplex C w

The elementary disk A --𝟙--> A --w•𝟙--> A on an object A. It is exposed so that its components unfold to A.

Equations

• TauCeti.CurvedDuplex.disk w A = { X₀ := A, X₁ := A, d₀ := CategoryTheory.CategoryStruct.id A, d₁ := w • CategoryTheory.CategoryStruct.id A, d₀_comp_d₁ := ⋯, d₁_comp_d₀ := ⋯ }

@[simp]

theorem TauCeti.CurvedDuplex.disk_d₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) (A : C) : (disk w A).d₁ = w • CategoryTheory.CategoryStruct.id A

@[simp]

theorem TauCeti.CurvedDuplex.disk_X₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) (A : C) : (disk w A).X₀ = A

@[simp]

theorem TauCeti.CurvedDuplex.disk_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) (A : C) : (disk w A).X₁ = A

@[simp]

theorem TauCeti.CurvedDuplex.disk_d₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) (A : C) : (disk w A).d₀ = CategoryTheory.CategoryStruct.id A

def TauCeti.CurvedDuplex.diskHomEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (A : C) (X : CurvedDuplex C w) : (disk w A ⟶ X) ≃ₗ[R] A ⟶ X.X₀

A morphism out of the disk on A is determined by its even component, which is an arbitrary morphism A ⟶ X₀; this correspondence is R-linear.

Equations

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

@[simp]

theorem TauCeti.CurvedDuplex.diskHomEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (A : C) (X : CurvedDuplex C w) (f : disk w A ⟶ X) : (diskHomEquiv A X) f = f.f₀

@[simp]

theorem TauCeti.CurvedDuplex.diskHomEquiv_symm_apply_f₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (A : C) (X : CurvedDuplex C w) (g : A ⟶ X.X₀) : ((diskHomEquiv A X).symm g).f₀ = g

@[simp]

theorem TauCeti.CurvedDuplex.diskHomEquiv_symm_apply_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (A : C) (X : CurvedDuplex C w) (g : A ⟶ X.X₀) : ((diskHomEquiv A X).symm g).f₁ = CategoryTheory.CategoryStruct.comp g X.d₀

theorem TauCeti.CurvedDuplex.nullHomotopicMap_disk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (A : C) : nullHomotopicMap 0 (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (disk w A)

The identity of the disk on A is null-homotopic: it is d h + h d for the odd map which is the identity from the odd to the even component.

The homotopy category

@[reducible, inline]

abbrev TauCeti.CurvedDuplex.HomotopyCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : Type (max u v)

The homotopy category of curved duplexes of curvature w: the quotient of the category of curved duplexes by the ideal of null-homotopic morphisms. It is preadditive and R-linear.

Equations

• TauCeti.CurvedDuplex.HomotopyCategory C w = (TauCeti.CurvedDuplex.nullHomotopic C w).Quotient

theorem TauCeti.CurvedDuplex.quotientFunctor_map_eq_quotientFunctor_map_iff {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} {f g : X ⟶ Y} : (nullHomotopic C w).quotientFunctor.map f = (nullHomotopic C w).quotientFunctor.map g ↔ ∃ (h₀ : X.X₀ ⟶ Y.X₁) (h₁ : X.X₁ ⟶ Y.X₀), nullHomotopicMap h₀ h₁ = f - g

Two morphisms of curved duplexes become equal in the homotopy category exactly when they are homotopic, that is when their difference is d h + h d for an odd map h.

noncomputable def TauCeti.CurvedDuplex.HomotopyCategory.parityShiftEquivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] (w : R) : HomotopyCategory C w ≌ HomotopyCategory C w

The parity shift of the homotopy category of curved duplexes, a self-equivalence induced by the parity shift of curved duplexes.

Equations

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

instance TauCeti.CurvedDuplex.instAdditiveHomotopyCategoryFunctorParityShiftEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : (HomotopyCategory.parityShiftEquivalence C w).functor.Additive

theorem TauCeti.CurvedDuplex.HomotopyCategory.quotientFunctor_comp_parityShiftEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} : (nullHomotopic C w).quotientFunctor.comp (parityShiftEquivalence C w).functor = (parityShift C w).comp (nullHomotopic C w).quotientFunctor

The parity shift of the homotopy category is induced by the parity shift of curved duplexes.

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.parityShiftEquivalence_functor_obj_quotientFunctor_obj {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) : (parityShiftEquivalence C w).functor.obj ((nullHomotopic C w).quotientFunctor.obj X) = (nullHomotopic C w).quotientFunctor.obj ((parityShift C w).obj X)

On the image of a curved duplex, the parity shift of the homotopy category is the image of its parity shift.

@[simp]

theorem TauCeti.CurvedDuplex.HomotopyCategory.parityShiftEquivalence_functor_map_quotientFunctor_map {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} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((parityShiftEquivalence C w).functor.map ((nullHomotopic C w).quotientFunctor.map f)) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((nullHomotopic C w).quotientFunctor.map ((parityShift C w).map f))

On the image of a morphism of curved duplexes, the parity shift of the homotopy category is the image of its parity shift, up to the identification of objects HomotopyCategory.parityShiftEquivalence_functor_obj_quotientFunctor_obj.

theorem TauCeti.CurvedDuplex.isZero_quotientFunctor_obj_disk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w'} [Semiring R] [CategoryTheory.Linear R C] {w : R} (A : C) : CategoryTheory.Limits.IsZero ((nullHomotopic C w).quotientFunctor.obj (disk w A))

The disk on A is contractible, hence a zero object of the homotopy category.