Additivity of the integer powers of an autoequivalence

Mathlib defines the integer powers e ^ j of an autoequivalence e : C ≌ C by recursion and records e ^ 0, e ^ 1 and e ^ (-1), but leaves the comparison of e ^ (a + b) with the composite e ^ a ⋙ e ^ b as an explicit TODO. This file supplies that comparison as an isomorphism of the underlying functors, together with the successor and predecessor forms which consume it.

Only the underlying functors are compared. e ^ (a + b) and (e ^ a).trans (e ^ b) are not equal as equivalences — the recursion inserts unitors — so the isomorphism below, and not an equation, is what downstream constructions use.

Main definitions

• CategoryTheory.Equivalence.powSuccIso: e ^ (j + 1) ≅ e ⋙ e ^ j, by case analysis on j.
• CategoryTheory.Equivalence.powPredIso: e⁻¹ ⋙ e ^ j ≅ e ^ (j - 1).
• CategoryTheory.Equivalence.powAddIso: e ^ (a + b) ≅ e ^ a ⋙ e ^ b.
• CategoryTheory.Equivalence.powSuccRightIso: e ^ (j + 1) ≅ e ^ j ⋙ e, the opposite-handed successor isomorphism, which the additivity isomorphism supplies but the recursion does not.

def CategoryTheory.Equivalence.powSuccIso {C : Type u} [Category.{v, u} C] (e : C ≌ C) (j : ℤ) : (e ^ (j + 1)).functor ≅ e.functor.comp (e ^ j).functor

The successor isomorphism e ^ (j + 1) ≅ e ⋙ e ^ j. Mathlib's power is built by prepending a copy of e, so at a positive exponent the isomorphism is the identity. Each of the remaining cases inserts exactly what the recursion leaves out there: a right unitor at j = 0, where e ^ 0 is the identity functor; the unit isomorphism at j = -1, where e ⋙ e ^ (-1) is e ⋙ e.inverse; and at every j ≤ -2 a composite of a left unitor, the unit isomorphism and an associator, which grows a negative power by inserting e ⋙ e.inverse in front of it.

Equations

• One or more equations did not get rendered due to their size.
• e.powSuccIso (Int.ofNat 0) = e.functor.rightUnitor.symm
• e.powSuccIso (Int.ofNat n.succ) = CategoryTheory.Iso.refl (e ^ (↑(n + 1) + 1)).functor
• e.powSuccIso (Int.negSucc 0) = e.unitIso

def CategoryTheory.Equivalence.powPredIso {C : Type u} [Category.{v, u} C] (e : C ≌ C) (j : ℤ) : e.inverse.comp (e ^ j).functor ≅ (e ^ (j - 1)).functor

The predecessor isomorphism e⁻¹ ⋙ e ^ j ≅ e ^ (j - 1).

Equations

• e.powPredIso j = e.inverse.isoWhiskerLeft (CategoryTheory.eqToIso ⋯ ≪≫ e.powSuccIso (j - 1)) ≪≫ e.invFunIdAssoc (e ^ (j - 1)).functor

def CategoryTheory.Equivalence.powAddIso {C : Type u} [Category.{v, u} C] (e : C ≌ C) (a b : ℤ) : (e ^ (a + b)).functor ≅ (e ^ a).functor.comp (e ^ b).functor

Additivity of the integer powers of an autoequivalence: e ^ (a + b) ≅ e ^ a ⋙ e ^ b.

Equations

• e.powAddIso (Int.ofNat n) x✝ = CategoryTheory.Equivalence.powAddNatIso✝ e x✝ n
• e.powAddIso (Int.negSucc n) x✝ = CategoryTheory.Equivalence.powSubNatIso✝ e x✝ (n + 1)

def CategoryTheory.Equivalence.powSuccRightIso {C : Type u} [Category.{v, u} C] (e : C ≌ C) (j : ℤ) : (e ^ (j + 1)).functor ≅ (e ^ j).functor.comp e.functor

The opposite-handed successor isomorphism e ^ (j + 1) ≅ e ^ j ⋙ e.

Equations

• e.powSuccRightIso j = e.powAddIso j 1