Connected limits in the over category #
Shows that the forgetful functor Over B ⥤ C creates connected limits, in particular Over B has
any connected limit which C has.
def
CategoryTheory.Over.CreatesConnected.natTransInOver
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{B : C}
(F : CategoryTheory.Functor J (CategoryTheory.Over B))
:
CategoryTheory.Functor.comp F (CategoryTheory.Over.forget B) ⟶ (CategoryTheory.Functor.const J).toPrefunctor.obj B
(Impl) Given a diagram in the over category, produce a natural transformation from the diagram legs to the specific object.
Equations
- CategoryTheory.Over.CreatesConnected.natTransInOver F = CategoryTheory.NatTrans.mk fun (j : J) => (F.toPrefunctor.obj j).hom
Instances For
@[simp]
theorem
CategoryTheory.Over.CreatesConnected.raiseCone_pt
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.IsConnected J]
{B : C}
{F : CategoryTheory.Functor J (CategoryTheory.Over B)}
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Over.forget B)))
:
(CategoryTheory.Over.CreatesConnected.raiseCone c).pt = CategoryTheory.Over.mk
(CategoryTheory.CategoryStruct.comp (c.π.app (Classical.arbitrary J))
(F.toPrefunctor.obj (Classical.arbitrary J)).hom)
@[simp]
theorem
CategoryTheory.Over.CreatesConnected.raiseCone_π_app
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.IsConnected J]
{B : C}
{F : CategoryTheory.Functor J (CategoryTheory.Over B)}
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Over.forget B)))
(j : J)
:
(CategoryTheory.Over.CreatesConnected.raiseCone c).π.app j = CategoryTheory.Over.homMk (c.π.app j)
def
CategoryTheory.Over.CreatesConnected.raiseCone
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.IsConnected J]
{B : C}
{F : CategoryTheory.Functor J (CategoryTheory.Over B)}
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Over.forget B)))
:
(Impl) Given a cone in the base category, raise it to a cone in the over category. Note this is where the connected assumption is used.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Over.CreatesConnected.raised_cone_lowers_to_original
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.IsConnected J]
{B : C}
{F : CategoryTheory.Functor J (CategoryTheory.Over B)}
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Over.forget B)))
:
(CategoryTheory.Over.forget B).mapCone (CategoryTheory.Over.CreatesConnected.raiseCone c) = c
def
CategoryTheory.Over.CreatesConnected.raisedConeIsLimit
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.IsConnected J]
{B : C}
{F : CategoryTheory.Functor J (CategoryTheory.Over B)}
{c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Over.forget B))}
(t : CategoryTheory.Limits.IsLimit c)
:
(Impl) Show that the raised cone is a limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Over.forgetCreatesConnectedLimits
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.IsConnected J]
{B : C}
:
The forgetful functor from the over category creates any connected limit.
Equations
- CategoryTheory.Over.forgetCreatesConnectedLimits = CategoryTheory.CreatesLimitsOfShape.mk
instance
CategoryTheory.Over.has_connected_limits
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{B : C}
[CategoryTheory.IsConnected J]
[CategoryTheory.Limits.HasLimitsOfShape J C]
:
The over category has any connected limit which the original category has.