Basic structures on product categories

This file supplies componentwise smallness, zero morphisms, and zero objects for Cartesian product categories. These structures let additive constructions and invariants apply to products.

It also shows that pushout and pullback squares in a product category are detected componentwise: a square in C × D is a pushout (resp. pullback) exactly when both of its projected squares are (CategoryTheory.IsPushout.fst, CategoryTheory.IsPushout.snd, CategoryTheory.IsPushout.prod, and their pullback counterparts).

@[instance_reducible]

instance TauCeti.instHasZeroMorphismsProd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] : CategoryTheory.Limits.HasZeroMorphisms (C × D)

Zero morphisms in a product category are computed componentwise.

Equations

• TauCeti.instHasZeroMorphismsProd = { zero := fun (X Y : C × D) => { zero := (0, 0) }, comp_zero := ⋯, zero_comp := ⋯ }

instance TauCeti.instEssentiallySmallProd_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.EssentiallySmall.{w₁, v₁, u₁} C] [CategoryTheory.EssentiallySmall.{w₂, v₂, u₂} D] : CategoryTheory.EssentiallySmall.{max w₁ w₂, max v₁ v₂, max u₂ u₁} (C × D)

The product of essentially small categories is essentially small.

instance TauCeti.instHasZeroObjectProd_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] : CategoryTheory.Limits.HasZeroObject (C × D)

A pair of zero objects is a zero object of the product category.

theorem CategoryTheory.IsPushout.fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A A' B B' : C × D} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') : IsPushout g.1 f.1 f'.1 g'.1

The first projection of a pushout square in a product category is a pushout square.

theorem CategoryTheory.IsPushout.snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A A' B B' : C × D} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') : IsPushout g.2 f.2 f'.2 g'.2

The second projection of a pushout square in a product category is a pushout square.

theorem CategoryTheory.IsPushout.prod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A A' B B' : C × D} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (h₁ : IsPushout g.1 f.1 f'.1 g'.1) (h₂ : IsPushout g.2 f.2 f'.2 g'.2) : IsPushout g f f' g'

A square in a product category whose two projections are pushout squares is a pushout square.

theorem CategoryTheory.IsPullback.fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A A' B B' : C × D} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPullback f g g' f') : IsPullback f.1 g.1 g'.1 f'.1

The first projection of a pullback square in a product category is a pullback square.

theorem CategoryTheory.IsPullback.snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A A' B B' : C × D} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPullback f g g' f') : IsPullback f.2 g.2 g'.2 f'.2

The second projection of a pullback square in a product category is a pullback square.

theorem CategoryTheory.IsPullback.prod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A A' B B' : C × D} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (h₁ : IsPullback f.1 g.1 g'.1 f'.1) (h₂ : IsPullback f.2 g.2 g'.2 f'.2) : IsPullback f g g' f'

A square in a product category whose two projections are pullback squares is a pullback square.