Documentation

Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Connected limits in the over category #

Shows that the forgetful functor Over B ⥤ C creates and preserves connected limits, the latter without assuming that C has any limits. In particular, Over B has any connected limit which C has.

source
def CategoryTheory.Over.CreatesConnected.natTransInOver {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {B : C} (F : Functor J (Over B)) :
F.comp (forget B) ⟶ (Functor.const J).obj B

(Impl) Given a diagram in the over category, produce a natural transformation from the diagram legs to the specific object.

Equations
Instances For
    source
    def CategoryTheory.Over.CreatesConnected.raiseCone {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} {F : Functor J (Over B)} (c : Limits.Cone (F.comp (forget B))) :
    Limits.Cone F

    (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
      source
      @[simp]
      theorem CategoryTheory.Over.CreatesConnected.raiseCone_pt {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} {F : Functor J (Over B)} (c : Limits.Cone (F.comp (forget B))) :
      (raiseCone c).pt = mk (CategoryStruct.comp (c.π.app (Classical.arbitrary J)) (F.obj (Classical.arbitrary J)).hom)
      source
      @[simp]
      theorem CategoryTheory.Over.CreatesConnected.raiseCone_π_app {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} {F : Functor J (Over B)} (c : Limits.Cone (F.comp (forget B))) (j : J) :
      (raiseCone c).π.app j = homMk (c.π.app j) ⋯
      source
      theorem CategoryTheory.Over.CreatesConnected.raised_cone_lowers_to_original {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} {F : Functor J (Over B)} (c : Limits.Cone (F.comp (forget B))) :
      (forget B).mapCone (raiseCone c) = c
      source
      def CategoryTheory.Over.CreatesConnected.raisedConeIsLimit {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} {F : Functor J (Over B)} {c : Limits.Cone (F.comp (forget B))} (t : Limits.IsLimit c) :
      Limits.IsLimit (raiseCone 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
        source
        instance CategoryTheory.Over.forgetCreatesConnectedLimits {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} :
        CreatesLimitsOfShape J (forget B)

        The forgetful functor from the over category creates any connected limit.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance CategoryTheory.Over.forgetPreservesConnectedLimits {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} :
        Limits.PreservesLimitsOfShape J (forget B)

        The forgetful functor from the over category preserves any connected limit.

        source
        instance CategoryTheory.Over.has_connected_limits {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {B : C} [IsConnected J] [Limits.HasLimitsOfShape J C] :
        Limits.HasLimitsOfShape J (Over B)

        The over category has any connected limit which the original category has.