Loogle!

Result

Found 64 declarations mentioning CategoryTheory.Over.pullback.

CategoryTheory.Over.pullback 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)
CategoryTheory.Over.instIsRightAdjointPullback 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] : (CategoryTheory.Over.pullback f).IsRightAdjoint
CategoryTheory.Over.pullbackIsRightAdjoint 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] : (CategoryTheory.Over.pullback f).IsRightAdjoint
CategoryTheory.Over.mapPullbackAdj 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] : CategoryTheory.Over.map f ⊣ CategoryTheory.Over.pullback f
CategoryTheory.Over.faithful_pullback 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] [∀ (Z : C) (g : Z ⟶ Y), CategoryTheory.Epi (CategoryTheory.Limits.pullback.fst g f)] : (CategoryTheory.Over.pullback f).Faithful
CategoryTheory.Over.pullbackId 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} : CategoryTheory.Over.pullback (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (CategoryTheory.Over X)
CategoryTheory.Over.pullback_obj_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] (g : CategoryTheory.Over Y) : ((CategoryTheory.Over.pullback f).obj g).left = CategoryTheory.Limits.pullback g.hom f
CategoryTheory.Over.starPullbackIsoStar 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Over.star Y).comp (CategoryTheory.Over.pullback f) ≅ CategoryTheory.Over.star X
CategoryTheory.Over.pullback_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] (g : CategoryTheory.Over Y) : ((CategoryTheory.Over.pullback f).obj g).hom = CategoryTheory.Limits.pullback.snd g.hom f
CategoryTheory.Over.pullbackComp 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullbacksAlong f] [CategoryTheory.Limits.HasPullbacksAlong g] : CategoryTheory.Over.pullback (CategoryTheory.CategoryStruct.comp f g) ≅ (CategoryTheory.Over.pullback g).comp (CategoryTheory.Over.pullback f)
CategoryTheory.Over.postAdjunctionLeft 📋 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) : CategoryTheory.Over.post F ⊣ (CategoryTheory.Over.post G).comp (CategoryTheory.Over.pullback (a.unit.app X))
CategoryTheory.Over.pullback_map_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] (g : CategoryTheory.Over Y) {h : CategoryTheory.Over Y} {k : g ⟶ h} : ((CategoryTheory.Over.pullback f).map k).left = CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g.hom f) (CategoryTheory.Over.Hom.left k)) (CategoryTheory.Limits.pullback.snd g.hom 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.starPullbackIsoStar_hom_app_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (X✝ : C) : ((CategoryTheory.Over.starPullbackIsoStar f).hom.app X✝).left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (Y ⨯ X✝))) CategoryTheory.Limits.prod.fst) f CategoryTheory.Limits.prod.fst f (CategoryTheory.CategoryStruct.id (Y ⨯ X✝)) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.prod.fst f).hom (CategoryTheory.Limits.pullbackProdFstIsoProd f X✝).hom)
CategoryTheory.Over.starPullbackIsoStar_inv_app_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (X✝ : C) : ((CategoryTheory.Over.starPullbackIsoStar f).inv.app X✝).left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f X✝).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.prod.fst f).inv (CategoryTheory.Limits.pullback.map CategoryTheory.Limits.prod.fst f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (Y ⨯ X✝))) CategoryTheory.Limits.prod.fst) f (CategoryTheory.CategoryStruct.id (Y ⨯ X✝)) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) ⋯ ⋯))
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.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.MorphismProperty.baseChange_obj 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {S S' : C} (f : S' ⟶ S) [CategoryTheory.Limits.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] (X : CategoryTheory.Over S) (H : P X.hom) : P ((CategoryTheory.Over.pullback f).obj X).hom
CategoryTheory.MorphismProperty.baseChange_map 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) [CategoryTheory.Limits.HasPullbacksAlong f] {X Y : CategoryTheory.Over S} (g : X ⟶ Y) (H : P (CategoryTheory.Over.Hom.left g)) : P (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map g))
CategoryTheory.MorphismProperty.overPullbackMap 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) [CategoryTheory.Limits.HasPullbacksAlong f] {X Y : CategoryTheory.Over S} (g : X ⟶ Y) (H : P (CategoryTheory.Over.Hom.left g)) : P (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map g))
CategoryTheory.GrothendieckTopology.coverPreserving_overPullback 📋 Mathlib.CategoryTheory.Sites.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CoverPreserving (J.over Y) (J.over X) (CategoryTheory.Over.pullback f)
CategoryTheory.GrothendieckTopology.instIsContinuousOverPullbackOver 📋 Mathlib.CategoryTheory.Sites.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Over.pullback f).IsContinuous (J.over Y) (J.over X)
CategoryTheory.Sheaf.toPushforwardOverPullback 📋 Mathlib.CategoryTheory.Sites.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Sheaf J A) {X Y : C} (f : X ⟶ Y) : F.over Y ⟶ ((CategoryTheory.Over.pullback f).sheafPushforwardContinuous A (J.over Y) (J.over X)).obj (F.over X)
CategoryTheory.Sheaf.toPushforwardOverPullback_hom_app 📋 Mathlib.CategoryTheory.Sites.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Sheaf J A) {X Y : C} (f : X ⟶ Y) (U : (CategoryTheory.Over Y)ᵒᵖ) : (F.toPushforwardOverPullback f).hom.app U = F.obj.map (CategoryTheory.Limits.pullback.fst (Opposite.unop U).hom f).op
CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] : (CategoryTheory.MorphismProperty.Over.pullback P Q f).comp (CategoryTheory.MorphismProperty.Over.forget P Q X) ≅ (CategoryTheory.MorphismProperty.Over.forget P Q Y).comp (CategoryTheory.Over.pullback f)
CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso_hom_app_left 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (X✝ : P.Over Q Y) : ((CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso f).hom.app X✝).left = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback X✝.hom f)
CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso_inv_app_left 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (X✝ : P.Over Q Y) : ((CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso f).inv.app X✝).left = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback X✝.hom f)
CategoryTheory.Over.instBraidedPullback 📋 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.Over.pullback f).Braided
CategoryTheory.Over.η_pullback_left 📋 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.Over.Hom.left (CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Over.pullback f)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id X) f
CategoryTheory.Over.ε_pullback_left 📋 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.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback f)) = CategoryTheory.inv (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id X) f)
CategoryTheory.Over.preservesTerminalIso_pullback 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {R S : C} (f : R ⟶ S) : CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso (CategoryTheory.Over.pullback f) = CategoryTheory.Over.isoMk (CategoryTheory.asIso (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id S) f)) ⋯
CategoryTheory.Over.monObjMkPullbackSnd_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [CategoryTheory.MonObj (CategoryTheory.Over.mk f)] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback g)) ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.one)
CategoryTheory.Over.grpObjMkPullbackSnd_one 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [CategoryTheory.GrpObj (CategoryTheory.Over.mk f)] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback g)) ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.one)
CategoryTheory.Over.grpObjMkPullbackSnd_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [CategoryTheory.GrpObj (CategoryTheory.Over.mk f)] : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback g) (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk f)) ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.mul)
CategoryTheory.Over.monObjMkPullbackSnd_mul 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [CategoryTheory.MonObj (CategoryTheory.Over.mk f)] : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback g) (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk f)) ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.mul)
CategoryTheory.Over.μ_pullback_left_snd 📋 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} (R✝ S : CategoryTheory.Over X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) R✝ S)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj R✝ S).hom f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj R✝).hom ((CategoryTheory.Over.pullback f).obj S).hom) (CategoryTheory.Limits.pullback.snd S.hom f)
CategoryTheory.Over.μ_pullback_left_fst_fst 📋 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} (R✝ S : CategoryTheory.Over X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) R✝ S)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R✝ S).hom f) (CategoryTheory.Limits.pullback.fst R✝.hom S.hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((CategoryTheory.Over.pullback f).obj R✝).hom ((CategoryTheory.Over.pullback f).obj S).hom) (CategoryTheory.Limits.pullback.fst R✝.hom f)
CategoryTheory.Over.μ_pullback_left_fst_snd 📋 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} (R✝ S : CategoryTheory.Over X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) R✝ S)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R✝ S).hom f) (CategoryTheory.Limits.pullback.snd R✝.hom S.hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj R✝).hom ((CategoryTheory.Over.pullback f).obj S).hom) (CategoryTheory.Limits.pullback.fst S.hom f)
CategoryTheory.Over.μ_pullback_left_snd' 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R Y Z : C} {f : R ⟶ X} (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk g₁) (CategoryTheory.Over.mk g₂))) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g₁ g₂) g₁) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₁)).hom ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₂)).hom) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Over.mk g₂).hom f)
CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst' 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X A B Y : C} (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk gA) (CategoryTheory.Over.mk gB)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst gA gB) gA) f) (CategoryTheory.Limits.pullback.fst gA gB)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd gA f) (CategoryTheory.Limits.pullback.snd gB f)) (CategoryTheory.Limits.pullback.fst gA f)
CategoryTheory.Over.μ_pullback_left_fst_fst' 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R Y Z : C} {f : R ⟶ X} (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk g₁) (CategoryTheory.Over.mk g₂))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g₁ g₂) g₁) f) (CategoryTheory.Limits.pullback.fst g₁ g₂)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₁)).hom ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₂)).hom) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Over.mk g₁).hom f)
CategoryTheory.Over.μ_pullback_left_fst_snd' 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X R Y Z : C} {f : R ⟶ X} (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk g₁) (CategoryTheory.Over.mk g₂))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g₁ g₂) g₁) f) (CategoryTheory.Limits.pullback.snd g₁ g₂)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₁)).hom ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₂)).hom) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Over.mk g₂).hom f)
CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd' 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X A B Y : C} (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk gA) (CategoryTheory.Over.mk gB)).inv) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst gA gB) gA) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk gA)).hom ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk gB)).hom) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Over.mk gB).hom f)
CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd' 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X A B Y : C} (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk gA) (CategoryTheory.Over.mk gB)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst gA gB) gA) f) (CategoryTheory.Limits.pullback.snd gA gB)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk gA)).hom ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk gB)).hom) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Over.mk gB).hom f)
CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (A B : CategoryTheory.Over Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (CategoryTheory.Over.pullback f) A B).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst A.hom B.hom) A.hom) f) (CategoryTheory.Limits.pullback.fst A.hom B.hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd A.hom f) (CategoryTheory.Limits.pullback.snd B.hom f)) (CategoryTheory.Limits.pullback.fst A.hom f)
AlgebraicGeometry.Scheme.monObjAsOverPullback_one 📋 Mathlib.AlgebraicGeometry.Pullbacks
{M S T : AlgebraicGeometry.Scheme} [M.Over S] {f : T ⟶ S} [CategoryTheory.MonObj (M.asOver S)] : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback f)) ((CategoryTheory.Over.pullback f).map CategoryTheory.MonObj.one)
AlgebraicGeometry.Scheme.monObjAsOverPullback_mul 📋 Mathlib.AlgebraicGeometry.Pullbacks
{M S T : AlgebraicGeometry.Scheme} [M.Over S] {f : T ⟶ S} [CategoryTheory.MonObj (M.asOver S)] : CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk (M ↘ S)) (CategoryTheory.Over.mk (M ↘ S))) ((CategoryTheory.Over.pullback f).map CategoryTheory.MonObj.mul)
CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong 📋 Mathlib.CategoryTheory.MorphismProperty.Descent
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} [(CategoryTheory.MorphismProperty.isomorphisms C).DescendsAlong P] [P.IsStableUnderBaseChange] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasEqualizers C] {S T : C} {f : T ⟶ S} (hf : P f) : (CategoryTheory.Over.pullback f).Faithful
AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation 📋 Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.Flat f] [AlgebraicGeometry.LocallyOfFinitePresentation f] : (CategoryTheory.Over.pullback f).Faithful
AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact 📋 Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.Flat f] [AlgebraicGeometry.QuasiCompact f] : (CategoryTheory.Over.pullback f).Faithful
AlgebraicGeometry.μ_pullback_left_fst 📋 Mathlib.AlgebraicGeometry.Group.Affine
(R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))) (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))))) (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))) (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom (AlgebraicGeometry.Scheme.Hom.asOver (CategoryTheory.Limits.pullbackSymmetry (AlgebraicGeometry.Spec (CommRingCat.of T) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) (AlgebraicGeometry.Spec (CommRingCat.of S) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) ≪≫ AlgebraicGeometry.pullbackSpecIso' R S T).hom (AlgebraicGeometry.Spec (CommRingCat.of S))) (AlgebraicGeometry.Scheme.Hom.asOver (CategoryTheory.Limits.pullbackSymmetry (AlgebraicGeometry.Spec (CommRingCat.of T) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) (AlgebraicGeometry.Spec (CommRingCat.of S) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) ≪≫ AlgebraicGeometry.pullbackSpecIso' R S T).hom (AlgebraicGeometry.Spec (CommRingCat.of S))))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso S (TensorProduct R S T) (TensorProduct R S T)).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.mapRingHom (algebraMap R S) Algebra.TensorProduct.includeRight.toRingHom Algebra.TensorProduct.includeRight.toRingHom ⋯ ⋯))) (AlgebraicGeometry.pullbackSpecIso R T T).inv))
CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong_pullback 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ⟶ X) [CategoryTheory.Limits.HasPullbacksAlong f] : CategoryTheory.ChosenPullbacksAlong.pullback f = CategoryTheory.Over.pullback f
CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong_mapPullbackAdj 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ⟶ X) [CategoryTheory.Limits.HasPullbacksAlong f] : CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f = CategoryTheory.Over.mapPullbackAdj f
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [CategoryTheory.ChosenPullbacksAlong g] : CategoryTheory.ChosenPullbacksAlong.pullback g ≅ CategoryTheory.Over.pullback g
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).hom.app T)) (CategoryTheory.Limits.pullback.snd T.hom g) = CategoryTheory.ChosenPullbacksAlong.snd T.hom g
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).hom.app T)) (CategoryTheory.Limits.pullback.fst T.hom g) = CategoryTheory.ChosenPullbacksAlong.fst T.hom g
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).inv.app T)) (CategoryTheory.ChosenPullbacksAlong.snd T.hom g) = CategoryTheory.Limits.pullback.snd T.hom g
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).inv.app T)) (CategoryTheory.ChosenPullbacksAlong.fst T.hom g) = CategoryTheory.Limits.pullback.fst T.hom g
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd_assoc 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).hom.app T)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd T.hom g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd T.hom g) h
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst_assoc 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) {Z✝ : C} (h : T.left ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).hom.app T)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst T.hom g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst T.hom g) h
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd_assoc 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).inv.app T)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd T.hom g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd T.hom g) h
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst_assoc 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) {Z✝ : C} (h : T.left ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).inv.app T)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst T.hom g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst T.hom g) h

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