Loogle!

Result

Found 111 declarations mentioning CategoryTheory.Limits.HasFiniteLimits.

• CategoryTheory.Limits.HasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
• CategoryTheory.Limits.hasFiniteLimits_of_hasLimits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfSize.{v', u', v, u} C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize₀ 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfSize.{0, 0, v, u} C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteWidePullbacks C
• CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  (C : Type u) [CategoryTheory.Category.{v, u} C] (h : ∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J} (x : CategoryTheory.FinCategory J), CategoryTheory.Limits.HasLimitsOfShape J C) : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] (J : Type w) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasLimitsOfShape J C
• CategoryTheory.Limits.HasFiniteLimits.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  {C : Type u} [CategoryTheory.Category.{v, u} C] (out : ∀ (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J], CategoryTheory.Limits.HasLimitsOfShape J C) : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Limits.HasFiniteLimits.out 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasFiniteLimits C] (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasLimitsOfShape J C
• CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteProducts C
• CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.ReflectsFiniteLimits F
• CategoryTheory.IsCofiltered.of_hasFiniteLimits 📋 Mathlib.CategoryTheory.Filtered.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.IsCofiltered C
• CategoryTheory.Limits.hasFiniteColimits_opposite 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteColimits Cᵒᵖ
• CategoryTheory.Limits.hasFiniteLimits_opposite 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteLimits Cᵒᵖ
• CategoryTheory.Limits.hasFiniteColimits_opposite_iff 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.HasFiniteColimits Cᵒᵖ ↔ CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Limits.hasFiniteLimits_opposite_iff 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.HasFiniteLimits Cᵒᵖ ↔ CategoryTheory.Limits.HasFiniteColimits C
• CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.CreatesFiniteLimits F] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Limits.preservesFiniteLimits_of_createsFiniteLimits_and_hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.CreatesFiniteLimits F] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Limits.PreservesFiniteLimits F
• CategoryTheory.Arrow.hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Comma
  {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasFiniteLimits T] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Arrow T)
• CategoryTheory.StructuredArrow.hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Comma
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.Limits.PreservesFiniteLimits G] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.StructuredArrow X G)
• CategoryTheory.Comma.hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Comma
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.Limits.HasFiniteLimits B] [CategoryTheory.Limits.PreservesFiniteLimits R] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Comma L R)
• CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Limits.HasFiniteLimits C
• FGModuleCat.instHasFiniteLimits 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {k : Type u} [Ring k] [IsNoetherianRing k] : CategoryTheory.Limits.HasFiniteLimits (FGModuleCat k)
• CategoryTheory.Abelian.hasFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.ShortComplex.hasFiniteLimits 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.ShortComplex C)
• CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₁ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₁
• CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₂ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₂
• CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₃ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₃
• CategoryTheory.MonoOver.hasFiniteLimits 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) [CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Over X)] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.MonoOver X)
• CategoryTheory.Subobject.hasFiniteLimits 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Over X)] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Subobject X)
• CategoryTheory.Limits.instHasFiniteLimitsFunctor 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {K : Type u_2} [CategoryTheory.Category.{v_2, u_2} K] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Functor K C)
• CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {K : Type u_2} [CategoryTheory.Category.{v_2, u_2} K] [CategoryTheory.Limits.HasFiniteLimits C] (k : K) : CategoryTheory.Limits.PreservesFiniteLimits ((CategoryTheory.evaluation K C).obj k)
• CategoryTheory.Limits.has_limits_of_finite_and_cofiltered 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C] : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C
• CategoryTheory.instPreservesFiniteLimitsFunctorObjWhiskeringLeftOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasFiniteLimits E] : CategoryTheory.Limits.PreservesFiniteLimits ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)
• CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits 📋 Mathlib.CategoryTheory.Limits.Shapes.Countable
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableLimits C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasCountableCoproducts C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4 C
• CategoryTheory.AB4.of_AB5 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] [CategoryTheory.AB5OfSize.{w, w, v, u} C] : CategoryTheory.AB4OfSize.{w, v, u} C
• CategoryTheory.CountableAB4.of_countableAB5 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasColimitsOfShape ℕ C] [CategoryTheory.HasExactColimitsOfShape ℕ C] [CategoryTheory.Limits.HasCountableCoproducts C] : CategoryTheory.CountableAB4 C
• CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat_and_finite 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCountableCoproducts C] [CategoryTheory.Limits.HasFiniteLimits C] [∀ (J : Type) [inst : Finite J], CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4 C
• CategoryTheory.hasExactColimitsOfShape_of_final 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] {J : Type u_1} {J' : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} J'] (F : CategoryTheory.Functor J J') [F.Final] [CategoryTheory.Limits.HasColimitsOfShape J' C] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C] : CategoryTheory.HasExactColimitsOfShape J' C
• CategoryTheory.HasExactColimitsOfShape.domain_of_functor 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} (J : Type u_2) [CategoryTheory.Category.{v_1, u_2} J] [CategoryTheory.Category.{v_2, u_1} D] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.HasExactColimitsOfShape J D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.ReflectsFiniteLimits F] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesColimitsOfShape J F] : CategoryTheory.HasExactColimitsOfShape J C
• CategoryTheory.hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] (J : Type u_1) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete J)) C] [CategoryTheory.HasExactColimitsOfShape (Finset (CategoryTheory.Discrete J)) C] : CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C
• CategoryTheory.Adjunction.hasExactColimitsOfShape 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.Full] [G.Faithful] (J : Type u') [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.HasExactColimitsOfShape J C] [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.HasExactColimitsOfShape J D
• CategoryTheory.preservesFiniteLimits_liftToFinset 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α)
• CategoryTheory.AsSmall.hasFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.Transfer
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.AsSmall C)
• CategoryTheory.ShrinkHoms.hasFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.Transfer
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.LocallySmall.{w, v_1, u_1} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.ShrinkHoms.{u_1} C)
• CategoryTheory.StructuredArrow.wellPowered_structuredArrow 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits T] : CategoryTheory.WellPowered.{w, v₁, max u₁ v₂} (CategoryTheory.StructuredArrow S T)
• CategoryTheory.StructuredArrow.projectSubobject 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits T] {A : CategoryTheory.StructuredArrow S T} : CategoryTheory.Subobject A → CategoryTheory.Subobject A.right
• CategoryTheory.StructuredArrow.projectSubobject_mk 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits T] {A P : CategoryTheory.StructuredArrow S T} (f : P ⟶ A) [CategoryTheory.Mono f] : CategoryTheory.StructuredArrow.projectSubobject (CategoryTheory.Subobject.mk f) = CategoryTheory.Subobject.mk (CategoryTheory.StructuredArrow.Hom.right f)
• CategoryTheory.StructuredArrow.lift_projectSubobject 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits T] {A : CategoryTheory.StructuredArrow S T} (P : CategoryTheory.Subobject A) {q : S ⟶ T.obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.StructuredArrow.projectSubobject P))} (hq : CategoryTheory.CategoryStruct.comp q (T.map (CategoryTheory.StructuredArrow.projectSubobject P).arrow) = A.hom) : CategoryTheory.StructuredArrow.liftSubobject (CategoryTheory.StructuredArrow.projectSubobject P) hq = P
• CategoryTheory.StructuredArrow.projectSubobject_factors 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits T] {A : CategoryTheory.StructuredArrow S T} (P : CategoryTheory.Subobject A) : ∃ q, CategoryTheory.CategoryStruct.comp q (T.map (CategoryTheory.StructuredArrow.projectSubobject P).arrow) = A.hom
• CategoryTheory.StructuredArrow.subobjectEquiv 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits T] (A : CategoryTheory.StructuredArrow S T) : CategoryTheory.Subobject A ≃o { P // ∃ q, CategoryTheory.CategoryStruct.comp q (T.map P.arrow) = A.hom }
• HomologicalComplex.instHasFiniteLimits 📋 Mathlib.Algebra.Homology.HomologicalComplexLimits
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (HomologicalComplex C c)
• HomologicalComplex.instPreservesFiniteLimitsEvalOfHasFiniteLimits 📋 Mathlib.Algebra.Homology.HomologicalComplexLimits
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] (n : ι) : CategoryTheory.Limits.PreservesFiniteLimits (HomologicalComplex.eval C c n)
• HomologicalComplex.instMonoFOfHasFiniteLimits 📋 Mathlib.Algebra.Homology.HomologicalComplexLimits
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] {K L : HomologicalComplex C c} (φ : K ⟶ L) [CategoryTheory.Mono φ] (n : ι) : CategoryTheory.Mono (φ.f n)
• CategoryTheory.instPreservesFiniteLimitsHomologicalComplexMapHomologicalComplexOfHasFiniteLimits 📋 Mathlib.Algebra.Homology.HomologicalComplexAbelian
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Limits.HasFiniteLimits C] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteLimits (F.mapHomologicalComplex c)
• PresheafOfModules.hasFiniteLimits 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.Limits.HasFiniteLimits (PresheafOfModules R)
• CategoryTheory.Sheaf.instHasFiniteLimits 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Sheaf J D)
• CategoryTheory.Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.sheafToPresheaf J D)
• CategoryTheory.Limits.instPreservesFiniteLimitsFunctorColimOfPreservesColimitsOfShapeOfHasFiniteLimitsOfReflectsIsomorphismsForget 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.IsFiltered K] {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasColimitsOfShape K C] [(CategoryTheory.forget C).ReflectsIsomorphisms] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
• CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [CategoryTheory.Limits.HasFiniteLimits D] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] : CategoryTheory.HasSheafify J D
• CategoryTheory.GrothendieckTopology.preserveFiniteLimits_plusFunctor 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : CategoryTheory.Limits.PreservesFiniteLimits (J.plusFunctor D)
• CategoryTheory.GrothendieckTopology.preservesFiniteLimits_sheafification 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : CategoryTheory.Limits.PreservesFiniteLimits (J.sheafification D)
• CategoryTheory.preservesFiniteLimits_presheafToSheaf 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.plusPlusSheaf J D)
• SheafOfModules.Finite.hasFiniteLimits 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : CategoryTheory.Limits.HasFiniteLimits (SheafOfModules R)
• CategoryTheory.flat_of_preservesFiniteLimits 📋 Mathlib.CategoryTheory.Functor.Flat
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.RepresentablyFlat F
• CategoryTheory.preservesFiniteLimits_iff_flat 📋 Mathlib.CategoryTheory.Functor.Flat
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) : CategoryTheory.RepresentablyFlat F ↔ CategoryTheory.Limits.PreservesFiniteLimits F
• CategoryTheory.flat_iff_lan_flat 📋 Mathlib.CategoryTheory.Functor.Flat
  {C D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) : CategoryTheory.RepresentablyFlat F ↔ CategoryTheory.RepresentablyFlat F.op.lan
• CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits 📋 Mathlib.CategoryTheory.Functor.Flat
  {C D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) : CategoryTheory.Limits.PreservesFiniteLimits F ↔ CategoryTheory.Limits.PreservesFiniteLimits F.op.lan
• CategoryTheory.lan_preservesFiniteLimits_of_preservesFiniteLimits 📋 Mathlib.CategoryTheory.Functor.Flat
  {C D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (E : Type u₂) [CategoryTheory.Category.{u₁, u₂} E] {FE : E → E → Type u_1} {CE : E → Type u₁} [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [CategoryTheory.ConcreteCategory E FE] [CategoryTheory.Limits.HasLimits E] [CategoryTheory.Limits.HasColimits E] [CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteLimits F.op.lan
• CategoryTheory.Functor.IsDenseSubsite.hasSheafify_of_isEquivalence 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_3} [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasSheafify J A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.HasSheafify K A
• CategoryTheory.Limits.CompleteLattice.hasFiniteLimits_of_semilatticeInf_orderTop 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} [SemilatticeInf α] [OrderTop α] : CategoryTheory.Limits.HasFiniteLimits α
• CategoryTheory.Over.hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasFiniteWidePullbacks C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Over B)
• CategoryTheory.MorphismProperty.Over.hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
  {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPullbacks T] [P.IsMultiplicative] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] : CategoryTheory.Limits.HasFiniteLimits (P.Over ⊤ X)
• CategoryTheory.MorphismProperty.Over.instHasFiniteLimitsTopOfHasFiniteWidePullbacks 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
  {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPullbacks T] [P.IsMultiplicative] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] [CategoryTheory.Limits.HasFiniteWidePullbacks T] : CategoryTheory.Limits.HasFiniteLimits (P.Over ⊤ X)
• CommRingCat.Under.hasFiniteLimits 📋 Mathlib.Algebra.Category.Ring.Under.Property
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQp : RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) (hQe : RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.HasFiniteLimits ((RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).Under ⊤ R)
• CochainComplex.Plus.instHasFiniteLimits 📋 Mathlib.Algebra.Homology.CochainComplexPlus
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CochainComplex.Plus C)
• HomotopicalAlgebra.ModelCategory.cm1a 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C] : CategoryTheory.Limits.HasFiniteLimits C
• HomotopicalAlgebra.ModelCategory.mk' 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasFiniteColimits C] [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : HomotopicalAlgebra.ModelCategory C
• HomotopicalAlgebra.ModelCategory.mk 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (categoryWithFibrations : HomotopicalAlgebra.CategoryWithFibrations C := by infer_instance) (categoryWithCofibrations : HomotopicalAlgebra.CategoryWithCofibrations C := by infer_instance) (categoryWithWeakEquivalences : HomotopicalAlgebra.CategoryWithWeakEquivalences C := by infer_instance) (cm1a : CategoryTheory.Limits.HasFiniteLimits C := by infer_instance) (cm1b : CategoryTheory.Limits.HasFiniteColimits C := by infer_instance) (cm2 : (HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty := by infer_instance) (cm3a : (HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts := by infer_instance) (cm3b : (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts := by infer_instance) (cm3c : (HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts := by infer_instance) (cm4a : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p := by intros; infer_instance) (cm4b : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence p], CategoryTheory.HasLiftingProperty i p := by intros; infer_instance) (cm5a : (HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C) := by infer_instance) (cm5b : (HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C) := by infer_instance) : HomotopicalAlgebra.ModelCategory C
• HomologicalComplex.ab5OfSize 📋 Mathlib.Algebra.Homology.GrothendieckAbelian
  (C : Type u) [CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.AB5OfSize.{w', w, v, u} C] : CategoryTheory.AB5OfSize.{w', w, max t v, max (max t u) v} (HomologicalComplex C c)
• HomologicalComplex.hasExactColimitsOfShape 📋 Mathlib.Algebra.Homology.GrothendieckAbelian
  (C : Type u) [CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms C] (J : Type w) [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C] : CategoryTheory.HasExactColimitsOfShape J (HomologicalComplex C c)
• AlgebraicGeometry.instHasFiniteLimitsScheme 📋 Mathlib.AlgebraicGeometry.Limits
  : CategoryTheory.Limits.HasFiniteLimits AlgebraicGeometry.Scheme
• AlgebraicGeometry.Scheme.instHasFiniteLimitsEtale 📋 Mathlib.AlgebraicGeometry.Morphisms.Etale
  (X : AlgebraicGeometry.Scheme) : CategoryTheory.Limits.HasFiniteLimits X.Etale
• CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] : CategoryTheory.Limits.PreservesFiniteLimits Φ.presheafFiber
• CategoryTheory.GrothendieckTopology.Point.instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.HasExactColimitsOfShape Φ.fiber.Elementsᵒᵖ A
• CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] : CategoryTheory.Limits.PreservesFiniteLimits Φ.sheafFiber
• CategoryTheory.instHasExactColimitsOfShapeFunctorOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
  {A : Type u_1} {C : Type u_2} {J : Type u_3} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} J] [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.HasExactColimitsOfShape J A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.HasExactColimitsOfShape J (CategoryTheory.Functor C A)
• CategoryTheory.Sheaf.ab5ofSize 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
  {C : Type u} {A : Type u₁} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v₁, u₁} A] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.HasSheafify J A] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A] [CategoryTheory.AB5OfSize.{v₂, u₂, v₁, u₁} A] : CategoryTheory.AB5OfSize.{v₂, u₂, max u v₁, max (max (max u₁ u) v₁) v} (CategoryTheory.Sheaf J A)
• CategoryTheory.Sheaf.hasExactColimitsOfShape 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
  {C : Type u} {A : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} K] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.HasSheafify J A] [CategoryTheory.Limits.HasColimitsOfShape K A] [CategoryTheory.HasExactColimitsOfShape K A] : CategoryTheory.HasExactColimitsOfShape K (CategoryTheory.Sheaf J A)
• CategoryTheory.Sheaf.instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
  {C : Type u} {A : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} K] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.Limits.HasColimitsOfShape K A] [CategoryTheory.HasExactColimitsOfShape K A] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.sheafToPresheaf J A)] : CategoryTheory.HasExactColimitsOfShape K (CategoryTheory.Sheaf J A)
• AlgebraicGeometry.Scheme.instHasFiniteLimitsProEt 📋 Mathlib.AlgebraicGeometry.Sites.Proetale
  (S : AlgebraicGeometry.Scheme) : CategoryTheory.Limits.HasFiniteLimits S.ProEt
• CategoryTheory.Functor.isCofiltered_elements 📋 Mathlib.CategoryTheory.Functor.TypeValuedFlat
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.IsCofiltered F.Elements
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.JointlyFaithful fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.JointlyReflectMonomorphisms fun Φ => Φ.obj.sheafFiber
• CategoryTheory.instHasFiniteLimitsInd 📋 Mathlib.CategoryTheory.Limits.Indization.Category
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Ind C)
• CategoryTheory.instCreatesFiniteLimitsIndFunctorOppositeTypeInclusionOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Indization.Category
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.CreatesFiniteLimits (CategoryTheory.Ind.inclusion C)
• CategoryTheory.Limits.instAB5IndOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.AB5 (CategoryTheory.Ind C)
• CategoryTheory.Limits.instHasExactColimitsOfShapeIndOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.HasExactColimitsOfShape J (CategoryTheory.Ind C)
• Action.instHasFiniteLimits 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Limits.HasFiniteLimits V] : CategoryTheory.Limits.HasFiniteLimits (Action V G)
• Action.instPreservesFiniteLimitsForgetOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Limits.HasFiniteLimits V] : CategoryTheory.Limits.PreservesFiniteLimits (Action.forget V G)
• Action.Functor.instPreservesFiniteLimitsMapActionOfHasFiniteLimits 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3} [CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [Monoid G] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.HasFiniteLimits V] : CategoryTheory.Limits.PreservesFiniteLimits (F.mapAction G)
• CategoryTheory.Limits.FintypeCat.hasFiniteLimits 📋 Mathlib.CategoryTheory.Limits.FintypeCat
  : CategoryTheory.Limits.HasFiniteLimits FintypeCat
• CategoryTheory.PreGaloisCategory.instHasFiniteLimits 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.instHasFiniteLimitsFullSubcategory 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteLimits
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasFiniteLimits C] [P.IsClosedUnderFiniteLimits] : CategoryTheory.Limits.HasFiniteLimits P.FullSubcategory
• CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.instPreservesFiniteLimitsFullSubcategoryι 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteLimits
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasFiniteLimits C] [P.IsClosedUnderFiniteLimits] : CategoryTheory.Limits.PreservesFiniteLimits P.ι
• CategoryTheory.Regular.toHasFiniteLimits 📋 Mathlib.CategoryTheory.RegularCategory.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Regular C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Regular.mk 📋 Mathlib.CategoryTheory.RegularCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [toHasFiniteLimits : CategoryTheory.Limits.HasFiniteLimits C] (hasCoequalizer_of_isKernelPair : ∀ {X Y Z : C} {f : X ⟶ Y} {g₁ g₂ : Z ⟶ X}, CategoryTheory.IsKernelPair f g₁ g₂ → CategoryTheory.Limits.HasCoequalizer g₁ g₂) (regularEpiIsStableUnderBaseChange : (CategoryTheory.MorphismProperty.regularEpi C).IsStableUnderBaseChange) : CategoryTheory.Regular C
• instHasFiniteLimitsCondensed 📋 Mathlib.Condensed.Limits
  {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.Limits.HasFiniteLimits (Condensed A)
• Condensed.hasExactColimitsOfShape 📋 Mathlib.Condensed.AB
  (A : Type u_1) (J : Type u_2) [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Preadditive A] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A] [CategoryTheory.HasWeakSheafify (CategoryTheory.extensiveTopology Stonean) A] [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.HasExactColimitsOfShape J A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.HasExactColimitsOfShape J (Condensed A)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c