Documentation

TauCeti.CategoryTheory.Functor.OfCubeEdges

Commutative cubes from their edge maps #

A commutative cube indexed by a type ι in a category C is a functor Finset ι ⥤ C on the finite subsets of ι, ordered by inclusion. Such a cube is usually given by its edges only: an object X S at every vertex, a map X S ⟶ X T along every edge, that is, whenever T covers S (S ⋖ T, so T = insert a S with a ∉ S), and the condition that every square face commutes. This file builds the cube from these data, CategoryTheory.Functor.ofCubeEdges: the map along an inclusion S ⊆ T is the composite of edge maps along any maximal chain from S to T, and the commuting faces make it independent of the chain.

Likewise a map of cubes only needs to commute with the edge maps: CategoryTheory.NatTrans.ofCubeEdges builds a natural transformation between functors Finset ι ⥤ C from components that are natural along every edge.

These are the analogues for the Boolean cube of CategoryTheory.Functor.ofSequence and CategoryTheory.NatTrans.ofSequence for the ordered set ℕ. The cube of resolutions of a link diagram, whose vertices are the circle tensors of the smoothings and whose edge maps are the saddle maps, is a cube of this kind; its signed totalization CategoryTheory.Functor.cubeComplex is the Khovanov complex.

Main definitions #

Main results #

References #

source
@[irreducible]
def CategoryTheory.Functor.OfCubeEdges.map {C : Type u} [Category.{v, u} C] {ι : Type w} {X : Finset ι → C} (d : ⦃S T : Finset ι⦄ → S ⋖ T → (X S ⟶ X T)) (S T : Finset ι) (h : S ⊆ T) :
X S ⟶ X T

The composite of edge maps from X S to X T along a maximal chain from S to T, whose first step is chosen arbitrarily; it does not depend on this choice once the square faces of edge maps commute. This is the map along S ⊆ T of CategoryTheory.Functor.ofCubeEdges.

Instances For
    source
    theorem CategoryTheory.Functor.OfCubeEdges.map_self {C : Type u} [Category.{v, u} C] {ι : Type w} {X : Finset ι → C} (d : ⦃S T : Finset ι⦄ → S ⋖ T → (X S ⟶ X T)) (S : Finset ι) (h : S ⊆ S) :
    map d S S h = CategoryStruct.id (X S)

    The empty chain from S to itself gives the identity.

    source
    theorem CategoryTheory.Functor.OfCubeEdges.map_comp {C : Type u} [Category.{v, u} C] {ι : Type w} {X : Finset ι → C} {d : ⦃S T : Finset ι⦄ → S ⋖ T → (X S ⟶ X T)} (hd : ∀ ⦃S T₁ T₂ U : Finset ι⦄ (h₁ : S ⋖ T₁) (h₁' : T₁ ⋖ U) (h₂ : S ⋖ T₂) (h₂' : T₂ ⋖ U), CategoryStruct.comp (d h₁) (d h₁') = CategoryStruct.comp (d h₂) (d h₂')) {S T U : Finset ι} (h₁ : S ⊆ T) (h₂ : T ⊆ U) :
    CategoryStruct.comp (map d S T h₁) (map d T U h₂) = map d S U ⋯

    Once the square faces commute, the composites of edge maps along chains compose.

    source
    noncomputable def CategoryTheory.Functor.ofCubeEdges {C : Type u} [Category.{v, u} C] {ι : Type w} {X : Finset ι → C} (d : ⦃S T : Finset ι⦄ → S ⋖ T → (X S ⟶ X T)) (hd : ∀ ⦃S T₁ T₂ U : Finset ι⦄ (h₁ : S ⋖ T₁) (h₁' : T₁ ⋖ U) (h₂ : S ⋖ T₂) (h₂' : T₂ ⋖ U), CategoryStruct.comp (d h₁) (d h₁') = CategoryStruct.comp (d h₂) (d h₂')) :
    Functor (Finset ι) C

    The commutative cube Finset ι ⥤ C with vertices X S and with the edge map d h along every edge h : S ⋖ T, given that every square face of edge maps commutes (hd). Along an inclusion S ⊆ T it is the composite of the edge maps along any maximal chain from S to T.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Functor.ofCubeEdges_obj {C : Type u} [Category.{v, u} C] {ι : Type w} {X : Finset ι → C} (d : ⦃S T : Finset ι⦄ → S ⋖ T → (X S ⟶ X T)) (hd : ∀ ⦃S T₁ T₂ U : Finset ι⦄ (h₁ : S ⋖ T₁) (h₁' : T₁ ⋖ U) (h₂ : S ⋖ T₂) (h₂' : T₂ ⋖ U), CategoryStruct.comp (d h₁) (d h₁') = CategoryStruct.comp (d h₂) (d h₂')) (a✝ : Finset ι) :
      (ofCubeEdges d hd).obj a✝ = X a✝
      source
      theorem CategoryTheory.Functor.ofCubeEdges_map_of_covBy {C : Type u} [Category.{v, u} C] {ι : Type w} {X : Finset ι → C} (d : ⦃S T : Finset ι⦄ → S ⋖ T → (X S ⟶ X T)) (hd : ∀ ⦃S T₁ T₂ U : Finset ι⦄ (h₁ : S ⋖ T₁) (h₁' : T₁ ⋖ U) (h₂ : S ⋖ T₂) (h₂' : T₂ ⋖ U), CategoryStruct.comp (d h₁) (d h₁') = CategoryStruct.comp (d h₂) (d h₂')) {S T : Finset ι} (f : S ⟶ T) (h : S ⋖ T) :
      (ofCubeEdges d hd).map f = d h

      Along an edge S ⋖ T, the cube ofCubeEdges d hd is the edge map d.

      source
      @[simp]
      theorem CategoryTheory.Functor.ofCubeEdges_map_homOfLE_insert {C : Type u} [Category.{v, u} C] {ι : Type w} {X : Finset ι → C} (d : ⦃S T : Finset ι⦄ → S ⋖ T → (X S ⟶ X T)) (hd : ∀ ⦃S T₁ T₂ U : Finset ι⦄ (h₁ : S ⋖ T₁) (h₁' : T₁ ⋖ U) (h₂ : S ⋖ T₂) (h₂' : T₂ ⋖ U), CategoryStruct.comp (d h₁) (d h₁') = CategoryStruct.comp (d h₂) (d h₂')) [DecidableEq ι] {S : Finset ι} {a : ι} (ha : a ∉ S) :
      (ofCubeEdges d hd).map (homOfLE ⋯) = d ⋯

      Along the edge from S to insert a S, for a ∉ S, the cube ofCubeEdges d hd is the edge map d.

      source
      def CategoryTheory.NatTrans.ofCubeEdges {C : Type u} [Category.{v, u} C] {ι : Type w} {F G : Functor (Finset ι) C} (app : (S : Finset ι) → F.obj S ⟶ G.obj S) (naturality : ∀ ⦃S T : Finset ι⦄ (h : S ⋖ T), CategoryStruct.comp (F.map (homOfLE ⋯)) (app T) = CategoryStruct.comp (app S) (G.map (homOfLE ⋯))) :
      F ⟶ G

      The map of cubes F ⟶ G with components app, which need only be natural along the edges S ⋖ T of the cube.

      Instances For
        source
        @[simp]
        theorem CategoryTheory.NatTrans.ofCubeEdges_app {C : Type u} [Category.{v, u} C] {ι : Type w} {F G : Functor (Finset ι) C} (app : (S : Finset ι) → F.obj S ⟶ G.obj S) (naturality : ∀ ⦃S T : Finset ι⦄ (h : S ⋖ T), CategoryStruct.comp (F.map (homOfLE ⋯)) (app T) = CategoryStruct.comp (app S) (G.map (homOfLE ⋯))) (S : Finset ι) :
        (ofCubeEdges app naturality).app S = app S

        The components of NatTrans.ofCubeEdges app naturality are app.