Loogle!

Result

Found 80 declarations mentioning CategoryTheory.Over.homMk.

CategoryTheory.Over.homMk 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} (f : U.left ⟶ V.left) (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom := by cat_disch) : U ⟶ V
CategoryTheory.Over.epi_homMk 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f : U.left ⟶ V.left} [CategoryTheory.Epi f] (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom) : CategoryTheory.Epi (CategoryTheory.Over.homMk f w)
CategoryTheory.Over.mono_homMk 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f : U.left ⟶ V.left} [CategoryTheory.Mono f] (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom) : CategoryTheory.Mono (CategoryTheory.Over.homMk f w)
CategoryTheory.Over.homMk_eta 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} (f : U ⟶ V) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f) V.hom = U.hom) : CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left f) h = f
CategoryTheory.Over.homMk_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} (f : U.left ⟶ V.left) (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom := by cat_disch) : (CategoryTheory.Over.homMk f w).left = f
CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).inverse.map f = CategoryTheory.Over.homMk f ⋯
CategoryTheory.Over.homMk_surjective 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : T} {X Y : CategoryTheory.Over S} (f : X ⟶ Y) : ∃ g, ∃ (hg : CategoryTheory.CategoryStruct.comp g Y.hom = X.hom), f = CategoryTheory.Over.homMk g ⋯
CategoryTheory.Over.iteratedSliceBackward_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) (g : CategoryTheory.Over f.left) : f.iteratedSliceBackward.obj g = CategoryTheory.Over.mk (CategoryTheory.Over.homMk g.hom ⋯)
CategoryTheory.Over.homMk_comp 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V W : CategoryTheory.Over X} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) (w_f : CategoryTheory.CategoryStruct.comp f V.hom = U.hom) (w_g : CategoryTheory.CategoryStruct.comp g W.hom = V.hom) : CategoryTheory.Over.homMk (CategoryTheory.CategoryStruct.comp f g) ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.homMk f w_f) (CategoryTheory.Over.homMk g w_g)
CategoryTheory.Over.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 : D ⟶ (CategoryTheory.Functor.const J).obj X) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : (CategoryTheory.Over.lift D s).map f = CategoryTheory.Over.homMk (D.map f) ⋯
CategoryTheory.Over.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.Over X} (f : X✝ ⟶ Y✝) : (CategoryTheory.Over.post F).map f = CategoryTheory.Over.homMk (F.map (CategoryTheory.Over.Hom.left f)) ⋯
CategoryTheory.Over.equivalenceOfIsTerminal_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (({ obj := fun Y => CategoryTheory.Over.mk (hX.from Y), map := fun {X_1 Y} f => CategoryTheory.Over.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.Over.forget X)).obj x)) ⋯
CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) {X : T} (Y : CategoryTheory.Over X) (Z : CategoryTheory.CostructuredArrow F Y.left) : (CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse F Y).obj Z = CategoryTheory.CostructuredArrow.mk (CategoryTheory.Over.homMk Z.hom ⋯)
CategoryTheory.Over.iteratedSliceForward_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) {X✝ Y✝ : CategoryTheory.Over f} (κ : X✝ ⟶ Y✝) : f.iteratedSliceForward.map κ = CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left (CategoryTheory.Over.Hom.left κ)) ⋯
CategoryTheory.Over.opEquivOpUnder_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : (CategoryTheory.Under X)ᵒᵖ} (f : Z ⟶ Y) : (CategoryTheory.Over.opEquivOpUnder X).inverse.map f = CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f.unop).op ⋯
CategoryTheory.Over.equivalenceOfIsTerminal_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Over X)).obj Y).left) ⋯) ⋯
CategoryTheory.Over.postMap_app 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} {F G : CategoryTheory.Functor T D} (e : F ⟶ G) (Y : CategoryTheory.Over X) : (CategoryTheory.Over.postMap e).app Y = CategoryTheory.Over.homMk (e.app Y.left) ⋯
CategoryTheory.Under.opEquivOpOver_functor_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : CategoryTheory.Under (Opposite.op X)} (f : Z ⟶ Y) : (CategoryTheory.Under.opEquivOpOver X).functor.map f = Opposite.op (CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f).unop ⋯)
CategoryTheory.Over.liftCone_π_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 : D ⟶ (CategoryTheory.Functor.const J).obj X) (c : CategoryTheory.Limits.Cone D) (p : c.pt ⟶ X) (hp : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.π.app j) (s.app j) = p) (j : J) : (CategoryTheory.Over.liftCone D s c p hp).π.app j = CategoryTheory.Over.homMk (c.π.app j) ⋯
CategoryTheory.Limits.Cone.overPost_π_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.Cone D) (j : J) (k : CategoryTheory.Over j) : (c.overPost j).π.app k = CategoryTheory.Over.homMk (c.π.app k.left) ⋯
CategoryTheory.Over.iteratedSliceBackward_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) {X✝ Y✝ : CategoryTheory.Over f.left} (α : X✝ ⟶ Y✝) : f.iteratedSliceBackward.map α = CategoryTheory.Over.homMk (CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left α) ⋯) ⋯
CategoryTheory.Over.postAdjunctionRight_unit_app 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : D} {F : CategoryTheory.Functor T D} {G : CategoryTheory.Functor D T} (a : F ⊣ G) (A : CategoryTheory.Over (G.obj Y)) : (CategoryTheory.Over.postAdjunctionRight a).unit.app A = CategoryTheory.Over.homMk (a.unit.app A.left) ⋯
CategoryTheory.Over.postAdjunctionRight_counit_app 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : D} {F : CategoryTheory.Functor T D} {G : CategoryTheory.Functor D T} (a : F ⊣ G) (A : CategoryTheory.Over ((CategoryTheory.Functor.id D).obj Y)) : (CategoryTheory.Over.postAdjunctionRight a).counit.app A = CategoryTheory.Over.homMk (a.counit.app A.left) ⋯
CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) {X : T} (Y : CategoryTheory.Over X) {X✝ Y✝ : CategoryTheory.CostructuredArrow F Y.left} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse F Y).map f = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.CostructuredArrow.homMk f.left ⋯) ⋯
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_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.CostructuredArrow (CategoryTheory.Comma.fst F G) c} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).map f).left = CategoryTheory.Over.homMk f.left.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 := ⋯ })
CategoryTheory.Over.coprod_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} {X✝ Y✝ : CategoryTheory.Over A} (k : X✝ ⟶ Y✝) (g : CategoryTheory.Over A) : (CategoryTheory.Over.coprod.map k).app g = CategoryTheory.Over.homMk (CategoryTheory.Limits.coprod.map (CategoryTheory.Over.Hom.left k) (CategoryTheory.CategoryStruct.id g.left)) ⋯
CategoryTheory.Over.coprodObj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (a✝ : CategoryTheory.Over A) {X✝ Y✝ : CategoryTheory.Over A} (k : X✝ ⟶ Y✝) : a✝.coprodObj.map k = CategoryTheory.Over.homMk (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id a✝.left) (CategoryTheory.Over.Hom.left k)) ⋯
CategoryTheory.coalgebraToOver_map 📋 Mathlib.CategoryTheory.Monad.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {X✝ Y✝ : (CategoryTheory.prodComonad X).Coalgebra} (f : X✝ ⟶ Y✝) : (CategoryTheory.coalgebraToOver X).map f = CategoryTheory.Over.homMk f.f ⋯
CategoryTheory.Over.mapPullbackAdj_unit_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] (X✝ : CategoryTheory.Over X) : (CategoryTheory.Over.mapPullbackAdj f).unit.app X✝ = CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id X✝.left) X✝.hom ⋯) ⋯
CategoryTheory.Over.mapPullbackAdj_counit_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] (Y✝ : CategoryTheory.Over Y) : (CategoryTheory.Over.mapPullbackAdj f).counit.app Y✝ = CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.fst Y✝.hom f) ⋯
CategoryTheory.Over.postAdjunctionLeft_counit_app_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasPullbacks C] {X : C} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) (X✝ : CategoryTheory.Over ((CategoryTheory.Functor.id D).obj (F.obj X))) : ((CategoryTheory.Over.postAdjunctionLeft a).counit.app X✝).left = CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl (F.obj Y.left)) ⋯) ⋯).inv.app ((CategoryTheory.Over.pullback (a.unit.app X)).obj (CategoryTheory.Over.mk (G.map X✝.hom)))).left (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.pullback.fst (G.map X✝.hom) (a.unit.app X))) (CategoryTheory.Over.Hom.left (CategoryTheory.Over.homMk (a.counit.app X✝.left) ⋯)))
CategoryTheory.Over.postAdjunctionLeft_unit_app_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasPullbacks C] {X : C} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) (X✝ : CategoryTheory.Over ((CategoryTheory.Functor.id C).obj X)) : ((CategoryTheory.Over.postAdjunctionLeft a).unit.app X✝).left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id X✝.left) X✝.hom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp X✝.hom (a.unit.app X)) (a.unit.app X)) (a.unit.app X✝.left)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp X✝.hom (a.unit.app X)) (a.unit.app X)) ⋯) (((CategoryTheory.Over.post G).comp (CategoryTheory.Over.pullback (a.unit.app X))).map ((CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl (F.obj Y.left)) ⋯) ⋯).hom.app X✝)).left)
CategoryTheory.Limits.colimit.toOver_ι_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) [CategoryTheory.Limits.HasColimit F] (j : J) : (CategoryTheory.Limits.colimit.toOver F).ι.app j = CategoryTheory.Over.homMk (CategoryTheory.Limits.colimit.ι F j) ⋯
CategoryTheory.Limits.Cocone.toOver_ι_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.Cocone F) (j : J) : c.toOver.ι.app j = CategoryTheory.Over.homMk (c.ι.app j) ⋯
CategoryTheory.Over.liftCocone_ι_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.Cocone F) {X : C} (f : c.pt ⟶ X) (j : J) : (CategoryTheory.Over.liftCocone c f).ι.app j = CategoryTheory.Over.homMk (c.ι.app j) ⋯
CategoryTheory.WithTerminal.coneEquiv_inverse_map_hom_left 📋 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.Over X)} {t₁ t₂ : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)} {f : t₁ ⟶ t₂} : (CategoryTheory.WithTerminal.coneEquiv.inverse.map f).hom.left = f.hom
CategoryTheory.MorphismProperty.Over.homMk_hom 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Over Q X} (f : A.left ⟶ B.left) (w : CategoryTheory.CategoryStruct.comp f B.hom = A.hom := by cat_disch) (hf : Q f := by trivial) : CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Over.homMk f w hf) = CategoryTheory.Over.homMk f w
CategoryTheory.Limits.diagonal_pullback_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f (CategoryTheory.Over.mk g).hom).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map (CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.diagonal g) ⋯))) (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv)
CategoryTheory.MonoOver.image_map 📋 Mathlib.CategoryTheory.Subobject.MonoOver
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C] {f g : CategoryTheory.Over X} (k : f ⟶ g) : CategoryTheory.MonoOver.image.map k = (CategoryTheory.MonoOver.forget X).preimage (CategoryTheory.Over.homMk (CategoryTheory.Limits.image.lift { I := CategoryTheory.Limits.image g.hom, m := CategoryTheory.Limits.image.ι g.hom, m_mono := ⋯, e := CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left k) (CategoryTheory.Limits.factorThruImage g.hom), fac := ⋯ }) ⋯)
CategoryTheory.Sieve.overEquiv_iff 📋 Mathlib.CategoryTheory.Sites.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y) {Z : C} (f : Z ⟶ Y.left) : ((CategoryTheory.Sieve.overEquiv Y) S).arrows f ↔ S.arrows (CategoryTheory.Over.homMk f ⋯)
CategoryTheory.Over.conePost_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
{J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (i : J) (c : CategoryTheory.Limits.Cone F) (X : CategoryTheory.Over i) : ((CategoryTheory.Over.conePost F i).obj c).π.app X = CategoryTheory.Over.homMk (c.π.app X.left) ⋯
CategoryTheory.Over.conePost_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
{J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (i : J) {X✝ Y✝ : CategoryTheory.Limits.Cone F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Over.conePost F i).map f).hom = CategoryTheory.Over.homMk f.hom ⋯
TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
{X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) {X✝ Y✝ : TopCat.Presheaf.SheafCondition.OpensLeCover U} (g : X✝ ⟶ Y✝) : (TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).map g = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk g.hom ⋯)
CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} (c : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.Limits.pullbackConeEquivBinaryFan.functor.obj c = CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Over.homMk c.fst ⋯) (CategoryTheory.Over.homMk c.snd ⋯)
CategoryTheory.Over.ConstructProducts.conesEquivFunctor_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)) (x✝ : CategoryTheory.Discrete J) : ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).obj c).π.app x✝ = match x✝ with | { as := j } => CategoryTheory.Over.homMk (c.π.app (some j)) ⋯
CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c₁ c₂ : CategoryTheory.Limits.PullbackCone f g} (a : c₁ ⟶ c₂) : (CategoryTheory.Limits.pullbackConeEquivBinaryFan.functor.map a).hom = CategoryTheory.Over.homMk a.hom ⋯
CategoryTheory.Over.ConstructProducts.conesEquivFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) {X✝ Y✝ : CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Over.ConstructProducts.conesEquivFunctor B F).map f).hom = CategoryTheory.Over.homMk f.hom ⋯
CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} : CategoryTheory.Limits.pullbackConeEquivBinaryFan.unitIso = CategoryTheory.NatIso.ofComponents (fun c => c.eta) ⋯
CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} : CategoryTheory.Limits.pullbackConeEquivBinaryFan.counitIso = CategoryTheory.NatIso.ofComponents (fun X_1 => CategoryTheory.Limits.BinaryFan.ext (CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl (({ obj := fun c => CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left c.fst) (CategoryTheory.Over.Hom.left c.snd) ⋯, map := fun {c₁ c₂} a => { hom := CategoryTheory.Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Over.homMk c.fst ⋯) (CategoryTheory.Over.homMk c.snd ⋯), map := fun {c₁ c₂} a => { hom := CategoryTheory.Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj X_1).pt.left) ⋯) ⋯ ⋯) ⋯
CategoryTheory.Over.isMonHom_pullbackFst_id_right 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R : C} {f : R ⟶ X} [CategoryTheory.MonObj (CategoryTheory.Over.mk f)] : CategoryTheory.IsMonHom (CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.fst f (CategoryTheory.CategoryStruct.id X)) ⋯)
AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor_map 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
(Y : AlgebraicGeometry.Scheme) {I J : Y.IdealSheafDataᵒᵖ} (h : I ⟶ J) : (AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor Y).map h = CategoryTheory.Over.homMk (AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯) ⋯
AlgebraicGeometry.Scheme.kerAdjunction_counit_app 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
(Y : AlgebraicGeometry.Scheme) (f : (CategoryTheory.Over Y)ᵒᵖ) : Y.kerAdjunction.counit.app f = (CategoryTheory.Over.homMk (AlgebraicGeometry.Scheme.Hom.toImage (Opposite.unop f).hom) ⋯).op
AlgebraicGeometry.one_spec_asOver_spec 📋 Mathlib.AlgebraicGeometry.Group.Affine
{R A : CommRingCat} [Bialgebra ↑R ↑A] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (AlgebraicGeometry.algSpec R)) (CategoryTheory.Over.homMk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom ↑R ↑A))) ⋯)
TopologicalSpace.Opens.overEquivalence_counitIso_hom_app 📋 Mathlib.Topology.Sheaves.Over
{X : Type u} [TopologicalSpace X] (U : TopologicalSpace.Opens X) (X✝ : TopologicalSpace.Opens ↥U) : U.overEquivalence.counitIso.hom.app X✝ = CategoryTheory.eqToHom ⋯
TopologicalSpace.Opens.overEquivalence_counitIso_inv_app 📋 Mathlib.Topology.Sheaves.Over
{X : Type u} [TopologicalSpace X] (U : TopologicalSpace.Opens X) (X✝ : TopologicalSpace.Opens ↥U) : U.overEquivalence.counitIso.inv.app X✝ = CategoryTheory.eqToHom ⋯
TopologicalSpace.Opens.overEquivalence_unitIso_hom_app_left 📋 Mathlib.Topology.Sheaves.Over
{X : Type u} [TopologicalSpace X] (U : TopologicalSpace.Opens X) (X✝ : CategoryTheory.Over U) : (U.overEquivalence.unitIso.hom.app X✝).left = CategoryTheory.eqToHom ⋯
TopologicalSpace.Opens.overEquivalence_unitIso_inv_app_left 📋 Mathlib.Topology.Sheaves.Over
{X : Type u} [TopologicalSpace X] (U : TopologicalSpace.Opens X) (X✝ : CategoryTheory.Over U) : (U.overEquivalence.unitIso.inv.app X✝).left = CategoryTheory.eqToHom ⋯
CategoryTheory.ChosenPullbacksAlong.iso_pullback_map 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) {Y✝ Z : CategoryTheory.Over X} (g : Y✝ ⟶ Z) : (CategoryTheory.ChosenPullbacksAlong.pullback f.hom).map g = CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left g) ⋯
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_map 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X Y : C) {X✝ Y✝ : CategoryTheory.Over X} (g : X✝ ⟶ Y✝) : (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)).map g = CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Over.Hom.left g) Y) ⋯
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_map 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X Y : C) {X✝ Y✝ : CategoryTheory.Over Y} (g : X✝ ⟶ Y✝) : (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).map g = CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Over.Hom.left g)) ⋯
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_map 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) {Y Z : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)} (g : Y ⟶ Z) : (CategoryTheory.ChosenPullbacksAlong.pullback f).map g = CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Over.Hom.left g) X) ⋯
CategoryTheory.ChosenPullbacksAlong.isoInv_mapPullbackAdj_unit_app_left 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (T : CategoryTheory.Over X) : ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f.inv).unit.app T).left = CategoryTheory.CategoryStruct.id T.left
CategoryTheory.ChosenPullbacksAlong.iso_mapPullbackAdj_unit_app 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (T : CategoryTheory.Over Y) : (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f.hom).unit.app T = CategoryTheory.Over.homMk (CategoryTheory.CategoryStruct.id T.left) ⋯
CategoryTheory.ChosenPullbacksAlong.iso_mapPullbackAdj_counit_app 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (U : CategoryTheory.Over X) : (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f.hom).counit.app U = CategoryTheory.Over.homMk (CategoryTheory.CategoryStruct.id (({ obj := fun Z => CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp Z.hom f.inv), map := fun {Y_1 Z} g => CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left g) ⋯, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.Over.map f.hom)).obj U).left) ⋯
CategoryTheory.ChosenPullbacksAlong.isoInv_mapPullbackAdj_counit_app_left 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (U : CategoryTheory.Over Y) : ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f.inv).counit.app U).left = CategoryTheory.CategoryStruct.id U.left
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X Y : C) (U : CategoryTheory.Over X) : (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)).counit.app U = CategoryTheory.Over.homMk (CategoryTheory.SemiCartesianMonoidalCategory.fst U.left Y) ⋯
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X Y : C) (U : CategoryTheory.Over Y) : (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).counit.app U = CategoryTheory.Over.homMk (CategoryTheory.SemiCartesianMonoidalCategory.snd X U.left) ⋯
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (T : CategoryTheory.Over X) : (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f).unit.app T = CategoryTheory.Over.homMk (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.Over X)).obj T).left) T.hom) ⋯
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (U : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) : (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f).counit.app U = CategoryTheory.Over.homMk (CategoryTheory.SemiCartesianMonoidalCategory.fst U.left X) ⋯
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X Y : C) (T : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) : (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)).unit.app T = CategoryTheory.Over.homMk (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))).obj T).left) (CategoryTheory.CategoryStruct.comp T.hom (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))) ⋯
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X Y : C) (T : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) : (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).unit.app T = CategoryTheory.Over.homMk (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp T.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))).obj T).left)) ⋯
CategoryTheory.toOver_map 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.Over
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X A A' : C} (f : A ⟶ A') : (CategoryTheory.toOver X).map f = CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) ⋯
CategoryTheory.forgetAdjToOver_unit_app 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.Over
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (Z : CategoryTheory.Over X) : (CategoryTheory.forgetAdjToOver X).unit.app Z = CategoryTheory.Over.homMk (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id Z.left) Z.hom) ⋯
CategoryTheory.toOverPullbackIsoToOver_inv_app_left 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.Over
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.ChosenPullbacksAlong f] (X✝ : C) : ((CategoryTheory.toOverPullbackIsoToOver f).inv.app X✝).left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f).unit.app ((CategoryTheory.toOver Y).obj X✝))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullback f).map (CategoryTheory.Over.homMk (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X✝ Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X✝ Y) f)) ⋯))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullback f).map (CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.Over.mapForget f).inv.app ((CategoryTheory.toOver Y).obj X✝)) X) ⋯))) (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullback f).map (CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.fst X✝ Y) X) ⋯)))))
CategoryTheory.regularTopology.parallelPair_pullback_initial 📋 Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X B : C} (π : X ⟶ B) (c : CategoryTheory.Limits.PullbackCone π π) (hc : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Limits.parallelPair (CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk c.fst ⋯)).op (CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk c.snd ⋯)).op).Initial
CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv 📋 Mathlib.CategoryTheory.Sites.Descent.DescentData
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {M N : ↑(F.obj { as := Opposite.op S })} : Subtype (CategoryTheory.Presieve.Arrows.Compatible (F.presheafHom M N) fun i => CategoryTheory.Over.homMk (f i) ⋯) ≃ ((F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff 📋 Mathlib.CategoryTheory.Sites.Descent.DescentData
{C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (M N : ↑(F.obj { as := Opposite.op S })) : Function.Bijective (F.toDescentData f).map ↔ CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N) (CategoryTheory.Presieve.ofArrows (fun i => CategoryTheory.Over.mk (f i)) fun i => CategoryTheory.Over.homMk (f i) ⋯)
CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv 📋 Mathlib.CategoryTheory.Sites.Descent.DescentData
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {M N : ↑(F.obj { as := Opposite.op S })} (φ : M ⟶ N) : (CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv F f) (CategoryTheory.Presieve.Arrows.toCompatible (F.presheafHom M N) (fun i => CategoryTheory.Over.homMk (f i) ⋯) (F.presheafHomObjHomEquiv φ)) = (F.toDescentData f).map φ

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