Theorems · Definition · category theory

CategoryTheory.Limits.piComparison

{β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (G : CategoryTheory.Functor C D) →
            (f : β → C) →
              [inst_2 : CategoryTheory.Limits.HasProduct f] →
                [inst_3 : CategoryTheory.Limits.HasProduct fun b => G.obj (f b)] →
                  G.obj (∏ᶜ f) ⟶ ∏ᶜ fun b => G.obj (f b)

The comparison morphism for the product of f. This is an iso iff G preserves the product of f, see PreservesProduct.ofIsoComparison.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

18 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasProductCategoryTheory.Limits.HasProduct