Documentation

TauCeti.CategoryTheory.Extensive

Base change of finite coproducts in finitary pre-extensive categories #

In a finitary pre-extensive category finite coproducts are universal: they are stable under pullback. Phrased in over categories, base change Over.pullback f : Over S ⥤ Over T along any morphism f : T ⟶ S preserves finite coproducts. This applies for instance to schemes, where it says that the fibre product of a finite disjoint union with T over S is the disjoint union of the fibre products.

Main results #

source
instance CategoryTheory.Over.preservesColimitsOfShape_discrete_pullback {C : Type u} [Category.{v, u} C] {S T : C} (f : T ⟶ S) [Limits.HasPullbacksAlong f] [FinitaryPreExtensive C] (J : Type u_1) [Finite J] :
Limits.PreservesColimitsOfShape (Discrete J) (pullback f)

In a finitary pre-extensive category, base change of objects over S along any f : T ⟶ S preserves finite coproducts.

source
instance CategoryTheory.Over.instPreservesFiniteCoproductsPullbackOfFinitaryPreExtensive_tauCeti {C : Type u} [Category.{v, u} C] {S T : C} (f : T ⟶ S) [Limits.HasPullbacksAlong f] [FinitaryPreExtensive C] :
Limits.PreservesFiniteCoproducts (pullback f)

In a finitary pre-extensive category, base change of objects over S preserves finite coproducts.

source
theorem CategoryTheory.FinitaryPreExtensive.isPullback_sigmaMap_sigmaDesc_id {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] {J : Type u_1} [Finite J] {S Y : C} (f : S ⟶ Y) [Limits.HasPullback (Limits.Sigma.desc fun (x : J) => CategoryStruct.id Y) f] :
IsPullback (Limits.Sigma.map fun (x : J) => f) (Limits.Sigma.desc fun (x : J) => CategoryStruct.id S) (Limits.Sigma.desc fun (x : J) => CategoryStruct.id Y) f

In a finitary pre-extensive category, the base change of the fold map ∐_j Y ⟶ Y along any morphism f : S ⟶ Y is the fold map ∐_j S ⟶ S, with first projection ∐_j f.