CategoryTheory.FinitaryExtensive.vanKampen
theorem CategoryTheory.FinitaryExtensive.vanKampen :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.FinitaryExtensive C]
{F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
(c : CategoryTheory.Limits.Cocone F), CategoryTheory.Limits.IsColimit c → CategoryTheory.IsVanKampenColimit c
The theorem `CategoryTheory.FinitaryExtensive.vanKampen` states that for any category `C`, that is finitarily extensive, and any functor `F` from the discrete category of a walking pair into `C`, if `c` is a cocone over `F` and is a colimit, then `c` is a Van Kampen colimit. In other words, in a finitarily extensive category, all colimits of functors from the discrete category of a walking pair are Van Kampen colimits.
More concisely: In a finitarily extensive category, every colimit of functors from the discrete category of a walking pair is a Van Kampen colimit.
|
CategoryTheory.FinitaryExtensive.van_kampen'
theorem CategoryTheory.FinitaryExtensive.van_kampen' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.FinitaryExtensive C] {X Y : C}
(c : CategoryTheory.Limits.BinaryCofan X Y),
CategoryTheory.Limits.IsColimit c → CategoryTheory.IsVanKampenColimit c
The theorem states that in a finitary extensive category, all coproducts are van Kampen. Specifically, for any category `C`, if it is finitary extensive, and given a binary cofan `c` on objects `X` and `Y` of `C`, if `c` is a colimit, then `c` is also a van Kampen colimit. In the context of category theory, van Kampen colimits represent a generalization of the Seifert-van Kampen theorem in algebraic topology, and extensive categories are categories with well-behaved coproducts.
More concisely: In a finitary extensive category, every coproduct that is a colimit is a van Kampen colimit.
|
CategoryTheory.FinitaryPreExtensive.universal'
theorem CategoryTheory.FinitaryPreExtensive.universal' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.FinitaryPreExtensive C] {X Y : C}
(c : CategoryTheory.Limits.BinaryCofan X Y),
CategoryTheory.Limits.IsColimit c → CategoryTheory.IsUniversalColimit c
This theorem states that in a finitary extensive category, all coproducts are van Kampen. More specifically, for any category `C`, and given any objects `X` and `Y` from `C`, if a binary cofan `c` exists and it is a colimit (as per the `CategoryTheory.Limits.IsColimit c` condition), then this colimit is a universal colimit.
In simpler terms, if we have a category with finite coproducts which behave nicely (i.e., the category is finitary extensive), and if we have a binary cofan (which is a way of expressing a type of coproduct) that forms a colimit (a specific way of "gluing" things together in a category), then this colimit is a universal one (it is the "best possible" in a specific sense).
More concisely: In a finitary extensive category, every binary coproduct that is a colimit is a universal coproduct.
|
CategoryTheory.finitaryExtensive_of_preserves_and_reflects
theorem CategoryTheory.finitaryExtensive_of_preserves_and_reflects :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''}
[inst_1 : CategoryTheory.Category.{v'', u''} D] (F : CategoryTheory.Functor C D)
[inst_2 : CategoryTheory.FinitaryExtensive D] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
[inst_4 : CategoryTheory.HasPullbacksOfInclusions C] [inst_5 : CategoryTheory.PreservesPullbacksOfInclusions F]
[inst_6 : CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
[inst_7 :
CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
[inst_8 :
CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F],
CategoryTheory.FinitaryExtensive C
This theorem states that for any two categories `C` and `D` and a functor `F` from `C` to `D`, if `D` is finitary extensive, `C` has finite coproducts, `C` has pullbacks of inclusions, `F` preserves pullbacks of inclusions, `F` reflects limits of the shape `WalkingCospan`, `F` preserves colimits of the shape `WalkingPair`, and `F` reflects colimits of the shape `WalkingPair`, then `C` is also finitary extensive.
In more detail, finitary extensiveness is a property of a category that relates to the ability to 'break apart' objects into a finite coproduct of smaller objects. The theorem is essentially saying that if these conditions are met, then this property is preserved under the functor `F`: if you can 'break apart' objects in `D`, then you can also 'break apart' their pre-images in `C`. The conditions on `F` mean that `F` behaves well with respect to certain limits and colimits, essentially that it 'respects' the ways in which objects can be 'broken apart' or 'put together'.
More concisely: If categories `C` and `D` have given properties, and functor `F` from `C` to `D` preserves certain limits and colimits, then `C` is finitarily extensive if `D` is.
|