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).

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

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₂)

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

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

theorem TotalComplexShape.ε₂_ε₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₁₂ : ComplexShape I₁₂} [self : TotalComplexShape c₁ c₂ c₁₂] {i₁ : I₁} {i₁' : I₁} {i₂ : I₂} {i₂' : I₂} (h₁ : c₁.Rel i₁ i₁') (h₂ : 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₂)

@[reducible, inline]

abbrev ComplexShape.π {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (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

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

@[reducible, inline]

abbrev ComplexShape.ε₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (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

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

@[reducible, inline]

abbrev ComplexShape.ε₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (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

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

theorem ComplexShape.rel_π₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {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 (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (i₁', i₂))

theorem ComplexShape.next_π₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {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₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁.π c₂ c₁₂ (i₁', i₂)

theorem ComplexShape.prev_π₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {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₁₂.prev (c₁.π c₂ c₁₂ (i₁', i₂)) = c₁.π c₂ c₁₂ (i₁, i₂)

theorem ComplexShape.rel_π₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (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 (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (i₁, i₂'))

theorem ComplexShape.next_π₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (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₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁.π c₂ c₁₂ (i₁, i₂')

theorem ComplexShape.prev_π₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (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₁₂.prev (c₁.π c₂ c₁₂ (i₁, i₂')) = c₁.π c₂ c₁₂ (i₁, i₂)

theorem ComplexShape.ε₂_ε₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {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₂') : c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') = -c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)

theorem ComplexShape.ε₁_ε₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {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₂') : c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

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

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

theorem ComplexShape.TensorSigns.rel_add {I : Type u_7} : ∀ {inst : AddMonoid I} {c : ComplexShape I} [self : c.TensorSigns] (p q r : I), c.Rel p q → c.Rel (p + r) (q + r)

theorem ComplexShape.TensorSigns.add_rel {I : Type u_7} : ∀ {inst : AddMonoid I} {c : ComplexShape I} [self : c.TensorSigns] (p q r : I), c.Rel p q → c.Rel (r + p) (r + q)

theorem ComplexShape.TensorSigns.ε'_succ {I : Type u_7} : ∀ {inst : AddMonoid I} {c : ComplexShape I} [self : c.TensorSigns] (p q : I), c.Rel p q → (ComplexShape.TensorSigns.ε' c) q = -(ComplexShape.TensorSigns.ε' c) p

@[reducible, inline]

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

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

Equations

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

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

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

@[simp]

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

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

class ComplexShape.Associative {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c] : Prop

When we have six complex shapes c₁, c₂, c₃, c₁₂, c₂₃, c, and total functors HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂, HomologicalComplex₂ C c₁₂ c₃ ⥤ HomologicalComplex C c, HomologicalComplex₂ C c₂ c₃ ⥤ HomologicalComplex C c₂₃, HomologicalComplex₂ C c₁ c₂₂₃ ⥤ HomologicalComplex C c, we get two ways to compute the total complex of a triple complex in HomologicalComplex₃ C c₁ c₂ c₃, then under this assumption [Associative c₁ c₂ c₃ c₁₂ c₂₃ c], these two complexes canonically identify (without introducing signs).

• assoc : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))
• ε₁_eq_mul : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁.ε₁ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
• ε₂_ε₁ : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
• ε₂_eq_mul : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)

theorem ComplexShape.Associative.assoc {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃} {c : ComplexShape J} : ∀ {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₁₂ c₃ c} {inst_2 : TotalComplexShape c₂ c₃ c₂₃} {inst_3 : TotalComplexShape c₁ c₂₃ c} [self : c₁.Associative c₂ c₃ c₁₂ c₂₃ c] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))

theorem ComplexShape.Associative.ε₁_eq_mul {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃} {c : ComplexShape J} : ∀ {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₁₂ c₃ c} {inst_2 : TotalComplexShape c₂ c₃ c₂₃} {inst_3 : TotalComplexShape c₁ c₂₃ c} [self : c₁.Associative c₂ c₃ c₁₂ c₂₃ c] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁.ε₁ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)

theorem ComplexShape.Associative.ε₂_ε₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃} {c : ComplexShape J} : ∀ {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₁₂ c₃ c} {inst_2 : TotalComplexShape c₂ c₃ c₂₃} {inst_3 : TotalComplexShape c₁ c₂₃ c} [self : c₁.Associative c₂ c₃ c₁₂ c₂₃ c] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

theorem ComplexShape.Associative.ε₂_eq_mul {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃} {c : ComplexShape J} : ∀ {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₁₂ c₃ c} {inst_2 : TotalComplexShape c₂ c₃ c₂₃} {inst_3 : TotalComplexShape c₁ c₂₃ c} [self : c₁.Associative c₂ c₃ c₁₂ c₂₃ c] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)

theorem ComplexShape.assoc {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) : c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))

theorem ComplexShape.associative_ε₁_eq_mul {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) : c₁.ε₁ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)

theorem ComplexShape.associative_ε₂_ε₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) : c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

theorem ComplexShape.associative_ε₂_eq_mul {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) : c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)

def ComplexShape.r {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c] : I₁ × I₂ × I₃ → J

The map I₁ × I₂ × I₃ → j that is obtained using TotalComplexShape c₁ c₂ c₁₂ and TotalComplexShape c₁₂ c₃ c when c₁ : ComplexShape I₁, c₂ : ComplexShape I₂, c₃ : ComplexShape I₃, c₁₂ : ComplexShape I₁₂ and c : ComplexShape J.

Equations

• c₁.r c₂ c₃ c₁₂ c (i₁, i₂, i₃) = c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃)

@[reducible]

def ComplexShape.ρ₁₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c] : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData (c₁.r c₂ c₃ c₁₂ c)

The GradedObject.BifunctorComp₁₂IndexData which arises from complex shapes.

Equations

• c₁.ρ₁₂ c₂ c₃ c₁₂ c = { I₁₂ := I₁₂, p := c₁.π c₂ c₁₂, q := c₁₂.π c₃ c, hpq := ⋯ }

@[reducible]

def ComplexShape.ρ₂₃ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c] : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData (c₁.r c₂ c₃ c₁₂ c)

The GradedObject.BifunctorComp₂₃IndexData which arises from complex shapes.

Equations

• c₁.ρ₂₃ c₂ c₃ c₁₂ c₂₃ c = { I₂₃ := I₂₃, p := c₂.π c₃ c₂₃, q := c₁.π c₂₃ c, hpq := ⋯ }

instance ComplexShape.instAssociative {I : Type u_7} [AddMonoid I] (c : ComplexShape I) [c.TensorSigns] : c.Associative c c c c c

Equations

• ⋯ = ⋯

class TotalComplexShapeSymmetry {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] : Type (max u_1 u_2)

A total complex shape symmetry contains the data and properties which allow the identification of the two total complex functors HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂ and HomologicalComplex₂ C c₂ c₁ ⥤ HomologicalComplex C c₁₂ via the flip.

• symm : ∀ (i₁ : I₁) (i₂ : I₂), c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)
• σ : I₁ → I₂ → ℤˣ

  the signs involved in the symmetry isomorphism of the total complex

• σ_ε₁ : ∀ {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) = c₂.ε₂ c₁ c₁₂ (i₂, i₁) * TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁' i₂
• σ_ε₂ : ∀ (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = c₂.ε₁ c₁ c₁₂ (i₂, i₁) * TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂'

theorem TotalComplexShapeSymmetry.symm {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₁₂ : ComplexShape I₁₂} : ∀ {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₂ c₁ c₁₂} [self : TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂), c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)

theorem TotalComplexShapeSymmetry.σ_ε₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₁₂ : ComplexShape I₁₂} : ∀ {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₂ c₁ c₁₂} [self : TotalComplexShapeSymmetry c₁ c₂ c₁₂] {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) = c₂.ε₂ c₁ c₁₂ (i₂, i₁) * TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁' i₂

theorem TotalComplexShapeSymmetry.σ_ε₂ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₁₂ : ComplexShape I₁₂} : ∀ {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₂ c₁ c₁₂} [self : TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = c₂.ε₁ c₁ c₁₂ (i₂, i₁) * TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂'

@[reducible, inline]

abbrev ComplexShape.σ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂) : ℤˣ

The signs involved in the symmetry isomorphism of the total complex.

Equations

• c₁.σ c₂ c₁₂ i₁ i₂ = TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂

theorem ComplexShape.π_symm {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂) : c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)

def ComplexShape.symmetryEquiv {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] (j : I₁₂) : ↑(c₂.π c₁ c₁₂ ⁻¹' {j}) ≃ ↑(c₁.π c₂ c₁₂ ⁻¹' {j})

The symmetry bijection (π c₂ c₁ c₁₂ ⁻¹' {j}) ≃ (π c₁ c₂ c₁₂ ⁻¹' {j}).

Equations

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

@[simp]

theorem ComplexShape.symmetryEquiv_apply_coe {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] (j : I₁₂) : ∀ (x : ↑(c₂.π c₁ c₁₂ ⁻¹' {j})), ↑((c₁.symmetryEquiv c₂ c₁₂ j) x) = (x.1.2, x.1.1)

@[simp]

theorem ComplexShape.symmetryEquiv_symm_apply_coe {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] (j : I₁₂) : ∀ (x : ↑(c₁.π c₂ c₁₂ ⁻¹' {j})), ↑((c₁.symmetryEquiv c₂ c₁₂ j).symm x) = (x.1.2, x.1.1)

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

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

instance ComplexShape.instTotalComplexShapeSymmetryIntUp : TotalComplexShapeSymmetry (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ)

Equations

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

@[simp]

theorem ComplexShape.instTotalComplexShapeSymmetryIntUp_σ (p : ℤ) (q : ℤ) : TotalComplexShapeSymmetry.σ (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ) p q = (p * q).negOnePow

def TotalComplexShapeSymmetry.symmetry {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] : TotalComplexShapeSymmetry c₂ c₁ c₁₂

The obvious TotalComplexShapeSymmetry c₂ c₁ c₁₂ deduced from a TotalComplexShapeSymmetry c₁ c₂ c₁₂.

Equations

• TotalComplexShapeSymmetry.symmetry c₁ c₂ c₁₂ = { symm := ⋯, σ := fun (i₂ : I₂) (i₁ : I₁) => c₁.σ c₂ c₁₂ i₁ i₂, σ_ε₁ := ⋯, σ_ε₂ := ⋯ }

class TotalComplexShapeSymmetrySymmetry {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] [TotalComplexShapeSymmetry c₂ c₁ c₁₂] : Prop

This typeclass expresses that the signs given by [TotalComplexShapeSymmetry c₁ c₂ c₁₂] and by [TotalComplexShapeSymmetry c₂ c₁ c₁₂] are compatible.

• σ_symm : ∀ (i₁ : I₁) (i₂ : I₂), c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂

theorem TotalComplexShapeSymmetrySymmetry.σ_symm {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₁₂ : ComplexShape I₁₂} : ∀ {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₂ c₁ c₁₂} {inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂} {inst_3 : TotalComplexShapeSymmetry c₂ c₁ c₁₂} [self : TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂), c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂

theorem ComplexShape.σ_symm {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] [TotalComplexShapeSymmetry c₂ c₁ c₁₂] [TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂) : c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂