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 yield 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.

Instances

source

@[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.

Instances For

source

@[implicit_reducible]

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.

Instances For

source

@[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

source

@[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

source

@[implicit_reducible]

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.

Instances For

source

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.

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[implicit_reducible]

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.

Instances For

source

@[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) ⋯

source

@[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)

source

@[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 ⋯

source

@[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) ⋯

source

@[implicit_reducible]

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.

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[implicit_reducible]

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.

Instances For

source

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.

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

@[implicit_reducible]

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.

Instances For

source

@[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) ⋯

source

@[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) ⋯

source

@[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) ⋯

source

@[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)

source

@[implicit_reducible]

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.

Instances For

source

@[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) ⋯

source

@[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))) ⋯

source

@[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) ⋯

source

@[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)

source

@[implicit_reducible]

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.

Instances For

source

@[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)) ⋯

source

@[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)) ⋯

source

@[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)

source

@[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) ⋯

source

@[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] :

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

Instances For

source

@[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.

Instances For

source

@[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.

Instances For

source

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

source

@[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.

Instances For

source

@[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.

Instances For

source

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

source

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

source

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)

source

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)) :

φ₁ = φ₂

source

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)

source

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.

Instances For

source

@[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

source

@[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✝

source

@[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

source

@[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✝

source

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.

Instances For

source

@[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') γ₁

source

@[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)

source

@[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') γ₂

source

@[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)

source

@[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)

source

@[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 δ₃ γ₃) ⋯ ⋯

source

@[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

source

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.

Instances For

source

@[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

source

@[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

source

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).

Instances For

source