Loogle!

Result

Found 59 declarations mentioning CategoryTheory.Under.mk.

CategoryTheory.Under.mk 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) : CategoryTheory.Under X
CategoryTheory.Under.mkIdInitial 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} : CategoryTheory.Limits.IsInitial (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))
CategoryTheory.Under.forall_iff 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (P : CategoryTheory.Under X → Prop) : (∀ (Y : CategoryTheory.Under X), P Y) ↔ ∀ (Y : T) (f : X ⟶ Y), P (CategoryTheory.Under.mk f)
CategoryTheory.Under.mk_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) : (CategoryTheory.Under.mk f).right = Y
CategoryTheory.Under.mk_surjective 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : T} (X : CategoryTheory.Under S) : ∃ Y f, CategoryTheory.Under.mk f = X
CategoryTheory.Under.mk_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) : (CategoryTheory.Under.mk f).hom = f
CategoryTheory.Under.equivalenceOfIsInitial_inverse_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) (Y : T) : (CategoryTheory.Under.equivalenceOfIsInitial hX).inverse.obj Y = CategoryTheory.Under.mk (hX.to Y)
CategoryTheory.Under.mkIdInitial_to_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (Y : CategoryTheory.Under X) : CategoryTheory.Under.Hom.right (CategoryTheory.Under.mkIdInitial.to Y) = Y.hom
CategoryTheory.Under.post_obj 📋 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 X) : (CategoryTheory.Under.post F).obj Y = CategoryTheory.Under.mk (F.map Y.hom)
CategoryTheory.Under.lift_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T} (s : (CategoryTheory.Functor.const J).obj X ⟶ D) (j : J) : (CategoryTheory.Under.lift D s).obj j = CategoryTheory.Under.mk (s.app j)
CategoryTheory.Under.equivalenceOfIsInitial_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (CategoryTheory.Under.equivalenceOfIsInitial hX).inverse.map f = CategoryTheory.Under.homMk f ⋯
CategoryTheory.Under.opEquivOpOver_inverse_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) (Y : (CategoryTheory.Over X)ᵒᵖ) : (CategoryTheory.Under.opEquivOpOver X).inverse.obj Y = CategoryTheory.Under.mk (Opposite.unop Y).hom.op
CategoryTheory.Over.opEquivOpUnder_functor_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) (Y : CategoryTheory.Over (Opposite.op X)) : (CategoryTheory.Over.opEquivOpUnder X).functor.obj Y = Opposite.op (CategoryTheory.Under.mk Y.hom.unop)
CategoryTheory.Limits.Cocone.underPost_pt 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] {D : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone D) (j : J) : (c.underPost j).pt = CategoryTheory.Under.mk (c.ι.app j)
CategoryTheory.Under.lift_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T} (s : (CategoryTheory.Functor.const J).obj X ⟶ D) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : (CategoryTheory.Under.lift D s).map f = CategoryTheory.Under.homMk (D.map f) ⋯
CategoryTheory.Under.post_map 📋 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) {X✝ Y✝ : CategoryTheory.Under X} (f : X✝ ⟶ Y✝) : (CategoryTheory.Under.post F).map f = CategoryTheory.Under.homMk (F.map (CategoryTheory.Under.Hom.right f)) ⋯
CategoryTheory.Under.liftCocone_pt 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T} (s : (CategoryTheory.Functor.const J).obj X ⟶ D) (c : CategoryTheory.Limits.Cocone D) (p : X ⟶ c.pt) (hp : ∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = p) : (CategoryTheory.Under.liftCocone D s c p hp).pt = CategoryTheory.Under.mk p
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).left = CategoryTheory.Under.mk X.hom
CategoryTheory.Under.equivalenceOfIsInitial_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (({ obj := fun Y => CategoryTheory.Under.mk (hX.to Y), map := fun {X_1 Y} f => CategoryTheory.Under.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.Under.forget X)).obj x)) ⋯
CategoryTheory.Under.opEquivOpOver_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : (CategoryTheory.Over X)ᵒᵖ} (f : Z ⟶ Y) : (CategoryTheory.Under.opEquivOpOver X).inverse.map f = CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f.unop).op ⋯
CategoryTheory.Under.equivalenceOfIsInitial_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Under X)).obj Y).right) ⋯) ⋯
CategoryTheory.Over.opEquivOpUnder_functor_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : CategoryTheory.Over (Opposite.op X)} (f : Z ⟶ Y) : (CategoryTheory.Over.opEquivOpUnder X).functor.map f = Opposite.op (CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f).unop ⋯)
CategoryTheory.Under.liftCocone_ι_app 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T} (s : (CategoryTheory.Functor.const J).obj X ⟶ D) (c : CategoryTheory.Limits.Cocone D) (p : X ⟶ c.pt) (hp : ∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = p) (j : J) : (CategoryTheory.Under.liftCocone D s c p hp).ι.app j = CategoryTheory.Under.homMk (c.ι.app j) ⋯
CategoryTheory.Limits.Cocone.underPost_ι_app 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] {D : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone D) (j : J) (k : CategoryTheory.Under j) : (c.underPost j).ι.app k = CategoryTheory.Under.homMk (c.ι.app k.right) ⋯
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).map f).right = (CategoryTheory.StructuredArrow.Hom.right f).right
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).map f).left = CategoryTheory.Under.homMk (CategoryTheory.StructuredArrow.Hom.right f).left ⋯
CategoryTheory.Over.opEquivOpUnder_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) : (CategoryTheory.Over.opEquivOpUnder X).counitIso = CategoryTheory.Iso.refl ({ obj := fun Y => CategoryTheory.Over.mk (Opposite.unop Y).hom.op, map := fun {Z Y} f => CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f.unop).op ⋯, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun Y => Opposite.op (CategoryTheory.Under.mk Y.hom.unop), map := fun {Z Y} f => Opposite.op (CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f).unop ⋯), map_id := ⋯, map_comp := ⋯ })
CategoryTheory.Under.opEquivOpOver_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) : (CategoryTheory.Under.opEquivOpOver X).counitIso = CategoryTheory.Iso.refl ({ obj := fun Y => CategoryTheory.Under.mk (Opposite.unop Y).hom.op, map := fun {Z Y} f => CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f.unop).op ⋯, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun Y => Opposite.op (CategoryTheory.Over.mk Y.hom.unop), map := fun {Z Y} f => Opposite.op (CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f).unop ⋯), map_id := ⋯, map_comp := ⋯ })
CommRingCat.monoidAlgebra_obj 📋 Mathlib.Algebra.Category.Ring.Adjunctions
(R : CommRingCat) (G : CommMonCat) : R.monoidAlgebra.obj G = CategoryTheory.Under.mk (CommRingCat.ofHom MonoidAlgebra.singleOneRingHom)
CommRingCat.monoidAlgebra_map 📋 Mathlib.Algebra.Category.Ring.Adjunctions
(R : CommRingCat) {X✝ Y✝ : CommMonCat} (f : X✝ ⟶ Y✝) : R.monoidAlgebra.map f = CategoryTheory.Under.homMk (CommRingCat.ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯
CategoryTheory.algebraToUnder_obj 📋 Mathlib.CategoryTheory.Monad.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (A : (CategoryTheory.coprodMonad X).Algebra) : (CategoryTheory.algebraToUnder X).obj A = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl A.a)
CategoryTheory.algebraToUnder_map 📋 Mathlib.CategoryTheory.Monad.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] {X✝ Y✝ : (CategoryTheory.coprodMonad X).Algebra} (f : X✝ ⟶ Y✝) : (CategoryTheory.algebraToUnder X).map f = CategoryTheory.Under.homMk f.f ⋯
CategoryTheory.Under.pushout_obj 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPushoutsAlong f] (x : CategoryTheory.Under X) : (CategoryTheory.Under.pushout f).obj x = CategoryTheory.Under.mk (CategoryTheory.Limits.pushout.inr x.hom f)
CategoryTheory.Under.pushout_map 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPushoutsAlong f] (x : CategoryTheory.Under X) {x' : CategoryTheory.Under X} {u : x ⟶ x'} : (CategoryTheory.Under.pushout f).map u = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right u) (CategoryTheory.Limits.pushout.inl x'.hom f)) (CategoryTheory.Limits.pushout.inr x'.hom f) ⋯) ⋯
CategoryTheory.Under.mapPushoutAdj_counit_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPushoutsAlong f] (Y✝ : CategoryTheory.Under Y) : (CategoryTheory.Under.mapPushoutAdj f).counit.app Y✝ = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.id Y✝.right) Y✝.hom ⋯) ⋯
CategoryTheory.Under.mapPushoutAdj_unit_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPushoutsAlong f] (X✝ : CategoryTheory.Under X) : (CategoryTheory.Under.mapPushoutAdj f).unit.app X✝ = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.inl X✝.hom f) ⋯
CategoryTheory.Under.postAdjunctionRight_unit_app_right 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasPushouts D] {Y : D} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) (X : CategoryTheory.Under ((CategoryTheory.Functor.id C).obj (G.1 Y))) : ((CategoryTheory.Under.postAdjunctionRight a).unit.app X).right = CategoryTheory.CategoryStruct.comp (a.unit.app X.right) (G.map (CategoryTheory.Limits.pushout.inl (F.map X.hom) (a.counit.app Y)))
CategoryTheory.Under.postAdjunctionRight_counit_app_right 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasPushouts D] {Y : D} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) (X : CategoryTheory.Under ((CategoryTheory.Functor.id D).obj Y)) : ((CategoryTheory.Under.postAdjunctionRight a).counit.app X).right = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.desc (CategoryTheory.Limits.pushout.inl (F.map (CategoryTheory.CategoryStruct.comp (a.unit.app (G.1 Y)) (G.map (CategoryTheory.CategoryStruct.comp (a.counit.app Y) X.hom)))) (a.counit.app Y)) (CategoryTheory.Limits.pushout.inr (F.map (CategoryTheory.CategoryStruct.comp (a.unit.app (G.1 Y)) (G.map (CategoryTheory.CategoryStruct.comp (a.counit.app Y) X.hom)))) (a.counit.app Y)) ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.comp (a.counit.app X.right) (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (a.counit.app Y) X.hom) (a.counit.app Y))) (CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (a.counit.app Y) X.hom) (a.counit.app Y)) ⋯) (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.id X.right) X.hom ⋯))
CategoryTheory.Limits.Cone.toUnder_pt 📋 Mathlib.CategoryTheory.Limits.ConeCategory
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c.toUnder.pt = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id c.pt)
CategoryTheory.Limits.Cone.toUnder_π_app 📋 Mathlib.CategoryTheory.Limits.ConeCategory
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (j : J) : c.toUnder.π.app j = CategoryTheory.Under.homMk (c.π.app j) ⋯
CategoryTheory.Under.liftCone_pt 📋 Mathlib.CategoryTheory.Limits.Over
{J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt) : (CategoryTheory.Under.liftCone c f).pt = CategoryTheory.Under.mk f
CategoryTheory.Under.liftCone_π_app 📋 Mathlib.CategoryTheory.Limits.Over
{J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt) (j : J) : (CategoryTheory.Under.liftCone c f).π.app j = CategoryTheory.Under.homMk (c.π.app j) ⋯
CategoryTheory.WithInitial.coconeEquiv_inverse_obj_ι_app_right 📋 Mathlib.CategoryTheory.WithTerminal.Cone
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} (t : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)) (a : J) : ((CategoryTheory.WithInitial.coconeEquiv.inverse.obj t).ι.app a).right = t.ι.app (CategoryTheory.WithInitial.of a)
CategoryTheory.WithInitial.coconeEquiv_inverse_map_hom_right 📋 Mathlib.CategoryTheory.WithTerminal.Cone
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t₁ t₂ : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)} {f : t₁ ⟶ t₂} : (CategoryTheory.WithInitial.coconeEquiv.inverse.map f).hom.right = f.hom
CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under 📋 Mathlib.CategoryTheory.Presentable.Finite
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D} (hc : CategoryTheory.Limits.IsColimit c) {X A : C} (p : X ⟶ A) (s : (CategoryTheory.Functor.const J).obj X ⟶ D) [CategoryTheory.IsFinitelyPresentable (CategoryTheory.Under.mk p)] (f : A ⟶ c.pt) (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = CategoryTheory.CategoryStruct.comp p f) : ∃ j q, CategoryTheory.CategoryStruct.comp p q = s.app j ∧ CategoryTheory.CategoryStruct.comp q (c.ι.app j) = f
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} : CategoryTheory.Limits.PushoutCocone f g ≌ CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)
CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : CategoryTheory.Limits.PushoutCocone f g} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.functor.obj c)
CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanInverse 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.inverse.obj c)
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : CategoryTheory.Limits.PushoutCocone f g) : CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.functor.obj c = CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c.inl ⋯) (CategoryTheory.Under.homMk c.inr ⋯)
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)) : CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.inverse.obj c = CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right c.inl) (CategoryTheory.Under.Hom.right c.inr) ⋯
CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : CategoryTheory.Limits.PushoutCocone f g} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)) : (hc.pushoutCoconeEquivBinaryCofanFunctor.desc s).right = hc.desc (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right s.inl) (CategoryTheory.Under.Hom.right s.inr) ⋯)
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c₁ c₂ : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)} (a : c₁ ⟶ c₂) : (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.inverse.map a).hom = CategoryTheory.Under.Hom.right a.hom
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c₁ c₂ : CategoryTheory.Limits.PushoutCocone f g} (a : c₁ ⟶ c₂) : (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.functor.map a).hom = CategoryTheory.Under.homMk a.hom ⋯
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} : CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.unitIso = CategoryTheory.NatIso.ofComponents (fun c => c.eta) ⋯
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} : CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.counitIso = CategoryTheory.NatIso.ofComponents (fun X_1 => CategoryTheory.Limits.BinaryCofan.ext (CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl (({ obj := fun c => CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right c.inl) (CategoryTheory.Under.Hom.right c.inr) ⋯, map := fun {c₁ c₂} a => { hom := CategoryTheory.Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c.inl ⋯) (CategoryTheory.Under.homMk c.inr ⋯), map := fun {c₁ c₂} a => { hom := CategoryTheory.Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj X_1).pt.right) ⋯) ⋯ ⋯) ⋯
CategoryTheory.underEquivOfIsTerminal_inverse 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).inverse = CategoryTheory.Functor.fromPUnit (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))
CategoryTheory.underEquivOfIsTerminal_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.fromPUnit (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))).comp (CategoryTheory.Functor.star (CategoryTheory.Under X)))
CategoryTheory.underEquivOfIsTerminal_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Under.isoMk (CategoryTheory.asIso A.hom).symm ⋯) ⋯
CategoryTheory.MorphismProperty.ind_iff_ind_underMk 📋 Mathlib.CategoryTheory.MorphismProperty.Ind
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y : C} (f : X ⟶ Y) : P.ind f ↔ P.underObj.ind (CategoryTheory.Under.mk f)

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

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

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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

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

Source code

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

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c