Loogle!

Result

Found 116 declarations mentioning CategoryTheory.Limits.HasBinaryProducts.

• CategoryTheory.Limits.HasBinaryProducts 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
• CategoryTheory.Limits.prod.functor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Functor C (CategoryTheory.Functor C C)
• CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [∀ {X Y : C}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)] : CategoryTheory.Limits.HasBinaryProducts C
• CategoryTheory.Limits.prod.functor_obj_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y : C) : (CategoryTheory.Limits.prod.functor.obj X).obj Y = (X ⨯ Y)
• CategoryTheory.Limits.prod.functorLeftComp 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y : C) : CategoryTheory.Limits.prod.functor.obj (X ⨯ Y) ≅ (CategoryTheory.Limits.prod.functor.obj Y).comp (CategoryTheory.Limits.prod.functor.obj X)
• CategoryTheory.Limits.prod.functor_obj_map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (CategoryTheory.Limits.prod.functor.obj X).map g = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g
• CategoryTheory.Limits.prod.associator 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (P Q R : C) : (P ⨯ Q) ⨯ R ≅ P ⨯ Q ⨯ R
• CategoryTheory.Limits.prod.functor_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : C) : (CategoryTheory.Limits.prod.functor.map f).app T = CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id T)
• CategoryTheory.Limits.prod_rightUnitor_inv_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).inv (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.rightUnitor Y).inv
• CategoryTheory.Limits.prod.leftUnitor_hom_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) (CategoryTheory.Limits.prod.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).hom f
• CategoryTheory.Limits.prod.leftUnitor_inv_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).inv (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.leftUnitor Y).inv
• CategoryTheory.Limits.prod.rightUnitor_hom_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) (CategoryTheory.Limits.prod.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).hom f
• CategoryTheory.Limits.prod_rightUnitor_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⨯ ⊤_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor Y).inv h)
• CategoryTheory.Limits.prod.leftUnitor_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Limits.prod.leftUnitor_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : (⊤_ C) ⨯ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (⊤_ C)) f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.leftUnitor Y).inv h)
• CategoryTheory.Limits.prod.rightUnitor_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor Y).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).hom (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Limits.braid_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.Limits.prod.braiding Y W).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding X Z).hom (CategoryTheory.Limits.prod.map g f)
• CategoryTheory.Limits.prod.associator_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (P Q R : C) : (CategoryTheory.Limits.prod.associator P Q R).hom = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
• CategoryTheory.Limits.prod.associator_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (P Q R : C) : (CategoryTheory.Limits.prod.associator P Q R).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
• CategoryTheory.Limits.braid_natural_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z✝ : C} (h : W ⨯ Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding Y W).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g f) h)
• CategoryTheory.Limits.prod.triangle 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X (⊤_ C) Y).hom (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.prod.leftUnitor Y).hom) = CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)
• CategoryTheory.Limits.prod.associator_naturality 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.map f₁ f₂) f₃) (CategoryTheory.Limits.prod.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X₁ X₂ X₃).hom (CategoryTheory.Limits.prod.map f₁ (CategoryTheory.Limits.prod.map f₂ f₃))
• CategoryTheory.Limits.prod.associator_naturality_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {Z : C} (h : Y₁ ⨯ Y₂ ⨯ Y₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.map f₁ f₂) f₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator Y₁ Y₂ Y₃).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator X₁ X₂ X₃).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f₁ (CategoryTheory.Limits.prod.map f₂ f₃)) h)
• CategoryTheory.Limits.prod.pentagon 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W (X ⨯ Y) Z).hom (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.Limits.prod.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator (W ⨯ X) Y Z).hom (CategoryTheory.Limits.prod.associator W X (Y ⨯ Z)).hom
• CategoryTheory.Limits.prod.pentagon_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (W X Y Z : C) {Z✝ : C} (h : W ⨯ X ⨯ Y ⨯ Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.prod.associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W (X ⨯ Y) Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.Limits.prod.associator X Y Z).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator (W ⨯ X) Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.associator W X (Y ⨯ Z)).hom h)
• CategoryTheory.Limits.prodComparisonNatTrans 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (F : CategoryTheory.Functor C D) (A : C) : (CategoryTheory.Limits.prod.functor.obj A).comp F ⟶ F.comp (CategoryTheory.Limits.prod.functor.obj (F.obj A))
• CategoryTheory.Limits.prodComparisonNatTrans_app 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (F : CategoryTheory.Functor C D) (A B : C) : (CategoryTheory.Limits.prodComparisonNatTrans F A).app B = CategoryTheory.Limits.prodComparison F A B
• CategoryTheory.Limits.prodComparisonNatIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : (CategoryTheory.Limits.prod.functor.obj A).comp F ≅ F.comp (CategoryTheory.Limits.prod.functor.obj (F.obj A))
• CategoryTheory.Limits.prodComparisonNatIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : (CategoryTheory.Limits.prodComparisonNatIso F A).hom = CategoryTheory.Limits.prodComparisonNatTrans F A
• CategoryTheory.Limits.prodComparisonNatIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.ProdComparison
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : (CategoryTheory.Limits.prodComparisonNatIso F A).inv = (CategoryTheory.asIso { app := fun B => CategoryTheory.Limits.prodComparison F A B, naturality := ⋯ }).inv
• CategoryTheory.Limits.preservesBinaryProducts_of_isIso_prodComparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] [i : ∀ {X Y : C}, CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison G X Y)] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G
• CategoryTheory.Limits.hasBinaryProducts_of_hasBinaryBiproducts 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Limits.HasBinaryProducts C
• CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Limits.HasBinaryBiproducts C
• CategoryTheory.Functor.additive_of_preserves_binary_products 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [F.PreservesZeroMorphisms] : F.Additive
• hasBinaryProducts_of_hasTerminal_and_pullbacks 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Limits.HasBinaryProducts C
• CategoryTheory.prodComonad 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Comonad C
• CategoryTheory.coalgebraEquivOver 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.prodComonad X).Coalgebra ≌ CategoryTheory.Over X
• CategoryTheory.coalgebraToOver 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Functor (CategoryTheory.prodComonad X).Coalgebra (CategoryTheory.Over X)
• CategoryTheory.overToCoalgebra 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.prodComonad X).Coalgebra
• CategoryTheory.prodComonad_obj 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (Y : C) : (CategoryTheory.prodComonad X).obj Y = (X ⨯ Y)
• CategoryTheory.overToCoalgebra_obj_A 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (f : CategoryTheory.Over X) : ((CategoryTheory.overToCoalgebra X).obj f).A = f.left
• CategoryTheory.coalgebraEquivOver_functor 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.coalgebraEquivOver X).functor = CategoryTheory.coalgebraToOver X
• CategoryTheory.coalgebraEquivOver_inverse 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.coalgebraEquivOver X).inverse = CategoryTheory.overToCoalgebra X
• CategoryTheory.prodComonad_ε_app 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (x✝ : C) : (CategoryTheory.prodComonad X).ε.app x✝ = CategoryTheory.Limits.prod.snd
• CategoryTheory.prodComonad_map 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (CategoryTheory.prodComonad X).map g = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g
• CategoryTheory.overToCoalgebra_obj_a 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (f : CategoryTheory.Over X) : ((CategoryTheory.overToCoalgebra X).obj f).a = CategoryTheory.Limits.prod.lift f.hom (CategoryTheory.CategoryStruct.id f.left)
• CategoryTheory.coalgebraToOver_obj 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (A : (CategoryTheory.prodComonad X).Coalgebra) : (CategoryTheory.coalgebraToOver X).obj A = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp A.a CategoryTheory.Limits.prod.fst)
• CategoryTheory.prodComonad_δ_app 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (x✝ : C) : (CategoryTheory.prodComonad X).δ.app x✝ = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ x✝))
• CategoryTheory.overToCoalgebra_map_f 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {X✝ Y✝ : CategoryTheory.Over X} (g : X✝ ⟶ Y✝) : ((CategoryTheory.overToCoalgebra X).map g).f = CategoryTheory.Over.Hom.left g
• CategoryTheory.coalgebraEquivOver_counitIso 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.coalgebraEquivOver X).counitIso = CategoryTheory.NatIso.ofComponents (fun f => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl (((CategoryTheory.overToCoalgebra X).comp (CategoryTheory.coalgebraToOver X)).obj f).left) ⋯) ⋯
• 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.coalgebraEquivOver_unitIso 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.coalgebraEquivOver X).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Comonad.Coalgebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.prodComonad X).Coalgebra).obj A).A) ⋯) ⋯
• CategoryTheory.Over.star 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Functor C (CategoryTheory.Over X)
• CategoryTheory.Over.instIsLeftAdjointForget 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.Over.forget X).IsLeftAdjoint
• CategoryTheory.Over.instIsRightAdjointStar 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.Over.star X).IsRightAdjoint
• CategoryTheory.Over.forgetAdjStar 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Over.forget X ⊣ CategoryTheory.Over.star X
• CategoryTheory.Over.star_obj_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (X✝ : C) : ((CategoryTheory.Over.star X).obj X✝).left = (X ⨯ X✝)
• 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.forgetAdjStar_counit_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y : C) : (CategoryTheory.Over.forgetAdjStar X).counit.app Y = CategoryTheory.Limits.prod.snd
• CategoryTheory.Over.star_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (X✝ : C) : ((CategoryTheory.Over.star X).obj X✝).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ X✝))) CategoryTheory.Limits.prod.fst
• CategoryTheory.Over.star_map_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Over.star X).map f).left = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f
• CategoryTheory.Over.forgetAdjStar_unit_app_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : CategoryTheory.Over X) : CategoryTheory.Over.Hom.left ((CategoryTheory.Over.forgetAdjStar X).unit.app Y) = CategoryTheory.Limits.prod.lift Y.hom (CategoryTheory.CategoryStruct.id Y.left)
• 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.prod_preservesConnectedLimits 📋 Mathlib.CategoryTheory.Limits.Connected
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] [CategoryTheory.IsConnected J] (X : C) : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Limits.prod.functor.obj X)
• CategoryTheory.ProdPreservesConnectedLimits.forgetCone 📋 Mathlib.CategoryTheory.Limits.Connected
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {X : C} {K : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))) : CategoryTheory.Limits.Cone K
• CategoryTheory.ProdPreservesConnectedLimits.γ₂ 📋 Mathlib.CategoryTheory.Limits.Connected
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) : K.comp (CategoryTheory.Limits.prod.functor.obj X) ⟶ K
• CategoryTheory.ProdPreservesConnectedLimits.γ₁ 📋 Mathlib.CategoryTheory.Limits.Connected
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) : K.comp (CategoryTheory.Limits.prod.functor.obj X) ⟶ (CategoryTheory.Functor.const J).obj X
• CategoryTheory.ProdPreservesConnectedLimits.forgetCone_pt 📋 Mathlib.CategoryTheory.Limits.Connected
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {X : C} {K : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))) : (CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).pt = s.pt
• CategoryTheory.ProdPreservesConnectedLimits.γ₂_app 📋 Mathlib.CategoryTheory.Limits.Connected
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) (x✝ : J) : (CategoryTheory.ProdPreservesConnectedLimits.γ₂ X).app x✝ = CategoryTheory.Limits.prod.snd
• CategoryTheory.ProdPreservesConnectedLimits.γ₁_app 📋 Mathlib.CategoryTheory.Limits.Connected
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) (x✝ : J) : (CategoryTheory.ProdPreservesConnectedLimits.γ₁ X).app x✝ = CategoryTheory.Limits.prod.fst
• CategoryTheory.ProdPreservesConnectedLimits.forgetCone_π 📋 Mathlib.CategoryTheory.Limits.Connected
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : Type v₂} [CategoryTheory.SmallCategory J] {X : C} {K : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))) : (CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).π = CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.ProdPreservesConnectedLimits.γ₂ X)
• CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasFiniteProducts C
• CategoryTheory.CartesianMonoidalCategory.tensorLeftIsoProd 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) : CategoryTheory.MonoidalCategory.tensorLeft X ≅ CategoryTheory.Limits.prod.functor.obj X
• CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Limits.HasEqualizers C
• CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.constructEqualizer 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : C
• CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerConeIsLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone F)
• CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.constructEqualizer F ⟶ F.obj CategoryTheory.Limits.WalkingParallelPair.zero
• CategoryTheory.Limits.preservesEqualizers_of_preservesPullbacks_and_binaryProducts 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G] : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G
• CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) : CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst F = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.zero)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.zero)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
• CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers 📋 Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasPullbacks C
• CategoryTheory.FunctorCategory.prod_preservesColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v₁, u} C] {D : Type u₂} [CategoryTheory.Category.{u, u₂} D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasColimits D] [∀ (X : D), CategoryTheory.Limits.PreservesColimits (CategoryTheory.Limits.prod.functor.obj X)] (F : CategoryTheory.Functor C D) : CategoryTheory.Limits.PreservesColimits (CategoryTheory.Limits.prod.functor.obj F)
• CategoryTheory.GrothendieckTopology.coverPreserving_over_star 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u'} [CategoryTheory.Category.{v_1, u'} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} (X : C) : CategoryTheory.CoverPreserving J (J.over X) (CategoryTheory.Over.star X)
• CategoryTheory.GrothendieckTopology.instIsContinuousOverStarOver 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u'} [CategoryTheory.Category.{v_1, u'} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} (X : C) : (CategoryTheory.Over.star X).IsContinuous J (J.over X)
• SheafOfModules.pushforwardOver 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C) : R ⟶ ((CategoryTheory.Over.star x).sheafPushforwardContinuous RingCat J (J.over x)).obj (R.over x)
• SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C) : (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over x))).IsLeftAdjoint
• SheafOfModules.overPushforwardOverAdj 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C) : SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over x)) ⊣ SheafOfModules.pushforward (SheafOfModules.pushforwardOver x)
• SheafOfModules.GeneratingSections.localGeneratorsData 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) : M.LocalGeneratorsData
• SheafOfModules.GeneratingSections.localGeneratorsData_I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) : G.localGeneratorsData.I = C
• SheafOfModules.GeneratingSections.localGeneratorsData_X 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (a : C) : G.localGeneratorsData.X a = id a
• SheafOfModules.GeneratingSections.localGeneratorsData_generators 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (x : C) : G.localGeneratorsData.generators x = G.map (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over x))) (CategoryTheory.Iso.refl (SheafOfModules.unit (R.over x)))
• SheafOfModules.Presentation.isQuasicoherent 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) : M.IsQuasicoherent
• SheafOfModules.Presentation.quasicoherentData 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) : M.QuasicoherentData
• SheafOfModules.Presentation.quasicoherentData_I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) : P.quasicoherentData.I = C
• SheafOfModules.Presentation.quasicoherentData_X 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) (a : C) : P.quasicoherentData.X a = id a
• SheafOfModules.isQuasicoherent_over 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] (M : SheafOfModules R) (X : C) [M.IsQuasicoherent] : (M.over X).IsQuasicoherent
• SheafOfModules.Presentation.quasicoherentData_presentation 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) (x : C) : P.quasicoherentData.presentation x = P.map (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over x))) (CategoryTheory.Iso.refl (SheafOfModules.unit (R.over x)))
• SheafOfModules.instIsLocallyFreeFree 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (I : Type u) : (SheafOfModules.free I).IsLocallyFree
• SheafOfModules.instIsLocallyFreeDataLocalGeneratorsDataGeneratingSections 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (I : Type u) : (SheafOfModules.free.generatingSections I).localGeneratorsData.IsLocallyFreeData
• Preorder.instHasBinaryProducts 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [SemilatticeInf C] : CategoryTheory.Limits.HasBinaryProducts C
• Preorder.semilatticeInfOfHasBinaryProducts 📋 Mathlib.CategoryTheory.Limits.Preorder
  (C : Type u) [PartialOrder C] [CategoryTheory.Limits.HasBinaryProducts C] : SemilatticeInf C
• CategoryTheory.Limits.CompleteLattice.instHasBinaryProductsOfOrderTop 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} [SemilatticeInf α] [OrderTop α] : CategoryTheory.Limits.HasBinaryProducts α
• CategoryTheory.Over.ConstructProducts.over_binaryProduct_of_pullback 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {B : C} : CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over B)
• HomotopicalAlgebra.PathObject.instIsGoodSymmOfRespectsIsoFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProducts C] [HomotopicalAlgebra.CategoryWithFibrations C] [P.IsGood] [(HomotopicalAlgebra.fibrations C).RespectsIso] : P.symm.IsGood
• HomotopicalAlgebra.PathObject.instIsVeryGoodSymmOfRespectsIsoFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.CategoryWithCofibrations C] [(HomotopicalAlgebra.fibrations C).RespectsIso] [CategoryTheory.Limits.HasBinaryProducts C] [P.IsVeryGood] : P.symm.IsVeryGood
• HomotopicalAlgebra.PrepathObject.symm_p 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A) [CategoryTheory.Limits.HasBinaryProducts C] : P.symm.p = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom
• HomotopicalAlgebra.PathObject.symm_p 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProducts C] : P.symm.p = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom
• HomotopicalAlgebra.PrepathObject.symm_p_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A) [CategoryTheory.Limits.HasBinaryProducts C] {Z : C} (h : A ⨯ A ⟶ Z) : CategoryTheory.CategoryStruct.comp P.symm.p h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom) h
• HomotopicalAlgebra.PathObject.symm_p_assoc 📋 Mathlib.AlgebraicTopology.ModelCategory.PathObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A) [CategoryTheory.Limits.HasBinaryProducts C] {Z : C} (h : A ⨯ A ⟶ Z) : CategoryTheory.CategoryStruct.comp P.symm.p h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom) h
• CategoryTheory.Functor.relativelyRepresentable.of_diag 📋 Mathlib.CategoryTheory.MorphismProperty.Representable
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D} (h : F.relativelyRepresentable (CategoryTheory.Limits.diag X)) ⦃a : C⦄ (g : F.obj a ⟶ X) : F.relativelyRepresentable g
• CategoryTheory.Functor.relativelyRepresentable.diag_of_map_from_obj 📋 Mathlib.CategoryTheory.MorphismProperty.Representable
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] {X : D} (h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g) : F.relativelyRepresentable (CategoryTheory.Limits.diag X)
• CategoryTheory.Functor.relativelyRepresentable.diag_iff 📋 Mathlib.CategoryTheory.MorphismProperty.Representable
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D} [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] : F.relativelyRepresentable (CategoryTheory.Limits.diag X) ↔ ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
• CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal 📋 Mathlib.CategoryTheory.MorphismProperty.Representable
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D} {a : C} [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] (g : F.obj a ⟶ CategoryTheory.Limits.pullback (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from X)) : F.relativelyRepresentable (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id (F.obj a)) (CategoryTheory.CategoryStruct.id (F.obj a)) ⋯)
• CategoryTheory.PreGaloisCategory.instHasBinaryProducts 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasBinaryProducts C
• CategoryTheory.Limits.hasWeakPullbacks_of_hasBinaryProducts_of_hasWeakEqualizers 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasWeakEqualizers C] : CategoryTheory.Limits.HasWeakPullbacks C

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