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 ofX ⟶ X ⨿ Y
andY ⟶ X ⨿ Y
is the initial object.CategoryTheory.types.finitaryExtensive
: The category of types is extensive.CategoryTheory.FinitaryExtensive_TopCat
: The categoryTop
is extensive.CategoryTheory.FinitaryExtensive_functor
: The categoryC ⥤ D
is extensive ifD
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)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasBinaryCoproducts C]
:
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
Instances
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]
:
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
Instances
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
Instances
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
Instances
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)
:
@[instance 100]
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
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
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
@[instance 100]
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]
:
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
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
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
@[instance 100]
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
instance
CategoryTheory.instMonoInr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.FinitaryExtensive C]
(X Y : C)
:
CategoryTheory.Mono CategoryTheory.Limits.coprod.inr
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]
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₀)
:
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
Instances For
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]
:
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]
:
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]
:
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]
:
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]
:
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)
:
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)
:
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)
:
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)
:
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 : ι)
:
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)
:
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 : α)
:
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))