Theorems · Definition · category theory

CategoryTheory.Mon.limitCone

{J : Type w} →
  [inst : CategoryTheory.Category.{v_1, w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) →
            (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) →
              CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.Cone F

Implementation of Mon.hasLimits: a limiting cone over a functor F : J ⥤ Mon C.

Defined in: Mathlib.CategoryTheory.Monoidal.Internal.Limits
Cited by: 5 results in Mathlib
Foundations: Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Category CategoryTheory.MonoidalCategory

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functorstatement and proof · cited by 16,252
CategoryTheory.NatTrans.appproof · cited by 7,406
CategoryTheory.Functor.compstatement and proof · cited by 6,529
CategoryTheory.MonoidalCategorystatement and proof · cited by 3,095
CategoryTheory.Limits.Conestatement and proof · cited by 710
CategoryTheory.Limits.IsLimitstatement and proof · cited by 664
CategoryTheory.Limits.Cone.πproof · cited by 500
CategoryTheory.Monstatement and proof · cited by 465
CategoryTheory.Mon.forgetstatement and proof · cited by 33
CategoryTheory.Mon.Hom.mk'proof · cited by 10
CategoryTheory.Mon.limitproof · cited by 5

Cited by8

Results whose statement or proof uses this declaration.

CategoryTheory.Mon.forgetMapConeLimitConeIsostatement and proof · cited by 2
CategoryTheory.Mon.limitConeIsLimitstatement · cited by 1
CategoryTheory.Mon.forgetMapConeLimitConeIso_hom_homstatement · cited by 0
CategoryTheory.Mon.forgetMapConeLimitConeIso_inv_homstatement · cited by 0
CategoryTheory.Mon.limitConeIsLimit_lift_homstatement · cited by 0
CategoryTheory.Mon.limitConeLiftsToLimitproof · cited by 0
CategoryTheory.Mon.limitCone_ptstatement and proof · cited by 0
CategoryTheory.Mon.limitCone_π_app_homstatement and proof · cited by 0