Walking pairs

We define a category WalkingPair, which is the index category for a binary (co)product diagram. A convenience method pair X Y, for X, Y objects of some category C, constructs the functor from the walking pair, hitting the given objects.

References

• Stacks: Products of pairs
• Stacks: coproducts of pairs

inductive CategoryTheory.Limits.WalkingPair : Type

The type of objects for the diagram indexing a binary (co)product.

• left : WalkingPair
• right : WalkingPair

@[instance_reducible]

instance CategoryTheory.Limits.instDecidableEqWalkingPair : DecidableEq WalkingPair

Equations

• CategoryTheory.Limits.instDecidableEqWalkingPair x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CategoryTheory.Limits.instInhabitedWalkingPair : Inhabited WalkingPair

Equations

• CategoryTheory.Limits.instInhabitedWalkingPair = { default := CategoryTheory.Limits.instInhabitedWalkingPair.default }

def CategoryTheory.Limits.WalkingPair.swap : WalkingPair ≃ WalkingPair

The equivalence swapping left and right.

Equations

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

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_apply_left : swap left = right

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_apply_right : swap right = left

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_tt : swap.symm left = right

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_ff : swap.symm right = left

def CategoryTheory.Limits.WalkingPair.equivBool : WalkingPair ≃ Bool

An equivalence from WalkingPair to Bool, sometimes useful when reindexing limits.

Equations

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

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_left : equivBool left = true

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_right : equivBool right = false

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_true : equivBool.symm true = left

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_false : equivBool.symm false = right

def CategoryTheory.Limits.pairFunction {C : Type u} (X Y : C) : WalkingPair → C

The function on the walking pair, sending the two points to X and Y.

Equations

• CategoryTheory.Limits.pairFunction X Y j = CategoryTheory.Limits.WalkingPair.casesOn j X Y

@[simp]

theorem CategoryTheory.Limits.pairFunction_left {C : Type u} (X Y : C) : pairFunction X Y WalkingPair.left = X

@[simp]

theorem CategoryTheory.Limits.pairFunction_right {C : Type u} (X Y : C) : pairFunction X Y WalkingPair.right = Y

@[implicit_reducible]

def CategoryTheory.Limits.pair {C : Type u} [Category.{v, u} C] (X Y : C) : Functor (Discrete WalkingPair) C

The diagram on the walking pair, sending the two points to X and Y.

Equations

• CategoryTheory.Limits.pair X Y = CategoryTheory.Discrete.functor fun (j : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.casesOn j X Y

@[simp]

theorem CategoryTheory.Limits.pair_obj_left {C : Type u} [Category.{v, u} C] (X Y : C) : (pair X Y).obj { as := WalkingPair.left } = X

@[simp]

theorem CategoryTheory.Limits.pair_obj_right {C : Type u} [Category.{v, u} C] (X Y : C) : (pair X Y).obj { as := WalkingPair.right } = Y

def CategoryTheory.Limits.mapPair {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ⟶ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ⟶ G.obj { as := WalkingPair.right }) : F ⟶ G

The natural transformation between two functors out of the walking pair, specified by its components.

Equations

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

@[simp]

theorem CategoryTheory.Limits.mapPair_left {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ⟶ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ⟶ G.obj { as := WalkingPair.right }) : (mapPair f g).app { as := WalkingPair.left } = f

@[simp]

theorem CategoryTheory.Limits.mapPair_right {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ⟶ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ⟶ G.obj { as := WalkingPair.right }) : (mapPair f g).app { as := WalkingPair.right } = g

def CategoryTheory.Limits.mapPairIso {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ≅ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ≅ G.obj { as := WalkingPair.right }) : F ≅ G

The natural isomorphism between two functors out of the walking pair, specified by its components.

Equations

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

@[simp]

theorem CategoryTheory.Limits.mapPairIso_hom_app {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ≅ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ≅ G.obj { as := WalkingPair.right }) (X : Discrete WalkingPair) : (mapPairIso f g).hom.app X = (match X with | { as := WalkingPair.left } => f | { as := WalkingPair.right } => g).hom

@[simp]

theorem CategoryTheory.Limits.mapPairIso_inv_app {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ≅ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ≅ G.obj { as := WalkingPair.right }) (X : Discrete WalkingPair) : (mapPairIso f g).inv.app X = (match X with | { as := WalkingPair.left } => f | { as := WalkingPair.right } => g).inv

def CategoryTheory.Limits.diagramIsoPair {C : Type u} [Category.{v, u} C] (F : Functor (Discrete WalkingPair) C) : F ≅ pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right })

Every functor out of the walking pair is naturally isomorphic (actually, equal) to a pair

Equations

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

@[simp]

theorem CategoryTheory.Limits.diagramIsoPair_inv_app {C : Type u} [Category.{v, u} C] (F : Functor (Discrete WalkingPair) C) (X : Discrete WalkingPair) : (diagramIsoPair F).inv.app X = (match X with | { as := WalkingPair.left } => Iso.refl (F.obj { as := WalkingPair.left }) | { as := WalkingPair.right } => Iso.refl (F.obj { as := WalkingPair.right })).inv

@[simp]

theorem CategoryTheory.Limits.diagramIsoPair_hom_app {C : Type u} [Category.{v, u} C] (F : Functor (Discrete WalkingPair) C) (X : Discrete WalkingPair) : (diagramIsoPair F).hom.app X = (match X with | { as := WalkingPair.left } => Iso.refl (F.obj { as := WalkingPair.left }) | { as := WalkingPair.right } => Iso.refl (F.obj { as := WalkingPair.right })).hom

def CategoryTheory.Limits.pairComp {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (X Y : C) (F : Functor C D) : (pair X Y).comp F ≅ pair (F.obj X) (F.obj Y)

The natural isomorphism between pair X Y ⋙ F and pair (F.obj X) (F.obj Y).

Equations

• CategoryTheory.Limits.pairComp X Y F = CategoryTheory.Limits.diagramIsoPair ((CategoryTheory.Limits.pair X Y).comp F)