Loogle!

Result

Found 105 declarations mentioning CategoryTheory.Functor.essImage.

• CategoryTheory.Functor.essImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.ObjectProperty D
• CategoryTheory.Functor.instIsClosedUnderIsomorphismsEssImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : F.essImage.IsClosedUnderIsomorphisms
• CategoryTheory.Functor.essImage.witness 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} (h : F.essImage Y) : C
• CategoryTheory.Functor.obj_mem_essImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) (Y : D) : F.essImage (F.obj Y)
• CategoryTheory.Functor.EssSurj.mem_essImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} (F : CategoryTheory.Functor C D) [self : F.EssSurj] (Y : D) : F.essImage Y
• CategoryTheory.Functor.EssSurj.mk 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (mem_essImage : ∀ (Y : D), F.essImage Y) : F.EssSurj
• CategoryTheory.Functor.toEssImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor C F.EssImageSubcategory
• CategoryTheory.Functor.essImage.ofIso 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y Y' : D} (h : Y ≅ Y') (hY : F.essImage Y) : F.essImage Y'
• CategoryTheory.Functor.EssSurj.toEssImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : F.toEssImage.EssSurj
• CategoryTheory.Functor.essImage.getIso 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} (h : F.essImage Y) : F.obj h.witness ≅ Y
• CategoryTheory.Functor.Faithful.toEssImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Faithful] : F.toEssImage.Faithful
• CategoryTheory.Functor.Full.toEssImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Full] : F.toEssImage.Full
• CategoryTheory.Functor.isoClosure_eq_essImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : (CategoryTheory.ObjectProperty.isoClosure fun x => x ∈ Set.range F.obj) = F.essImage
• CategoryTheory.ObjectProperty.map_top 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : ⊤.map F = F.essImage
• CategoryTheory.Functor.essImage.ofNatIso 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F F' : CategoryTheory.Functor C D} (h : F ≅ F') {Y : D} (hY : F.essImage Y) : F'.essImage Y
• CategoryTheory.Functor.essImage_eq_of_natIso 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F F' : CategoryTheory.Functor C D} (h : F ≅ F') : F.essImage = F'.essImage
• CategoryTheory.Functor.essImage_comp_apply_of_essSurj 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.EssSurj] {X : E} : (F.comp G).essImage X ↔ G.essImage X
• CategoryTheory.Functor.essImage.liftFunctor 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) : CategoryTheory.Functor J C
• CategoryTheory.Functor.essImage_comp_of_essSurj 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.EssSurj] : (F.comp G).essImage = G.essImage
• CategoryTheory.Functor.toEssImage_obj_obj 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : (F.toEssImage.obj X).obj = F.obj X
• CategoryTheory.Functor.essImage_ι_comp 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) : (P.ι.comp F).essImage = P.map F
• CategoryTheory.Functor.toEssImageCompι 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : F.toEssImage.comp F.essImage.ι ≅ F
• CategoryTheory.Functor.essImage.liftFunctorCompIso 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) : (CategoryTheory.Functor.essImage.liftFunctor G F hG).comp F ≅ G
• CategoryTheory.Functor.essImage.liftFunctor_obj 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (j : J) : (CategoryTheory.Functor.essImage.liftFunctor G F hG).obj j = F.toEssImage.objPreimage { obj := G.obj j, property := ⋯ }
• CategoryTheory.Functor.toEssImage_map_hom 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (F.toEssImage.map f).hom = F.map f
• CategoryTheory.Functor.essImage_ext 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : F.EssImageSubcategory} (f g : X ⟶ Y) (h : F.essImage.ι.map f = F.essImage.ι.map g) : f = g
• CategoryTheory.Functor.toEssImageCompι_hom_app 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.toEssImageCompι.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.toEssImageCompι_inv_app 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.toEssImageCompι.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.essImage.liftFunctorCompIso_hom_app 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (X : J) : (CategoryTheory.Functor.essImage.liftFunctorCompIso G F hG).hom.app X = (F.toEssImage.objObjPreimageIso { obj := G.obj X, property := ⋯ }).hom.hom
• CategoryTheory.Functor.essImage.liftFunctorCompIso_inv_app 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (X : J) : (CategoryTheory.Functor.essImage.liftFunctorCompIso G F hG).inv.app X = (F.toEssImage.objObjPreimageIso { obj := G.obj X, property := ⋯ }).inv.hom
• CategoryTheory.Functor.essImage.liftFunctor_map 📋 Mathlib.CategoryTheory.EssentialImage
  {J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) {i j : J} (f : i ⟶ j) : (CategoryTheory.Functor.essImage.liftFunctor G F hG).map f = F.preimage (CategoryTheory.CategoryStruct.comp (F.toEssImage.objObjPreimageIso { obj := G.obj i, property := ⋯ }).hom.hom (CategoryTheory.CategoryStruct.comp (G.map f) (F.toEssImage.objObjPreimageIso { obj := G.obj j, property := ⋯ }).inv.hom))
• CategoryTheory.Equivalence.fullyFaithfulToEssImage 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] : F.toEssImage.IsEquivalence
• CategoryTheory.Functor.essImage.of_overPost 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} {F : CategoryTheory.Functor T D} {Y : CategoryTheory.Over (F.obj X)} : (CategoryTheory.Over.post F).essImage Y → F.essImage Y.left
• CategoryTheory.Functor.essImage.of_underPost 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} {F : CategoryTheory.Functor T D} {Y : CategoryTheory.Under (F.obj X)} : (CategoryTheory.Under.post F).essImage Y → F.essImage Y.right
• CategoryTheory.Functor.essImage_overPost 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} {F : CategoryTheory.Functor T D} [F.Full] {Y : CategoryTheory.Over (F.obj X)} : (CategoryTheory.Over.post F).essImage Y ↔ F.essImage Y.left
• CategoryTheory.Functor.essImage_underPost 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} {F : CategoryTheory.Functor T D} [F.Full] {Y : CategoryTheory.Under (F.obj X)} : (CategoryTheory.Under.post F).essImage Y ↔ F.essImage Y.right
• CategoryTheory.Adjunction.mem_essImage_of_counit_isIso 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (A : D) [CategoryTheory.IsIso (h.counit.app A)] : L.essImage A
• CategoryTheory.Adjunction.mem_essImage_of_unit_isIso 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (A : C) [CategoryTheory.IsIso (h.unit.app A)] : R.essImage A
• CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Faithful] [L.Full] {X : D} : CategoryTheory.IsIso (h.counit.app X) ↔ L.essImage X
• CategoryTheory.Adjunction.isIso_unit_app_iff_mem_essImage 📋 Mathlib.CategoryTheory.Adjunction.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Faithful] [R.Full] {Y : C} : CategoryTheory.IsIso (h.unit.app Y) ↔ R.essImage Y
• CategoryTheory.Functor.essImage_mapAddMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] [F.Full] [F.Faithful] {M : CategoryTheory.AddMon D} : F.mapAddMon.essImage M ↔ F.essImage M.X
• CategoryTheory.Functor.essImage_mapMon 📋 Mathlib.CategoryTheory.Monoidal.Mon
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] [F.Full] [F.Faithful] {M : CategoryTheory.Mon D} : F.mapMon.essImage M ↔ F.essImage M.X
• CategoryTheory.ObjectProperty.instEssentiallySmallEssImageOfEssentiallySmall 📋 Mathlib.CategoryTheory.ObjectProperty.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w, v, u} C] (F : CategoryTheory.Functor C D) : CategoryTheory.ObjectProperty.EssentiallySmall.{w, v', u'} F.essImage
• CategoryTheory.EssentiallySmall.of_functor 📋 Mathlib.CategoryTheory.ObjectProperty.Small
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [CategoryTheory.LocallySmall.{w, v_1, u_1} C] (H₁ : CategoryTheory.ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage) (H₂ : ∀ (Y : D), CategoryTheory.ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun x => Nonempty (F.obj x ≅ Y)) : CategoryTheory.EssentiallySmall.{w, v_1, u_1} C
• CategoryTheory.Limits.instIsClosedUnderColimitsOfShapeEssImageOfHasColimitsOfShapeOfPreservesColimitsOfShapeOfFullOfFaithful 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.PreservesColimitsOfShape J F] [F.Full] [F.Faithful] : F.essImage.IsClosedUnderColimitsOfShape J
• CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.PreservesLimitsOfShape J F] [F.Full] [F.Faithful] : F.essImage.IsClosedUnderLimitsOfShape J
• CategoryTheory.Functor.EssImageSubcategory.tensor_obj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [CategoryTheory.Limits.PreservesFiniteProducts F] (X Y : F.EssImageSubcategory) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj = CategoryTheory.MonoidalCategoryStruct.tensorObj X.obj Y.obj
• CategoryTheory.Functor.EssImageSubcategory.toUnit_def 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [CategoryTheory.Limits.PreservesFiniteProducts F] (X : F.EssImageSubcategory) : CategoryTheory.SemiCartesianMonoidalCategory.toUnit X = CategoryTheory.ObjectProperty.homMk (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X.obj)
• CategoryTheory.Functor.EssImageSubcategory.lift_def 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [CategoryTheory.Limits.PreservesFiniteProducts F] {T X Y : F.EssImageSubcategory} (f : T ⟶ X) (g : T ⟶ Y) : CategoryTheory.CartesianMonoidalCategory.lift f g = CategoryTheory.ObjectProperty.homMk (CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom)
• CategoryTheory.Functor.EssImageSubcategory.associator_hom_def 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [CategoryTheory.Limits.PreservesFiniteProducts F] (X Y Z : F.EssImageSubcategory) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).hom
• CategoryTheory.Functor.EssImageSubcategory.associator_inv_def 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [CategoryTheory.Limits.PreservesFiniteProducts F] (X Y Z : F.EssImageSubcategory) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).inv
• CategoryTheory.essImage_yonedaAddMon 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaAddMon.essImage = fun F => (F.comp (CategoryTheory.forget AddMonCat)).IsRepresentable
• CategoryTheory.essImage_yonedaMon 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaMon.essImage = fun F => (F.comp (CategoryTheory.forget MonCat)).IsRepresentable
• CategoryTheory.Functor.essImage_mapAddGrp 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] [F.Full] [F.Faithful] {G : CategoryTheory.AddGrp D} : F.mapAddGrp.essImage G ↔ F.essImage G.X
• CategoryTheory.Functor.essImage_mapGrp 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] [F.Full] [F.Faithful] {G : CategoryTheory.Grp D} : F.mapGrp.essImage G ↔ F.essImage G.X
• CategoryTheory.equivEssImageOfReflective 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : D ≌ i.EssImageSubcategory
• CategoryTheory.unitCompPartialBijective 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (A : C) {B : C} (hB : i.essImage B) : (A ⟶ B) ≃ (i.obj ((CategoryTheory.reflector i).obj A) ⟶ B)
• CategoryTheory.equivEssImageOfReflective_functor 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : CategoryTheory.equivEssImageOfReflective.functor = i.toEssImage
• CategoryTheory.equivEssImageOfReflective_inverse 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : CategoryTheory.equivEssImageOfReflective.inverse = i.essImage.ι.comp (CategoryTheory.reflector i)
• CategoryTheory.mem_essImage_of_counit_isSplitEpi 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {j : CategoryTheory.Functor C D} [CategoryTheory.Coreflective j] {A : D} [CategoryTheory.IsSplitEpi ((CategoryTheory.coreflectorAdjunction j).counit.app A)] : j.essImage A
• CategoryTheory.mem_essImage_of_unit_isSplitMono 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] {A : C} [CategoryTheory.IsSplitMono ((CategoryTheory.reflectorAdjunction i).unit.app A)] : i.essImage A
• CategoryTheory.Functor.essImage.counit_isIso 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {j : CategoryTheory.Functor C D} [CategoryTheory.Coreflective j] {A : D} (h : j.essImage A) : CategoryTheory.IsIso ((CategoryTheory.coreflectorAdjunction j).counit.app A)
• CategoryTheory.Functor.essImage.unit_isIso 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] {A : C} (h : i.essImage A) : CategoryTheory.IsIso ((CategoryTheory.reflectorAdjunction i).unit.app A)
• CategoryTheory.instIsIsoAppUnitReflectorAdjunctionObjEssImage 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (X : i.EssImageSubcategory) : CategoryTheory.IsIso ((CategoryTheory.reflectorAdjunction i).unit.app X.obj)
• CategoryTheory.equivEssImageOfReflective_unitIso 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : CategoryTheory.equivEssImageOfReflective.unitIso = (CategoryTheory.asIso (CategoryTheory.reflectorAdjunction i).counit).symm
• CategoryTheory.Functor.essImage_ext_iff 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X Y : F.EssImageSubcategory} {f g : X ⟶ Y} : f = g ↔ F.essImage.ι.map f = F.essImage.ι.map g
• CategoryTheory.unitCompPartialBijective_symm_apply 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (A : C) {B : C} (hB : i.essImage B) (f : i.obj ((CategoryTheory.reflector i).obj A) ⟶ B) : (CategoryTheory.unitCompPartialBijective A hB).symm f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.reflectorAdjunction i).unit.app A) f
• CategoryTheory.unitCompPartialBijective_natural 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (A : C) {B B' : C} (h : B ⟶ B') (hB : i.essImage B) (hB' : i.essImage B') (f : A ⟶ B) : (CategoryTheory.unitCompPartialBijective A hB') (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.unitCompPartialBijective A hB) f) h
• CategoryTheory.unitCompPartialBijective_symm_natural 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] (A : C) {B B' : C} (h : B ⟶ B') (hB : i.essImage B) (hB' : i.essImage B') (f : i.obj ((CategoryTheory.reflector i).obj A) ⟶ B) : (CategoryTheory.unitCompPartialBijective A hB').symm (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.unitCompPartialBijective A hB).symm f) h
• CategoryTheory.equivEssImageOfReflective_counitIso 📋 Mathlib.CategoryTheory.Adjunction.Reflective
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.Reflective i] : CategoryTheory.equivEssImageOfReflective.counitIso = CategoryTheory.Functor.fullyFaithfulCancelRight i.essImage.ι (CategoryTheory.NatIso.ofComponents (fun X => (CategoryTheory.asIso ((CategoryTheory.reflectorAdjunction i).unit.app X.obj)).symm) ⋯)
• CategoryTheory.ObjectProperty.instIsTriangulatedEssImageOfIsTriangulatedOfFull 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [F.Full] : F.essImage.IsTriangulated
• AlgebraicGeometry.essImage_Spec 📋 Mathlib.AlgebraicGeometry.AffineScheme
  {X : AlgebraicGeometry.Scheme} : AlgebraicGeometry.Scheme.Spec.essImage X ↔ AlgebraicGeometry.IsAffine X
• AlgebraicGeometry.isAffine_affineScheme 📋 Mathlib.AlgebraicGeometry.AffineScheme
  (X : AlgebraicGeometry.AffineScheme) : AlgebraicGeometry.IsAffine X.obj
• AlgebraicGeometry.AffineScheme.mk_obj 📋 Mathlib.AlgebraicGeometry.AffineScheme
  (X : AlgebraicGeometry.Scheme) (x✝ : AlgebraicGeometry.IsAffine X) : (AlgebraicGeometry.AffineScheme.mk X x✝).obj = X
• AlgebraicGeometry.AffineScheme.forgetToScheme_obj 📋 Mathlib.AlgebraicGeometry.AffineScheme
  (self : AlgebraicGeometry.Scheme.Spec.essImage.FullSubcategory) : AlgebraicGeometry.AffineScheme.forgetToScheme.obj self = self.obj
• AlgebraicGeometry.AffineScheme.forgetToScheme_map 📋 Mathlib.AlgebraicGeometry.AffineScheme
  {X✝ Y✝ : CategoryTheory.InducedCategory AlgebraicGeometry.Scheme CategoryTheory.ObjectProperty.FullSubcategory.obj} (f : X✝ ⟶ Y✝) : AlgebraicGeometry.AffineScheme.forgetToScheme.map f = f.hom
• CategoryTheory.essImage_yonedaAddGrp 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaAddGrp.essImage = fun F => (F.comp (CategoryTheory.forget AddGrpCat)).IsRepresentable
• CategoryTheory.essImage_yonedaGrp 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.yonedaGrp.essImage = fun F => (F.comp (CategoryTheory.forget GrpCat)).IsRepresentable
• AlgebraicGeometry.essImage_algSpec 📋 Mathlib.AlgebraicGeometry.Group.Affine
  {R : CommRingCat} {G : CategoryTheory.Over (AlgebraicGeometry.Spec R)} : (AlgebraicGeometry.algSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.left
• AlgebraicGeometry.essImage_hopfSpec 📋 Mathlib.AlgebraicGeometry.Group.Affine
  {R : CommRingCat} {G : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec R))} : (AlgebraicGeometry.hopfSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.X.left
• AlgebraicGeometry.essImage_bialgSpec 📋 Mathlib.AlgebraicGeometry.Group.Affine
  {R : CommRingCat} {G : CategoryTheory.Mon (CategoryTheory.Over (AlgebraicGeometry.Spec R))} : (AlgebraicGeometry.bialgSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.X.left
• AlgebraicGeometry.isIso_fromTildeΓ_iff 📋 Mathlib.AlgebraicGeometry.Modules.Tilde
  {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} : CategoryTheory.IsIso M.fromTildeΓ ↔ (AlgebraicGeometry.tilde.functor R).essImage M
• AlgebraicGeometry.essImage_tilde 📋 Mathlib.AlgebraicGeometry.Modules.Tilde
  {R : CommRingCat} : (AlgebraicGeometry.tilde.functor R).essImage = SheafOfModules.isQuasicoherent (AlgebraicGeometry.Spec R).ringCatSheaf
• CategoryTheory.Sheaf.mem_essImage_of_isConstant 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] (F : CategoryTheory.Sheaf J D) [CategoryTheory.Sheaf.IsConstant J F] : (CategoryTheory.constantSheaf J D).essImage F
• CategoryTheory.Sheaf.IsConstant.mem_essImage 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {J : CategoryTheory.GrothendieckTopology C} {D : Type u_2} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} D} {inst✝² : CategoryTheory.HasWeakSheafify J D} {F : CategoryTheory.Sheaf J D} [self : CategoryTheory.Sheaf.IsConstant J F] : (CategoryTheory.constantSheaf J D).essImage F
• CategoryTheory.Sheaf.IsConstant.mk 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Sheaf J D} (mem_essImage : (CategoryTheory.constantSheaf J D).essImage F) : CategoryTheory.Sheaf.IsConstant J F
• CategoryTheory.Sheaf.isConstant_iff_mem_essImage 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {L : CategoryTheory.Functor D (CategoryTheory.Sheaf J D)} {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (adj : L ⊣ (CategoryTheory.sheafSections J D).obj (Opposite.op T)) (F : CategoryTheory.Sheaf J D) : CategoryTheory.Sheaf.IsConstant J F ↔ L.essImage F
• CategoryTheory.ObjectProperty.SerreClassLocalization.essImage_whiskeringLeft 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (E : Type u'') [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : (CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).essImage = fun G => P.isoModSerre.IsInvertedBy G.obj
• CategoryTheory.ExponentialIdeal.mk' 📋 Mathlib.CategoryTheory.Monoidal.Closed.Ideal
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] (i : CategoryTheory.Functor D C) [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)) : CategoryTheory.ExponentialIdeal i
• CategoryTheory.ExponentialIdeal.exp_closed 📋 Mathlib.CategoryTheory.Monoidal.Closed.Ideal
  {C : Type u₁} {D : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.Category.{v₁, u₂} D} {i : CategoryTheory.Functor D C} {inst✝² : CategoryTheory.CartesianMonoidalCategory C} {inst✝³ : CategoryTheory.MonoidalClosed C} [self : CategoryTheory.ExponentialIdeal i] {B : C} : i.essImage B → ∀ (A : C), i.essImage (A ⟹ B)
• CategoryTheory.ExponentialIdeal.mk 📋 Mathlib.CategoryTheory.Monoidal.Closed.Ideal
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {i : CategoryTheory.Functor D C} [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (exp_closed : ∀ {B : C}, i.essImage B → ∀ (A : C), i.essImage (A ⟹ B)) : CategoryTheory.ExponentialIdeal i
• CategoryTheory.cartesianClosedOfReflective' 📋 Mathlib.CategoryTheory.Monoidal.Closed.Ideal
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] (i : CategoryTheory.Functor D C) [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Reflective i] [CategoryTheory.MonoidalClosed C] [CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.ExponentialIdeal i] (l : CategoryTheory.Functor i.EssImageSubcategory D) (φ : l.comp i ≅ i.essImage.ι) : CategoryTheory.MonoidalClosed D
• CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ofHasDayConvolutions 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor D (CategoryTheory.Functor C V)) (ffι : ι.FullyFaithful) [hasDayConvolution : ∀ (d d' : D), (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d'))] (essImageDayConvolution : ∀ (d d' : D), ι.essImage ((CategoryTheory.MonoidalCategory.tensor C).pointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d')))) [hasDayConvolutionUnit : (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] (essImageDayConvolutionUnit : ι.essImage ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).pointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)))) : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
• CategoryTheory.MonoidalCategory.monoidalOfHasDayConvolutions 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor D (CategoryTheory.Functor C V)) (ffι : ι.FullyFaithful) [hasDayConvolution : ∀ (d d' : D), (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d'))] (essImageDayConvolution : ∀ (d d' : D), ι.essImage ((CategoryTheory.MonoidalCategory.tensor C).pointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d')))) [hasDayConvolutionUnit : (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] (essImageDayConvolutionUnit : ι.essImage ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).pointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)))) [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.Functor.id C).prod (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] : CategoryTheory.MonoidalCategory D
• CategoryTheory.MonoidalCategory.lawfulDayConvolutionMonoidalCategoryStructOfHasDayConvolutions 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor D (CategoryTheory.Functor C V)) (ffι : ι.FullyFaithful) [hasDayConvolution : ∀ (d d' : D), (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d'))] (essImageDayConvolution : ∀ (d d' : D), ι.essImage ((CategoryTheory.MonoidalCategory.tensor C).pointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct (ι.obj d) (ι.obj d')))) [hasDayConvolutionUnit : (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] (essImageDayConvolutionUnit : ι.essImage ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).pointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)))) [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.Functor.id C).prod (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D
• CategoryTheory.ObjectProperty.localEpi_essImage 📋 Mathlib.CategoryTheory.MorphismProperty.LocalEpi
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.Faithful] [G.Full] : G.essImage.localEpi = (CategoryTheory.MorphismProperty.epimorphisms D).inverseImage F
• CategoryTheory.Triangulated.TStructure.essImage_ιHeart 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Heart
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (H : Type u') [CategoryTheory.Category.{v', u'} H] [CategoryTheory.Preadditive H] [t.Heart H] : t.ιHeart.essImage = t.heart
• CategoryTheory.Triangulated.TStructure.Heart.essImage_eq_heart 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Heart
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.HasShift C ℤ} {inst✝⁴ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝⁵ : CategoryTheory.Pretriangulated C} {t : CategoryTheory.Triangulated.TStructure C} {H : Type u'} {inst✝⁶ : CategoryTheory.Category.{v', u'} H} {inst✝⁷ : CategoryTheory.Preadditive H} [self : t.Heart H] : (CategoryTheory.Triangulated.TStructure.Heart.ι t).essImage = t.heart
• CategoryTheory.Triangulated.TStructure.Heart.mk 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Heart
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {t : CategoryTheory.Triangulated.TStructure C} {H : Type u'} [CategoryTheory.Category.{v', u'} H] [CategoryTheory.Preadditive H] (ι : CategoryTheory.Functor H C) (additive_ι : ι.Additive := by infer_instance) (full_ι : ι.Full := by infer_instance) (faithful_ι : ι.Faithful := by infer_instance) (essImage_eq_heart : ι.essImage = t.heart := by simp) : t.Heart H
• LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone 📋 Mathlib.Condensed.Discrete.Characterization
  (X : LightCondSet) (h : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (X.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : LightCondSet.LocallyConstant.functor.essImage X
• CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone 📋 Mathlib.Condensed.Discrete.Characterization
  (X : CondensedSet) (h : (S : Profinite) → CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.obj).mapCocone S.asLimitCone.op)) : CondensedSet.LocallyConstant.functor.essImage X
• LightCondSet.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (X : LightCondSet) : [LightCondensed.IsDiscrete X, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X), (LightCondensed.discrete (Type u)).essImage X, LightCondSet.LocallyConstant.functor.essImage X, CategoryTheory.IsIso (LightCondSet.LocallyConstant.adjunction.counit.app X), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (X.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE
• LightCondMod.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (R : Type u) [Ring R] (M : LightCondMod R) : [LightCondensed.IsDiscrete M, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), (LightCondensed.discrete (ModuleCat R)).essImage M, (LightCondMod.LocallyConstant.functor R).essImage M, CategoryTheory.IsIso ((LightCondMod.LocallyConstant.adjunction R).counit.app M), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (M.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE
• CondensedSet.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (X : CondensedSet) : [Condensed.IsDiscrete X, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (Type (u + 1))).counit.app X), (Condensed.discrete (Type (u + 1))).essImage X, CondensedSet.LocallyConstant.functor.essImage X, CategoryTheory.IsIso (CondensedSet.LocallyConstant.adjunction.counit.app X), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.obj).mapCocone S.asLimitCone.op))].TFAE
• CondensedMod.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (R : Type (u + 1)) [Ring R] (M : CondensedMod R) : [Condensed.IsDiscrete M, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), (Condensed.discrete (ModuleCat R)).essImage M, (CondensedMod.LocallyConstant.functor R).essImage M, CategoryTheory.IsIso ((CondensedMod.LocallyConstant.adjunction R).counit.app M), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp M.obj).mapCocone S.asLimitCone.op))].TFAE

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