Weak limits

If F : J ⥤ C is a functor and c : Cone F, we say that c is a weak limit of F if every cone over F admits a (not necessarily unique) morphism to c. In other words, a weak limit satisfies the same "versal property" as a limit, without the uniqueness condition. In particular, weak limits are not unique, and they are not functorial.

We set up some API for weak limits, mostly copied from that for limits, prove that any limit cone is a weak limit cone, and that, if a limit exists, then it is a retract of any weak limit (see IsWeakLimit.retractOfIsLimit).

In the files WeakEqualizers.lean, WeakKernels.lean and WeakPullbacks.lean, we specialize to weak equalizers, weak kernels and weak pullbacks, and give some API for those shapes, again inspired from the non-weak case. We prove that a category with weak equalizers and pullbacks has weak pullbacks, and that a preadditive category has weak equalizers if and only if it has weak kernels.

References

• Peter J Freyd, Representations in Abelian categories, p. 99

structure CategoryTheory.Limits.IsWeakLimit {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} (t : Cone F) : Type (max (max u_1 u_3) v_3)

A cone t over F is a weak limit cone if each cone over F admits a cone morphism to t.

• lift (s : Cone F) : s.pt ⟶ t.pt

  There is a morphism from any cone point to t.pt

• fac (s : Cone F) (j : J) : CategoryStruct.comp (self.lift s) (t.π.app j) = s.π.app j

  The map makes the triangle with the two natural transformations commute

@[simp]

theorem CategoryTheory.Limits.IsWeakLimit.fac_assoc {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {t : Cone F} (self : IsWeakLimit t) (s : Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (self.lift s) (CategoryStruct.comp (t.π.app j) h) = CategoryStruct.comp (s.π.app j) h

The map makes the triangle with the two natural transformations commute

def CategoryTheory.Limits.IsWeakLimit.retractOfIsLimit {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {t t' : Cone F} (l : IsLimit t) (l' : IsWeakLimit t') : Retract t.pt t'.pt

If F has a limit, then it is a retract of any weak limit of F.

Equations

• CategoryTheory.Limits.IsWeakLimit.retractOfIsLimit l l' = { i := l'.lift t, r := l.lift t', retract := ⋯ }

def CategoryTheory.Limits.IsLimit.isWeakLimit {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {t : Cone F} (l : IsLimit t) : IsWeakLimit t

If c : Cone F is a limit, then it is a weak limit.

Equations

• l.isWeakLimit = { lift := l.lift, fac := ⋯ }

structure CategoryTheory.Limits.WeakLimitCone {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) : Type (max (max u_1 u_3) v_3)

WeakLimitCone F contains a cone over F together with the information that it is a weak limit.

• cone : Cone F

  The cone itself

• isWeakLimit : IsWeakLimit self.cone

  The proof that is the weak limit cone

def CategoryTheory.Limits.WeakLimitCone.ofLimitCone {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} (c : LimitCone F) : WeakLimitCone F

Any limit cone defines a weak limit cone with the same underlying cone over F and the same lifts.

Equations

• CategoryTheory.Limits.WeakLimitCone.ofLimitCone c = { cone := c.cone, isWeakLimit := c.isLimit.isWeakLimit }

class CategoryTheory.Limits.HasWeakLimit {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) : Prop

HasWeakLimit F represents the mere existence of a weak limit for F.

• mk' :: (
• exists_weakLimitCone : Nonempty (WeakLimitCone F)

  There is some weak limit cone for F

• )

instance CategoryTheory.Limits.instHasWeakLimitOfHasLimit {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasLimit F] : HasWeakLimit F

If F has a limit, then it has a weak limit.

theorem CategoryTheory.Limits.HasWeakLimit.mk {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} (d : WeakLimitCone F) : HasWeakLimit F

noncomputable def CategoryTheory.Limits.getWeakLimitCone {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] : WeakLimitCone F

Use the axiom of choice to extract explicit WeakLimitCone F from HasWeakLimit F.

Equations

• CategoryTheory.Limits.getWeakLimitCone F = Classical.choice ⋯

class CategoryTheory.Limits.HasWeakLimitsOfShape (J : Type u_1) [Category.{v_1, u_1} J] (C : Type u_3) [Category.{v_3, u_3} C] : Prop

C has weak limits of shape J if there exists a weak limit for every functor F : J ⥤ C.

• hasWeakLimit (F : Functor J C) : HasWeakLimit F

  All functors F : J ⥤ C from J have weak limits

@[instance 100]

instance CategoryTheory.Limits.instHasWeakLimitsOfShapeOfHasLimitsOfShape {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] [HasLimitsOfShape J C] : HasWeakLimitsOfShape J C

noncomputable def CategoryTheory.Limits.weakLimit.cone {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] : Cone F

An arbitrary choice of weak limit cone for a functor.

Equations

• CategoryTheory.Limits.weakLimit.cone F = (CategoryTheory.Limits.getWeakLimitCone F).cone

noncomputable def CategoryTheory.Limits.weakLimit {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] : C

An arbitrary choice of weak limit object of a functor.

Equations

• CategoryTheory.Limits.weakLimit F = (CategoryTheory.Limits.weakLimit.cone F).pt

noncomputable def CategoryTheory.Limits.weakLimit.π {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] (j : J) : weakLimit F ⟶ F.obj j

The projection from the weak limit object to a value of the functor.

Equations

• CategoryTheory.Limits.weakLimit.π F j = (CategoryTheory.Limits.weakLimit.cone F).π.app j

theorem CategoryTheory.Limits.weakLimit.π_comp_eqToHom {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] {j j' : J} (hj : j = j') : CategoryStruct.comp (π F j) (eqToHom ⋯) = π F j'

theorem CategoryTheory.Limits.weakLimit.π_comp_eqToHom_assoc {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] {j j' : J} (hj : j = j') {Z : C} (h : F.obj j' ⟶ Z) : CategoryStruct.comp (π F j) (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (π F j') h

@[simp]

theorem CategoryTheory.Limits.weakLimit.cone_pt {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} [HasWeakLimit F] : (cone F).pt = weakLimit F

@[simp]

theorem CategoryTheory.Limits.weakLimit.cone_π {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} [HasWeakLimit F] : (cone F).π.app = π F

@[simp]

theorem CategoryTheory.Limits.weakLimit.w {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] {j j' : J} (f : j ⟶ j') : CategoryStruct.comp (π F j) (F.map f) = π F j'

@[simp]

theorem CategoryTheory.Limits.weakLimit.w_assoc {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] {j j' : J} (f : j ⟶ j') {Z : C} (h : F.obj j' ⟶ Z) : CategoryStruct.comp (π F j) (CategoryStruct.comp (F.map f) h) = CategoryStruct.comp (π F j') h

noncomputable def CategoryTheory.Limits.weakLimit.isWeakLimit {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] : IsWeakLimit (cone F)

Evidence that the arbitrary choice of cone provided by weakLimit.cone F is a weak limit cone.

Equations

• CategoryTheory.Limits.weakLimit.isWeakLimit F = (CategoryTheory.Limits.getWeakLimitCone F).isWeakLimit

noncomputable def CategoryTheory.Limits.weakLimit.lift {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] (F : Functor J C) [HasWeakLimit F] (c : Cone F) : c.pt ⟶ weakLimit F

A morphism from the cone point of any other cone to the weak limit object.

Equations

• CategoryTheory.Limits.weakLimit.lift F c = (CategoryTheory.Limits.weakLimit.isWeakLimit F).lift c

@[simp]

theorem CategoryTheory.Limits.weakLimit.isWeakLimit_lift {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} [HasWeakLimit F] (c : Cone F) : (isWeakLimit F).lift c = lift F c

@[simp]

theorem CategoryTheory.Limits.weakLimit.lift_π {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} [HasWeakLimit F] (c : Cone F) (j : J) : CategoryStruct.comp (lift F c) (π F j) = c.π.app j

@[simp]

theorem CategoryTheory.Limits.weakLimit.lift_π_assoc {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} [HasWeakLimit F] (c : Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (lift F c) (CategoryStruct.comp (π F j) h) = CategoryStruct.comp (c.π.app j) h

def CategoryTheory.Limits.IsWeakLimit.ofIsoWeakLimit {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {r t : Cone F} (P : IsWeakLimit r) (i : r ≅ t) : IsWeakLimit t

Transport evidence that a cone is a weak limit cone across an isomorphism of cones.

Equations

• P.ofIsoWeakLimit i = { lift := fun (s : CategoryTheory.Limits.Cone F) => CategoryTheory.CategoryStruct.comp (P.lift s) i.hom.hom, fac := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsWeakLimit.ofIsoWeakLimit_lift {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {r t : Cone F} (P : IsWeakLimit r) (i : r ≅ t) (s : Cone F) : (P.ofIsoWeakLimit i).lift s = CategoryStruct.comp (P.lift s) i.hom.hom

def CategoryTheory.Limits.IsWeakLimit.equivIsoWeakLimit {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {r t : Cone F} (i : r ≅ t) : IsWeakLimit r ≃ IsWeakLimit t

Isomorphism of cones preserves whether or not they are weak limit cones.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.IsWeakLimit.equivIsoWeakLimit_apply {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {r t : Cone F} (i : r ≅ t) (P : IsWeakLimit r) : (equivIsoWeakLimit i) P = P.ofIsoWeakLimit i

@[simp]

theorem CategoryTheory.Limits.IsWeakLimit.equivIsoWeakLimit_symm_apply {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {r t : Cone F} (i : r ≅ t) (P : IsWeakLimit t) : (equivIsoWeakLimit i).symm P = P.ofIsoWeakLimit i.symm

def CategoryTheory.Limits.IsWeakLimit.liftConeMorphism {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {t : Cone F} (h : IsWeakLimit t) (s : Cone F) : s ⟶ t

The versal morphism from any other cone to a weak limit cone.

Equations

• h.liftConeMorphism s = { hom := h.lift s, w := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsWeakLimit.liftConeMorphism_hom {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {t : Cone F} (h : IsWeakLimit t) (s : Cone F) : (h.liftConeMorphism s).hom = h.lift s

def CategoryTheory.Limits.IsWeakLimit.mkOfConeMorphism {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {t : Cone F} (lift : (s : Cone F) → s ⟶ t) : IsWeakLimit t

Alternative constructor for isWeakLimit, providing a morphism of cones rather than a morphism between the cone points and separately the factorisation condition.

Equations

• CategoryTheory.Limits.IsWeakLimit.mkOfConeMorphism lift = { lift := fun (s : CategoryTheory.Limits.Cone F) => (lift s).hom, fac := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsWeakLimit.mkOfConeMorphism_lift {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {t : Cone F} (lift : (s : Cone F) → s ⟶ t) (s : Cone F) : (mkOfConeMorphism lift).lift s = (lift s).hom

def CategoryTheory.Limits.IsWeakLimit.ofRightAdjoint {J : Type u_1} [Category.{v_1, u_1} J] {K : Type u_2} [Category.{v_2, u_2} K] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {D : Type u_4} [Category.{v_4, u_4} D] {G : Functor K D} {left : Functor (Cone F) (Cone G)} {right : Functor (Cone G) (Cone F)} (adj : left ⊣ right) {c : Cone G} (t : IsWeakLimit c) : IsWeakLimit (right.obj c)

Given a right adjoint functor between categories of cones, the image of a weak limit cone is a weak limit cone.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.IsWeakLimit.iff_of_cone_equiv {J : Type u_1} [Category.{v_1, u_1} J] {K : Type u_2} [Category.{v_2, u_2} K] {C : Type u_3} [Category.{v_3, u_3} C] {F : Functor J C} {D : Type u_5} [Category.{v_5, u_5} D] {G : Functor K D} (h : Cone G ≌ Cone F) {c : Cone G} : Nonempty (IsWeakLimit (h.functor.obj c)) ↔ Nonempty (IsWeakLimit c)

Given two functors which have equivalent categories of cones, we can transport evidence of a weak limit cone across the equivalence.

theorem CategoryTheory.Limits.IsWeakLimit.postcompose_hom_iff_of_iso {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F G : Functor J C} (α : F ≅ G) (c : Cone F) : Nonempty (IsWeakLimit ((Cone.postcompose α.hom).obj c)) ↔ Nonempty (IsWeakLimit c)

A cone postcomposed with a natural isomorphism is a weak limit cone if and only if the original cone is.

theorem CategoryTheory.Limits.IsWeakLimit.postcompose_inv_iff_of_iso {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F G : Functor J C} (α : F ≅ G) (c : Cone G) : Nonempty (IsWeakLimit ((Cone.postcompose α.inv).obj c)) ↔ Nonempty (IsWeakLimit c)

A cone postcomposed with the inverse of a natural isomorphism is a weak limit cone if and only if the original cone is.

theorem CategoryTheory.Limits.IsWeakLimit.iff_of_natIso_of_iso {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F G : Functor J C} (α : F ≅ G) (c : Cone F) (d : Cone G) (w : (Cone.postcompose α.hom).obj c ≅ d) : Nonempty (IsWeakLimit c) ↔ Nonempty (IsWeakLimit d)

Constructing an equivalence between Nonempty (IsWeakLimit c) and Nonempty (IsWeakLimit d) from a natural isomorphism between the underlying functors, and then an isomorphism between c transported along this and d.

theorem CategoryTheory.Limits.hasWeakLimit_of_iso {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F G : Functor J C} [HasWeakLimit F] (α : F ≅ G) : HasWeakLimit G

If a functor F has a weak limit, so does any naturally isomorphic functor.

theorem CategoryTheory.Limits.hasWeakLimit_iff_of_iso {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_3} [Category.{v_3, u_3} C] {F G : Functor J C} (α : F ≅ G) : HasWeakLimit F ↔ HasWeakLimit G