Loogle!

Result

Found 91 declarations mentioning CategoryTheory.Limits.HasFiniteColimits.

CategoryTheory.Limits.HasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
(C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
CategoryTheory.Limits.hasFiniteColimits_of_hasColimits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{v', u', v, u} C] : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{0, 0, v, u} C] : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteWidePushouts C
CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] (J : Type w) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasColimitsOfShape J C
CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_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.HasColimitsOfShape J C) : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.Limits.HasFiniteColimits.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.HasColimitsOfShape J C) : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.Limits.HasFiniteColimits.out 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasFiniteColimits C] (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasColimitsOfShape J C
CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteCoproducts C
CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms 📋 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.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.ReflectsFiniteColimits F
CategoryTheory.IsFiltered.of_hasFiniteColimits 📋 Mathlib.CategoryTheory.Filtered.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.IsFiltered 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
ModuleCat.instHasFiniteColimits 📋 Mathlib.Algebra.Category.ModuleCat.Colimits
(R : Type w) [Ring R] : CategoryTheory.Limits.HasFiniteColimits (ModuleCat R)
CategoryTheory.Limits.hasFiniteColimits_of_hasColimits_of_createsFiniteColimits 📋 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.HasFiniteColimits D] [CategoryTheory.Limits.CreatesFiniteColimits F] : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.Limits.preservesFiniteColimits_of_createsFiniteColimits_and_hasFiniteColimits 📋 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.CreatesFiniteColimits F] [CategoryTheory.Limits.HasFiniteColimits D] : CategoryTheory.Limits.PreservesFiniteColimits F
CategoryTheory.Arrow.hasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Comma
{T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasFiniteColimits T] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Arrow T)
CategoryTheory.CostructuredArrow.hasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Comma
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasFiniteColimits A] [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.CostructuredArrow G X)
CategoryTheory.Comma.hasFiniteColimits 📋 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.HasFiniteColimits A] [CategoryTheory.Limits.HasFiniteColimits B] [CategoryTheory.Limits.PreservesFiniteColimits L] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Comma L R)
CategoryTheory.Over.instHasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Over X)
CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.Limits.hasFiniteColimits_of_hasInitial_and_pushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] : CategoryTheory.Limits.HasFiniteColimits C
FGModuleCat.instHasFiniteColimits 📋 Mathlib.Algebra.Category.FGModuleCat.Colimits
{k : Type u} [Ring k] : CategoryTheory.Limits.HasFiniteColimits (FGModuleCat k)
CategoryTheory.Abelian.hasFiniteColimits 📋 Mathlib.CategoryTheory.Abelian.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.ShortComplex.hasFiniteColimits 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
{C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.ShortComplex C)
CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₁ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
{C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₁
CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₂ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
{C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₂
CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₃ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
{C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₃
CategoryTheory.Limits.instHasFiniteColimitsFunctor 📋 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.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Functor K C)
CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits 📋 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.HasFiniteColimits C] (k : K) : CategoryTheory.Limits.PreservesFiniteColimits ((CategoryTheory.evaluation K C).obj k)
CategoryTheory.Limits.has_colimits_of_finite_and_filtered 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C
CategoryTheory.instPreservesFiniteColimitsFunctorObjWhiskeringLeftOfHasFiniteColimits 📋 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.HasFiniteColimits E] : CategoryTheory.Limits.PreservesFiniteColimits ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)
CategoryTheory.Limits.hasFiniteColimits_of_hasCountableColimits 📋 Mathlib.CategoryTheory.Limits.Shapes.Countable
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableColimits C] : CategoryTheory.Limits.HasFiniteColimits C
CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasCountableProducts C] [CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4Star C
CategoryTheory.AB4Star.of_AB5Star 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C] [CategoryTheory.AB5StarOfSize.{w, w, v, u} C] : CategoryTheory.AB4StarOfSize.{w, v, u} C
CategoryTheory.CountableAB4Star.of_countableAB5Star 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] [CategoryTheory.HasExactLimitsOfShape ℕᵒᵖ C] [CategoryTheory.Limits.HasCountableProducts C] : CategoryTheory.CountableAB4Star C
CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCountableProducts C] [CategoryTheory.Limits.HasFiniteColimits C] [∀ (J : Type) [inst : Finite J], CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete ℕ) C] : CategoryTheory.CountableAB4Star C
CategoryTheory.hasExactLimitsOfShape_of_initial 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits 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.Initial] [CategoryTheory.Limits.HasLimitsOfShape J' C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C] : CategoryTheory.HasExactLimitsOfShape J' C
CategoryTheory.HasExactLimitsOfShape.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_1} D] [CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.HasExactLimitsOfShape J D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.ReflectsFiniteColimits F] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesLimitsOfShape J F] : CategoryTheory.HasExactLimitsOfShape J C
CategoryTheory.Adjunction.hasExactLimitsOfShape 📋 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) [F.Full] [F.Faithful] (J : Type u') [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.HasExactLimitsOfShape J D] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.HasExactLimitsOfShape J C
CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] (J : Type u_1) [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete J))ᵒᵖ C] [CategoryTheory.HasExactLimitsOfShape (Finset (CategoryTheory.Discrete J))ᵒᵖ C] : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C
CategoryTheory.preservesFiniteColimits_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.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α)
CategoryTheory.CostructuredArrow.projectQuotient 📋 Mathlib.CategoryTheory.Subobject.Comma
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T} : CategoryTheory.Subobject (Opposite.op A) → CategoryTheory.Subobject (Opposite.op A.left)
CategoryTheory.CostructuredArrow.well_copowered_costructuredArrow 📋 Mathlib.CategoryTheory.Subobject.Comma
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} Cᵒᵖ] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] : CategoryTheory.WellPowered.{w, v₁, max u₁ v₂} (CategoryTheory.CostructuredArrow S T)ᵒᵖ
CategoryTheory.CostructuredArrow.projectQuotient_mk 📋 Mathlib.CategoryTheory.Subobject.Comma
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T} {P : (CategoryTheory.CostructuredArrow S T)ᵒᵖ} (f : P ⟶ Opposite.op A) [CategoryTheory.Mono f] : CategoryTheory.CostructuredArrow.projectQuotient (CategoryTheory.Subobject.mk f) = CategoryTheory.Subobject.mk f.unop.left.op
CategoryTheory.CostructuredArrow.lift_projectQuotient 📋 Mathlib.CategoryTheory.Subobject.Comma
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T} (P : CategoryTheory.Subobject (Opposite.op A)) {q : S.obj (Opposite.unop (CategoryTheory.Subobject.underlying.obj (CategoryTheory.CostructuredArrow.projectQuotient P))) ⟶ T} (hq : CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q = A.hom) : CategoryTheory.CostructuredArrow.liftQuotient (CategoryTheory.CostructuredArrow.projectQuotient P) hq = P
CategoryTheory.CostructuredArrow.projectQuotient_factors 📋 Mathlib.CategoryTheory.Subobject.Comma
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T} (P : CategoryTheory.Subobject (Opposite.op A)) : ∃ q, CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q = A.hom
CategoryTheory.CostructuredArrow.quotientEquiv 📋 Mathlib.CategoryTheory.Subobject.Comma
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] (A : CategoryTheory.CostructuredArrow S T) : CategoryTheory.Subobject (Opposite.op A) ≃o { P // ∃ q, CategoryTheory.CategoryStruct.comp (S.map P.arrow.unop) q = A.hom }
HomologicalComplex.instHasFiniteColimits 📋 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.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteColimits (HomologicalComplex C c)
HomologicalComplex.instPreservesFiniteColimitsEvalOfHasFiniteColimits 📋 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.HasFiniteColimits C] (n : ι) : CategoryTheory.Limits.PreservesFiniteColimits (HomologicalComplex.eval C c n)
HomologicalComplex.instEpiFOfHasFiniteColimits 📋 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.HasFiniteColimits C] {K L : HomologicalComplex C c} (φ : K ⟶ L) [CategoryTheory.Epi φ] (n : ι) : CategoryTheory.Epi (φ.f n)
CategoryTheory.instPreservesFiniteColimitsHomologicalComplexMapHomologicalComplexOfHasFiniteColimits 📋 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.HasFiniteColimits C] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteColimits (F.mapHomologicalComplex c)
PresheafOfModules.Finite.hasFiniteColimits 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.Limits.HasFiniteColimits (PresheafOfModules R)
CategoryTheory.Sheaf.instHasFiniteColimits 📋 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.HasWeakSheafify J D] [CategoryTheory.Limits.HasFiniteColimits D] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Sheaf J D)
CategoryTheory.coflat_of_preservesFiniteColimits 📋 Mathlib.CategoryTheory.Functor.Flat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteColimits C] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.RepresentablyCoflat F
CategoryTheory.preservesFiniteColimits_iff_coflat 📋 Mathlib.CategoryTheory.Functor.Flat
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteColimits C] (F : CategoryTheory.Functor C D) : CategoryTheory.RepresentablyCoflat F ↔ CategoryTheory.Limits.PreservesFiniteColimits F
CategoryTheory.Limits.CompleteLattice.hasFiniteColimits_of_semilatticeSup_orderBot 📋 Mathlib.CategoryTheory.Limits.Lattice
{α : Type u} [SemilatticeSup α] [OrderBot α] : CategoryTheory.Limits.HasFiniteColimits α
CategoryTheory.Under.instHasFiniteColimitsOfHasFiniteWidePushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasFiniteWidePushouts C] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Under B)
CategoryTheory.MorphismProperty.Under.instHasFiniteColimitsTopOfHasFiniteWidePushouts 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.ContainsIdentities] [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] [CategoryTheory.Limits.HasFiniteWidePushouts T] : CategoryTheory.Limits.HasFiniteColimits (P.Under ⊤ X)
CochainComplex.Plus.instHasFiniteColimits 📋 Mathlib.Algebra.Homology.CochainComplexPlus
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteColimits (CochainComplex.Plus C)
HomotopicalAlgebra.ModelCategory.cm1b 📋 Mathlib.AlgebraicTopology.ModelCategory.Basic
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C] : CategoryTheory.Limits.HasFiniteColimits 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
CategoryTheory.instHasExactLimitsOfShapeFunctorOfHasFiniteColimits 📋 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.HasLimitsOfShape J A] [CategoryTheory.HasExactLimitsOfShape J A] [CategoryTheory.Limits.HasFiniteColimits A] : CategoryTheory.HasExactLimitsOfShape J (CategoryTheory.Functor C A)
CategoryTheory.Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf 📋 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.HasFiniteColimits A] [CategoryTheory.Limits.HasLimitsOfShape K A] [CategoryTheory.HasExactLimitsOfShape K A] [CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.sheafToPresheaf J A)] : CategoryTheory.HasExactLimitsOfShape K (CategoryTheory.Sheaf J A)
CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Presheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) [CategoryTheory.Limits.PreservesFiniteLimits A] : CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
CategoryTheory.Limits.preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda 📋 Mathlib.CategoryTheory.Limits.Preserves.Presheaf
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] : CategoryTheory.Limits.PreservesFiniteLimits A
CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_iff_nonempty_preservesFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Presheaf
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) : CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) ↔ CategoryTheory.Limits.PreservesFiniteLimits A
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Presheaf
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] : A.obj (CategoryTheory.Limits.limit K) ≅ CategoryTheory.Limits.limit (K.comp A)
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isIso_post 📋 Mathlib.CategoryTheory.Limits.Preserves.Presheaf
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.post K A)
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Presheaf
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] : (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso A K).hom = CategoryTheory.Limits.limit.post K A
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux 📋 Mathlib.CategoryTheory.Limits.Preserves.Presheaf
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) : (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A).comp (CategoryTheory.yoneda.comp ((CategoryTheory.evaluation Cᵒᵖ (Type u)).obj (CategoryTheory.Limits.limit K))) ≅ (CategoryTheory.coyoneda.comp ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) C (Type u)).obj (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A))).obj (CategoryTheory.Limits.limit K)
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Presheaf
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) : (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux A K).hom.app = fun X => CategoryTheory.CategoryStruct.id (Opposite.unop (CategoryTheory.Limits.limit K) ⟶ X.left)
CategoryTheory.Limits.isIndObject_iff_preservesFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Indization.IndObject
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) : CategoryTheory.Limits.IsIndObject A ↔ CategoryTheory.Limits.PreservesFiniteLimits A
CategoryTheory.instHasColimitsIndOfHasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Indization.Category
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasColimits (CategoryTheory.Ind C)
CategoryTheory.Ind.leftExactFunctorEquivalence 📋 Mathlib.CategoryTheory.Limits.Indization.Category
(C : Type u) [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Ind C ≌ Cᵒᵖ ⥤ₗ Type u
CategoryTheory.instPreadditiveInd 📋 Mathlib.CategoryTheory.Preadditive.Indization
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Preadditive (CategoryTheory.Ind C)
CategoryTheory.instHasFiniteBiproductsInd 📋 Mathlib.CategoryTheory.Preadditive.Indization
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)
CategoryTheory.Ind.isSeparator_range_yoneda 📋 Mathlib.CategoryTheory.Generator.Indization
{C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.IsSeparator (∐ CategoryTheory.Ind.yoneda.obj)
Action.instHasFiniteColimits 📋 Mathlib.CategoryTheory.Action.Limits
{V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Limits.HasFiniteColimits V] : CategoryTheory.Limits.HasFiniteColimits (Action V G)
Action.instPreservesFiniteColimitsForgetOfHasFiniteColimits 📋 Mathlib.CategoryTheory.Action.Limits
{V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Limits.HasFiniteColimits V] : CategoryTheory.Limits.PreservesFiniteColimits (Action.forget V G)
Action.Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits 📋 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.PreservesFiniteColimits F] [CategoryTheory.Limits.HasFiniteColimits V] : CategoryTheory.Limits.PreservesFiniteColimits (F.mapAction G)
CategoryTheory.Limits.FintypeCat.hasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.FintypeCat
: CategoryTheory.Limits.HasFiniteColimits FintypeCat
CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.instHasFiniteColimitsFullSubcategory 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteLimits
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasFiniteColimits C] [P.IsClosedUnderFiniteColimits] : CategoryTheory.Limits.HasFiniteColimits P.FullSubcategory
CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.instPreservesFiniteColimitsFullSubcategoryι 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteLimits
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasFiniteColimits C] [P.IsClosedUnderFiniteColimits] : CategoryTheory.Limits.PreservesFiniteColimits P.ι
CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits 📋 Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
{A : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.FinitaryExtensive C] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteColimits A] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.sheafToPresheaf (CategoryTheory.extensiveTopology C) A)
instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology 📋 Mathlib.Condensed.Limits
{A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Limits.HasFiniteColimits A] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A] : CategoryTheory.Limits.HasFiniteColimits (Condensed A)
Condensed.hasExactLimitsOfShape 📋 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.HasLimitsOfShape J A] [CategoryTheory.HasExactLimitsOfShape J A] [CategoryTheory.Limits.HasFiniteColimits A] : CategoryTheory.HasExactLimitsOfShape 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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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