Weighted limits

In this file, we define weighted limits (in the non enriched case). Given a weight W : J ⥤ Type w and a functor F : J ⥤ C, the W-weighted limit of J is the limit of the functor CategoryOfElements.π W ⋙ F : W.Elements ⥤ C.

References

• https://ncatlab.org/nlab/show/weighted+limit

@[reducible, inline]

abbrev CategoryTheory.Limits.WeightedCone {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) : Type (max (max (max u w) u') v')

Given W : J ⥤ Type w and F : J ⥤ C, this is the type of cones for the functor CategoryOfElements.π W ⋙ F : W.Elements ⥤ C.

Equations

• CategoryTheory.Limits.WeightedCone W F = CategoryTheory.Limits.Cone ((CategoryTheory.CategoryOfElements.π W).comp F)

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWeightedLimit {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) : Prop

Given a weight W : J ⥤ Type w and F : J ⥤ C, we say that the W-weighted limit of F exists if the functor CategoryOfElements.π W ⋙ F : W.Elements ⥤ C has a limit.

Equations

• CategoryTheory.Limits.HasWeightedLimit W F = CategoryTheory.Limits.HasLimit ((CategoryTheory.CategoryOfElements.π W).comp F)

@[reducible, inline]

abbrev CategoryTheory.Limits.WeightedCone.π {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} (c : WeightedCone W F) {j : J} (x : W.obj j) : c.pt ⟶ F.obj j

The projection c.pt ⟶ F.obj j for c : WeightedCone W F and x : W.obj j.

Equations

• c.π x = c.π.app (W.elementsMk j x)

@[simp]

theorem CategoryTheory.Limits.WeightedCone.w {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} (c : WeightedCone W F) {i j : J} (x : W.obj i) (f : i ⟶ j) : CategoryStruct.comp (c.π x) (F.map f) = c.π ((ConcreteCategory.hom (W.map f)) x)

@[simp]

theorem CategoryTheory.Limits.WeightedCone.w_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} (c : WeightedCone W F) {i j : J} (x : W.obj i) (f : i ⟶ j) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (c.π x) (CategoryStruct.comp (F.map f) h) = CategoryStruct.comp (c.π ((ConcreteCategory.hom (W.map f)) x)) h

def CategoryTheory.Limits.WeightedCone.mk {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} (pt : C) (π : ⦃j : J⦄ → W.obj j → (pt ⟶ F.obj j)) (hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), CategoryStruct.comp (π x) (F.map f) = π ((ConcreteCategory.hom (W.map f)) x)) : WeightedCone W F

Constructor for weighted cones.

Equations

• CategoryTheory.Limits.WeightedCone.mk pt π hπ = { pt := pt, π := { app := fun (x : W.Elements) => π x.snd, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Limits.WeightedCone.mk_pt {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} (pt : C) (π : ⦃j : J⦄ → W.obj j → (pt ⟶ F.obj j)) (hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), CategoryStruct.comp (π x) (F.map f) = π ((ConcreteCategory.hom (W.map f)) x)) : (mk pt π hπ).pt = pt

@[simp]

theorem CategoryTheory.Limits.WeightedCone.mk_π {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} (pt : C) (π : ⦃j : J⦄ → W.obj j → (pt ⟶ F.obj j)) (hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), CategoryStruct.comp (π x) (F.map f) = π ((ConcreteCategory.hom (W.map f)) x)) {j : J} (x : W.obj j) : (mk pt π hπ).π x = π x

@[reducible, inline]

abbrev CategoryTheory.Limits.WeightedCone.IsLimit {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} (c : WeightedCone W F) : Type (max (max (max u w) u') v')

A weighted cone c : WeightedCone W F is a limit if it is so as a cone of CategoryOfElements.π W ⋙ F : W.Elements ⥤ C.

Equations

• c.IsLimit = CategoryTheory.Limits.IsLimit c

theorem CategoryTheory.Limits.WeightedCone.IsLimit.hasWeightedLimit {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} {c : WeightedCone W F} (hc : c.IsLimit) : HasWeightedLimit W F

def CategoryTheory.Limits.WeightedCone.IsLimit.lift {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} {c : WeightedCone W F} (hc : c.IsLimit) {Z : C} (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j)) (hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), CategoryStruct.comp (π x) (F.map f) = π ((ConcreteCategory.hom (W.map f)) x)) : Z ⟶ c.pt

Constructor for morphisms from the point of a limit weighted cone.

Equations

• hc.lift π hπ = hc.lift (CategoryTheory.Limits.WeightedCone.mk Z π hπ)

@[simp]

theorem CategoryTheory.Limits.WeightedCone.IsLimit.fac {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} {c : WeightedCone W F} (hc : c.IsLimit) {Z : C} (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j)) (hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), CategoryStruct.comp (π x) (F.map f) = π ((ConcreteCategory.hom (W.map f)) x)) {j : J} (x : W.obj j) : CategoryStruct.comp (hc.lift π hπ) (c.π x) = π x

@[simp]

theorem CategoryTheory.Limits.WeightedCone.IsLimit.fac_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} {c : WeightedCone W F} (hc : c.IsLimit) {Z : C} (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j)) (hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), CategoryStruct.comp (π x) (F.map f) = π ((ConcreteCategory.hom (W.map f)) x)) {j : J} (x : W.obj j) {Z✝ : C} (h : F.obj j ⟶ Z✝) : CategoryStruct.comp (hc.lift π hπ) (CategoryStruct.comp (c.π x) h) = CategoryStruct.comp (π x) h

theorem CategoryTheory.Limits.WeightedCone.IsLimit.hom_ext {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} {c : WeightedCone W F} (hc : c.IsLimit) {Z : C} {f g : Z ⟶ c.pt} (h : ∀ {j : J} (x : W.obj j), CategoryStruct.comp f (c.π x) = CategoryStruct.comp g (c.π x)) : f = g

@[reducible, inline]

abbrev CategoryTheory.Limits.WeightedCone.coyoneda {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) (j : J) : WeightedCone (coyoneda.obj (Opposite.op j)) F

If the weight is coyoneda.obj (op j) : J ⥤ Type _, this is the limit weighted cone for F : J ⥤ C with point F.obj j.

Equations

• CategoryTheory.Limits.WeightedCone.coyoneda F j = { pt := F.obj j, π := { app := fun (u : (CategoryTheory.coyoneda.obj (Opposite.op j)).Elements) => F.map u.snd, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Limits.WeightedCone.coyoneda_pt {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) (j : J) : (WeightedCone.coyoneda F j).pt = F.obj j

@[simp]

theorem CategoryTheory.Limits.WeightedCone.coyoneda_π_app {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) (j : J) (u : (coyoneda.obj (Opposite.op j)).Elements) : (WeightedCone.coyoneda F j).π.app u = F.map u.snd

def CategoryTheory.Limits.WeightedCone.isLimitCoyoneda {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) (j : J) : (WeightedCone.coyoneda F j).IsLimit

The weighted limit of F for the weight coyoneda.obj (op j) is F.obj j.

Equations

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

noncomputable def CategoryTheory.Functor.weightedLimObjObj {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) [Limits.HasWeightedLimit W F] : C

Given a weight W : J ⥤ Type w and F : J ⥤ C, this is the W-weighted limit of F.

Equations

• W.weightedLimObjObj F = CategoryTheory.Limits.limit ((CategoryTheory.CategoryOfElements.π W).comp F)

noncomputable def CategoryTheory.Functor.weightedLimObjObjπ {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) [Limits.HasWeightedLimit W F] ⦃j : J⦄ (x : W.obj j) : W.weightedLimObjObj F ⟶ F.obj j

The projections from the weighted limit.

Equations

• W.weightedLimObjObjπ F x = CategoryTheory.Limits.limit.π ((CategoryTheory.CategoryOfElements.π W).comp F) (W.elementsMk j x)

@[simp]

theorem CategoryTheory.Functor.weightedLimObjObj_w {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) [Limits.HasWeightedLimit W F] ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂) : CategoryStruct.comp (W.weightedLimObjObjπ F x) (F.map f) = W.weightedLimObjObjπ F ((ConcreteCategory.hom (W.map f)) x)

@[simp]

theorem CategoryTheory.Functor.weightedLimObjObj_w_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) [Limits.HasWeightedLimit W F] ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂) {Z : C} (h : F.obj j₂ ⟶ Z) : CategoryStruct.comp (W.weightedLimObjObjπ F x) (CategoryStruct.comp (F.map f) h) = CategoryStruct.comp (W.weightedLimObjObjπ F ((ConcreteCategory.hom (W.map f)) x)) h

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.weightedLimCone {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) [Limits.HasWeightedLimit W F] : Limits.WeightedCone W F

A choice of limit weighted cone.

Equations

• W.weightedLimCone F = CategoryTheory.Limits.WeightedCone.mk (W.weightedLimObjObj F) (fun (j : J) (x : W.obj j) => W.weightedLimObjObjπ F x) ⋯

noncomputable def CategoryTheory.Functor.isLimitWeightedLimCone {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) [Limits.HasWeightedLimit W F] : (W.weightedLimCone F).IsLimit

The weighted cone W.weightedLimCone F is a limit.

Equations

• W.isLimitWeightedLimCone F = CategoryTheory.Limits.limit.isLimit ((CategoryTheory.CategoryOfElements.π W).comp F)

@[simp]

theorem CategoryTheory.Functor.isLimitWeightedLimCone_fac {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) [Limits.HasWeightedLimit W F] {Z : C} (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j)) (hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), CategoryStruct.comp (π x) (F.map f) = π ((ConcreteCategory.hom (W.map f)) x)) ⦃j : J⦄ (x : W.obj j) : CategoryStruct.comp ((W.isLimitWeightedLimCone F).lift π hπ) (W.weightedLimObjObjπ F x) = π x

theorem CategoryTheory.Functor.isLimitWeightedLimCone_fac_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) [Limits.HasWeightedLimit W F] {Z : C} (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j)) (hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), CategoryStruct.comp (π x) (F.map f) = π ((ConcreteCategory.hom (W.map f)) x)) ⦃j : J⦄ (x : W.obj j) {Z✝ : C} (h : F.obj j ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp ((W.isLimitWeightedLimCone F).lift π hπ) (W.weightedLimObjObjπ F x)) h = CategoryStruct.comp (π x) h

theorem CategoryTheory.Functor.weightedLimObjObj.hom_ext {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} [Limits.HasWeightedLimit W F] {Z : C} {f g : Z ⟶ W.weightedLimObjObj F} (h : ∀ {j : J} (x : W.obj j), CategoryStruct.comp f (W.weightedLimObjObjπ F x) = CategoryStruct.comp g (W.weightedLimObjObjπ F x)) : f = g

theorem CategoryTheory.Functor.weightedLimObjObj.hom_ext_iff {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} {F : Functor J C} [Limits.HasWeightedLimit W F] {Z : C} {f g : Z ⟶ W.weightedLimObjObj F} : f = g ↔ ∀ {j : J} (x : W.obj j), CategoryStruct.comp f (W.weightedLimObjObjπ F x) = CategoryStruct.comp g (W.weightedLimObjObjπ F x)

noncomputable def CategoryTheory.Functor.weightedLimObjMap {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) {F₁ F₂ : Functor J C} [Limits.HasWeightedLimit W F₁] [Limits.HasWeightedLimit W F₂] (f : F₁ ⟶ F₂) : W.weightedLimObjObj F₁ ⟶ W.weightedLimObjObj F₂

Functoriality of the weighted limits with fixed weight W : J ⥤ Type w with respect to the functor in J ⥤ C.

Equations

• W.weightedLimObjMap f = CategoryTheory.Limits.limMap ((CategoryTheory.CategoryOfElements.π W).whiskerLeft f)

@[simp]

theorem CategoryTheory.Functor.weightedLimObjMap_π {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) {F₁ F₂ : Functor J C} [Limits.HasWeightedLimit W F₁] [Limits.HasWeightedLimit W F₂] (f : F₁ ⟶ F₂) ⦃j : J⦄ (x : W.obj j) : CategoryStruct.comp (W.weightedLimObjMap f) (W.weightedLimObjObjπ F₂ x) = CategoryStruct.comp (W.weightedLimObjObjπ F₁ x) (f.app j)

@[simp]

theorem CategoryTheory.Functor.weightedLimObjMap_π_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) {F₁ F₂ : Functor J C} [Limits.HasWeightedLimit W F₁] [Limits.HasWeightedLimit W F₂] (f : F₁ ⟶ F₂) ⦃j : J⦄ (x : W.obj j) {Z : C} (h : F₂.obj j ⟶ Z) : CategoryStruct.comp (W.weightedLimObjMap f) (CategoryStruct.comp (W.weightedLimObjObjπ F₂ x) h) = CategoryStruct.comp (W.weightedLimObjObjπ F₁ x) (CategoryStruct.comp (f.app j) h)

@[simp]

theorem CategoryTheory.Functor.weightedLimObjMap_id {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) (F : Functor J C) [Limits.HasWeightedLimit W F] : W.weightedLimObjMap (CategoryStruct.id F) = CategoryStruct.id (W.weightedLimObjObj F)

theorem CategoryTheory.Functor.weightedLimObjMap_comp {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) {F₁ F₂ F₃ : Functor J C} [Limits.HasWeightedLimit W F₁] [Limits.HasWeightedLimit W F₂] [Limits.HasWeightedLimit W F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) : W.weightedLimObjMap (CategoryStruct.comp f g) = CategoryStruct.comp (W.weightedLimObjMap f) (W.weightedLimObjMap g)

theorem CategoryTheory.Functor.weightedLimObjMap_comp_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (W : Functor J (Type w)) {F₁ F₂ F₃ : Functor J C} [Limits.HasWeightedLimit W F₁] [Limits.HasWeightedLimit W F₂] [Limits.HasWeightedLimit W F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) {Z : C} (h : W.weightedLimObjObj F₃ ⟶ Z) : CategoryStruct.comp (W.weightedLimObjMap (CategoryStruct.comp f g)) h = CategoryStruct.comp (W.weightedLimObjMap f) (CategoryStruct.comp (W.weightedLimObjMap g) h)

noncomputable def CategoryTheory.Functor.weightedLimFlipObjMap {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W W' : Functor J (Type w)} (g : W ⟶ W') (F : Functor J C) [Limits.HasWeightedLimit W F] [Limits.HasWeightedLimit W' F] : W'.weightedLimObjObj F ⟶ W.weightedLimObjObj F

The (contravariant) functoriality of weighted limits with respect to the weight.

Equations

• CategoryTheory.Functor.weightedLimFlipObjMap g F = (W.isLimitWeightedLimCone F).lift (fun (j : J) (x : W.obj j) => W'.weightedLimObjObjπ F ((CategoryTheory.ConcreteCategory.hom (g.app j)) x)) ⋯

@[simp]

theorem CategoryTheory.Functor.weightedLimObjObjMap_π {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W W' : Functor J (Type w)} (g : W ⟶ W') (F : Functor J C) [Limits.HasWeightedLimit W F] [Limits.HasWeightedLimit W' F] ⦃j : J⦄ (x : W.obj j) : CategoryStruct.comp (weightedLimFlipObjMap g F) (W.weightedLimObjObjπ F x) = W'.weightedLimObjObjπ F ((ConcreteCategory.hom (g.app j)) x)

@[simp]

theorem CategoryTheory.Functor.weightedLimObjObjMap_π_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W W' : Functor J (Type w)} (g : W ⟶ W') (F : Functor J C) [Limits.HasWeightedLimit W F] [Limits.HasWeightedLimit W' F] ⦃j : J⦄ (x : W.obj j) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (weightedLimFlipObjMap g F) (CategoryStruct.comp (W.weightedLimObjObjπ F x) h) = CategoryStruct.comp (W'.weightedLimObjObjπ F ((ConcreteCategory.hom (g.app j)) x)) h

@[simp]

theorem CategoryTheory.Functor.weightedLimFlipObjMap_id {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W : Functor J (Type w)} (F : Functor J C) [Limits.HasWeightedLimit W F] : weightedLimFlipObjMap (CategoryStruct.id W) F = CategoryStruct.id (W.weightedLimObjObj F)

theorem CategoryTheory.Functor.weightedLimFlipObjMap_comp {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W W' W'' : Functor J (Type w)} (g : W ⟶ W') (g' : W' ⟶ W'') (F : Functor J C) [Limits.HasWeightedLimit W F] [Limits.HasWeightedLimit W' F] [Limits.HasWeightedLimit W'' F] : CategoryStruct.comp (weightedLimFlipObjMap g' F) (weightedLimFlipObjMap g F) = weightedLimFlipObjMap (CategoryStruct.comp g g') F

theorem CategoryTheory.Functor.weightedLimFlipObjMap_comp_assoc {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] {W W' W'' : Functor J (Type w)} (g : W ⟶ W') (g' : W' ⟶ W'') (F : Functor J C) [Limits.HasWeightedLimit W F] [Limits.HasWeightedLimit W' F] [Limits.HasWeightedLimit W'' F] {Z : C} (h : W.weightedLimObjObj F ⟶ Z) : CategoryStruct.comp (weightedLimFlipObjMap g' F) (CategoryStruct.comp (weightedLimFlipObjMap g F) h) = CategoryStruct.comp (weightedLimFlipObjMap (CategoryStruct.comp g g') F) h