Signs in constructions on homological complexes

In this file, we shall introduce various typeclasses which will allow the construction of the total complex of a bicomplex and of the the monoidal category structure on categories of homological complexes (TODO).

The most important definition is that of TotalComplexShape c₁ c₂ c₁₂ given three complex shapes c₁, c₂, c₁₂: it allows the definition of a total complex functor HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂ (at least when suitable coproducts exist).

In particular, we construct an instance of TotalComplexShape c c c when c : ComplexShape I and I is an additive monoid equipped with a group homomorphism ε' : Multiplicative I → ℤˣ satisfying certain properties (see ComplexShape.TensorSigns).

TODO @joelriou: add more classes for the symmetry of the total complex, the associativity, etc.

class TotalComplexShape {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) : Type (max (max u_1 u_2) u_3)

A total complex shape for three complexes shapes c₁, c₂, c₁₂ on three types I₁, I₂ and I₁₂ consists of the data and properties that will allow the construction of a total complex functor HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂ which sends K to a complex which in degree i₁₂ : I₁₂ consists of the coproduct of the (K.X i₁).X i₂ such that π ⟨i₁, i₂⟩ = i₁₂.

• π : I₁ × I₂ → I₁₂

  a map on indices

• ε₁ : I₁ × I₂ → ℤˣ

  the sign of the horizontal differential in the total complex

• ε₂ : I₁ × I₂ → ℤˣ

  the sign of the vertical differential in the total complex

• rel₁ : ∀ {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), c₁₂.Rel (TotalComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) (TotalComplexShape.π c₁ c₂ c₁₂ (i₁', i₂))
• rel₂ : ∀ (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → c₁₂.Rel (TotalComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) (TotalComplexShape.π c₁ c₂ c₁₂ (i₁, i₂'))
• ε₂_ε₁ : ∀ {i₁ i₁' : I₁} {i₂ i₂' : I₂}, c₁.Rel i₁ i₁' → c₂.Rel i₂ i₂' → TotalComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂) * TotalComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂') = -TotalComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂) * TotalComplexShape.ε₂ c₁ c₂ c₁₂ (i₁', i₂)

@[inline, reducible]

abbrev ComplexShape.π {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] (i : I₁ × I₂) : I₁₂

The map I₁ × I₂ → I₁₂ on indices given by TotalComplexShape c₁ c₂ c₁₂.

Equations

• ComplexShape.π c₁ c₂ c₁₂ i = TotalComplexShape.π c₁ c₂ c₁₂ i

@[inline, reducible]

abbrev ComplexShape.ε₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] (i : I₁ × I₂) : ℤˣ

The sign of the horizontal differential in the total complex.

Equations

• ComplexShape.ε₁ c₁ c₂ c₁₂ i = TotalComplexShape.ε₁ c₁ c₂ c₁₂ i

@[inline, reducible]

abbrev ComplexShape.ε₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] (i : I₁ × I₂) : ℤˣ

The sign of the vertical differential in the total complex.

Equations

• ComplexShape.ε₂ c₁ c₂ c₁₂ i = TotalComplexShape.ε₂ c₁ c₂ c₁₂ i

theorem ComplexShape.rel_π₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) : c₁₂.Rel (ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) (ComplexShape.π c₁ c₂ c₁₂ (i₁', i₂))

theorem ComplexShape.next_π₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) : ComplexShape.next c₁₂ (ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) = ComplexShape.π c₁ c₂ c₁₂ (i₁', i₂)

theorem ComplexShape.rel_π₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} (c₁ : ComplexShape I₁) {c₂ : ComplexShape I₂} (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') : c₁₂.Rel (ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) (ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂'))

theorem ComplexShape.next_π₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} (c₁ : ComplexShape I₁) {c₂ : ComplexShape I₂} (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') : ComplexShape.next c₁₂ (ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) = ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂')

theorem ComplexShape.ε₂_ε₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] {i₁ : I₁} {i₁' : I₁} {i₂ : I₂} {i₂' : I₂} (h₁ : c₁.Rel i₁ i₁') (h₂ : c₂.Rel i₂ i₂') : ComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂) * ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂') = -ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂) * ComplexShape.ε₂ c₁ c₂ c₁₂ (i₁', i₂)

class ComplexShape.TensorSigns {I : Type u_4} [AddMonoid I] (c : ComplexShape I) : Type u_4

If I is an additive monoid and c : ComplexShape I, c.TensorSigns contains the data of map ε : I → ℤˣ and properties which allows the construction of a TotalComplexShape c c c.

• ε' : Multiplicative I →* ℤˣ

  the signs which appear in the vertical differential of the total complex

• rel_add : ∀ (p q r : I), c.Rel p q → c.Rel (p + r) (q + r)
• add_rel : ∀ (p q r : I), c.Rel p q → c.Rel (r + p) (r + q)
• ε'_succ : ∀ (p q : I), c.Rel p q → (ComplexShape.TensorSigns.ε' c) q = -(ComplexShape.TensorSigns.ε' c) p

@[inline, reducible]

abbrev ComplexShape.ε {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] (i : I) : ℤˣ

The signs which appear in the vertical differential of the total complex.

Equations

• ComplexShape.ε c i = (ComplexShape.TensorSigns.ε' c) i

theorem ComplexShape.rel_add {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] {p : I} {q : I} (hpq : c.Rel p q) (r : I) : c.Rel (p + r) (q + r)

theorem ComplexShape.add_rel {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] (r : I) {p : I} {q : I} (hpq : c.Rel p q) : c.Rel (r + p) (r + q)

@[simp]

theorem ComplexShape.ε_zero {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] : ComplexShape.ε c 0 = 1

theorem ComplexShape.ε_succ {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] {p : I} {q : I} (hpq : c.Rel p q) : ComplexShape.ε c q = -ComplexShape.ε c p

theorem ComplexShape.ε_add {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] (p : I) (q : I) : ComplexShape.ε c (p + q) = ComplexShape.ε c p * ComplexShape.ε c q

theorem ComplexShape.next_add {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] (p : I) (q : I) (hp : c.Rel p (ComplexShape.next c p)) : ComplexShape.next c (p + q) = ComplexShape.next c p + q

theorem ComplexShape.next_add' {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] (p : I) (q : I) (hq : c.Rel q (ComplexShape.next c q)) : ComplexShape.next c (p + q) = p + ComplexShape.next c q

@[simp]

theorem ComplexShape.instTotalComplexShape_π {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] : ∀ (x : I × I), TotalComplexShape.π c c c x = match x with | (p, q) => p + q

@[simp]

theorem ComplexShape.instTotalComplexShape_ε₂ {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] : ∀ (x : I × I), TotalComplexShape.ε₂ c c c x = match x with | (p, snd) => ComplexShape.ε c p

@[simp]

theorem ComplexShape.instTotalComplexShape_ε₁ {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] : ∀ (x : I × I), TotalComplexShape.ε₁ c c c x = 1

instance ComplexShape.instTotalComplexShape {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [ComplexShape.TensorSigns c] : TotalComplexShape c c c

Equations

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

instance ComplexShape.instTensorSignsNatAddMonoidDownToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiring : ComplexShape.TensorSigns (ComplexShape.down ℕ)

Equations

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

@[simp]

theorem ComplexShape.ε_down_ℕ (n : ℕ) : ComplexShape.ε (ComplexShape.down ℕ) n = (-1) ^ n

instance ComplexShape.instTensorSignsIntInstAddMonoidIntUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringInt : ComplexShape.TensorSigns (ComplexShape.up ℤ)

Equations

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

@[simp]

theorem ComplexShape.ε_up_ℤ (n : ℤ) : ComplexShape.ε (ComplexShape.up ℤ) n = n.negOnePow