Loogle!

Result

Found 25 declarations mentioning CategoryTheory.Limits.Pi.map.

• CategoryTheory.Limits.Pi.map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g
• CategoryTheory.Limits.Pi.map_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} [CategoryTheory.Limits.HasProduct f] : (CategoryTheory.Limits.Pi.map fun a => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∏ᶜ f)
• CategoryTheory.Limits.Pi.map_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) [∀ (i : β), CategoryTheory.Mono (p i)] : CategoryTheory.Mono (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.Pi.map'_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : α → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : α) → f b ⟶ g b) : CategoryTheory.Limits.Pi.map' id p = CategoryTheory.Limits.Pi.map p
• CategoryTheory.Limits.Pi.map_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), CategoryTheory.IsIso (p b)] : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.Pi.map_comp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h : α → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h a) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map q') = CategoryTheory.Limits.Pi.map fun a => CategoryTheory.CategoryStruct.comp (q a) (q' a)
• CategoryTheory.Limits.Pi.map'_comp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g h : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (q' : (b : β) → g b ⟶ h b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.map q') = CategoryTheory.Limits.Pi.map' p fun b => CategoryTheory.CategoryStruct.comp (q b) (q' b)
• CategoryTheory.Limits.Pi.map_comp_map' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : α → C} {h : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (p : β → α) (q : (a : α) → f a ⟶ g a) (q' : (b : β) → g (p b) ⟶ h b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map' p q') = CategoryTheory.Limits.Pi.map' p fun b => CategoryTheory.CategoryStruct.comp (q (p b)) (q' b)
• CategoryTheory.Limits.piConst_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (n : Type wᵒᵖ) : (CategoryTheory.Limits.piConst.map f).app n = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.Limits.Pi.map_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Epi (p j)] : CategoryTheory.Epi (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset.eq_1 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteProducts C] : CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α = { obj := CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj, map := fun {X Y} β => { app := fun x => CategoryTheory.Limits.Pi.map fun x_1 => β.app ↑x_1, naturality := ⋯ }, map_id := ⋯, map_comp := ⋯ }
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_map_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteProducts C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.Discrete α) C} (β : X✝ ⟶ Y✝) (x✝ : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : ((CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).map β).app x✝ = CategoryTheory.Limits.Pi.map fun x => β.app ↑x
• CategoryTheory.Limits.Types.pi_map_π_apply 📋 Mathlib.CategoryTheory.Limits.Types.Shapes
  {β : Type v} [Small.{u, v} β] {f g : β → Type u} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ᶜ f) : CategoryTheory.Limits.Pi.π g b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π f b x)
• CategoryTheory.Limits.Types.pi_map_π_apply' 📋 Mathlib.CategoryTheory.Limits.Types.Shapes
  {β : Type v} {f g : β → Type v} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ᶜ f) : CategoryTheory.Limits.Pi.π g b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π f b x)
• CategoryTheory.Pretriangulated.productTriangle_mor₁ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).mor₁ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₁
• CategoryTheory.Pretriangulated.productTriangle_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).mor₂ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₂
• CategoryTheory.Pretriangulated.productTriangle_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).mor₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map fun j => (T j).mor₃) (CategoryTheory.inv (CategoryTheory.Limits.piComparison (CategoryTheory.shiftFunctor C 1) fun j => (T j).obj₁))
• CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1) [W.RespectsIso] (hW : ∀ (X₁ X₂ : J → C) [inst : CategoryTheory.Limits.HasProduct X₁] [inst_1 : CategoryTheory.Limits.HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Pi.map f)) : W.IsStableUnderProductsOfShape J
• CategoryTheory.instHasLiftingPropertyMap 📋 Mathlib.CategoryTheory.LiftingProperties.Limits
  {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {J : Type u_2} {A B : J → C} [CategoryTheory.Limits.HasProduct A] [CategoryTheory.Limits.HasProduct B] (f : (j : J) → A j ⟶ B j) {X Y : C} (p : X ⟶ Y) [∀ (j : J), CategoryTheory.HasLiftingProperty p (f j)] : CategoryTheory.HasLiftingProperty p (CategoryTheory.Limits.Pi.map f)
• CategoryTheory.Limits.pointwiseProduct_map 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → CategoryTheory.Category.{v₁, u₁} (I i)] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] (F : (i : α) → CategoryTheory.Functor (I i) C) {X✝ Y✝ : (i : α) → I i} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.pointwiseProduct F).map f = CategoryTheory.Limits.Pi.map fun s => (F s).map (f s)
• CategoryTheory.Limits.coconePointwiseProduct_ι_app 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → CategoryTheory.Category.{v₁, u₁} (I i)] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] (F : (i : α) → CategoryTheory.Functor (I i) C) [∀ (i : α), CategoryTheory.Limits.HasColimitsOfShape (I i) C] (k : (i : α) → I i) : (CategoryTheory.Limits.coconePointwiseProduct F).ι.app k = CategoryTheory.Limits.Pi.map fun s => CategoryTheory.Limits.colimit.ι (F s) (k s)
• CategoryTheory.Limits.Pi.map_eq_prod_map 📋 Mathlib.CategoryTheory.Limits.Shapes.PiProd
  {C : Type u_1} {I : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] {X Y : I → C} (f : (i : I) → X i ⟶ Y i) (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => Y ↑i] [CategoryTheory.Limits.HasProduct fun i => Y ↑i] [(i : I) → Decidable (P i)] : CategoryTheory.Limits.Pi.map f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.Pi.map fun i => f ↑i) (CategoryTheory.Limits.Pi.map fun i => f ↑i)) ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).inv)
• CategoryTheory.Limits.SequentialProduct.cone_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
  {C : Type u_1} {M N : ℕ → C} [CategoryTheory.Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [CategoryTheory.Limits.HasProductsOfShape ℕ C] (n : ℕ) : (CategoryTheory.Limits.SequentialProduct.cone f).π.app (Opposite.op n) = CategoryTheory.Limits.Pi.map fun m => if h : m < n then CategoryTheory.eqToHom ⋯ else CategoryTheory.CategoryStruct.comp (f m) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Limits.SequentialProduct.functorMap.eq_1 📋 Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
  {C : Type u_1} {M N : ℕ → C} [CategoryTheory.Category.{u_2, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [CategoryTheory.Limits.HasProductsOfShape ℕ C] (n : ℕ) : CategoryTheory.Limits.SequentialProduct.functorMap f n = CategoryTheory.Limits.Pi.map fun m => if h : m < n then CategoryTheory.eqToHom ⋯ else if h' : m < n + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (f m) (CategoryTheory.eqToHom ⋯)) else CategoryTheory.eqToHom ⋯
• LightCondensed.instEpiLightCondModMapNat 📋 Mathlib.Condensed.Light.Epi
  {R : Type u} [Ring R] {M N : ℕ → LightCondMod R} (f : (n : ℕ) → M n ⟶ N n) [∀ (n : ℕ), CategoryTheory.Epi (f n)] : CategoryTheory.Epi (CategoryTheory.Limits.Pi.map f)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 19971e9 serving mathlib revision 40fea08