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

@[implicit_reducible]

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) := by cat_disch) : 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) := by cat_disch) : (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) := by cat_disch) {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

def CategoryTheory.Limits.WeightedCone.IsLimit.mk {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} (lift : (s : WeightedCone W F) → s.pt ⟶ c.pt) (fac : ∀ (s : WeightedCone W F) ⦃j : J⦄ (x : W.obj j), CategoryStruct.comp (lift s) (c.π x) = s.π x) (uniq : ∀ (s : WeightedCone W F) (m : s.pt ⟶ c.pt), (∀ ⦃j : J⦄ (x : W.obj j), CategoryStruct.comp m (c.π x) = s.π x) → m = lift s) : IsLimit c

Helper definition in order to show that a weighted cone is a limit.

Equations

• CategoryTheory.Limits.WeightedCone.IsLimit.mk lift fac uniq = { lift := lift, fac := ⋯, uniq := ⋯ }

@[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 = CategoryTheory.Limits.WeightedCone.mk (F.obj j) (fun (j' : J) (f : (CategoryTheory.coyoneda.obj (Opposite.op j)).obj j') => F.map f) ⋯

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

@[simp]

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 ((W.isLimitWeightedLimCone F).lift π hπ) (CategoryStruct.comp (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

@[reducible, inline]

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

Given a weight W : J ⥤ Type w, this is the property that all W-weighted limits exist for functors F : J ⥤ C. Under this condition, we define a weighted limit functor W.weightedLimObj : (J ⥤ C) ⥤ C. (See also HasWeightedLimFlipObj for the "flipped" property for F : J ⥤ C.)

Equations

• W.HasWeightedLimObj C = ∀ (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasWeightedLimit W F

@[implicit_reducible]

noncomputable def CategoryTheory.Functor.weightedLimObj {J : Type u} [Category.{v, u} J] (W : Functor J (Type w)) {C : Type u'} [Category.{v', u'} C] [W.HasWeightedLimObj C] : Functor (Functor J C) C

Weighted limits for a fixed weight W : J ⥤p Type w, as a functor (J ⥤ C) ⥤ C.

Equations

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

@[simp]

theorem CategoryTheory.Functor.weightedLimObj_map {J : Type u} [Category.{v, u} J] (W : Functor J (Type w)) {C : Type u'} [Category.{v', u'} C] [W.HasWeightedLimObj C] {X✝ Y✝ : Functor J C} (f : X✝ ⟶ Y✝) : W.weightedLimObj.map f = W.weightedLimObjMap f

@[simp]

theorem CategoryTheory.Functor.weightedLimObj_obj {J : Type u} [Category.{v, u} J] (W : Functor J (Type w)) {C : Type u'} [Category.{v', u'} C] [W.HasWeightedLimObj C] (F : Functor J C) : W.weightedLimObj.obj F = W.weightedLimObjObj F

instance CategoryTheory.Functor.instHasWeightedLimObjObjOppositeTypeCoyoneda {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (j : Jᵒᵖ) : (coyoneda.obj j).HasWeightedLimObj C

@[reducible, inline]

abbrev CategoryTheory.Functor.hasWeightedLimit {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) : ObjectProperty (Functor J (Type w))

Given a functor F : J ⥤ C, this is the property satisfied by weights W : J ⥤ Type w such that the W-weighted limit of F exists.

Equations

• F.hasWeightedLimit W = CategoryTheory.Limits.HasWeightedLimit W F

instance CategoryTheory.Functor.instHasWeightedLimitObjTypeHasWeightedLimit {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) (W : F.hasWeightedLimit.FullSubcategory) : Limits.HasWeightedLimit W.obj F

@[implicit_reducible]

noncomputable def CategoryTheory.Functor.weightedLimFlipObj' {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) : Functor F.hasWeightedLimit.FullSubcategoryᵒᵖ C

Given a functor F : J ⥤ C, this is the functor which sends a weight W : J ⥤ Type w to the W-weighted limit of F. This is defined on the full subcategory of J ⥤ Type w where this weighted limit exists.

Equations

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

@[simp]

theorem CategoryTheory.Functor.weightedLimFlipObj'_map {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) {X✝ Y✝ : F.hasWeightedLimit.FullSubcategoryᵒᵖ} (g : X✝ ⟶ Y✝) : F.weightedLimFlipObj'.map g = weightedLimFlipObjMap g.unop.hom F

@[simp]

theorem CategoryTheory.Functor.weightedLimFlipObj'_obj {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) (W : F.hasWeightedLimit.FullSubcategoryᵒᵖ) : F.weightedLimFlipObj'.obj W = (Opposite.unop W).obj.weightedLimObjObj F

@[reducible, inline]

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

Given F : J ⥤ C, this is the property that weighted limits of F exist for all weights W : J ⥤ Type w. Under this condition, we define a weighted limit functor F.weightedLimFlipObj : (J ⥤ Type w)ᵒᵖ ⥤ C. (See also HasWeightedLimObj for the "flipped" property for W : J ⥤ Type w.)

Equations

• F.HasWeightedLimFlipObj = ∀ (W : CategoryTheory.Functor J (Type ?u.5)), CategoryTheory.Limits.HasWeightedLimit W F

theorem CategoryTheory.Functor.hasWeightedLimit_eq_top {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) [F.HasWeightedLimFlipObj] : F.hasWeightedLimit = ⊤

@[implicit_reducible]

noncomputable def CategoryTheory.Functor.weightedLimFlipObj {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) [F.HasWeightedLimFlipObj] : Functor (Functor J (Type w))ᵒᵖ C

Given a functor F : J ⥤ C, this is the functor (J ⥤ Type w)ᵒᵖ ⥤ C which sends a weight W : J ⥤ Type w to the W-weighted limit of F. Here, we assume that all such weighted limits exist.

Equations

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

@[simp]

theorem CategoryTheory.Functor.weightedLimFlipObj_obj {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) [F.HasWeightedLimFlipObj] (W : (Functor J (Type w))ᵒᵖ) : F.weightedLimFlipObj.obj W = (Opposite.unop W).weightedLimObjObj F

@[simp]

theorem CategoryTheory.Functor.weightedLimFlipObj_map {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) [F.HasWeightedLimFlipObj] {X✝ Y✝ : (Functor J (Type w))ᵒᵖ} (g : X✝ ⟶ Y✝) : F.weightedLimFlipObj.map g = weightedLimFlipObjMap g.unop F

noncomputable def CategoryTheory.Functor.weightedLimFlipObjIso' {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) [F.HasWeightedLimFlipObj] : F.hasWeightedLimit.ι.op.comp F.weightedLimFlipObj ≅ F.weightedLimFlipObj'

When HasWeightedLimFlipObj.{w} F holds, the composition of the equivalence F.hasWeightedLimit.ι.op with weightedLimFlipObj.{w} F identifies to weightedLimFlipObj'.{w} F.

Equations

• F.weightedLimFlipObjIso' = CategoryTheory.Iso.refl (F.hasWeightedLimit.ι.op.comp F.weightedLimFlipObj)

instance CategoryTheory.Functor.instIsEquivalenceFullSubcategoryTypeHasWeightedLimitι {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) [F.HasWeightedLimFlipObj] : F.hasWeightedLimit.ι.IsEquivalence

noncomputable def CategoryTheory.Functor.weightedLimFlipObjIso {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (F : Functor J C) [F.HasWeightedLimFlipObj] : F.hasWeightedLimit.ι.inv.op.comp F.weightedLimFlipObj' ≅ F.weightedLimFlipObj

When HasWeightedLimFlipObj.{w} F holds, the composition of the inverse of the equivalence F.hasWeightedLimit.ι.op with weightedLimFlipObj'.{w} F identifies to weightedLimFlipObj.{w} F.

Equations

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

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.weightedLim {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] [∀ (W : Functor J (Type w)), W.HasWeightedLimObj C] : Functor (Functor J (Type w))ᵒᵖ (Functor (Functor J C) C)

When all weighted limits exists, this is the weighted limit bifunctor (J ⥤ Type w)ᵒᵖ ⥤ (J ⥤ C) ⥤ C.

Equations

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

@[simp]

theorem CategoryTheory.Limits.weightedLim_obj {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] [∀ (W : Functor J (Type w)), W.HasWeightedLimObj C] (W : (Functor J (Type w))ᵒᵖ) : weightedLim.obj W = (Opposite.unop W).weightedLimObj

@[simp]

theorem CategoryTheory.Limits.weightedLim_map_app {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] [∀ (W : Functor J (Type w)), W.HasWeightedLimObj C] {X✝ Y✝ : (Functor J (Type w))ᵒᵖ} (g : X✝ ⟶ Y✝) (F : Functor J C) : (weightedLim.map g).app F = Functor.weightedLimFlipObjMap g.unop F

noncomputable def CategoryTheory.Limits.WeightedCone.IsLimit.iso {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] : W.weightedLimObjObj F ≅ c.pt

The isomorphism weightedLimObjObj W F ≅ c.pt when c : WeightedCone W F is a limit.

Equations

• hc.iso = (CategoryTheory.Limits.limit.isLimit ((CategoryTheory.CategoryOfElements.π W).comp F)).conePointUniqueUpToIso hc

@[simp]

theorem CategoryTheory.Limits.WeightedCone.IsLimit.iso_hom_π {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] {j : J} (x : W.obj j) : CategoryStruct.comp hc.iso.hom (c.π x) = W.weightedLimObjObjπ F x

@[simp]

theorem CategoryTheory.Limits.WeightedCone.IsLimit.iso_hom_π_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) [HasWeightedLimit W F] {j : J} (x : W.obj j) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp hc.iso.hom (CategoryStruct.comp (c.π x) h) = CategoryStruct.comp (W.weightedLimObjObjπ F x) h

@[simp]

theorem CategoryTheory.Limits.WeightedCone.IsLimit.iso_inv_π {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] {j : J} (x : W.obj j) : CategoryStruct.comp hc.iso.inv (W.weightedLimObjObjπ F x) = c.π x

@[simp]

theorem CategoryTheory.Limits.WeightedCone.IsLimit.iso_inv_π_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) [HasWeightedLimit W F] {j : J} (x : W.obj j) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp hc.iso.inv (CategoryStruct.comp (W.weightedLimObjObjπ F x) h) = CategoryStruct.comp (c.π x) h

noncomputable def CategoryTheory.Limits.weightedLimObjCoyonedaObjIso {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (j : J) : (coyoneda.obj (Opposite.op j)).weightedLimObj ≅ (evaluation J C).obj j

Let j : J, the weighted limit functor with weight coyoneda.obj (op j) : J ⥤ Type _ identifies to the evaluation functor (J ⥤ C) ⥤ C at j.

Equations

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

@[simp]

theorem CategoryTheory.Limits.weightedLimObjCoyonedaObjIso_inv_app {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (j : J) (X : Functor J C) : (weightedLimObjCoyonedaObjIso j).inv.app X = (WeightedCone.isLimitCoyoneda X j).iso.inv

@[simp]

theorem CategoryTheory.Limits.weightedLimObjCoyonedaObjIso_hom_app {J : Type u} [Category.{v, u} J] {C : Type u'} [Category.{v', u'} C] (j : J) (X : Functor J C) : (weightedLimObjCoyonedaObjIso j).hom.app X = (WeightedCone.isLimitCoyoneda X j).iso.hom