Theorems · Definition · category theory

CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (B : C) →
      {J : Type w} →
        CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B) →
          CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C

(Implementation) Given a product diagram in C/B, construct the corresponding wide pullback diagram in C.

Defined in

Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Cited by

16 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category