Extensive categories

Main definitions

• CategoryTheory.FinitaryExtensive: A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.

Main Results

• CategoryTheory.hasStrictInitialObjects_of_finitaryExtensive: The initial object in extensive categories is strict.
• CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit: Coproduct injections are monic in extensive categories.
• CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen: In extensive categories, sums are disjoint, i.e. the pullback of X ⟶ X ⨿ Y and Y ⟶ X ⨿ Y is the initial object.
• CategoryTheory.types.finitaryExtensive: The category of types is extensive.
• CategoryTheory.FinitaryExtensive_TopCat: The category Top is extensive.
• CategoryTheory.FinitaryExtensive_functor: The category C ⥤ D is extensive if D has all pullbacks and is extensive.
• CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts: Finite coproducts in a finitary extensive category are van Kampen.

TODO

Show that the following are finitary extensive:

• Scheme
• AffineScheme (CommRingᵒᵖ)

References

• https://ncatlab.org/nlab/show/extensive+category
• Carboni et al, Introduction to extensive and distributive categories

class CategoryTheory.HasPullbacksOfInclusions (C : Type u) [Category.{v, u} C] [Limits.HasBinaryCoproducts C] : Prop

A category has pullback of inclusions if it has all pullbacks along coproduct injections.

• hasPullbackInl {X Y Z : C} (f : Z ⟶ X ⨿ Y) : Limits.HasPullback Limits.coprod.inl f

class CategoryTheory.PreservesPullbacksOfInclusions {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] (F : Functor C D) [Limits.HasBinaryCoproducts C] : Prop

A functor preserves pullback of inclusions if it preserves all pullbacks along coproduct injections.

• preservesPullbackInl {X Y Z : C} (f : Z ⟶ X ⨿ Y) : Limits.PreservesLimit (Limits.cospan Limits.coprod.inl f) F

class CategoryTheory.FinitaryPreExtensive (C : Type u) [Category.{v, u} C] : Prop

A category is (finitary) pre-extensive if it has finite coproducts, and binary coproducts are universal.

• hasFiniteCoproducts : Limits.HasFiniteCoproducts C
• hasPullbacksOfInclusions : HasPullbacksOfInclusions C
• universal' {X Y : C} (c : Limits.BinaryCofan X Y) : ∀ (a : Limits.IsColimit c), IsUniversalColimit c

  In a finitary extensive category, all coproducts are van Kampen

class CategoryTheory.FinitaryExtensive (C : Type u) [Category.{v, u} C] : Prop

A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.

• hasFiniteCoproducts : Limits.HasFiniteCoproducts C
• hasPullbacksOfInclusions : HasPullbacksOfInclusions C
• van_kampen' {X Y : C} (c : Limits.BinaryCofan X Y) : ∀ (a : Limits.IsColimit c), IsVanKampenColimit c

  In a finitary extensive category, all coproducts are van Kampen

theorem CategoryTheory.FinitaryExtensive.vanKampen {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] {F : Functor (Discrete Limits.WalkingPair) C} (c : Limits.Cocone F) (hc : Limits.IsColimit c) : IsVanKampenColimit c

@[instance 100]

instance CategoryTheory.HasPullbacksOfInclusions.instOfHasPullbacks {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] [Limits.HasPullbacks C] : HasPullbacksOfInclusions C

instance CategoryTheory.HasPullbacksOfInclusions.preservesPullbackInl' {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] [HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : Limits.HasPullback f Limits.coprod.inl

instance CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr' {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] [HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : Limits.HasPullback f Limits.coprod.inr

instance CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] [HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : Limits.HasPullback Limits.coprod.inr f

@[instance 100]

instance CategoryTheory.PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Limits.HasBinaryCoproducts C] (F : Functor C D) [Limits.PreservesLimitsOfShape Limits.WalkingCospan F] : PreservesPullbacksOfInclusions F

instance CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl' {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Limits.HasBinaryCoproducts C] (F : Functor C D) [PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : Limits.PreservesLimit (Limits.cospan f Limits.coprod.inl) F

instance CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr' {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Limits.HasBinaryCoproducts C] (F : Functor C D) [PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : Limits.PreservesLimit (Limits.cospan f Limits.coprod.inr) F

instance CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Limits.HasBinaryCoproducts C] (F : Functor C D) [PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y) : Limits.PreservesLimit (Limits.cospan Limits.coprod.inr f) F

@[instance 100]

instance CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] : FinitaryPreExtensive C

theorem CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit {C : Type u} [Category.{v, u} C] {X Y : C} [FinitaryExtensive C] {c : Limits.BinaryCofan X Y} (hc : Limits.IsColimit c) : Mono c.inr

theorem CategoryTheory.FinitaryExtensive.mono_inl_of_isColimit {C : Type u} [Category.{v, u} C] {X Y : C} [FinitaryExtensive C] {c : Limits.BinaryCofan X Y} (hc : Limits.IsColimit c) : Mono c.inl

instance CategoryTheory.instMonoInl {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] (X Y : C) : Mono Limits.coprod.inl

instance CategoryTheory.instMonoInr {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] (X Y : C) : Mono Limits.coprod.inr

theorem CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan {C : Type u} [Category.{v, u} C] {X Y : C} [FinitaryExtensive C] {c : Limits.BinaryCofan X Y} (hc : Limits.IsColimit c) : IsPullback (Limits.initial.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.left })) (Limits.initial.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.right })) c.inl c.inr

@[instance 100]

instance CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] : Limits.HasStrictInitialObjects C

theorem CategoryTheory.finitaryExtensive_iff_of_isTerminal (C : Type u) [Category.{v, u} C] [Limits.HasFiniteCoproducts C] [HasPullbacksOfInclusions C] (T : C) (HT : Limits.IsTerminal T) (c₀ : Limits.BinaryCofan T T) (hc₀ : Limits.IsColimit c₀) : FinitaryExtensive C ↔ IsVanKampenColimit c₀

instance CategoryTheory.types.finitaryExtensive : FinitaryExtensive (Type u)

noncomputable def CategoryTheory.finitaryExtensiveTopCatAux (Z : TopCat) (f : Z ⟶ { carrier := PUnit.{u + 1} ⊕ PUnit.{u + 1}, str := instTopologicalSpaceSum }) : Limits.IsColimit (Limits.BinaryCofan.mk (TopCat.pullbackFst f ({ carrier := PUnit.{u + 1}, str := instTopologicalSpacePUnit }.binaryCofan { carrier := PUnit.{u + 1}, str := instTopologicalSpacePUnit }).inl) (TopCat.pullbackFst f ({ carrier := PUnit.{u + 1}, str := instTopologicalSpacePUnit }.binaryCofan { carrier := PUnit.{u + 1}, str := instTopologicalSpacePUnit }).inr))

(Implementation) An auxiliary lemma for the proof that TopCat is finitary extensive.

Equations

• CategoryTheory.finitaryExtensiveTopCatAux Z f = ⋯.some

instance CategoryTheory.finitaryExtensive_TopCat : FinitaryExtensive TopCat

theorem CategoryTheory.finitaryExtensive_of_reflective {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] [Limits.HasFiniteCoproducts D] [HasPullbacksOfInclusions D] [FinitaryExtensive C] {Gl : Functor C D} {Gr : Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] [∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), Limits.HasPullback (Gr.map f) (adj.unit.app Y)] [∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), Limits.PreservesLimit (Limits.cospan (Gr.map f) (adj.unit.app Y)) Gl] [PreservesPullbacksOfInclusions Gl] : FinitaryExtensive D

instance CategoryTheory.finitaryExtensive_functor {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] [Limits.HasPullbacks C] [FinitaryExtensive C] : FinitaryExtensive (Functor D C)

instance CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso {C : Type u_1} [Category.{u_2, u_1} C] {D : Type u_3} [Category.{u_4, u_3} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso f] : Limits.PreservesLimit (Limits.cospan f g) F

instance CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_1 {C : Type u_1} [Category.{u_2, u_1} C] {D : Type u_3} [Category.{u_4, u_3} D] (F : Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [IsIso g] : Limits.PreservesLimit (Limits.cospan f g) F

theorem CategoryTheory.finitaryExtensive_of_preserves_and_reflects {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] (F : Functor C D) [FinitaryExtensive D] [Limits.HasFiniteCoproducts C] [HasPullbacksOfInclusions C] [PreservesPullbacksOfInclusions F] [Limits.ReflectsLimitsOfShape Limits.WalkingCospan F] [Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) F] [Limits.ReflectsColimitsOfShape (Discrete Limits.WalkingPair) F] : FinitaryExtensive C

theorem CategoryTheory.finitaryExtensive_of_preserves_and_reflects_isomorphism {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] (F : Functor C D) [FinitaryExtensive D] [Limits.HasFiniteCoproducts C] [Limits.HasPullbacks C] [Limits.PreservesLimitsOfShape Limits.WalkingCospan F] [Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) F] [F.ReflectsIsomorphisms] : FinitaryExtensive C

theorem CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] {n : ℕ} {F : Functor (Discrete (Fin n)) C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) : IsUniversalColimit c

theorem CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] {ι : Type u_1} [Finite ι] {F : Functor (Discrete ι) C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) : IsUniversalColimit c

theorem CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts_Fin {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] {n : ℕ} {F : Functor (Discrete (Fin n)) C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) : IsVanKampenColimit c

theorem CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] {ι : Type u_1} [Finite ι] {F : Functor (Discrete ι) C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) : IsVanKampenColimit c

theorem CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] {ι : Type u_1} [Finite ι] {F : Functor (Discrete ι) C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) (i : Discrete ι) {X : C} (g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj i) : Limits.HasPullback g (c.ι.app i)

theorem CategoryTheory.FinitaryExtensive.mono_ι {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] {ι : Type u_1} [Finite ι] {F : Functor (Discrete ι) C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) (i : Discrete ι) : Mono (c.ι.app i)

instance CategoryTheory.instMonoι {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] {ι : Type u_1} [Finite ι] (X : ι → C) (i : ι) : Mono (Limits.Sigma.ι X i)

theorem CategoryTheory.FinitaryExtensive.isPullback_initial_to {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] {ι : Type u_1} [Finite ι] {F : Functor (Discrete ι) C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) (i j : Discrete ι) (e : i ≠ j) : IsPullback (Limits.initial.to (F.obj i)) (Limits.initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

theorem CategoryTheory.FinitaryExtensive.isPullback_initial_to_sigma_ι {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] {ι : Type u_1} [Finite ι] (X : ι → C) (i j : ι) (e : i ≠ j) : IsPullback (Limits.initial.to (X i)) (Limits.initial.to (X j)) (Limits.Sigma.ι X i) (Limits.Sigma.ι X j)

instance CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_inclusions {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] {X Z : C} {α : Type u_1} (f : X ⟶ Z) {Y : α → C} (i : (a : α) → Y a ⟶ Z) [Finite α] [hi : IsIso (Limits.Sigma.desc i)] (a : α) : Limits.HasPullback f (i a)

theorem CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_fst {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] {α : Type} [Finite α] {X : C} {Z : α → C} (π : (a : α) → Z a ⟶ X) {Y : C} (f : Y ⟶ X) (hπ : IsIso (Limits.Sigma.desc π)) : IsIso (Limits.Sigma.desc fun (x : α) => Limits.pullback.fst f (π x))

@[deprecated CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_fst (since := "2025-06-20")]

theorem CategoryTheory.FinitaryPreExtensive.sigma_desc_iso {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] {α : Type} [Finite α] {X : C} {Z : α → C} (π : (a : α) → Z a ⟶ X) {Y : C} (f : Y ⟶ X) (hπ : IsIso (Limits.Sigma.desc π)) : IsIso (Limits.Sigma.desc fun (x : α) => Limits.pullback.fst f (π x))

Alias of CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_fst.

instance CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_map {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [FinitaryPreExtensive C] {ι : Type u_1} {ι' : Type u_2} [Finite ι] [Finite ι'] {S : C} {X : ι → C} {Y : ι' → C} (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) : IsIso (Limits.Sigma.desc fun (p : ι × ι') => Limits.pullback.map (f p.1) (g p.2) (Limits.Sigma.desc f) (Limits.Sigma.desc g) (Limits.Sigma.ι X p.1) (Limits.Sigma.ι Y p.2) (CategoryStruct.id S) ⋯ ⋯)

If C has pullbacks and is finitary (pre-)extensive, pullbacks distribute over finite coproducts, i.e., ∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ). For an IsPullback version, see FinitaryPreExtensive.isPullback_sigmaDesc.

theorem CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [FinitaryPreExtensive C] {ι : Type u_1} {ι' : Type u_2} [Finite ι] [Finite ι'] {S : C} {X : ι → C} {Y : ι' → C} (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) : IsPullback (Limits.Sigma.desc fun (p : ι × ι') => CategoryStruct.comp (Limits.pullback.fst (f p.1) (g p.2)) (Limits.Sigma.ι X p.1)) (Limits.Sigma.desc fun (p : ι × ι') => CategoryStruct.comp (Limits.pullback.snd (f p.1) (g p.2)) (Limits.Sigma.ι Y p.2)) (Limits.Sigma.desc f) (Limits.Sigma.desc g)

If C has pullbacks and is finitary (pre-)extensive, pullbacks distribute over finite coproducts, i.e., ∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ). For a variant, see FinitaryPreExtensive.isIso_sigmaDesc_map.