Chosen pullbacks along a morphism

Main declarations

• ChosenPullbacksAlong : For a morphism f : Y ⟶ X in C, the type class ChosenPullbacksAlong f provides the data of a pullback functor Over X ⥤ Over Y as a right adjoint to Over.map f.

Main results

• We prove that ChosenPullbacksAlong has good closure properties: isos have chosen pullbacks, and composition of morphisms with chosen pullbacks have chosen pullbacks.

• We prove that chosen pullbacks yields usual pullbacks: ChosenPullbacksAlong.isPullback proves that for morphisms f and g with the same codomain, the object ChosenPullbacksAlong.pullbackObj f g together with morphisms ChosenPullbacksAlong.fst f g and ChosenPullbacksAlong.snd f g form a pullback square over f and g.

• We prove that in cartesian monoidal categories, morphisms to the terminal tensor unit and the product projections have chosen pullbacks.

class CategoryTheory.ChosenPullbacksAlong {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ⟶ X) : Type (max u₁ v₁)

A functorial choice of pullbacks along a morphism f : Y ⟶ X in C given by a functor Over X ⥤ Over Y which is a right adjoint to the functor Over.map f.

• pullback : Functor (Over X) (Over Y)

  The pullback functor along f.

• mapPullbackAdj : Over.map f ⊣ pullback f

  The adjunction between Over.map f and pullback f.

@[reducible, inline]

abbrev CategoryTheory.ChosenPullbacks (C : Type u₁) [Category.{v₁, u₁} C] : Type (max u₁ v₁)

A category has chosen pullbacks if every morphism has a chosen pullback.

noncomputable def CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ⟶ X) [Limits.HasPullbacksAlong f] : ChosenPullbacksAlong f

Relating the existing noncomputable HasPullbacksAlong typeclass to ChosenPullbacksAlong.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong_pullback {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ⟶ X) [Limits.HasPullbacksAlong f] : pullback f = Over.pullback f

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong_mapPullbackAdj {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ⟶ X) [Limits.HasPullbacksAlong f] : mapPullbackAdj f = Over.mapPullbackAdj f

def CategoryTheory.ChosenPullbacksAlong.id {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : ChosenPullbacksAlong (CategoryStruct.id X)

The identity morphism has a functorial choice of pullbacks.

def CategoryTheory.ChosenPullbacksAlong.pullbackId {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [ChosenPullbacksAlong (CategoryStruct.id X)] : pullback (CategoryStruct.id X) ≅ Functor.id (Over X)

Any chosen pullback functor of the identity morphism is naturally isomorphic to the identity functor.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [ChosenPullbacksAlong (CategoryStruct.id X)] (Y : Over X) : CategoryStruct.comp ((mapPullbackAdj (CategoryStruct.id X)).unit.app Y) ((pullbackId X).hom.app ((Over.map (CategoryStruct.id X)).obj Y)) = (mapPullbackAdj (CategoryStruct.id X)).unit.app Y

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [ChosenPullbacksAlong (CategoryStruct.id X)] (Y : Over X) {Z : Over X} (h : (Over.map (CategoryStruct.id X)).obj Y ⟶ Z) : CategoryStruct.comp ((mapPullbackAdj (CategoryStruct.id X)).unit.app Y) (CategoryStruct.comp ((pullbackId X).hom.app ((Over.map (CategoryStruct.id X)).obj Y)) h) = CategoryStruct.comp ((mapPullbackAdj (CategoryStruct.id X)).unit.app Y) h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [ChosenPullbacksAlong (CategoryStruct.id X)] : CategoryStruct.comp (mapPullbackAdj (CategoryStruct.id X)).unit ((Over.map (CategoryStruct.id X)).whiskerLeft (pullbackId X).hom) = (mapPullbackAdj (CategoryStruct.id X)).unit

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [ChosenPullbacksAlong (CategoryStruct.id X)] {Z : Functor (Over X) (Over X)} (h : (Over.map (CategoryStruct.id X)).comp (Functor.id (Over X)) ⟶ Z) : CategoryStruct.comp (mapPullbackAdj (CategoryStruct.id X)).unit (CategoryStruct.comp ((Over.map (CategoryStruct.id X)).whiskerLeft (pullbackId X).hom) h) = CategoryStruct.comp (mapPullbackAdj (CategoryStruct.id X)).unit h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackId_hom_counit {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [ChosenPullbacksAlong (CategoryStruct.id X)] : CategoryStruct.comp (Functor.whiskerRight (pullbackId X).hom (Over.map (CategoryStruct.id X))) (mapPullbackAdj (CategoryStruct.id X)).counit = (mapPullbackAdj (CategoryStruct.id X)).counit

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackId_hom_counit_assoc {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [ChosenPullbacksAlong (CategoryStruct.id X)] {Z : Functor (Over X) (Over X)} (h : Functor.id (Over X) ⟶ Z) : CategoryStruct.comp (Functor.whiskerRight (pullbackId X).hom (Over.map (CategoryStruct.id X))) (CategoryStruct.comp (mapPullbackAdj (CategoryStruct.id X)).counit h) = CategoryStruct.comp (mapPullbackAdj (CategoryStruct.id X)).counit h

def CategoryTheory.ChosenPullbacksAlong.iso {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) : ChosenPullbacksAlong f.hom

Every isomorphism has a functorial choice of pullbacks.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.iso_mapPullbackAdj_counit_app {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (U : Over X) : (mapPullbackAdj f.hom).counit.app U = Over.homMk (CategoryStruct.id (({ obj := fun (Z : Over X) => Over.mk (CategoryStruct.comp Z.hom f.inv), map := fun {Y_1 Z : Over X} (g : Y_1 ⟶ Z) => Over.homMk g.left ⋯, map_id := ⋯, map_comp := ⋯ }.comp (Over.map f.hom)).obj U).left) ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.iso_pullback_obj {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (Z : Over X) : (pullback f.hom).obj Z = Over.mk (CategoryStruct.comp Z.hom f.inv)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.iso_mapPullbackAdj_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (T : Over Y) : (mapPullbackAdj f.hom).unit.app T = Over.homMk (CategoryStruct.id T.left) ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.iso_pullback_map {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) {Y✝ Z : Over X} (g : Y✝ ⟶ Z) : (pullback f.hom).map g = Over.homMk g.left ⋯

def CategoryTheory.ChosenPullbacksAlong.isoInv {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) : ChosenPullbacksAlong f.inv

The inverse of an isomorphism has a functorial choice of pullbacks.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.isoInv_pullback_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (Z : Over Y) : ((pullback f.inv).obj Z).left = Z.left

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.isoInv_pullback_obj_hom {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (Z : Over Y) : ((pullback f.inv).obj Z).hom = CategoryStruct.comp Z.hom f.hom

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.isoInv_pullback_obj_right_as {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (Z : Over Y) : ((pullback f.inv).obj Z).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.isoInv_pullback_map_left {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) {Y✝ Z : Over Y} (g : Y✝ ⟶ Z) : ((pullback f.inv).map g).left = g.left

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.isoInv_mapPullbackAdj_unit_app_left {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (T : Over X) : ((mapPullbackAdj f.inv).unit.app T).left = CategoryStruct.id T.left

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.isoInv_mapPullbackAdj_counit_app_left {C : Type u₁} [Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (U : Over Y) : ((mapPullbackAdj f.inv).counit.app U).left = CategoryStruct.id U.left

def CategoryTheory.ChosenPullbacksAlong.comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [ChosenPullbacksAlong f] [ChosenPullbacksAlong g] : ChosenPullbacksAlong (CategoryStruct.comp f g)

The composition of morphisms with chosen pullbacks has a chosen pullback.

def CategoryTheory.ChosenPullbacksAlong.pullbackComp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [ChosenPullbacksAlong f] [ChosenPullbacksAlong g] [ChosenPullbacksAlong (CategoryStruct.comp f g)] : pullback (CategoryStruct.comp f g) ≅ (pullback g).comp (pullback f)

Any chosen pullback of a composite of morphisms is naturally isomorphic to the composition of chosen pullback functors.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.unit_pullbackComp_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [ChosenPullbacksAlong f] [ChosenPullbacksAlong g] [ChosenPullbacksAlong (CategoryStruct.comp f g)] : CategoryStruct.comp (mapPullbackAdj (CategoryStruct.comp f g)).unit ((Over.map (CategoryStruct.comp f g)).whiskerLeft (pullbackComp f g).hom) = (mapPullbackAdj (CategoryStruct.comp f g)).unit

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.unit_pullbackComp_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [ChosenPullbacksAlong f] [ChosenPullbacksAlong g] [ChosenPullbacksAlong (CategoryStruct.comp f g)] {Z✝ : Functor (Over X) (Over X)} (h : (Over.map (CategoryStruct.comp f g)).comp ((pullback g).comp (pullback f)) ⟶ Z✝) : CategoryStruct.comp (mapPullbackAdj (CategoryStruct.comp f g)).unit (CategoryStruct.comp ((Over.map (CategoryStruct.comp f g)).whiskerLeft (pullbackComp f g).hom) h) = CategoryStruct.comp (mapPullbackAdj (CategoryStruct.comp f g)).unit h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackComp_hom_counit {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [ChosenPullbacksAlong f] [ChosenPullbacksAlong g] [ChosenPullbacksAlong (CategoryStruct.comp f g)] : CategoryStruct.comp (Functor.whiskerRight (pullbackComp f g).hom (Over.map (CategoryStruct.comp f g))) (mapPullbackAdj (CategoryStruct.comp f g)).counit = (mapPullbackAdj (CategoryStruct.comp f g)).counit

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackComp_hom_counit_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [ChosenPullbacksAlong f] [ChosenPullbacksAlong g] [ChosenPullbacksAlong (CategoryStruct.comp f g)] {Z✝ : Functor (Over Z) (Over Z)} (h : Functor.id (Over Z) ⟶ Z✝) : CategoryStruct.comp (Functor.whiskerRight (pullbackComp f g).hom (Over.map (CategoryStruct.comp f g))) (CategoryStruct.comp (mapPullbackAdj (CategoryStruct.comp f g)).counit h) = CategoryStruct.comp (mapPullbackAdj (CategoryStruct.comp f g)).counit h

def CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X : C} (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) : ChosenPullbacksAlong f

In cartesian monoidal categories, any morphism to the terminal tensor unit has a functorial choice of pullbacks.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_unit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X : C} (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) (T : Over X) : (mapPullbackAdj f).unit.app T = Over.homMk (CartesianMonoidalCategory.lift (CategoryStruct.id ((Functor.id (Over X)).obj T).left) T.hom) ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X : C} (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) (U : Over (MonoidalCategoryStruct.tensorUnit C)) : (mapPullbackAdj f).counit.app U = Over.homMk (SemiCartesianMonoidalCategory.fst U.left X) ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_map {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X : C} (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) {Y Z : Over (MonoidalCategoryStruct.tensorUnit C)} (g : Y ⟶ Z) : (pullback f).map g = Over.homMk (MonoidalCategoryStruct.whiskerRight g.left X) ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X : C} (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) (Y : Over (MonoidalCategoryStruct.tensorUnit C)) : (pullback f).obj Y = Over.mk (SemiCartesianMonoidalCategory.snd Y.left X)

def CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) : ChosenPullbacksAlong (SemiCartesianMonoidalCategory.fst X Y)

In cartesian monoidal categories, the first product projections fst have a functorial choice of pullbacks.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) (T : Over (MonoidalCategoryStruct.tensorObj X Y)) : (mapPullbackAdj (SemiCartesianMonoidalCategory.fst X Y)).unit.app T = Over.homMk (CartesianMonoidalCategory.lift (CategoryStruct.id ((Functor.id (Over (MonoidalCategoryStruct.tensorObj X Y))).obj T).left) (CategoryStruct.comp T.hom (SemiCartesianMonoidalCategory.snd X Y))) ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_counit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) (U : Over X) : (mapPullbackAdj (SemiCartesianMonoidalCategory.fst X Y)).counit.app U = Over.homMk (SemiCartesianMonoidalCategory.fst ((Functor.id C).obj U.left) Y) ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) (Z : Over X) : (pullback (SemiCartesianMonoidalCategory.fst X Y)).obj Z = Over.mk (MonoidalCategoryStruct.whiskerRight Z.hom Y)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_pullback_map {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) {X✝ Y✝ : Over X} (g : X✝ ⟶ Y✝) : (pullback (SemiCartesianMonoidalCategory.fst X Y)).map g = Over.homMk (MonoidalCategoryStruct.whiskerRight g.left Y) ⋯

def CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) : ChosenPullbacksAlong (SemiCartesianMonoidalCategory.snd X Y)

In cartesian monoidal categories, the second product projections snd have a functorial choice of pullbacks.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) (Z : Over Y) : (pullback (SemiCartesianMonoidalCategory.snd X Y)).obj Z = Over.mk (MonoidalCategoryStruct.whiskerLeft X Z.hom)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_counit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) (U : Over Y) : (mapPullbackAdj (SemiCartesianMonoidalCategory.snd X Y)).counit.app U = Over.homMk (SemiCartesianMonoidalCategory.snd X ((Functor.id C).obj U.left)) ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_map {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) {X✝ Y✝ : Over Y} (g : X✝ ⟶ Y✝) : (pullback (SemiCartesianMonoidalCategory.snd X Y)).map g = Over.homMk (MonoidalCategoryStruct.whiskerLeft X g.left) ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X Y : C) (T : Over (MonoidalCategoryStruct.tensorObj X Y)) : (mapPullbackAdj (SemiCartesianMonoidalCategory.snd X Y)).unit.app T = Over.homMk (CartesianMonoidalCategory.lift (CategoryStruct.comp T.hom (SemiCartesianMonoidalCategory.fst X Y)) (CategoryStruct.id ((Functor.id (Over (MonoidalCategoryStruct.tensorObj X Y))).obj T).left)) ⋯

@[reducible, inline]

abbrev CategoryTheory.ChosenPullbacksAlong.pullbackObj {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : C

The underlying object of the chosen pullback along g of f.

@[reducible, inline]

abbrev CategoryTheory.ChosenPullbacksAlong.fst' {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : (Over.map g).obj ((pullback g).obj (Over.mk f)) ⟶ Over.mk f

A morphism in Over X from the chosen pullback along g of f to Over.mk f.

@[reducible, inline]

abbrev CategoryTheory.ChosenPullbacksAlong.fst {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : pullbackObj f g ⟶ Y

The first projection from the chosen pullback along g of f to the domain of f.

theorem CategoryTheory.ChosenPullbacksAlong.fst'_left {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : (fst' f g).left = fst f g

@[reducible, inline]

abbrev CategoryTheory.ChosenPullbacksAlong.snd {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : pullbackObj f g ⟶ Z

The second projection from the chosen pullback along g of f to the domain of g.

@[reducible, inline]

abbrev CategoryTheory.ChosenPullbacksAlong.snd' {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : (Over.map g).obj ((pullback g).obj (Over.mk f)) ⟶ Over.mk g

A morphism in Over X from the chosen pullback along g of f to Over.mk g.

theorem CategoryTheory.ChosenPullbacksAlong.snd'_left {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : (snd' f g).left = snd f g

theorem CategoryTheory.ChosenPullbacksAlong.condition {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] : CategoryStruct.comp (fst f g) f = CategoryStruct.comp (snd f g) g

theorem CategoryTheory.ChosenPullbacksAlong.condition_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (fst f g) (CategoryStruct.comp f h) = CategoryStruct.comp (snd f g) (CategoryStruct.comp g h)

theorem CategoryTheory.ChosenPullbacksAlong.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] {W : C} {φ₁ φ₂ : W ⟶ pullbackObj f g} (h₁ : CategoryStruct.comp φ₁ (fst f g) = CategoryStruct.comp φ₂ (fst f g)) (h₂ : CategoryStruct.comp φ₁ (snd f g) = CategoryStruct.comp φ₂ (snd f g)) : φ₁ = φ₂

theorem CategoryTheory.ChosenPullbacksAlong.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {W : C} {φ₁ φ₂ : W ⟶ pullbackObj f g} : φ₁ = φ₂ ↔ CategoryStruct.comp φ₁ (fst f g) = CategoryStruct.comp φ₂ (fst f g) ∧ CategoryStruct.comp φ₁ (snd f g) = CategoryStruct.comp φ₂ (snd f g)

def CategoryTheory.ChosenPullbacksAlong.lift {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z) (h : CategoryStruct.comp a f = CategoryStruct.comp b g := by cat_disch) : W ⟶ pullbackObj f g

Given morphisms a : W ⟶ Y and b : W ⟶ Z satisfying a ≫ f = b ≫ g, constructs the unique morphism W ⟶ pullbackObj f g which lifts a and b.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.lift_fst {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z) (h : CategoryStruct.comp a f = CategoryStruct.comp b g := by cat_disch) : CategoryStruct.comp (lift a b h) (fst f g) = a

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.lift_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z) (h : CategoryStruct.comp a f = CategoryStruct.comp b g := by cat_disch) {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryStruct.comp (lift a b h) (CategoryStruct.comp (fst f g) h✝) = CategoryStruct.comp a h✝

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.lift_snd {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z) (h : CategoryStruct.comp a f = CategoryStruct.comp b g := by cat_disch) : CategoryStruct.comp (lift a b h) (snd f g) = b

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.lift_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z) (h : CategoryStruct.comp a f = CategoryStruct.comp b g := by cat_disch) {Z✝ : C} (h✝ : Z ⟶ Z✝) : CategoryStruct.comp (lift a b h) (CategoryStruct.comp (snd f g) h✝) = CategoryStruct.comp b h✝

def CategoryTheory.ChosenPullbacksAlong.pullbackMap {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] {Y' Z' X' : C} (f' : Y' ⟶ X') (g' : Z' ⟶ X') [ChosenPullbacksAlong g'] (γ₁ : Y' ⟶ Y) (γ₂ : Z' ⟶ Z) (γ₃ : X' ⟶ X) (comm₁ : CategoryStruct.comp f' γ₃ = CategoryStruct.comp γ₁ f := by cat_disch) (comm₂ : CategoryStruct.comp g' γ₃ = CategoryStruct.comp γ₂ g := by cat_disch) : pullbackObj f' g' ⟶ 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.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackMap_fst {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {Y' Z' X' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'} [ChosenPullbacksAlong g'] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X} (comm₁ : CategoryStruct.comp f' γ₃ = CategoryStruct.comp γ₁ f := by cat_disch) (comm₂ : CategoryStruct.comp g' γ₃ = CategoryStruct.comp γ₂ g := by cat_disch) : CategoryStruct.comp (pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) (fst f g) = CategoryStruct.comp (fst f' g') γ₁

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackMap_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {Y' Z' X' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'} [ChosenPullbacksAlong g'] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X} (comm₁ : CategoryStruct.comp f' γ₃ = CategoryStruct.comp γ₁ f := by cat_disch) (comm₂ : CategoryStruct.comp g' γ₃ = CategoryStruct.comp γ₂ g := by cat_disch) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) (CategoryStruct.comp (fst f g) h) = CategoryStruct.comp (fst f' g') (CategoryStruct.comp γ₁ h)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {Y' Z' X' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'} [ChosenPullbacksAlong g'] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X} (comm₁ : CategoryStruct.comp f' γ₃ = CategoryStruct.comp γ₁ f := by cat_disch) (comm₂ : CategoryStruct.comp g' γ₃ = CategoryStruct.comp γ₂ g := by cat_disch) : CategoryStruct.comp (pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) (snd f g) = CategoryStruct.comp (snd f' g') γ₂

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {Y' Z' X' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'} [ChosenPullbacksAlong g'] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X} (comm₁ : CategoryStruct.comp f' γ₃ = CategoryStruct.comp γ₁ f := by cat_disch) (comm₂ : CategoryStruct.comp g' γ₃ = CategoryStruct.comp γ₂ g := by cat_disch) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) (CategoryStruct.comp (snd f g) h) = CategoryStruct.comp (snd f' g') (CategoryStruct.comp γ₂ h)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackMap_id {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] : pullbackMap f g f g (CategoryStruct.id Y) (CategoryStruct.id Z) (CategoryStruct.id X) ⋯ ⋯ = CategoryStruct.id (pullbackObj f g)

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {Y' Z' X' Y'' Z'' X'' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'} {f'' : Y'' ⟶ X''} {g'' : Z'' ⟶ X''} [ChosenPullbacksAlong g'] [ChosenPullbacksAlong g''] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X} {δ₁ : Y'' ⟶ Y'} {δ₂ : Z'' ⟶ Z'} {δ₃ : X'' ⟶ X'} (comm₁ : CategoryStruct.comp f' γ₃ = CategoryStruct.comp γ₁ f := by cat_disch) (comm₂ : CategoryStruct.comp g' γ₃ = CategoryStruct.comp γ₂ g := by cat_disch) (comm₁' : CategoryStruct.comp f'' δ₃ = CategoryStruct.comp δ₁ f' := by cat_disch) (comm₂' : CategoryStruct.comp g'' δ₃ = CategoryStruct.comp δ₂ g' := by cat_disch) : CategoryStruct.comp (pullbackMap f' g' f'' g'' δ₁ δ₂ δ₃ comm₁' comm₂') (pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) = pullbackMap f g f'' g'' (CategoryStruct.comp δ₁ γ₁) (CategoryStruct.comp δ₂ γ₂) (CategoryStruct.comp δ₃ γ₃) ⋯ ⋯

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X} [ChosenPullbacksAlong g] {Y' Z' X' Y'' Z'' X'' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'} {f'' : Y'' ⟶ X''} {g'' : Z'' ⟶ X''} [ChosenPullbacksAlong g'] [ChosenPullbacksAlong g''] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X} {δ₁ : Y'' ⟶ Y'} {δ₂ : Z'' ⟶ Z'} {δ₃ : X'' ⟶ X'} (comm₁ : CategoryStruct.comp f' γ₃ = CategoryStruct.comp γ₁ f := by cat_disch) (comm₂ : CategoryStruct.comp g' γ₃ = CategoryStruct.comp γ₂ g := by cat_disch) (comm₁' : CategoryStruct.comp f'' δ₃ = CategoryStruct.comp δ₁ f' := by cat_disch) (comm₂' : CategoryStruct.comp g'' δ₃ = CategoryStruct.comp δ₂ g' := by cat_disch) {Z✝ : C} (h : pullbackObj f g ⟶ Z✝) : CategoryStruct.comp (pullbackMap f' g' f'' g'' δ₁ δ₂ δ₃ comm₁' comm₂') (CategoryStruct.comp (pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) h) = CategoryStruct.comp (pullbackMap f g f'' g'' (CategoryStruct.comp δ₁ γ₁) (CategoryStruct.comp δ₂ γ₂) (CategoryStruct.comp δ₃ γ₃) ⋯ ⋯) h

def CategoryTheory.ChosenPullbacksAlong.pullbackCone {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : Limits.PullbackCone f g

The canonical pullback cone from the data of a chosen pullback of f along g.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackCone_fst {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : (pullbackCone f g).fst = fst f g

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackCone_snd {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : (pullbackCone f g).snd = snd f g

def CategoryTheory.ChosenPullbacksAlong.isLimitPullbackCone {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : Limits.IsLimit (pullbackCone f g)

The canonical pullback cone is a limit cone. Note: this limit cone is computable as lifts are constructed from the data contained in the ChosenPullbackAlong instance, contrary to IsPullback.isLimit, which constructs lifting data from CategoryTheory.Square.IsPullback (a Prop).

theorem CategoryTheory.ChosenPullbacksAlong.isPullback {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : IsPullback (fst f g) (snd f g) f g

def CategoryTheory.ChosenPullbacksAlong.chosenPullbacksAlongFst {C : Type u₁} [Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X) [ChosenPullbacksAlong g] : ChosenPullbacksAlong (fst f g)

If g has a chosen pullback, then Over.ChosenPullbacksAlong.fst f g has a chosen pullback.

instance CategoryTheory.ChosenPullbacksAlong.hasPullbackAlong {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] : Limits.HasPullbacksAlong g

instance CategoryTheory.ChosenPullbacksAlong.hasPullbacks {C : Type u₁} [Category.{v₁, u₁} C] [ChosenPullbacks C] : Limits.HasPullbacks C

noncomputable def CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] : pullback g ≅ Over.pullback g

The computable ChosenPullbacksAlong.pullback g is naturally isomorphic to the noncomputable Over.pullback g.

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] (T : Over X) : CategoryStruct.comp ((pullbackIsoOverPullback g).hom.app T).left (Limits.pullback.fst T.hom g) = fst T.hom g

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] (T : Over X) {Z✝ : C} (h : T.left ⟶ Z✝) : CategoryStruct.comp ((pullbackIsoOverPullback g).hom.app T).left (CategoryStruct.comp (Limits.pullback.fst T.hom g) h) = CategoryStruct.comp (fst T.hom g) h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] (T : Over X) : CategoryStruct.comp ((pullbackIsoOverPullback g).hom.app T).left (Limits.pullback.snd T.hom g) = snd T.hom g

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] (T : Over X) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp ((pullbackIsoOverPullback g).hom.app T).left (CategoryStruct.comp (Limits.pullback.snd T.hom g) h) = CategoryStruct.comp (snd T.hom g) h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] (T : Over X) : CategoryStruct.comp ((pullbackIsoOverPullback g).inv.app T).left (fst T.hom g) = Limits.pullback.fst T.hom g

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] (T : Over X) {Z✝ : C} (h : T.left ⟶ Z✝) : CategoryStruct.comp ((pullbackIsoOverPullback g).inv.app T).left (CategoryStruct.comp (fst T.hom g) h) = CategoryStruct.comp (Limits.pullback.fst T.hom g) h

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] (T : Over X) : CategoryStruct.comp ((pullbackIsoOverPullback g).inv.app T).left (snd T.hom g) = Limits.pullback.snd T.hom g

@[simp]

theorem CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X) [ChosenPullbacksAlong g] (T : Over X) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp ((pullbackIsoOverPullback g).inv.app T).left (CategoryStruct.comp (snd T.hom g) h) = CategoryStruct.comp (Limits.pullback.snd T.hom g) h