Theorems · Definition · category theory

CategoryTheory.ChosenPullbacksAlong.pullbackMap

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      (f : Y ⟶ X) →
        (g : Z ⟶ X) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong g] →
            {Y' Z' X' : C} →
              (f' : Y' ⟶ X') →
                (g' : Z' ⟶ X') →
                  [inst_2 : CategoryTheory.ChosenPullbacksAlong g'] →
                    (γ₁ : Y' ⟶ Y) →
                      (γ₂ : Z' ⟶ Z) →
                        (γ₃ : X' ⟶ X) →
                          autoParam (CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
                              CategoryTheory.ChosenPullbacksAlong.pullbackMap._auto_1 →
                            autoParam
                                (CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g)
                                CategoryTheory.ChosenPullbacksAlong.pullbackMap._auto_3 →
                              (CategoryTheory.ChosenPullbacksAlong.pullbackObj f' g' ⟶
                                CategoryTheory.ChosenPullbacksAlong.pullbackObj f g)

The functoriality of pullbackObj f g in both arguments: Given a map from the pullback cospans of f' : Y' ⟶ X' and g' : Z' ⟶ X' to the pullback cospan of f : Y ⟶ X and g : Z ⟶ X as in the diagram below `` Y' ⟶ Y ↘ ↘ X' ⟶ X ↗ ↗ Z' ⟶ Z ` if the morphisms g' and g both have chosen pullbacks, then we get an induced morphism pullbackMap f g f' g' comm₁ comm₂ from the chosen pullback of f' : Y' ⟶ X' along g' to the chosen pullback of f : Y ⟶ X along g. Here comm₁ and comm₂` are the commutativity conditions of the squares in the diagram above.

Defined in

Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.ChosenPullbacksAlongCategoryTheory.ChosenPullbacksAlong