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] : Prop

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 100]

instance CategoryTheory.HasPullbacksOfInclusions.instOfHasPullbacks {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 Y 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 Y 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 Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inr f

Equations

• ⋯ = ⋯

@[instance 100]

noncomputable instance CategoryTheory.PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan {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

• ⋯ = ⋯

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 Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f CategoryTheory.Limits.coprod.inl) F

Equations

• ⋯ = ⋯

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 Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f CategoryTheory.Limits.coprod.inr) F

Equations

• ⋯ = ⋯

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 Y Z : C} (f : Z ⟶ X ⨿ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inr f) F

Equations

• ⋯ = ⋯

@[instance 100]

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 Y : C} [CategoryTheory.FinitaryExtensive C] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Mono c.inr

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

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

Equations

• ⋯ = ⋯

instance CategoryTheory.instMonoInr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] (X 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 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 })) c.inl c.inr

@[instance 100]

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 ((TopCat.of PUnit.{u + 1} ).binaryCofan (TopCat.of PUnit.{u + 1} )).inl) (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1} ).binaryCofan (TopCat.of PUnit.{u + 1} )).inr))

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

Equations

• CategoryTheory.finitaryExtensiveTopCatAux Z f = ⋯.some

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) [Gr.Full] [Gr.Faithful] [∀ (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

• ⋯ = ⋯

instance CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso {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 Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F

Equations

• ⋯ = ⋯

instance CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_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 Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso g] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F

Equations

• ⋯ = ⋯

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] [F.ReflectsIsomorphisms] : 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.instMonoι {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 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 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 f (π x))