Documentation

TauCeti.CategoryTheory.Shift.Periodicity

Iterated periodicity isomorphisms #

Let C be a category with a shift by an additive monoid A and let G : C ⥤ E be a functor. An isomorphism α : shiftFunctor C a ⋙ G ≅ G says that G does not see the shift by a. Two such isomorphisms α (in degree a) and β (in degree b) compose to one in degree a + b, whose component at X is

G (X⟦a + b⟧) ≅ G (X⟦a⟧⟦b⟧) ≅ G (X⟦a⟧) ≅ G X,

the first map being shiftFunctorAdd' and the other two β at X⟦a⟧ and α at X. This composition CategoryTheory.Iso.shiftComp is associative, has the isomorphisms coming from shiftFunctorZero' as two-sided units, and over an additive group every such isomorphism has a two-sided inverse CategoryTheory.Iso.shiftInv in the opposite degree.

A single periodicity isomorphism φ : shiftFunctor C n ⋙ G ≅ G for an integral shift therefore has well-defined integral powers φ.periodicityZPow i : shiftFunctor C (n * i) ⋙ G ≅ G, and these satisfy the cocycle law φ.periodicityZPow_add_hom_app. They are the coherence data needed to descend G to the orbit category D/[n] (Keller's universal property), where a morphism X ⟶ Y⟦n * i⟧ is sent to G.map f followed by the i-th power of φ at Y.

Main definitions #

Main results #

References #

source
def CategoryTheory.Iso.shiftComp {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddMonoid A] [HasShift C A] {a b c : A} (α : (shiftFunctor C a).comp G ≅ G) (β : (shiftFunctor C b).comp G ≅ G) (h : a + b = c) :
(shiftFunctor C c).comp G ≅ G

The composition of shift-invariance isomorphisms of degrees a and b, in degree c = a + b. Its component at X is G (X⟦c⟧) ≅ G (X⟦a⟧⟦b⟧) ≅ G (X⟦a⟧) ≅ G X.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Iso.shiftComp_hom_app {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddMonoid A] [HasShift C A] {a b c : A} (α : (shiftFunctor C a).comp G ≅ G) (β : (shiftFunctor C b).comp G ≅ G) (h : a + b = c) (X : C) :
    (α.shiftComp β h).hom.app X = CategoryStruct.comp (G.map ((shiftFunctorAdd' C a b c h).hom.app X)) (CategoryStruct.comp (β.hom.app (X⟦a⟧)) (α.hom.app X))
    source
    theorem CategoryTheory.Iso.shiftComp_assoc {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddMonoid A] [HasShift C A] {a b c ab bc abc : A} (α : (shiftFunctor C a).comp G ≅ G) (β : (shiftFunctor C b).comp G ≅ G) (γ : (shiftFunctor C c).comp G ≅ G) (hab : a + b = ab) (hbc : b + c = bc) (habc : a + b + c = abc) :
    (α.shiftComp β hab).shiftComp γ ⋯ = α.shiftComp (β.shiftComp γ hbc) ⋯

    Composition of shift-invariance isomorphisms is associative.

    source
    theorem CategoryTheory.Iso.shiftComp_zero_left {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddMonoid A] [HasShift C A] {a b : A} (ha : a = 0) (β : (shiftFunctor C b).comp G ≅ G) :
    (Functor.isoWhiskerRight (shiftFunctorZero' C a ha) G ≪≫ G.leftUnitor).shiftComp β ⋯ = β

    The shift-invariance isomorphism in a degree a = 0 coming from shiftFunctorZero' is a left unit for shiftComp.

    source
    theorem CategoryTheory.Iso.shiftComp_zero_right {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddMonoid A] [HasShift C A] {a b : A} (α : (shiftFunctor C a).comp G ≅ G) (hb : b = 0) :
    α.shiftComp (Functor.isoWhiskerRight (shiftFunctorZero' C b hb) G ≪≫ G.leftUnitor) ⋯ = α

    The shift-invariance isomorphism in a degree b = 0 coming from shiftFunctorZero' is a right unit for shiftComp.

    source
    def CategoryTheory.Iso.shiftInv {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddMonoid A] [HasShift C A] {a : A} (α : (shiftFunctor C a).comp G ≅ G) (b : A) (h : b + a = 0) :
    (shiftFunctor C b).comp G ≅ G

    The inverse of a shift-invariance isomorphism α of degree a, in a degree b with b + a = 0. Its component at X is G (X⟦b⟧) ≅ G (X⟦b⟧⟦a⟧) ≅ G X.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Iso.shiftInv_hom_app {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddMonoid A] [HasShift C A] {a : A} (α : (shiftFunctor C a).comp G ≅ G) (b : A) (h : b + a = 0) (X : C) :
      (α.shiftInv b h).hom.app X = CategoryStruct.comp (α.inv.app (X⟦b⟧)) (G.map ((shiftFunctorCompIsoId C b a h).hom.app X))
      source
      theorem CategoryTheory.Iso.shiftInv_shiftComp {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddMonoid A] [HasShift C A] {a b c : A} (α : (shiftFunctor C a).comp G ≅ G) (h : b + a = c) (hc : c = 0) :
      (α.shiftInv b ⋯).shiftComp α h = Functor.isoWhiskerRight (shiftFunctorZero' C c hc) G ≪≫ G.leftUnitor

      α.shiftInv b is a left inverse of α for shiftComp.

      source
      theorem CategoryTheory.Iso.shiftComp_shiftInv {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddGroup A] [HasShift C A] {a b c : A} (α : (shiftFunctor C a).comp G ≅ G) (h : a + b = c) (hc : c = 0) :
      α.shiftComp (α.shiftInv b ⋯) h = Functor.isoWhiskerRight (shiftFunctorZero' C c hc) G ≪≫ G.leftUnitor

      α.shiftInv b is a right inverse of α for shiftComp.

      source
      theorem CategoryTheory.Iso.shiftComp_left_cancel_iff {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {A : Type u_1} {G : Functor C E} [AddGroup A] [HasShift C A] {a b c : A} (α : (shiftFunctor C a).comp G ≅ G) {β β' : (shiftFunctor C b).comp G ≅ G} (h : a + b = c) :
      α.shiftComp β h = α.shiftComp β' h ↔ β = β'

      Composition with a shift-invariance isomorphism is cancellable.

      source
      def CategoryTheory.Iso.periodicityZPow {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {G : Functor C E} [HasShift C ℤ] {n : ℤ} (φ : (shiftFunctor C n).comp G ≅ G) (i : ℤ) :
      (shiftFunctor C (n * i)).comp G ≅ G

      The integral powers φ^i : shiftFunctor C (n * i) ⋙ G ≅ G of a periodicity isomorphism φ : shiftFunctor C n ⋙ G ≅ G, for the composition shiftComp. They are characterised by periodicityZPow_zero and periodicityZPow_succ, and satisfy the cocycle law periodicityZPow_add.

      Instances For
        source
        theorem CategoryTheory.Iso.periodicityZPow_zero {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {G : Functor C E} [HasShift C ℤ] {n : ℤ} (φ : (shiftFunctor C n).comp G ≅ G) :
        φ.periodicityZPow 0 = Functor.isoWhiskerRight (shiftFunctorZero' C (n * 0) ⋯) G ≪≫ G.leftUnitor

        The zeroth power of a periodicity isomorphism is the unit coming from shiftFunctorZero'.

        source
        theorem CategoryTheory.Iso.periodicityZPow_zero_hom_app {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {G : Functor C E} [HasShift C ℤ] {n : ℤ} (φ : (shiftFunctor C n).comp G ≅ G) (X : C) :
        (φ.periodicityZPow 0).hom.app X = G.map ((shiftFunctorZero' C (n * 0) ⋯).hom.app X)

        The zeroth power of a periodicity isomorphism, on components.

        source
        theorem CategoryTheory.Iso.periodicityZPow_succ {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {G : Functor C E} [HasShift C ℤ] {n : ℤ} (φ : (shiftFunctor C n).comp G ≅ G) (i j : ℤ) (h : i + 1 = j) :
        φ.periodicityZPow j = φ.shiftComp (φ.periodicityZPow i) ⋯

        The power φ^(i + 1) is φ composed with φ^i.

        source
        theorem CategoryTheory.Iso.periodicityZPow_add {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {G : Functor C E} [HasShift C ℤ] {n : ℤ} (φ : (shiftFunctor C n).comp G ≅ G) (i j k : ℤ) (h : i + j = k) :
        φ.periodicityZPow k = (φ.periodicityZPow i).shiftComp (φ.periodicityZPow j) ⋯

        The cocycle law: φ^(i + j) is φ^i composed with φ^j.

        source
        theorem CategoryTheory.Iso.periodicityZPow_add_hom_app {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {G : Functor C E} [HasShift C ℤ] {n : ℤ} (φ : (shiftFunctor C n).comp G ≅ G) (i j k : ℤ) (h : i + j = k) (X : C) :
        (φ.periodicityZPow k).hom.app X = CategoryStruct.comp (G.map ((shiftFunctorAdd' C (n * i) (n * j) (n * k) ⋯).hom.app X)) (CategoryStruct.comp ((φ.periodicityZPow j).hom.app (X⟦n * i⟧)) ((φ.periodicityZPow i).hom.app X))

        The cocycle law of the powers of a periodicity isomorphism, on components.

        source
        @[simp]
        theorem CategoryTheory.Iso.periodicityZPow_one_hom_app {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {G : Functor C E} [HasShift C ℤ] {n : ℤ} (φ : (shiftFunctor C n).comp G ≅ G) (X : C) :
        (φ.periodicityZPow 1).hom.app X = CategoryStruct.comp (G.map (eqToHom ⋯)) (φ.hom.app X)

        The first power of a periodicity isomorphism is the isomorphism itself.

        source
        theorem CategoryTheory.Iso.periodicityZPow_unique {C : Type u₁} {E : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} E] {G : Functor C E} [HasShift C ℤ] {n : ℤ} (φ : (shiftFunctor C n).comp G ≅ G) (ψ : (i : ℤ) → (shiftFunctor C (n * i)).comp G ≅ G) (h₀ : ψ 0 = Functor.isoWhiskerRight (shiftFunctorZero' C (n * 0) ⋯) G ≪≫ G.leftUnitor) (hsucc : ∀ (i j : ℤ) (h : i + 1 = j), ψ j = φ.shiftComp (ψ i) ⋯) :
        ψ = φ.periodicityZPow

        The powers of a periodicity isomorphism are the only family of shift-invariance isomorphisms that starts with the unit and is built by composing with φ.