Loogle!

Result

Found 305 declarations mentioning CategoryTheory.Functor.sections. Of these, only the first 200 are shown.

• CategoryTheory.Functor.sections 📋 Mathlib.CategoryTheory.Types.Basic
  {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w)) : Set ((j : J) → F.obj j)
• CategoryTheory.Functor.sectionsFunctor_obj 📋 Mathlib.CategoryTheory.Types.Basic
  (J : Type u) [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w)) : (CategoryTheory.Functor.sectionsFunctor J).obj F = ↑F.sections
• CategoryTheory.Functor.sections_ext_iff 📋 Mathlib.CategoryTheory.Types.Basic
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} {x y : ↑F.sections} : x = y ↔ ∀ (j : J), ↑x j = ↑y j
• CategoryTheory.Functor.sections_property 📋 Mathlib.CategoryTheory.Types.Basic
  {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} (s : ↑F.sections) {j j' : J} (f : j ⟶ j') : (CategoryTheory.ConcreteCategory.hom (F.map f)) (↑s j) = ↑s j'
• CategoryTheory.Functor.sectionsFunctor_map 📋 Mathlib.CategoryTheory.Types.Basic
  (J : Type u) [CategoryTheory.Category.{v, u} J] {F G : CategoryTheory.Functor J (Type w)} (φ : F ⟶ G) : (CategoryTheory.Functor.sectionsFunctor J).map φ = TypeCat.ofHom fun x => ⟨fun j => (CategoryTheory.ConcreteCategory.hom (φ.app j)) (↑x j), ⋯⟩
• CategoryTheory.Functor.sectionsEquivHom 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type u₂)) (X : Type u₂) [Unique X] : ↑F.sections ≃ ((CategoryTheory.Functor.const C).obj X ⟶ F)
• CategoryTheory.Functor.sectionsEquivHom_apply_app 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type u₂)) (X : Type u₂) [Unique X] (s : ↑F.sections) (j : C) : ((F.sectionsEquivHom X) s).app j = TypeCat.ofHom fun x => ↑s j
• CategoryTheory.sectionsFunctorNatIsoCoyoneda_hom_app_hom_apply_app_hom_apply 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : CategoryTheory.Functor C (Type (max u₁ u₂))) (x : ↑X✝.sections) (j : C) (x✝ : ((CategoryTheory.Functor.const C).obj X).obj j) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.sectionsFunctorNatIsoCoyoneda X).hom.app X✝)) x).app j)) x✝ = ↑x j
• CategoryTheory.sectionsFunctorNatIsoCoyoneda_inv_app_hom_apply_coe 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : CategoryTheory.Functor C (Type (max u₁ u₂))) (x : (CategoryTheory.Functor.const C).obj X ⟶ X✝) (j : C) : ↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.sectionsFunctorNatIsoCoyoneda X).inv.app X✝)) x) j = (CategoryTheory.ConcreteCategory.hom (x.app j)) default
• CategoryTheory.Functor.sectionsEquivHom_naturality 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C (Type u₂)} (f : F ⟶ G) (X : Type u₂) [Unique X] (x : ↑F.sections) : (G.sectionsEquivHom X) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.sectionsFunctor C).map f)) x) = CategoryTheory.CategoryStruct.comp ((F.sectionsEquivHom X) x) f
• CategoryTheory.Functor.sectionsEquivHom_naturality_symm 📋 Mathlib.CategoryTheory.Yoneda
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C (Type u₂)} (f : F ⟶ G) (X : Type u₂) [Unique X] (τ : (CategoryTheory.Functor.const C).obj X ⟶ F) : (G.sectionsEquivHom X).symm (CategoryTheory.CategoryStruct.comp τ f) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.sectionsFunctor C).map f)) ((F.sectionsEquivHom X).symm τ)
• CategoryTheory.Limits.Types.Small.limitCone 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.Types.hasLimit_iff_small_sections 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑F.sections
• CategoryTheory.Limits.Types.limitCone_pt 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type (max v u))) : (CategoryTheory.Limits.Types.limitCone F).pt = ↑F.sections
• CategoryTheory.Limits.Types.Small.limitConeIsLimit 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.Small.limitCone F)
• CategoryTheory.Limits.Types.sectionOfCone 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cone F) (x : c.pt) : ↑F.sections
• CategoryTheory.Limits.Types.limitEquivSections 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] : CategoryTheory.Limits.limit F ≃ ↑F.sections
• CategoryTheory.Limits.Types.isLimitEquivSections 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) : c.pt ≃ ↑F.sections
• CategoryTheory.Limits.Types.isLimit_iff_bijective_sectionOfCone 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cone F) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ Function.Bijective (CategoryTheory.Limits.Types.sectionOfCone c)
• CategoryTheory.Limits.Types.Small.limitCone_pt 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : (CategoryTheory.Limits.Types.Small.limitCone F).pt = Shrink.{u, max u v} ↑F.sections
• CategoryTheory.Limits.Types.coneOfSection 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {s : (j : J) → F.obj j} (hs : s ∈ F.sections) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.Types.limitCone_π_app 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type (max v u))) (j : J) : (CategoryTheory.Limits.Types.limitCone F).π.app j = TypeCat.ofHom fun u => ↑u j
• CategoryTheory.Limits.Types.limitEquivSections_apply 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x : CategoryTheory.Limits.limit F) (j : J) : ↑((CategoryTheory.Limits.Types.limitEquivSections F) x) j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x
• CategoryTheory.Limits.Types.limitEquivSections_symm_apply 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x : ↑F.sections) (j : J) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) ((CategoryTheory.Limits.Types.limitEquivSections F).symm x) = ↑x j
• CategoryTheory.Limits.Types.isLimit_iff 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cone F) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x = s j
• CategoryTheory.Limits.Types.limitConeIsLimit_lift 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type (max v u))) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Types.limitConeIsLimit F).lift s = TypeCat.ofHom fun v => ⟨fun j => (CategoryTheory.ConcreteCategory.hom (s.π.app j)) v, ⋯⟩
• CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) (x : ↑F.sections) (j : J) : (CategoryTheory.ConcreteCategory.hom (c.π.app j)) ((CategoryTheory.Limits.Types.isLimitEquivSections t).symm x) = ↑x j
• CategoryTheory.Limits.Types.isLimitEquivSections_apply 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) (j : J) (x : c.pt) : ↑((CategoryTheory.Limits.Types.isLimitEquivSections t) x) j = (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x
• CategoryTheory.Limits.Types.Small.limitCone_π_app 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone F).π.app j = TypeCat.ofHom fun u => ↑((equivShrink ↑F.sections).symm u) j
• CategoryTheory.Limits.Types.Small.limitCone_pt_ext 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] {x y : (CategoryTheory.Limits.Types.Small.limitCone F).pt} (w : (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y) : x = y
• CategoryTheory.Limits.Types.Small.limitCone_pt_ext_iff 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [Small.{u, max u v} ↑F.sections] {x y : (CategoryTheory.Limits.Types.Small.limitCone F).pt} : x = y ↔ (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y
• CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift 📋 Mathlib.CategoryTheory.Limits.Types.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Types.Small.limitConeIsLimit F).lift s = TypeCat.ofHom fun v => (equivShrink ↑F.sections) ⟨fun j => (CategoryTheory.ConcreteCategory.hom (s.π.app j)) v, ⋯⟩
• CategoryTheory.Limits.Types.sectionsEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Ulift
  {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (K : CategoryTheory.Functor J (Type u)) : ↑K.sections ≃ ↑(K.comp CategoryTheory.uliftFunctor.{v, u}).sections
• CategoryTheory.Limits.coneOfSectionCompCoyoneda 📋 Mathlib.CategoryTheory.Limits.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : ↑(F.comp (CategoryTheory.coyoneda.obj X)).sections) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.coneOfSectionCompCoyoneda_pt 📋 Mathlib.CategoryTheory.Limits.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : ↑(F.comp (CategoryTheory.coyoneda.obj X)).sections) : (CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s).pt = Opposite.unop X
• CategoryTheory.Limits.coneOfSectionCompYoneda 📋 Mathlib.CategoryTheory.Limits.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.coneOfSectionCompYoneda_pt 📋 Mathlib.CategoryTheory.Limits.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) : (CategoryTheory.Limits.coneOfSectionCompYoneda F X s).pt = Opposite.op X
• CategoryTheory.Limits.coneOfSectionCompCoyoneda_π_app 📋 Mathlib.CategoryTheory.Limits.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : ↑(F.comp (CategoryTheory.coyoneda.obj X)).sections) (j : J) : (CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s).π.app j = ↑s j
• CategoryTheory.Limits.coneOfSectionCompYoneda_π_app 📋 Mathlib.CategoryTheory.Limits.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) : (CategoryTheory.Limits.coneOfSectionCompYoneda F X s).π.app j = Quiver.Hom.op (↑s j)
• CategoryTheory.Limits.Concrete.small_sections_of_hasLimit 📋 Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type v)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] [(CategoryTheory.forget C).IsCorepresentable] {J : Type w} [CategoryTheory.Category.{t, w} J] (G : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit G] : Small.{v, max v w} ↑(G.comp (CategoryTheory.forget C)).sections
• AddMonCat.sectionsAddMonoid 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) : AddMonoid ↑(F.comp (CategoryTheory.forget AddMonCat)).sections
• MonCat.sectionsMonoid 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) : Monoid ↑(F.comp (CategoryTheory.forget MonCat)).sections
• AddMonCat.HasLimits.hasLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] : CategoryTheory.Limits.HasLimit F
• AddMonCat.HasLimits.limitCone 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] : CategoryTheory.Limits.Cone F
• MonCat.HasLimits.hasLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] : CategoryTheory.Limits.HasLimit F
• MonCat.HasLimits.limitCone 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] : CategoryTheory.Limits.Cone F
• AddMonCat.HasLimits.limitConeIsLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] : CategoryTheory.Limits.IsLimit (AddMonCat.HasLimits.limitCone F)
• MonCat.HasLimits.limitConeIsLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] : CategoryTheory.Limits.IsLimit (MonCat.HasLimits.limitCone F)
• AddCommMonCat.hasLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.Limits.HasLimit F
• AddCommMonCat.limitCone 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.Limits.Cone F
• CommMonCat.hasLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.Limits.HasLimit F
• CommMonCat.limitCone 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.Limits.Cone F
• AddCommMonCat.limitConeIsLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.Limits.IsLimit (AddCommMonCat.limitCone F)
• CommMonCat.limitConeIsLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.Limits.IsLimit (CommMonCat.limitCone F)
• AddCommMonCat.forget_createsLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget AddCommMonCat)
• CommMonCat.forget_createsLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget CommMonCat)
• AddMonCat.limitAddMonoid 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] : AddMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt
• MonCat.limitMonoid 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] : Monoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt
• AddCommMonCat.forget₂CreatesLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ AddCommMonCat AddMonCat)
• CommMonCat.forget₂CreatesLimit 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommMonCat MonCat)
• AddCommMonCat.limitAddCommMonoid 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : AddCommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddCommMonCat))).pt
• CommMonCat.limitCommMonoid 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : CommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommMonCat))).pt
• AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] : Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)).comp (CategoryTheory.forget AddMonCat)).sections
• CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections] : Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ CommMonCat MonCat)).comp (CategoryTheory.forget MonCat)).sections
• AddMonCat.limitπAddMonoidHom 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt →+ ↑(F.obj j)
• MonCat.limitπMonoidHom 📋 Mathlib.Algebra.Category.MonCat.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt →* ↑(F.obj j)
• AddGrpCat.sectionsAddGroup 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) : AddGroup ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections
• GrpCat.sectionsGroup 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) : Group ↑(F.comp (CategoryTheory.forget GrpCat)).sections
• AddGrpCat.hasLimit 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections] : CategoryTheory.Limits.HasLimit F
• AddGrpCat.limitCone 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections] : CategoryTheory.Limits.Cone F
• GrpCat.hasLimit 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections] : CategoryTheory.Limits.HasLimit F
• GrpCat.limitCone 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections] : CategoryTheory.Limits.Cone F
• AddGrpCat.hasLimit_iff_small_sections 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections
• GrpCat.hasLimit_iff_small_sections 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections
• AddGrpCat.limitConeIsLimit 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections] : CategoryTheory.Limits.IsLimit (AddGrpCat.limitCone F)
• GrpCat.limitConeIsLimit 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections] : CategoryTheory.Limits.IsLimit (GrpCat.limitCone F)
• AddCommGrpCat.hasLimit 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections] : CategoryTheory.Limits.HasLimit F
• AddCommGrpCat.limitCone 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections] : CategoryTheory.Limits.Cone F
• CommGrpCat.hasLimit 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] : CategoryTheory.Limits.HasLimit F
• CommGrpCat.limitCone 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] : CategoryTheory.Limits.Cone F
• AddCommGrpCat.hasLimit_iff_small_sections 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections
• CommGrpCat.hasLimit_iff_small_sections 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections
• AddCommGrpCat.limitConeIsLimit 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections] : CategoryTheory.Limits.IsLimit (AddCommGrpCat.limitCone F)
• CommGrpCat.limitConeIsLimit 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] : CategoryTheory.Limits.IsLimit (CommGrpCat.limitCone F)
• AddGrpCat.limitAddGroup 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections] : AddGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddGrpCat))).pt
• GrpCat.limitGroup 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections] : Group (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget GrpCat))).pt
• AddCommGrpCat.limitAddCommGroup 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections] : AddCommGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddCommGrpCat))).pt
• CommGrpCat.limitCommGroup 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] : CommGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommGrpCat))).pt
• AddCommGrpCat.forget₂AddCommMon_preservesLimitsAux 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat).mapCone (AddCommGrpCat.limitCone F))
• CommGrpCat.forget₂CommMon_preservesLimitsAux 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ CommGrpCat CommMonCat).mapCone (CommGrpCat.limitCone F))
• AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections] : Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)).comp (CategoryTheory.forget AddMonCat)).sections
• GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections] : Small.{u, max u v} ↑((F.comp (CategoryTheory.forget₂ GrpCat MonCat)).comp (CategoryTheory.forget MonCat)).sections
• AddGrpCat.sectionsπAddMonoidHom 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat) (j : J) : ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections →+ ↑(F.obj j)
• GrpCat.sectionsπMonoidHom 📋 Mathlib.Algebra.Category.Grp.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat) (j : J) : ↑(F.comp (CategoryTheory.forget GrpCat)).sections →* ↑(F.obj j)
• AddCommGrpCat.kernelIsoKer 📋 Mathlib.Algebra.Category.Grp.Limits
  {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.Limits.kernel f ≅ AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom f).ker
• AddCommGrpCat.kernelIsoKerOver 📋 Mathlib.Algebra.Category.Grp.Limits
  {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.Over.mk (CategoryTheory.Limits.kernel.ι f) ≅ CategoryTheory.Over.mk (AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f).ker.subtype)
• AddCommGrpCat.kernelIsoKer_inv_comp_ι 📋 Mathlib.Algebra.Category.Grp.Limits
  {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (AddCommGrpCat.kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) = AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f).ker.subtype
• AddCommGrpCat.kernelIsoKer_hom_comp_subtype 📋 Mathlib.Algebra.Category.Grp.Limits
  {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (AddCommGrpCat.kernelIsoKer f).hom (AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f).ker.subtype) = CategoryTheory.Limits.kernel.ι f
• ModuleCat.instAddCommMonoidElemForallObjCompForgetLinearMapIdCarrierSections 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) : AddCommMonoid ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections
• ModuleCat.hasLimit 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] : CategoryTheory.Limits.HasLimit F
• ModuleCat.instModuleElemForallObjCompForgetLinearMapIdCarrierSections 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) : Module R ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections
• ModuleCat.HasLimits.limitCone 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] : CategoryTheory.Limits.Cone F
• ModuleCat.HasLimits.limitConeIsLimit 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] : CategoryTheory.Limits.IsLimit (ModuleCat.HasLimits.limitCone F)
• ModuleCat.forget₂AddCommGroup_preservesLimit 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
• ModuleCat.limitAddCommGroup 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] : AddCommGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt
• ModuleCat.limitAddCommMonoid 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] : AddCommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt
• ModuleCat.limitModule 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] : Module R (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt
• ModuleCat.forget₂AddCommGroup_preservesLimitsAux 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).mapCone (ModuleCat.HasLimits.limitCone F))
• ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] : Small.{w, max v w} ↥(ModuleCat.sectionsSubmodule F)
• ModuleCat.limitπLinearMap 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (ModuleCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt →ₗ[R] (F.comp (CategoryTheory.forget (ModuleCat R))).obj j
• SemiRingCat.sectionsSemiring 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) : Semiring ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections
• SemiRingCat.hasLimit 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.HasLimit F
• SemiRingCat.HasLimits.limitCone 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.Cone F
• SemiRingCat.HasLimits.limitConeIsLimit 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.IsLimit (SemiRingCat.HasLimits.limitCone F)
• CommSemiRingCat.hasLimit 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CategoryTheory.Limits.HasLimit F
• CommSemiRingCat.limitCone 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CategoryTheory.Limits.Cone F
• RingCat.hasLimit 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.Limits.HasLimit F
• RingCat.limitCone 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.Limits.Cone F
• CommSemiRingCat.limitConeIsLimit 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CategoryTheory.Limits.IsLimit (CommSemiRingCat.limitCone F)
• RingCat.limitConeIsLimit 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.Limits.IsLimit (RingCat.limitCone F)
• CommRingCat.hasLimit 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.Limits.HasLimit F
• CommRingCat.limitCone 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.Limits.Cone F
• CommRingCat.limitConeIsLimit 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.Limits.IsLimit (CommRingCat.limitCone F)
• SemiRingCat.limitSemiring 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : Semiring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget SemiRingCat))).pt
• CommSemiRingCat.instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)
• RingCat.instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ RingCat SemiRingCat)
• CommSemiRingCat.limitCommSemiring 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] : CommSemiring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommSemiRingCat))).pt
• RingCat.limitRing 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : Ring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget RingCat))).pt
• CommRingCat.instCreatesLimitRingCatForget₂RingHomCarrierCarrier 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommRingCat RingCat)
• CommRingCat.limitCommRing 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CommRing (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommRingCat))).pt
• SemiRingCat.forget₂MonPreservesLimitsAux 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ SemiRingCat MonCat).mapCone (SemiRingCat.HasLimits.limitCone F))
• SemiRingCat.forget₂AddCommMonPreservesLimitsAux 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).mapCone (SemiRingCat.HasLimits.limitCone F))
• CommRingCat.forget₂CommSemiRingPreservesLimitsAux 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ CommRingCat CommSemiRingCat).mapCone (CommRingCat.limitCone F))
• SemiRingCat.limitπRingHom 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget SemiRingCat))).pt →+* (F.comp (CategoryTheory.forget SemiRingCat)).obj j
• RingCat.forget₂AddCommGroupPreservesLimitsAux 📋 Mathlib.Algebra.Category.Ring.Limits
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J RingCat) [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ RingCat AddCommGrpCat).mapCone (RingCat.limitCone F))
• AlgCat.instRingElemForallObjCompForgetAlgHomCarrierSections 📋 Mathlib.Algebra.Category.AlgCat.Limits
  {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) : Ring ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections
• AlgCat.HasLimits.limitCone 📋 Mathlib.Algebra.Category.AlgCat.Limits
  {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] : CategoryTheory.Limits.Cone F
• AlgCat.HasLimits.limitConeIsLimit 📋 Mathlib.Algebra.Category.AlgCat.Limits
  {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] : CategoryTheory.Limits.IsLimit (AlgCat.HasLimits.limitCone F)
• AlgCat.limitSemiring 📋 Mathlib.Algebra.Category.AlgCat.Limits
  {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] : Ring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (AlgCat R)))).pt
• AlgCat.instAlgebraElemForallObjCompForgetAlgHomCarrierSections 📋 Mathlib.Algebra.Category.AlgCat.Limits
  {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) : Algebra R ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections
• AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra 📋 Mathlib.Algebra.Category.AlgCat.Limits
  {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] : Small.{w, max v w} ↥(AlgCat.sectionsSubalgebra F)
• AlgCat.limitAlgebra 📋 Mathlib.Algebra.Category.AlgCat.Limits
  {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] : Algebra R (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (AlgCat R)))).pt
• AlgCat.limitπAlgHom 📋 Mathlib.Algebra.Category.AlgCat.Limits
  {R : Type u} [CommRing R] {J : Type v} [CategoryTheory.Category.{t, v} J] (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] (j : J) : (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (AlgCat R)))).pt →ₐ[R] (F.comp (CategoryTheory.forget (AlgCat R))).obj j
• ModuleCat.preservesLimit_restrictScalars 📋 Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
  {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {J : Type u_3} [CategoryTheory.Category.{v_1, u_3} J] (F : CategoryTheory.Functor J (ModuleCat S)) [Small.{v, max u_3 v} ↑(F.comp (CategoryTheory.forget (ModuleCat S))).sections] : CategoryTheory.Limits.PreservesLimit F (ModuleCat.restrictScalars f)
• CommRingCat.piIsoPi 📋 Mathlib.Algebra.Category.Ring.Constructions
  {ι : Type u} (R : ι → CommRingCat) : ∏ᶜ R ≅ CommRingCat.of ((i : ι) → ↑(R i))
• CommRingCat.equalizer_limit_isLocalRing 📋 Mathlib.Algebra.Category.Ring.Constructions
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CommRingCat) [IsLocalRing ↑(F.obj CategoryTheory.Limits.WalkingParallelPair.zero)] : IsLocalRing ↑(CategoryTheory.Limits.limit F)
• CommRingCat.pullback_isLocalRing 📋 Mathlib.Algebra.Category.Ring.Constructions
  {A B C : CommRingCat} (f : A ⟶ C) (g : B ⟶ C) [IsLocalHom (CommRingCat.Hom.hom g)] [IsLocalRing ↑A] : IsLocalRing ↑(CategoryTheory.Limits.pullback f g)
• RingEquiv.piEquivPi 📋 Mathlib.Algebra.Category.Ring.Constructions
  {ι : Type u} (R : ι → Type u) [(i : ι) → CommRing (R i)] : ↑(∏ᶜ fun i => CommRingCat.of (R i)) ≃+* ((i : ι) → R i)
• CommRingCat.equalizer_ι_isLocalHom 📋 Mathlib.Algebra.Category.Ring.Constructions
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CommRingCat) : IsLocalHom (CommRingCat.Hom.hom (CategoryTheory.Limits.limit.π F CategoryTheory.Limits.WalkingParallelPair.zero))
• CommRingCat.equalizer_ι_isLocalHom' 📋 Mathlib.Algebra.Category.Ring.Constructions
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPairᵒᵖ CommRingCat) : IsLocalHom (CommRingCat.Hom.hom (CategoryTheory.Limits.limit.π F (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one)))
• CommRingCat.pullbackFst_isLocalHom 📋 Mathlib.Algebra.Category.Ring.Constructions
  {A B C : CommRingCat} (f : A ⟶ C) (g : B ⟶ C) [IsLocalHom (CommRingCat.Hom.hom g)] : IsLocalHom (CommRingCat.Hom.hom (CategoryTheory.Limits.pullback.fst f g))
• FGModuleCat.instFiniteCarrierPiObjModuleCatOfFinite 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {k : Type u} [Ring k] {J : Type} [Finite J] (Z : J → ModuleCat k) [∀ (j : J), Module.Finite k ↑(Z j)] : Module.Finite k ↑(∏ᶜ fun j => Z j)
• FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] [IsNoetherianRing k] (F : CategoryTheory.Functor J (FGModuleCat k)) : Module.Finite k ↑(CategoryTheory.Limits.limit (F.comp (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))))
• CategoryTheory.Limits.compCoyonedaSectionsEquiv 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C) (X : C) : ↑(F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).sections ≃ ((CategoryTheory.Functor.const J).obj X ⟶ F)
• CategoryTheory.Limits.opCompYonedaSectionsEquiv 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C) (X : C) : ↑(F.op.comp (CategoryTheory.yoneda.obj X)).sections ≃ (F ⟶ (CategoryTheory.Functor.const J).obj X)
• CategoryTheory.Limits.compYonedaSectionsEquiv 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections ≃ ((CategoryTheory.Functor.const J).obj (Opposite.op X) ⟶ F)
• CategoryTheory.Limits.compCoyonedaSectionsEquiv_apply_app 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (s : ↑(F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).sections) (j : J) : ((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X) s).app j = ↑s j
• CategoryTheory.Limits.compCoyonedaSectionsEquiv_symm_apply_coe 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (τ : (CategoryTheory.Functor.const J).obj X ⟶ F) (X✝ : J) : ↑((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X).symm τ) X✝ = τ.app X✝
• CategoryTheory.Limits.compYonedaSectionsEquiv_apply_app 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) : ((CategoryTheory.Limits.compYonedaSectionsEquiv F X) s).app j = Quiver.Hom.op (↑s j)
• CategoryTheory.Limits.opCompYonedaSectionsEquiv_apply_app 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (s : ↑(F.op.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) : ((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X) s).app j = ↑s (Opposite.op j)
• CategoryTheory.Limits.opCompYonedaSectionsEquiv_symm_apply_coe 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (τ : F ⟶ (CategoryTheory.Functor.const J).obj X) (j : Jᵒᵖ) : ↑((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X).symm τ) j = τ.app (Opposite.unop j)
• CategoryTheory.Limits.compYonedaSectionsEquiv_symm_apply_coe 📋 Mathlib.CategoryTheory.Limits.Types.Yoneda
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (τ : (CategoryTheory.Functor.const J).obj (Opposite.op X) ⟶ F) (j : J) : ↑((CategoryTheory.Limits.compYonedaSectionsEquiv F X).symm τ) j = (τ.app j).unop
• CategoryTheory.Limits.Concrete.multiequalizerEquivAux 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) : ↑(I.multicospan.comp (CategoryTheory.forget C)).sections ≃ { x // ∀ (i : J.R), (CategoryTheory.ConcreteCategory.hom (I.fst i)) (x (J.fst i)) = (CategoryTheory.ConcreteCategory.hom (I.snd i)) (x (J.snd i)) }
• PresheafOfModules.sections_ext 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s t : M.sections) (h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X) : s = t
• PresheafOfModules.sections_ext_iff 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {s t : M.sections} : s = t ↔ ∀ (X : Cᵒᵖ), ↑s X = ↑t X
• PresheafOfModules.unitHomEquiv_apply_coe 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (f : PresheafOfModules.unit R ⟶ M) (X : Cᵒᵖ) : ↑(M.unitHomEquiv f) X = (CategoryTheory.ConcreteCategory.hom (f.app X)) 1
• PresheafOfModules.sectionsMap_coe 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M N : PresheafOfModules R} (f : M ⟶ N) (s : M.sections) (X : Cᵒᵖ) : ↑(PresheafOfModules.sectionsMap f s) X = (CategoryTheory.ConcreteCategory.hom (f.app X)) (↑s X)
• PresheafOfModules.sectionsMk_coe 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : (X : Cᵒᵖ) → ↑(M.obj X)) (hs : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), (CategoryTheory.ConcreteCategory.hom (M.map f)) (s X) = s Y) (X : Cᵒᵖ) : ↑(PresheafOfModules.sectionsMk s hs) X = s X
• PresheafOfModules.sections_property 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : M.sections) {X Y : Cᵒᵖ} (f : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (M.map f)) (↑s X) = ↑s Y
• PresheafOfModules.limitPresheafOfModules 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : PresheafOfModules R
• PresheafOfModules.hasLimit 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.HasLimit F
• PresheafOfModules.limitCone 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.Cone F
• PresheafOfModules.isLimitLimitCone 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.IsLimit (PresheafOfModules.limitCone F)
• PresheafOfModules.toPresheaf_preservesLimit 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : CategoryTheory.Limits.PreservesLimit F (PresheafOfModules.toPresheaf R)
• PresheafOfModules.limitCone_pt 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] : (PresheafOfModules.limitCone F).pt = PresheafOfModules.limitPresheafOfModules F
• PresheafOfModules.evaluation_preservesLimit 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimit F (PresheafOfModules.evaluation R X)
• PresheafOfModules.limitPresheafOfModules_obj 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (X : Cᵒᵖ) : (PresheafOfModules.limitPresheafOfModules F).obj X = CategoryTheory.Limits.limit (F.comp (PresheafOfModules.evaluation R X))
• PresheafOfModules.evaluationJointlyReflectsLimits 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (c : CategoryTheory.Limits.Cone F) (hc : (X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((PresheafOfModules.evaluation R X).mapCone c)) : CategoryTheory.Limits.IsLimit c
• PresheafOfModules.instHasLimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.Limits.HasLimit (F.comp ((PresheafOfModules.evaluation R Y).comp (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))))
• PresheafOfModules.limitCone_π_app_app 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] (j : J) (X : Cᵒᵖ) : ((PresheafOfModules.limitCone F).π.app j).app X = CategoryTheory.Limits.limit.π (F.comp (PresheafOfModules.evaluation R X)) j
• PresheafOfModules.limitPresheafOfModules_map 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] {x✝ Y : Cᵒᵖ} (f : x✝ ⟶ Y) : (PresheafOfModules.limitPresheafOfModules F).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap (F.whiskerLeft (PresheafOfModules.restriction R f))) (CategoryTheory.preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F.comp (PresheafOfModules.evaluation R Y))).inv
• PresheafOfModules.toFreeYonedaCoproduct 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
  {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : (CategoryTheory.Limits.kernel M.fromFreeYonedaCoproduct).freeYonedaCoproduct ⟶ M.freeYonedaCoproduct
• PresheafOfModules.freeYonedaCoproductsCokernelCofork 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
  {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : CategoryTheory.Limits.CokernelCofork M.toFreeYonedaCoproduct
• PresheafOfModules.isColimitFreeYonedaCoproductsCokernelCofork 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
  {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : CategoryTheory.Limits.IsColimit M.freeYonedaCoproductsCokernelCofork
• PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
  {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : CategoryTheory.CategoryStruct.comp M.toFreeYonedaCoproduct M.fromFreeYonedaCoproduct = 0
• PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
  {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {Z : PresheafOfModules R} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp M.toFreeYonedaCoproduct (CategoryTheory.CategoryStruct.comp M.fromFreeYonedaCoproduct h) = CategoryTheory.CategoryStruct.comp 0 h
• TopCat.hasLimit_iff_small_sections 📋 Mathlib.Topology.Category.TopCat.Limits.Basic
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget TopCat)).sections
• SheafOfModules.unitHomEquiv_apply_coe 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) (f : SheafOfModules.unit R ⟶ M) (X : Cᵒᵖ) : ↑(M.unitHomEquiv f) X = (CategoryTheory.ConcreteCategory.hom (f.val.app X)) 1
• SheafOfModules.forgetToSheafModuleCatOfIso 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X Y : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (hY : CategoryTheory.Limits.IsInitial Y) (φ : X ≅ Y) : SheafOfModules.forgetToSheafModuleCat R X hX ≅ (SheafOfModules.forgetToSheafModuleCat R Y hY).comp (CategoryTheory.sheafCompose J (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map φ.hom))))
• PresheafOfModules.isSheaf_of_isLimit 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {F : CategoryTheory.Functor D (PresheafOfModules R)} [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] {c : CategoryTheory.Limits.Cone F} [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] (hc : CategoryTheory.Limits.IsLimit c) (hF : ∀ (j : D), CategoryTheory.Presheaf.IsSheaf J (F.obj j).presheaf) : CategoryTheory.Presheaf.IsSheaf J c.pt.presheaf
• SheafOfModules.hasLimit 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections] [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] : CategoryTheory.Limits.HasLimit F
• SheafOfModules.createsLimit 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections] [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] : CategoryTheory.CreatesLimit F (SheafOfModules.forget R)
• SheafOfModules.evaluationPreservesLimit 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections] [CategoryTheory.Limits.HasLimitsOfShape D AddCommGrpCat] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimit F (SheafOfModules.evaluation R X)
• SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Sheaf J RingCat} (F : CategoryTheory.Functor D (SheafOfModules R)) [∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F.comp (SheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections] (X : Cᵒᵖ) : Small.{v, max u₂ v} ↑(((F.comp (SheafOfModules.forget R)).comp (PresheafOfModules.evaluation R.obj X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj.obj X)))).sections
• SheafOfModules.pushforwardCompForgetToSheafModuleCat 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (hX' : CategoryTheory.Limits.IsInitial (F.op.obj X)) : (SheafOfModules.pushforward φ).comp (SheafOfModules.forgetToSheafModuleCat S X hX) ≅ (SheafOfModules.forgetToSheafModuleCat R (F.op.obj X) hX').comp ((CategoryTheory.sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X)))).comp (F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K))
• CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_ 📋 Mathlib.CategoryTheory.Sites.CoversTop.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) : ↑F.sections
• CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_apply 📋 Mathlib.CategoryTheory.Sites.CoversTop.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) (i : I) : ↑(hx.section_ hY hF) (Opposite.op (Y i)) = x i
• CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.existsUnique_section 📋 Mathlib.CategoryTheory.Sites.CoversTop.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) : ∃! s, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i
• CategoryTheory.GrothendieckTopology.CoversTop.sections_ext 📋 Mathlib.CategoryTheory.Sites.CoversTop.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {I : Type u_1} {Y : I → C} (hY : J.CoversTop Y) (F : CategoryTheory.Sheaf J (Type u_2)) {x y : ↑F.obj.sections} (h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))) : x = y
• SheafOfModules.Presentation.mk 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (generators : M.GeneratingSections) (relations : (CategoryTheory.Limits.kernel generators.π).GeneratingSections) : M.Presentation

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