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 ⨿ YandY ⟶ X ⨿ Yis the initial object.CategoryTheory.types.finitaryExtensive: The category of types is extensive.CategoryTheory.FinitaryExtensive_TopCat: The categoryTopis extensive.CategoryTheory.FinitaryExtensive_functor: The categoryC ⥤ Dis extensive ifDhas 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:
SchemeAffineScheme(CommRingᵒᵖ)
References #
- https://ncatlab.org/nlab/show/extensive+category
- Carboni et al, Introduction to extensive and distributive categories
structure
CategoryTheory.HasPullbacksOfInclusions
(C : Type u)
[Category C]
[Limits.HasBinaryCoproducts C]
:
A category has pullback of inclusions if it has all pullbacks along coproduct injections.
- hasPullbackInl {X Y Z : C} (f : Quiver.Hom Z (Limits.coprod X Y)) : Limits.HasPullback Limits.coprod.inl f
Instances For
structure
CategoryTheory.PreservesPullbacksOfInclusions
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[Limits.HasBinaryCoproducts C]
:
A functor preserves pullback of inclusions if it preserves all pullbacks along coproduct injections.
- preservesPullbackInl {X Y Z : C} (f : Quiver.Hom Z (Limits.coprod X Y)) : Limits.PreservesLimit (Limits.cospan Limits.coprod.inl f) F
Instances For
A category is (finitary) pre-extensive if it has finite coproducts, and binary coproducts are universal.
- hasFiniteCoproducts : Limits.HasFiniteCoproducts C
- hasPullbacksOfInclusions : HasPullbacksOfInclusions C
In a finitary extensive category, all coproducts are van Kampen
Instances For
A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.
- hasFiniteCoproducts : Limits.HasFiniteCoproducts C
- hasPullbacksOfInclusions : HasPullbacksOfInclusions C
In a finitary extensive category, all coproducts are van Kampen
Instances For
theorem
CategoryTheory.FinitaryExtensive.vanKampen
{C : Type u}
[Category C]
[FinitaryExtensive C]
{F : Functor (Discrete Limits.WalkingPair) C}
(c : Limits.Cocone F)
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.HasPullbacksOfInclusions.preservesPullbackInl'
{C : Type u}
[Category C]
[Limits.HasBinaryCoproducts C]
[HasPullbacksOfInclusions C]
{X Y Z : C}
(f : Quiver.Hom Z (Limits.coprod X Y))
:
theorem
CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr'
{C : Type u}
[Category C]
[Limits.HasBinaryCoproducts C]
[HasPullbacksOfInclusions C]
{X Y Z : C}
(f : Quiver.Hom Z (Limits.coprod X Y))
:
theorem
CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr
{C : Type u}
[Category C]
[Limits.HasBinaryCoproducts C]
[HasPullbacksOfInclusions C]
{X Y Z : C}
(f : Quiver.Hom Z (Limits.coprod X Y))
:
theorem
CategoryTheory.PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan
{C : Type u}
[Category C]
{D : Type u_1}
[Category D]
[Limits.HasBinaryCoproducts C]
(F : Functor C D)
[Limits.PreservesLimitsOfShape Limits.WalkingCospan F]
:
theorem
CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl'
{C : Type u}
[Category C]
{D : Type u_1}
[Category D]
[Limits.HasBinaryCoproducts C]
(F : Functor C D)
[PreservesPullbacksOfInclusions F]
{X Y Z : C}
(f : Quiver.Hom Z (Limits.coprod X Y))
:
theorem
CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr'
{C : Type u}
[Category C]
{D : Type u_1}
[Category D]
[Limits.HasBinaryCoproducts C]
(F : Functor C D)
[PreservesPullbacksOfInclusions F]
{X Y Z : C}
(f : Quiver.Hom Z (Limits.coprod X Y))
:
theorem
CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr
{C : Type u}
[Category C]
{D : Type u_1}
[Category D]
[Limits.HasBinaryCoproducts C]
(F : Functor C D)
[PreservesPullbacksOfInclusions F]
{X Y Z : C}
(f : Quiver.Hom Z (Limits.coprod X Y))
:
theorem
CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive
{C : Type u}
[Category C]
[FinitaryExtensive C]
:
theorem
CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit
{C : Type u}
[Category C]
{X Y : C}
[FinitaryExtensive C]
{c : Limits.BinaryCofan X Y}
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.FinitaryExtensive.mono_inl_of_isColimit
{C : Type u}
[Category C]
{X Y : C}
[FinitaryExtensive C]
{c : Limits.BinaryCofan X Y}
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan
{C : Type u}
[Category 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
theorem
CategoryTheory.finitaryExtensive_iff_of_isTerminal
(C : Type u)
[Category C]
[Limits.HasFiniteCoproducts C]
[HasPullbacksOfInclusions C]
(T : C)
(HT : Limits.IsTerminal T)
(c₀ : Limits.BinaryCofan T T)
(hc₀ : Limits.IsColimit c₀)
:
Iff (FinitaryExtensive C) (IsVanKampenColimit c₀)
noncomputable def
CategoryTheory.finitaryExtensiveTopCatAux
(Z : TopCat)
(f : Quiver.Hom Z (TopCat.of (Sum PUnit PUnit)))
:
(Implementation) An auxiliary lemma for the proof that TopCat is finitary extensive.
Equations
Instances For
theorem
CategoryTheory.finitaryExtensive_of_reflective
{C : Type u}
[Category C]
{D : Type u''}
[Category D]
[Limits.HasFiniteCoproducts D]
[HasPullbacksOfInclusions D]
[FinitaryExtensive C]
{Gl : Functor C D}
{Gr : Functor D C}
(adj : Adjunction Gl Gr)
[Gr.Full]
[Gr.Faithful]
[∀ (X : D) (Y : C) (f : Quiver.Hom X (Gl.obj Y)), Limits.HasPullback (Gr.map f) (adj.unit.app Y)]
[∀ (X : D) (Y : C) (f : Quiver.Hom X (Gl.obj Y)), Limits.PreservesLimit (Limits.cospan (Gr.map f) (adj.unit.app Y)) Gl]
[PreservesPullbacksOfInclusions Gl]
:
theorem
CategoryTheory.finitaryExtensive_functor
{C : Type u}
[Category C]
{D : Type u''}
[Category D]
[Limits.HasPullbacks C]
[FinitaryExtensive C]
:
FinitaryExtensive (Functor D C)
theorem
CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso
{C : Type u_1}
[Category C]
{D : Type u_3}
[Category D]
(F : Functor C D)
{X Y Z : C}
(f : Quiver.Hom X Z)
(g : Quiver.Hom Y Z)
[IsIso f]
:
Limits.PreservesLimit (Limits.cospan f g) F
theorem
CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_1
{C : Type u_1}
[Category C]
{D : Type u_3}
[Category D]
(F : Functor C D)
{X Y Z : C}
(f : Quiver.Hom X Z)
(g : Quiver.Hom Y Z)
[IsIso g]
:
Limits.PreservesLimit (Limits.cospan f g) F
theorem
CategoryTheory.finitaryExtensive_of_preserves_and_reflects
{C : Type u}
[Category C]
{D : Type u''}
[Category 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]
:
theorem
CategoryTheory.finitaryExtensive_of_preserves_and_reflects_isomorphism
{C : Type u}
[Category C]
{D : Type u''}
[Category 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]
:
theorem
CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin
{C : Type u}
[Category C]
[FinitaryPreExtensive C]
{n : Nat}
{F : Functor (Discrete (Fin n)) C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
{C : Type u}
[Category C]
[FinitaryPreExtensive C]
{ι : Type u_1}
[Finite ι]
{F : Functor (Discrete ι) C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts_Fin
{C : Type u}
[Category C]
[FinitaryExtensive C]
{n : Nat}
{F : Functor (Discrete (Fin n)) C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts
{C : Type u}
[Category C]
[FinitaryExtensive C]
{ι : Type u_1}
[Finite ι]
{F : Functor (Discrete ι) C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct
{C : Type u}
[Category C]
[FinitaryPreExtensive C]
{ι : Type u_1}
[Finite ι]
{F : Functor (Discrete ι) C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
(i : Discrete ι)
{X : C}
(g : Quiver.Hom X (((Functor.const (Discrete ι)).obj c.pt).obj i))
:
Limits.HasPullback g (c.ι.app i)
theorem
CategoryTheory.FinitaryExtensive.mono_ι
{C : Type u}
[Category C]
[FinitaryExtensive C]
{ι : Type u_1}
[Finite ι]
{F : Functor (Discrete ι) C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
(i : Discrete ι)
:
theorem
CategoryTheory.instMonoι
{C : Type u}
[Category 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 C]
[FinitaryExtensive C]
{ι : Type u_1}
[Finite ι]
{F : Functor (Discrete ι) C}
{c : Limits.Cocone F}
(hc : Limits.IsColimit c)
(i j : Discrete ι)
(e : Ne 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 C]
[FinitaryExtensive C]
{ι : Type u_1}
[Finite ι]
(X : ι → C)
(i j : ι)
(e : Ne i j)
:
IsPullback (Limits.initial.to (X i)) (Limits.initial.to (X j)) (Limits.Sigma.ι X i) (Limits.Sigma.ι X j)
theorem
CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_inclusions
{C : Type u}
[Category C]
[FinitaryPreExtensive C]
{X Z : C}
{α : Type u_1}
(f : Quiver.Hom X Z)
{Y : α → C}
(i : (a : α) → Quiver.Hom (Y a) Z)
[Finite α]
[hi : IsIso (Limits.Sigma.desc i)]
(a : α)
:
Limits.HasPullback f (i a)
theorem
CategoryTheory.FinitaryPreExtensive.sigma_desc_iso
{C : Type u}
[Category C]
[FinitaryPreExtensive C]
{α : Type}
[Finite α]
{X : C}
{Z : α → C}
(π : (a : α) → Quiver.Hom (Z a) X)
{Y : C}
(f : Quiver.Hom Y X)
(hπ : IsIso (Limits.Sigma.desc π))
:
IsIso (Limits.Sigma.desc fun (x : α) => Limits.pullback.fst f (π x))