Coherence of base change in over categories

Mathlib identifies base change Over.pullback along an identity with the identity functor (Over.pullbackId) and base change along a composite with the composite of base changes (Over.pullbackComp). This file records that these identifications are coherent, up to the equalities f ≫ 𝟙 Y = f and f ≫ g ≫ h = (f ≫ g) ≫ h:

• CategoryTheory.Over.pullbackComp_id_inv_app_comp_eqToHom: pullbackComp f (𝟙 Y) is the base change along f of pullbackId;
• CategoryTheory.Over.pullbackComp_comp_inv_app_comp_eqToHom: the two identifications of base change along f ≫ g ≫ h with the composite of the three base changes agree.

theorem CategoryTheory.Over.pullbackComp_id_inv_app_comp_eqToHom {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPullbacksAlong f] (A : Over Y) : CategoryStruct.comp ((pullbackComp f (CategoryStruct.id Y)).inv.app A) (eqToHom ⋯) = (pullback f).map (pullbackId.hom.app A)

Base change along f : X ⟶ Y of the identification pullbackId of base change along the identity is the composition isomorphism pullbackComp f (𝟙 Y), up to the equality f ≫ 𝟙 Y = f.

theorem CategoryTheory.Over.pullbackComp_id_inv_app_comp_eqToHom_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPullbacksAlong f] (A : Over Y) {Z : Over X} (h : (pullback f).obj A ⟶ Z) : CategoryStruct.comp ((pullbackComp f (CategoryStruct.id Y)).inv.app A) (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp ((pullback f).map (pullbackId.hom.app A)) h

Base change along f : X ⟶ Y of the identification pullbackId of base change along the identity is the composition isomorphism pullbackComp f (𝟙 Y), up to the equality f ≫ 𝟙 Y = f.

theorem CategoryTheory.Over.pullbackComp_comp_inv_app_comp_eqToHom {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) [Limits.HasPullbacksAlong f] [Limits.HasPullbacksAlong g] [Limits.HasPullbacksAlong h] (A : Over Z) : CategoryStruct.comp ((pullbackComp f (CategoryStruct.comp g h)).inv.app A) (eqToHom ⋯) = CategoryStruct.comp ((pullback f).map ((pullbackComp g h).hom.app A)) (CategoryStruct.comp ((pullbackComp f g).inv.app ((pullback h).obj A)) ((pullbackComp (CategoryStruct.comp f g) h).inv.app A))

The two ways of identifying base change along f ≫ g ≫ h with the composite of the base changes along h, g and f agree, up to the equality f ≫ g ≫ h = (f ≫ g) ≫ h.

theorem CategoryTheory.Over.pullbackComp_comp_inv_app_comp_eqToHom_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) [Limits.HasPullbacksAlong f] [Limits.HasPullbacksAlong g] [Limits.HasPullbacksAlong h] (A : Over Z) {Z✝ : Over W} (h✝ : (pullback (CategoryStruct.comp (CategoryStruct.comp f g) h)).obj A ⟶ Z✝) : CategoryStruct.comp ((pullbackComp f (CategoryStruct.comp g h)).inv.app A) (CategoryStruct.comp (eqToHom ⋯) h✝) = CategoryStruct.comp ((pullback f).map ((pullbackComp g h).hom.app A)) (CategoryStruct.comp ((pullbackComp f g).inv.app ((pullback h).obj A)) (CategoryStruct.comp ((pullbackComp (CategoryStruct.comp f g) h).inv.app A) h✝))

The two ways of identifying base change along f ≫ g ≫ h with the composite of the base changes along h, g and f agree, up to the equality f ≫ g ≫ h = (f ≫ g) ≫ h.