Loogle!

Result

Found 50 declarations mentioning CategoryTheory.Limits.BinaryFan.fst.

• CategoryTheory.Limits.BinaryFan.fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }
• CategoryTheory.Limits.isoBinaryFanMk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryFan X Y) : c ≅ CategoryTheory.Limits.BinaryFan.mk c.fst c.snd
• CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsTerminal Y) (c : CategoryTheory.Limits.BinaryFan X Y) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.fst
• CategoryTheory.Limits.BinaryFan.swap_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.swap.fst = s.snd
• CategoryTheory.Limits.BinaryFan.swap_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.swap.snd = s.fst
• CategoryTheory.Limits.BinaryFan.mk_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).fst = π₁
• CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g) s.fst = f
• CategoryTheory.Limits.BinaryFan.π_app_left 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.π.app { as := CategoryTheory.Limits.WalkingPair.left } = s.fst
• CategoryTheory.Limits.BinaryFan.isLimitFlip 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan X Y} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk c.snd c.fst)
• CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h✝ : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g) (CategoryTheory.CategoryStruct.comp s.fst h✝) = CategoryTheory.CategoryStruct.comp f h✝
• CategoryTheory.Limits.BinaryFan.braiding_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom t.fst = s.snd
• CategoryTheory.Limits.BinaryFan.braiding_hom_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom t.snd = s.fst
• CategoryTheory.Limits.BinaryFan.braiding_inv_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv s.fst = t.snd
• CategoryTheory.Limits.BinaryFan.braiding_inv_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv s.snd = t.fst
• CategoryTheory.Limits.BinaryFan.rightUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.rightUnitor P Q).hom = t.fst
• CategoryTheory.Limits.BinaryFan.isLimitCompLeftIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y X' : C} (c : CategoryTheory.Limits.BinaryFan X Y) (f : X ⟶ X') [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp c.fst f) c.snd)
• CategoryTheory.Limits.BinaryFan.isLimitCompRightIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Y' : C} (c : CategoryTheory.Limits.BinaryFan X Y) (f : Y ⟶ Y') [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk c.fst (CategoryTheory.CategoryStruct.comp c.snd f))
• CategoryTheory.Limits.BinaryFan.IsLimit.lift' 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : { l // CategoryTheory.CategoryStruct.comp l s.fst = f ∧ CategoryTheory.CategoryStruct.comp l s.snd = g }
• CategoryTheory.Limits.BinaryFan.map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : (CategoryTheory.Limits.BinaryFan.map F s).fst = F.map s.fst
• CategoryTheory.Limits.BinaryFan.braiding_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : (CategoryTheory.Limits.pair Y X).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom (CategoryTheory.CategoryStruct.comp t.fst h) = CategoryTheory.CategoryStruct.comp s.snd h
• CategoryTheory.Limits.BinaryFan.braiding_hom_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : (CategoryTheory.Limits.pair Y X).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom (CategoryTheory.CategoryStruct.comp t.snd h) = CategoryTheory.CategoryStruct.comp s.fst h
• CategoryTheory.Limits.BinaryFan.braiding_inv_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv (CategoryTheory.CategoryStruct.comp s.fst h) = CategoryTheory.CategoryStruct.comp t.snd h
• CategoryTheory.Limits.BinaryFan.braiding_inv_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv (CategoryTheory.CategoryStruct.comp s.snd h) = CategoryTheory.CategoryStruct.comp t.fst h
• CategoryTheory.Limits.BinaryFan.IsLimit.lift'_coe 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : ↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' h f g) = h.lift (CategoryTheory.Limits.BinaryFan.mk f g)
• CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) {f g : W ⟶ s.pt} (h₁ : CategoryTheory.CategoryStruct.comp f s.fst = CategoryTheory.CategoryStruct.comp g s.fst) (h₂ : CategoryTheory.CategoryStruct.comp f s.snd = CategoryTheory.CategoryStruct.comp g s.snd) : f = g
• CategoryTheory.Limits.BinaryFan.assoc_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) (s : CategoryTheory.Limits.BinaryFan sXY.pt Z) : (CategoryTheory.Limits.BinaryFan.assoc Q s).fst = CategoryTheory.CategoryStruct.comp s.fst sXY.fst
• CategoryTheory.Limits.BinaryFan.isLimitMk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : (s : CategoryTheory.Limits.BinaryFan X Y) → s.pt ⟶ W) (fac_left : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : CategoryTheory.Limits.BinaryFan X Y) (m : s.pt ⟶ W), CategoryTheory.CategoryStruct.comp m fst = s.fst → CategoryTheory.CategoryStruct.comp m snd = s.snd → m = lift s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd)
• CategoryTheory.Limits.BinaryFan.assocInv_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY) (s : CategoryTheory.Limits.BinaryFan X sYZ.pt) : (CategoryTheory.Limits.BinaryFan.assocInv P s).fst = CategoryTheory.Limits.BinaryFan.IsLimit.lift P s.fst (CategoryTheory.CategoryStruct.comp s.snd sYZ.fst)
• CategoryTheory.Limits.BinaryFan.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryTheory.CategoryStruct.comp e.hom c'.fst) (h₂ : c.snd = CategoryTheory.CategoryStruct.comp e.hom c'.snd) : c ≅ c'
• CategoryTheory.Limits.BinaryFan.assoc_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) (s : CategoryTheory.Limits.BinaryFan sXY.pt Z) : (CategoryTheory.Limits.BinaryFan.assoc Q s).snd = Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp s.fst sXY.snd) s.snd)
• CategoryTheory.Limits.BinaryFan.IsLimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) (lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)) (hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.fst = f) (hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.snd = g) (uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), CategoryTheory.CategoryStruct.comp m s.fst = f → CategoryTheory.CategoryStruct.comp m s.snd = g → m = lift f g) : CategoryTheory.Limits.IsLimit s
• CategoryTheory.Limits.BinaryFan.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryTheory.CategoryStruct.comp e.hom c'.fst) (h₂ : c.snd = CategoryTheory.CategoryStruct.comp e.hom c'.snd) : (CategoryTheory.Limits.BinaryFan.ext e h₁ h₂).hom.hom = e.hom
• CategoryTheory.Limits.BinaryBicone.binary_fan_fst_toCone 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.Limits.BinaryFan.fst c.toCone = c.fst
• CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan X Y} (hc : CategoryTheory.Limits.IsLimit c) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.IsPullback c.fst c.snd (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
• CategoryTheory.IsPullback.of_is_product 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {c : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit c) (t : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.IsPullback c.fst c.snd (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
• CategoryTheory.Limits.Types.binaryProductCone_fst 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) : (CategoryTheory.Limits.Types.binaryProductCone X Y).fst = TypeCat.ofHom Prod.fst
• CategoryTheory.Limits.Types.binaryProductLimit_lift 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) (s : CategoryTheory.Limits.BinaryFan X Y) : (CategoryTheory.Limits.Types.binaryProductLimit X Y).lift s = TypeCat.ofHom fun x => ((CategoryTheory.ConcreteCategory.hom s.fst) x, (CategoryTheory.ConcreteCategory.hom s.snd) x)
• CategoryTheory.extendFan_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendFan c₁ c₂).π.app X = Fin.cases c₂.fst (fun i => CategoryTheory.CategoryStruct.comp c₂.snd (c₁.π.app { as := i })) X.as
• CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] (X Y : P.FullSubcategory) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)) : ((CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct X Y).lift t).hom = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.Limits.BinaryFan.fst t).hom (CategoryTheory.Limits.BinaryFan.snd t).hom
• AddCommGrpCat.binaryProductLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.Biproducts
  (G H : AddCommGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : (G.binaryProductLimitCone H).isLimit.lift t = AddCommGrpCat.ofHom ((AddCommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod (AddCommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
• AddGrpCat.binaryProductLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : AddGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : (G.binaryProductLimitCone H).isLimit.lift t = AddGrpCat.ofHom ((AddGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod (AddGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
• GrpCat.binaryProductLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : GrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : (G.binaryProductLimitCone H).isLimit.lift t = GrpCat.ofHom ((GrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod (GrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
• CommGrpCat.binaryProductLimitCone_isLimit_lift 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : CommGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)) : (G.binaryProductLimitCone H).isLimit.lift t = CommGrpCat.ofHom ((CommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod (CommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
• CategoryTheory.Over.isPullback_of_binaryFan_isLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y Z : CategoryTheory.Over X} (c : CategoryTheory.Limits.BinaryFan Y Z) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsPullback (CategoryTheory.Over.Hom.left c.fst) (CategoryTheory.Over.Hom.left c.snd) Y.hom Z.hom
• CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_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.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)) : CategoryTheory.Limits.pullbackConeEquivBinaryFan.inverse.obj c = CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left c.fst) (CategoryTheory.Over.Hom.left c.snd) ⋯
• CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left 📋 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} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)) : (hc.pullbackConeEquivBinaryFanFunctor.lift s).left = hc.lift (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left s.fst) (CategoryTheory.Over.Hom.left s.snd) ⋯)
• CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_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.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)} (a : c₁ ⟶ c₂) : (CategoryTheory.Limits.pullbackConeEquivBinaryFan.inverse.map a).hom = CategoryTheory.Over.Hom.left a.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.FunctorToTypes.binaryProductLimit_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (s : CategoryTheory.Limits.BinaryFan F G) : (CategoryTheory.FunctorToTypes.binaryProductLimit F G).lift s = CategoryTheory.FunctorToTypes.prod.lift s.fst s.snd

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

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

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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

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

Source code

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

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c