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.

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.

Equations

CategoryTheory.ChosenPullbacks C = ({X Y : C} → (f : Y ⟶ X) → CategoryTheory.ChosenPullbacksAlong f)

Instances For

source

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.

Equations

CategoryTheory.ChosenPullbacksAlong.ofHasPullbacksAlong f = { pullback := CategoryTheory.Over.pullback f, mapPullbackAdj := CategoryTheory.Over.mapPullbackAdj f }

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

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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

One or more equations did not get rendered due to their size.

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

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.

Equations

One or more equations did not get rendered due to their size.

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

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.

Equations

CategoryTheory.ChosenPullbacksAlong.isoInv f = CategoryTheory.ChosenPullbacksAlong.iso f.symm

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

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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

One or more equations did not get rendered due to their size.

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

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.

Equations

One or more equations did not get rendered due to their size.

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

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.

Equations

One or more equations did not get rendered due to their size.

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

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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

CategoryTheory.ChosenPullbacksAlong.pullbackObj f g = ((CategoryTheory.ChosenPullbacksAlong.pullback g).obj (CategoryTheory.Over.mk f)).left

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.

Equations

CategoryTheory.ChosenPullbacksAlong.fst' f g = (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj g).counit.app (CategoryTheory.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.

Equations

CategoryTheory.ChosenPullbacksAlong.fst f g = (CategoryTheory.ChosenPullbacksAlong.fst' f g).left

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.

Equations

CategoryTheory.ChosenPullbacksAlong.snd f g = ((CategoryTheory.ChosenPullbacksAlong.pullback g).obj (CategoryTheory.Over.mk f)).hom

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.

Equations

CategoryTheory.ChosenPullbacksAlong.snd' f g = CategoryTheory.Over.homMk (CategoryTheory.ChosenPullbacksAlong.snd f 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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

One or more equations did not get rendered due to their size.

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.

Equations

CategoryTheory.ChosenPullbacksAlong.pullbackCone f g = CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.ChosenPullbacksAlong.fst f g) (CategoryTheory.ChosenPullbacksAlong.snd f 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).

Equations