CategoryTheory.mapPair_equifibered
theorem CategoryTheory.mapPair_equifibered :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
{F F' : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (α : F ⟶ F'),
CategoryTheory.NatTrans.Equifibered α
The theorem `CategoryTheory.mapPair_equifibered` states that for any category `C` and any two functors `F` and `F'` from the discrete category associated with the walking pair to `C`, any natural transformation `α` from `F` to `F'` is equifibered. In other words, given any two objects `i` and `j` in the walking pair and any morphism `f` from `i` to `j`, the square involving `F.map f`, `α.app i`, `α.app j`, and `F'.map f` is a pullback.
More concisely: For any category C and functors F and F' from the discrete walking pair to C, and any natural transformation α from F to F', the square formed by F.map, α.app, and F'.map is a pullback for all morphisms in the walking pair.
|
CategoryTheory.IsVanKampenColimit.precompose_isIso
theorem CategoryTheory.IsVanKampenColimit.precompose_isIso :
∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F G : CategoryTheory.Functor J C} (α : F ⟶ G) [inst_2 : CategoryTheory.IsIso α]
{c : CategoryTheory.Limits.Cocone G},
CategoryTheory.IsVanKampenColimit c →
CategoryTheory.IsVanKampenColimit ((CategoryTheory.Limits.Cocones.precompose α).obj c)
This theorem states that for any two functors `F` and `G` from a category `J` to a category `C`, if there is an isomorphism `α` from `F` to `G`, and if `c` is a colimit of `G` that satisfies Van Kampen's condition (i.e., `c` is a Van Kampen colimit), then the colimit of `F` obtained by precomposing `c` with `α` (denoted as `((CategoryTheory.Limits.Cocones.precompose α).obj c)`) also satisfies Van Kampen's condition. In other words, the property of being a Van Kampen colimit is preserved under precomposition with an isomorphism in category theory.
More concisely: Given functors `F` and `G` from category `J` to category `C`, an isomorphism `α: F ≅ G`, and an object `c` in `C` that is a Van Kampen colimit of `G`, then `((CategoryTheory.Limits.Cocones.precompose α).obj c)` is also a Van Kampen colimit of `F`.
|
CategoryTheory.IsVanKampenColimit.of_iso
theorem CategoryTheory.IsVanKampenColimit.of_iso :
∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F},
CategoryTheory.IsVanKampenColimit c → (c ≅ c') → CategoryTheory.IsVanKampenColimit c'
This theorem states that for any type `J` with a given category structure, and any type `C` also with a category structure, given a functor `F` from `J` to `C` and two cocones `c` and `c'` over `F`, if `c` is a Van Kampen colimit then so is `c'`, provided that `c` is isomorphic to `c'`. In simpler terms, the Van Kampen property is preserved under isomorphism between cocones in a category.
More concisely: If two isomorphic cocones over a functor between two category structures represent Van Kampen colimits, then each is a Van Kampen colimit.
|