Documentation

Mathlib.Algebra.Homology.ComplexShapeSigns

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 associativity of the total complex, 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₂)

Instances

@[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

Instances For

@[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

Instances For

@[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

Instances For

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.prev_π₁ {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.prev 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.prev_π₂ {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.prev 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₂)

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

Instances

@[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

Instances For

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, 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

@[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

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.instTensorSignsNatInstAddMonoidDownToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidInstStrictOrderedSemiringToOneInstCanonicallyOrderedCommSemiring :

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.instTensorSignsIntInstAddMonoidUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupToOneInstSemiring :

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

class TotalComplexShapeSymmetry {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₁₂] [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₂), ComplexShape.π c₂ c₁ c₁₂ (i₂, i₁) = ComplexShape.π 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₂ * ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂) = ComplexShape.ε₂ 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₂ * ComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂) = ComplexShape.ε₁ c₂ c₁ c₁₂ (i₂, i₁) * TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂'

Instances

@[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₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂) :

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

Equations

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

Instances For

theorem ComplexShape.π_symm {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₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂) :

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₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] {i₁ : I₁} {i₁' : I₁} (h₁ : c₁.Rel i₁ i₁') (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₂

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₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) {i₂ : I₂} {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₂'

@[simp]

theorem ComplexShape.instTotalComplexShapeSymmetryIntUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupToOneInstSemiringInstTotalComplexShapeInstAddMonoidInstTensorSignsIntInstAddMonoidUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupToOneInstSemiring_σ (p : ℤ) (q : ℤ) :

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

instance ComplexShape.instTotalComplexShapeSymmetryIntUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupToOneInstSemiringInstTotalComplexShapeInstAddMonoidInstTensorSignsIntInstAddMonoidUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupToOneInstSemiring :

TotalComplexShapeSymmetry (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ)

Equations

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

class TotalComplexShapeSymmetrySymmetry {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₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] [TotalComplexShapeSymmetry c₂ c₁ c₁₂] :

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₂), ComplexShape.σ c₂ c₁ c₁₂ i₂ i₁ = ComplexShape.σ c₁ c₂ c₁₂ i₁ i₂

Instances

theorem ComplexShape.σ_symm {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₁₂] [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂] [TotalComplexShapeSymmetry c₂ c₁ c₁₂] [TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂) :

ComplexShape.σ c₂ c₁ c₁₂ i₂ i₁ = ComplexShape.σ c₁ c₂ c₁₂ i₁ i₂