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][CARBONI1993145]

class CategoryTheory.HasPullbacksOfInclusions (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.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), CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl f

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

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

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

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

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

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

  In a finitary extensive category, all coproducts are van Kampen

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

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

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

  In a finitary extensive category, all coproducts are van Kampen

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.PreservesPullbacksOfInclusions.instPreservesPullbacksOfInclusions F = CategoryTheory.PreservesPullbacksOfInclusions.mk

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

Equations

• CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl' F f = CategoryTheory.Limits.preservesPullbackSymmetry F CategoryTheory.Limits.coprod.inl f

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

Equations

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

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

Equations

• CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr F f = CategoryTheory.Limits.preservesPullbackSymmetry F f CategoryTheory.Limits.coprod.inr

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• CategoryTheory.types.finitaryExtensive = ⋯

noncomputable def CategoryTheory.finitaryExtensiveTopCatAux (Z : TopCat) (f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1} )) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (TopCat.pullbackFst f (CategoryTheory.Limits.BinaryCofan.inl (TopCat.binaryCofan (TopCat.of PUnit.{u + 1} ) (TopCat.of PUnit.{u + 1} )))) (TopCat.pullbackFst f (CategoryTheory.Limits.BinaryCofan.inr (TopCat.binaryCofan (TopCat.of PUnit.{u + 1} ) (TopCat.of PUnit.{u + 1} )))))

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

Equations

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

instance CategoryTheory.finitaryExtensive_TopCat : CategoryTheory.FinitaryExtensive TopCat

Equations

• CategoryTheory.finitaryExtensive_TopCat = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

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

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

Equations

• CategoryTheory.instPreservesLimitWalkingCospanCategoryWalkingPairCospan_1 F f g = CategoryTheory.Limits.preservesPullbackSymmetry F g f

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

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

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

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

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

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

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

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

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