Loogle!

Result

Found 163 declarations mentioning CategoryTheory.Limits.HasProduct.

CategoryTheory.Limits.HasProduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) : Prop
CategoryTheory.Limits.piObj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) [CategoryTheory.Limits.HasProduct f] : C
CategoryTheory.Limits.hasProduct_unique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Nonempty β] [Subsingleton β] (f : β → C) : CategoryTheory.Limits.HasProduct f
CategoryTheory.Limits.Pi.π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) : ∏ᶜ f ⟶ f b
CategoryTheory.Limits.Pi.cone 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : CategoryTheory.Limits.Cone X
CategoryTheory.Limits.Pi.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) : P ⟶ ∏ᶜ f
CategoryTheory.Limits.productIsProduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) [CategoryTheory.Limits.HasProduct f] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (∏ᶜ f) (CategoryTheory.Limits.Pi.π f))
CategoryTheory.Limits.productIsProduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Pi.cone X)
CategoryTheory.Limits.hasProduct_of_equiv_of_iso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : α → C) (g : β → C) [CategoryTheory.Limits.HasProduct f] (e : β ≃ α) (iso : (j : β) → g j ≅ f (e j)) : CategoryTheory.Limits.HasProduct g
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' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g
CategoryTheory.Limits.instHasProductSigmaFstSndOfPiObj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i] : CategoryTheory.Limits.HasProduct fun p => g p.fst p.snd
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.cone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Pi.cone X).pt = ∏ᶜ fun j => X.obj { as := j }
CategoryTheory.Limits.Pi.map'_id_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' id fun a => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∏ᶜ f)
CategoryTheory.Limits.Pi.whiskerEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] : ∏ᶜ f ≅ ∏ᶜ g
CategoryTheory.Limits.Pi.isoLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] : (∏ᶜ fun j => X.obj { as := j }) ≅ CategoryTheory.Limits.limit X
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.piComparison 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] : G.obj (∏ᶜ f) ⟶ ∏ᶜ fun b => G.obj (f b)
CategoryTheory.Limits.Pi.lift_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C} [CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift p) (CategoryTheory.Limits.Pi.π f b) = p b
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.instMonoLiftπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] [CategoryTheory.Limits.HasProduct F.obj] : CategoryTheory.Mono (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.limit.π F))
CategoryTheory.Limits.Fan.isLimitOfIsIsoPiLift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] (c : CategoryTheory.Limits.Fan f) [hc : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)] : CategoryTheory.Limits.IsLimit c
CategoryTheory.Limits.Pi.reindex 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] : ∏ᶜ f ∘ ⇑ε ≅ ∏ᶜ f
CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] (c : CategoryTheory.Limits.Fan f) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)
CategoryTheory.Limits.Pi.π_comp_eqToHom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C) [CategoryTheory.Limits.HasProduct f] {j j' : J} (w : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.Limits.Pi.π f j'
CategoryTheory.Limits.piPiIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i] : (∏ᶜ fun i => ∏ᶜ g i) ≅ ∏ᶜ fun p => g p.fst p.snd
CategoryTheory.Limits.Pi.lift_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C} [CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) {Z : C} (h : f b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) = CategoryTheory.CategoryStruct.comp (p b) h
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) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map p) (CategoryTheory.Limits.Pi.π g b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (p b)
CategoryTheory.Limits.Pi.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ᶜ f) (h : ∀ (b : β), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Pi.π f b)) : g₁ = g₂
CategoryTheory.Limits.Pi.π_comp_eqToHom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C) [CategoryTheory.Limits.HasProduct f] {j j' : J} (w : j = j') {Z : C} (h : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j') h
CategoryTheory.Limits.Pi.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] {X : C} {g₁ g₂ : X ⟶ ∏ᶜ f} : g₁ = g₂ ↔ ∀ (b : β), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Pi.π f b)
CategoryTheory.Limits.Pi.map'_comp_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.π g b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (p b)) (q b)
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_π_assoc 📋 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) (b : β) {Z : C} (h : g b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (CategoryTheory.CategoryStruct.comp (p b) h)
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.piComparison_comp_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f) (CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b) = G.map (CategoryTheory.Limits.Pi.π f b)
CategoryTheory.Limits.Pi.whiskerEquiv_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] : (CategoryTheory.Limits.Pi.whiskerEquiv e w).inv = CategoryTheory.Limits.Pi.map' ⇑e fun j => (w j).hom
CategoryTheory.Limits.Pi.map'_comp_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (b : β) {Z : C} (h : g b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (p b)) (CategoryTheory.CategoryStruct.comp (q b) h)
CategoryTheory.Limits.Pi.map'_comp_map' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {α : Type w₂} {γ : Type w₃} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} {h : γ → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (p : β → α) (p' : γ → β) (q : (b : β) → f (p b) ⟶ g b) (q' : (c : γ) → g (p' c) ⟶ h c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.map' p' q') = CategoryTheory.Limits.Pi.map' (p ∘ p') fun c => CategoryTheory.CategoryStruct.comp (q (p' c)) (q' c)
CategoryTheory.Limits.Pi.map'_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] {p p' : β → α} {q : (b : β) → f (p b) ⟶ g b} {q' : (b : β) → f (p' b) ⟶ g b} (hp : p = p') (hq : ∀ (b : β), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (q b) = q' b) : CategoryTheory.Limits.Pi.map' p q = CategoryTheory.Limits.Pi.map' p' q'
CategoryTheory.Limits.Pi.isoLimit_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) = CategoryTheory.Limits.limit.π X { as := j }
CategoryTheory.Limits.map_lift_piComparison 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (P : C) (g : (j : β) → P ⟶ f j) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.lift g)) (CategoryTheory.Limits.piComparison G f) = CategoryTheory.Limits.Pi.lift fun j => G.map (g j)
CategoryTheory.Limits.Pi.isoLimit_hom_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom (CategoryTheory.Limits.limit.π X { as := j }) = CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j
CategoryTheory.Limits.Pi.cone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Pi.cone X).π = CategoryTheory.Discrete.natTrans fun x => CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) x.as
CategoryTheory.Limits.Pi.lift_π_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C} [CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) {F : C → C → Type uF} {carrier : C → Type w_1} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier P) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.lift p)) x) = (CategoryTheory.ConcreteCategory.hom (p b)) x
CategoryTheory.Limits.piComparison_comp_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (b : β) {Z : D} (h : G.obj (f b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.π f b)) h
CategoryTheory.Limits.map_lift_piComparison_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (P : C) (g : (j : β) → P ⟶ f j) {Z : D} (h : (∏ᶜ fun b => G.obj (f b)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.lift g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piComparison G f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift fun j => G.map (g j)) h
CategoryTheory.Limits.Pi.isoLimit_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h
CategoryTheory.Limits.Pi.reindex_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).inv (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) = CategoryTheory.Limits.Pi.π f (ε b)
CategoryTheory.Limits.Pi.isoLimit_hom_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) h
CategoryTheory.Limits.Pi.reindex_hom_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).hom (CategoryTheory.Limits.Pi.π f (ε b)) = CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b
CategoryTheory.Limits.piPiIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i] : (CategoryTheory.Limits.piPiIso f g).inv = CategoryTheory.Limits.Pi.lift fun i => CategoryTheory.Limits.Pi.lift fun x => CategoryTheory.Limits.Pi.π (fun p => g p.fst p.snd) ⟨i, x⟩
CategoryTheory.Limits.Pi.map_π_apply 📋 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) (b : β) {F : C → C → Type uF} {carrier : C → Type w_1} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (∏ᶜ f)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map p)) x) = (CategoryTheory.ConcreteCategory.hom (p b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
CategoryTheory.Limits.Pi.reindex_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) {Z : C} (h : (f ∘ ⇑ε) b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (ε b)) h
CategoryTheory.Limits.Pi.reindex_hom_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β) {Z : C} (h : f (ε b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (ε b)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b) h
CategoryTheory.Limits.piPiIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i] : (CategoryTheory.Limits.piPiIso f g).hom = CategoryTheory.Limits.Pi.lift fun x => match x with | ⟨i, x⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => ∏ᶜ g i) i) (CategoryTheory.Limits.Pi.π (g i) x)
CategoryTheory.Limits.Pi.whiskerEquiv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] : (CategoryTheory.Limits.Pi.whiskerEquiv e w).hom = CategoryTheory.Limits.Pi.map' ⇑e.symm fun k => CategoryTheory.CategoryStruct.comp (w (e.symm k)).inv (CategoryTheory.eqToHom ⋯)
CategoryTheory.Limits.piComparison_comp_π_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
{β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] (b : β) {F : D → D → Type uF} {carrier : D → Type w_1} {instFunLike : (X Y : D) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory D F] (x : carrier (G.obj (∏ᶜ f))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun b => G.obj (f b)) b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.piComparison G f)) x) = (CategoryTheory.ConcreteCategory.hom (G.map (CategoryTheory.Limits.Pi.π f b))) x
CategoryTheory.Limits.Pi.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) : f b ⟶ ∏ᶜ f
CategoryTheory.Limits.instMonoι_1 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) : CategoryTheory.Mono (CategoryTheory.Limits.Pi.ι f b)
CategoryTheory.Limits.Pi.ι_π_eq_id 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.id (f b)
CategoryTheory.Limits.Pi.ι_π_eq_id_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) {Z : C} (h : f b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) = h
CategoryTheory.Limits.Pi.ι_π_of_ne 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] {b c : β} (h : b ≠ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f c) = 0
CategoryTheory.Limits.Pi.ι_π_of_ne_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] {b c : β} (h : b ≠ c) {Z : C} (h✝ : f c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f c) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
CategoryTheory.Limits.Pi.ι_π 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b c : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f c) = if h : b = c then CategoryTheory.eqToHom ⋯ else 0
CategoryTheory.Limits.Pi.ι_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b c : β) {Z : C} (h : f c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f c) h) = CategoryTheory.CategoryStruct.comp (if h : b = c then CategoryTheory.eqToHom ⋯ else 0) h
CategoryTheory.Limits.hasProduct_of_hasBiproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
{J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.HasProduct F
CategoryTheory.Limits.PreservesProduct.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : G.obj (∏ᶜ f) ≅ ∏ᶜ fun j => G.obj (f j)
CategoryTheory.Limits.instIsIsoPiComparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)
CategoryTheory.Limits.PreservesProduct.of_iso_comparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G
CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj (∏ᶜ f)) fun j => G.map (CategoryTheory.Limits.Pi.π f j))
CategoryTheory.Limits.PreservesProduct.iso_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : (CategoryTheory.Limits.PreservesProduct.iso G f).hom = CategoryTheory.Limits.piComparison G f
CategoryTheory.Limits.inv_piComparison_comp_map_π 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.piComparison G f)) (G.map (CategoryTheory.Limits.Pi.π f j)) = CategoryTheory.Limits.Pi.π (fun x => G.obj (f x)) j
CategoryTheory.Limits.inv_piComparison_comp_map_π_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)] (j : J) {Z : D} (h : G.obj (f j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.piComparison G f)) (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Pi.π f j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => G.obj (f x)) j) h
CategoryTheory.Limits.HasBiproduct.of_hasProduct 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Finite J] (f : J → C) [CategoryTheory.Limits.HasProduct f] : CategoryTheory.Limits.HasBiproduct f
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.ObjectProperty.prop_pi 📋 Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u_3} [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J)] (X : J → C) [CategoryTheory.Limits.HasProduct X] (hF : ∀ (j : J), P (X j)) : P (∏ᶜ X)
ModuleCat.piIsoPi 📋 Mathlib.Algebra.Category.ModuleCat.Products
{R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] : ∏ᶜ Z ≅ ModuleCat.of R ((i : ι) → ↑(Z i))
ModuleCat.piIsoPi_hom_ker_subtype 📋 Mathlib.Algebra.Category.ModuleCat.Products
{R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (ModuleCat.piIsoPi Z).hom (ModuleCat.ofHom (LinearMap.proj i)) = CategoryTheory.Limits.Pi.π Z i
ModuleCat.piIsoPi_inv_kernel_ι 📋 Mathlib.Algebra.Category.ModuleCat.Products
{R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (ModuleCat.piIsoPi Z).inv (CategoryTheory.Limits.Pi.π Z i) = ModuleCat.ofHom (LinearMap.proj i)
ModuleCat.piIsoPi_inv_kernel_ι_apply 📋 Mathlib.Algebra.Category.ModuleCat.Products
{R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) (x : (i : ι) → ↑(Z i)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i)) ((CategoryTheory.ConcreteCategory.hom (ModuleCat.piIsoPi Z).inv) x) = x i
ModuleCat.piIsoPi_hom_ker_subtype_apply 📋 Mathlib.Algebra.Category.ModuleCat.Products
{R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) (x : ↑(∏ᶜ Z)) : (CategoryTheory.ConcreteCategory.hom (ModuleCat.piIsoPi Z).hom) x i = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i)) x
CategoryTheory.Injective.instPiObj 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Type v} (c : β → C) [CategoryTheory.Limits.HasProduct c] [∀ (b : β), CategoryTheory.Injective (c b)] : CategoryTheory.Injective (∏ᶜ c)
CategoryTheory.Limits.instHasCoproductOppositeOp 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasProduct Z] : CategoryTheory.Limits.HasCoproduct fun x => Opposite.op (Z x)
CategoryTheory.Limits.instHasProductOppositeOp 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasCoproduct Z] : CategoryTheory.Limits.HasProduct fun x => Opposite.op (Z x)
CategoryTheory.Limits.instHasColimitOppositeDiscreteOpFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasProduct Z] : CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor Z).op
CategoryTheory.Limits.opProductIsoCoproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [CategoryTheory.Limits.HasProduct Z] : Opposite.op (∏ᶜ Z) ≅ ∐ fun x => Opposite.op (Z x)
CategoryTheory.Limits.instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasProduct Z] : CategoryTheory.Limits.HasColimit ((CategoryTheory.Discrete.opposite α).inverse.comp (CategoryTheory.Discrete.functor Z).op)
CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [CategoryTheory.Limits.HasProduct Z] (b : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π Z b).op (CategoryTheory.Limits.opProductIsoCoproduct Z).hom = CategoryTheory.Limits.Sigma.ι (fun x => Opposite.op (Z x)) b
CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasProduct Z] {X : C} (π : (a : α) → X ⟶ Z a) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct Z).inv (CategoryTheory.Limits.Pi.lift π).op = CategoryTheory.Limits.Sigma.desc fun a => (π a).op
CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
{C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] (f : α → C) [CategoryTheory.Limits.HasProduct f] : CategoryTheory.Limits.Cone (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj (CategoryTheory.Discrete.functor f))
CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
{C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] (f : α → C) [CategoryTheory.Limits.HasProduct f] : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).pt = ∏ᶜ f
CategoryTheory.Limits.ProductsFromFiniteCofiltered.isLimitFiniteSubproductsCone 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
{C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] (f : α → C) [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C] [CategoryTheory.Limits.HasProduct f] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f)
CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
{C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] (f : α → C) [CategoryTheory.Limits.HasProduct f] (S : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).π.app S = CategoryTheory.Limits.Pi.lift fun s => CategoryTheory.Limits.Pi.π f (↑s).as
CategoryTheory.isCoseparator_pi_of_isCoseparator 📋 Mathlib.CategoryTheory.Generator.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} (f : β → C) [CategoryTheory.Limits.HasProduct f] (b : β) (hb : CategoryTheory.IsCoseparator (f b)) : CategoryTheory.IsCoseparator (∏ᶜ f)
CategoryTheory.isCoseparator_pi 📋 Mathlib.CategoryTheory.Generator.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} (f : β → C) [CategoryTheory.Limits.HasProduct f] : CategoryTheory.IsCoseparator (∏ᶜ f) ↔ (CategoryTheory.ObjectProperty.ofObj f).IsCoseparating
CategoryTheory.ObjectProperty.productTo 📋 Mathlib.CategoryTheory.Generator.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) (X : C) [CategoryTheory.Limits.HasProduct (P.productToFamily X)] : X ⟶ ∏ᶜ P.productToFamily X
CategoryTheory.ObjectProperty.IsCoseparating.mono_productTo 📋 Mathlib.CategoryTheory.Generator.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} (hP : P.IsCoseparating) (X : C) [CategoryTheory.Limits.HasProduct (P.productToFamily X)] : CategoryTheory.Mono (P.productTo X)
CategoryTheory.ObjectProperty.isCoseparating_iff_mono 📋 Mathlib.CategoryTheory.Generator.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) [∀ (X : C), CategoryTheory.Limits.HasProduct (P.productToFamily X)] : P.IsCoseparating ↔ ∀ (X : C), CategoryTheory.Mono (P.productTo X)
CategoryTheory.ObjectProperty.πProductTo 📋 Mathlib.CategoryTheory.Generator.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) {X : C} [CategoryTheory.Limits.HasProduct (P.productToFamily X)] {Y : C} (f : X ⟶ Y) (hY : P Y) : ∏ᶜ P.productToFamily X ⟶ Y
CategoryTheory.isCoseparator_iff_mono 📋 Mathlib.CategoryTheory.Generator.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : C) [∀ (A : C), CategoryTheory.Limits.HasProduct fun x => G] : CategoryTheory.IsCoseparator G ↔ ∀ (A : C), CategoryTheory.Mono (CategoryTheory.Limits.Pi.lift fun f => f)
CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
CategoryTheory.Limits.MulticospanIndex.fstPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : ∏ᶜ I.left ⟶ ∏ᶜ I.right
CategoryTheory.Limits.MulticospanIndex.sndPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : ∏ᶜ I.left ⟶ ∏ᶜ I.right
CategoryTheory.Limits.Multiequalizer.ιPi 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.multiequalizer I ⟶ ∏ᶜ I.left
CategoryTheory.Limits.Multiequalizer.instMonoιPi 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Mono (CategoryTheory.Limits.Multiequalizer.ιPi I)
CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (x : CategoryTheory.Limits.WalkingParallelPair) : I.parallelPairDiagram.obj x = CategoryTheory.Limits.parallelPair.parallelPairObj (∏ᶜ I.left) (∏ᶜ I.right) x
CategoryTheory.Limits.Multiequalizer.instHasEqualizerFstPiMapSndPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.HasEqualizer I.fstPiMap I.sndPiMap
CategoryTheory.Limits.Multiequalizer.isoEqualizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.multiequalizer I ≅ CategoryTheory.Limits.equalizer I.fstPiMap I.sndPiMap
CategoryTheory.Limits.Multiequalizer.ιPi_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : J.L) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.Limits.Pi.π I.left a) = CategoryTheory.Limits.Multiequalizer.ι I a
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap
CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {X✝ Y✝ : CategoryTheory.Limits.WalkingParallelPair} (h : X✝ ⟶ Y✝) : I.parallelPairDiagram.map h = CategoryTheory.Limits.parallelPair.parallelPairHom I.fstPiMap I.sndPiMap h
CategoryTheory.Limits.MulticospanIndex.fstPiMap_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) : CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.fst b)) (I.fst b)
CategoryTheory.Limits.MulticospanIndex.sndPiMap_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) : CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.snd b)) (I.snd b)
CategoryTheory.Limits.Multiequalizer.ιPi_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : J.L) {Z : C} (h : I.left a ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left a) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h
CategoryTheory.Limits.MulticospanIndex.fstPiMap_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) {Z : C} (h : I.right b ⟶ Z) : CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.fst b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h)
CategoryTheory.Limits.MulticospanIndex.sndPiMap_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : J.R) {Z : C} (h : I.right b ⟶ Z) : CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.snd b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.functor.obj K).pt = K.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.inverse.obj a).pt = a.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.functor.map f).hom = f.hom
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) (X : CategoryTheory.Limits.WalkingParallelPair) : (I.multiforkEquivPiFork.functor.obj K).π.app X = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t => X = t → (K.pt ⟶ (CategoryTheory.Limits.parallelPair (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))).obj X)) (fun h => ⋯ ▸ CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) X ⋯
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) (x✝ : CategoryTheory.Limits.WalkingMulticospan J) : (I.multiforkEquivPiFork.inverse.obj a).π.app x✝ = match x✝ with | CategoryTheory.Limits.WalkingMulticospan.left a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) a_1) | CategoryTheory.Limits.WalkingMulticospan.right a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (J.fst a_1)) (I.fst a_1))
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.inverse.map f).hom = f.hom
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.Concrete.productEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : Type w} (F : J → C) [CategoryTheory.Limits.HasProduct F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)] : CategoryTheory.ToType (∏ᶜ F) ≃ ((j : J) → CategoryTheory.ToType (F j))
CategoryTheory.Limits.Concrete.productEquiv_apply_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : Type w} (F : J → C) [CategoryTheory.Limits.HasProduct F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)] (x : CategoryTheory.ToType (∏ᶜ F)) (j : J) : (CategoryTheory.Limits.Concrete.productEquiv F) x j = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) x
CategoryTheory.Limits.Concrete.productEquiv_symm_apply_π 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : Type w} (F : J → C) [CategoryTheory.Limits.HasProduct F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)] (x : (j : J) → CategoryTheory.ToType (F j)) (j : J) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) ((CategoryTheory.Limits.Concrete.productEquiv F).symm x) = x j
CategoryTheory.Limits.Concrete.Pi.map_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] {D : Type t} [CategoryTheory.Category.{r, t} D] {FD : D → D → Type u_1} {DD : D → Type (max w r)} [(X Y : D) → FunLike (FD X Y) (DD X) (DD Y)] [CategoryTheory.ConcreteCategory D FD] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F] [CategoryTheory.Limits.HasProduct fun j => F.obj (f j)] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun b => F.obj (f b)) (CategoryTheory.forget D)] (x y : CategoryTheory.ToType (F.obj (∏ᶜ f))) (h : ∀ (i : J), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.Pi.π f i))) x = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.Pi.π f i))) y) : x = y
CategoryTheory.Pretriangulated.productTriangle 📋 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.Triangle C
CategoryTheory.Pretriangulated.productTriangle.fan 📋 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.Limits.Fan T
CategoryTheory.Pretriangulated.productTriangle_obj₁ 📋 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).obj₁ = ∏ᶜ fun j => (T j).obj₁
CategoryTheory.Pretriangulated.productTriangle_obj₂ 📋 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).obj₂ = ∏ᶜ fun j => (T j).obj₂
CategoryTheory.Pretriangulated.productTriangle_obj₃ 📋 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).obj₃ = ∏ᶜ fun j => (T j).obj₃
CategoryTheory.Pretriangulated.productTriangle.π 📋 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₁] (j : J) : CategoryTheory.Pretriangulated.productTriangle T ⟶ T j
CategoryTheory.Pretriangulated.productTriangle.isLimitFan 📋 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.Limits.IsLimit (CategoryTheory.Pretriangulated.productTriangle.fan T)
CategoryTheory.Pretriangulated.productTriangle.lift 📋 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₁] {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j) : T' ⟶ CategoryTheory.Pretriangulated.productTriangle T
CategoryTheory.Pretriangulated.productTriangle.π_hom₁ 📋 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₁] (j : J) : (CategoryTheory.Pretriangulated.productTriangle.π T j).hom₁ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₁) j
CategoryTheory.Pretriangulated.productTriangle.π_hom₂ 📋 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₁] (j : J) : (CategoryTheory.Pretriangulated.productTriangle.π T j).hom₂ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₂) j
CategoryTheory.Pretriangulated.productTriangle.π_hom₃ 📋 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₁] (j : J) : (CategoryTheory.Pretriangulated.productTriangle.π T j).hom₃ = CategoryTheory.Limits.Pi.π (fun j => (T j).obj₃) j
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.lift_hom₁ 📋 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₁] {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j) : (CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₁ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₁
CategoryTheory.Pretriangulated.productTriangle.lift_hom₂ 📋 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₁] {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j) : (CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₂ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₂
CategoryTheory.Pretriangulated.productTriangle.lift_hom₃ 📋 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₁] {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j) : (CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₃ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₃
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.Pretriangulated.productTriangle.zero₃₁ 📋 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.Limits.HasZeroMorphisms C] (h : ∀ (j : J), CategoryTheory.CategoryStruct.comp (T j).mor₃ ((CategoryTheory.shiftFunctor C 1).map (T j).mor₁) = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Pretriangulated.productTriangle T).mor₃ ((CategoryTheory.shiftFunctor C 1).map (CategoryTheory.Pretriangulated.productTriangle T).mor₁) = 0
CategoryTheory.Pretriangulated.productTriangle_distinguished 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) (hT : ∀ (j : J), T j ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) [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 ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.ObjectProperty.prop_product 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderFiniteProducts] {J : Type u_2} [Finite J] {f : J → C} [CategoryTheory.Limits.HasProduct f] (h : ∀ (j : J), P (f j)) : P (∏ᶜ f)
CategoryTheory.instHasLiftingPropertyMap 📋 Mathlib.CategoryTheory.LiftingProperties.Limits
{C : Type u_1} [CategoryTheory.Category.{v_1, 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)
HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Fibration (f i)] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : HomotopicalAlgebra.Fibration (CategoryTheory.Limits.Pi.map f)
HomotopicalAlgebra.instWeakEquivalenceMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
{C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Fibration (f i)] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] [∀ (i : J), HomotopicalAlgebra.WeakEquivalence (f i)] : HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.Pi.map f)
CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum 📋 Mathlib.CategoryTheory.Preadditive.LiftToFinset
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteProducts C] {α : Type w} [DecidableEq α] (f : α → C) [CategoryTheory.Limits.HasProduct f] (S : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).π.app S = ∑ a ∈ (Opposite.unop S).attach, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (↑a).as) (CategoryTheory.Limits.Pi.ι (fun a => f (↑a).as) a)
CategoryTheory.Limits.hasWidePullback_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) [CategoryTheory.Limits.HasProduct objs] (hB : CategoryTheory.Limits.IsTerminal B) : CategoryTheory.Limits.HasWidePullback B objs arrows
CategoryTheory.Limits.hasBinaryProduct_of_products 📋 Mathlib.CategoryTheory.Limits.Shapes.PiProd
{C : Type u_1} {I : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] {X : I → C} (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => X ↑i] : CategoryTheory.Limits.HasBinaryProduct (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i)
CategoryTheory.Limits.Pi.binaryFanOfProp 📋 Mathlib.CategoryTheory.Limits.Shapes.PiProd
{C : Type u_1} {I : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] (X : I → C) (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => X ↑i] : CategoryTheory.Limits.BinaryFan (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i)
CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.PiProd
{C : Type u_1} {I : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] (X : I → C) (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [(i : I) → Decidable (P i)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Pi.binaryFanOfProp X P)
CategoryTheory.Limits.Pi.map_eq_prod_map 📋 Mathlib.CategoryTheory.Limits.Shapes.PiProd
{C : Type u_1} {I : Type u_2} [CategoryTheory.Category.{v_1, 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)
ωCPO.HasProducts.instHasProduct 📋 Mathlib.Order.Category.OmegaCompletePartialOrder
(J : Type v) (f : J → ωCPO) : CategoryTheory.Limits.HasProduct f

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

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

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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

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

Source code

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

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c