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

theorem TotalComplexShape.rel₁ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_3} {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_3} {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_3} {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_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

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

Instances For

@[reducible, inline]

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

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

Instances For

@[reducible, inline]

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

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 (c₁.π c₂ c₁₂ (i₁, i₂)) (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₂) :

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_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₁₂.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_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 (c₁.π c₂ c₁₂ (i₁, i₂)) (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₂') :

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_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₁₂.prev (c₁.π c₂ c₁₂ (i₁, i₂')) = 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₂') :

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_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₂') :

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

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

c.Rel (p + r) (q + r)

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

c.Rel (r + p) (r + q)

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

(ComplexShape.TensorSigns.ε' c) q = -(ComplexShape.TensorSigns.ε' c) p

@[reducible, inline]

abbrev ComplexShape.ε {I : Type u_4} [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

Instances For

theorem ComplexShape.rel_add {I : Type u_4} [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_4} [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_4} [AddMonoid I] (c : ComplexShape I) [c.TensorSigns] :

c.ε 0 = 1

theorem ComplexShape.ε_succ {I : Type u_4} [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_4} [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_4} [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_4} [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

@[simp]

theorem ComplexShape.instTotalComplexShape_ε₁ {I : Type u_4} [AddMonoid I] (c : ComplexShape I) [c.TensorSigns] :

∀ (x : I × I), TotalComplexShape.ε₁ c c c x = 1

@[simp]

theorem ComplexShape.instTotalComplexShape_π {I : Type u_4} [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_4} [AddMonoid I] (c : ComplexShape I) [c.TensorSigns] :

∀ (x : I × I), TotalComplexShape.ε₂ c c c x = match x with | (p, snd) => c.ε p

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

TotalComplexShape c c c

Equations

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

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

Instances

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

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

c₂.π c₁ c₁₂ (i₂, i₁) = 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₂) :

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_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₂') :

c₁.σ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.σ c₂ c₁₂ i₁ i₂'

@[simp]

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

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

instance ComplexShape.instTotalComplexShapeSymmetryIntUp :

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

Instances

theorem TotalComplexShapeSymmetrySymmetry.σ_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₁₂] [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_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₂) :

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