Preservation of pullback/pushout squares

If a functor F : C ⥤ D preserves suitable cospans (resp. spans), and sq : Square C is a pullback square (resp. a pushout square) then so is the square sq.map F.

The lemma Square.isPullback_iff_map_coyoneda_isPullback also shows that a square is a pullback square iff it is so after the application of the functor coyoneda.obj X for all X : Cᵒᵖ. Similarly, a square is a pushout square iff the opposite square becomes a pullback square after the application of the functor yoneda.obj X for all X : C.

theorem CategoryTheory.Square.IsPullback.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {sq : Square C} (h : sq.IsPullback) (F : Functor C D) [Limits.PreservesLimit (Limits.cospan sq.f₂₄ sq.f₃₄) F] : (sq.map F).IsPullback

theorem CategoryTheory.Square.IsPullback.of_map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {sq : Square C} (F : Functor C D) [Limits.ReflectsLimit (Limits.cospan sq.f₂₄ sq.f₃₄) F] (h : (sq.map F).IsPullback) : sq.IsPullback

theorem CategoryTheory.Square.IsPullback.map_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) [Limits.PreservesLimit (Limits.cospan sq.f₂₄ sq.f₃₄) F] [Limits.ReflectsLimit (Limits.cospan sq.f₂₄ sq.f₃₄) F] : (sq.map F).IsPullback ↔ sq.IsPullback

theorem CategoryTheory.Square.IsPushout.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {sq : Square C} (h : sq.IsPushout) (F : Functor C D) [Limits.PreservesColimit (Limits.span sq.f₁₂ sq.f₁₃) F] : (sq.map F).IsPushout

theorem CategoryTheory.Square.IsPushout.of_map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {sq : Square C} (F : Functor C D) [Limits.ReflectsColimit (Limits.span sq.f₁₂ sq.f₁₃) F] (h : (sq.map F).IsPushout) : sq.IsPushout

theorem CategoryTheory.Square.IsPushout.map_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) [Limits.PreservesColimit (Limits.span sq.f₁₂ sq.f₁₃) F] [Limits.ReflectsColimit (Limits.span sq.f₁₂ sq.f₁₃) F] : (sq.map F).IsPushout ↔ sq.IsPushout

theorem CategoryTheory.Square.isPullback_iff_map_coyoneda_isPullback {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.IsPullback ↔ ∀ (X : Cᵒᵖ), (sq.map (coyoneda.obj X)).IsPullback

theorem CategoryTheory.Square.isPushout_iff_op_map_yoneda_isPullback {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.IsPushout ↔ ∀ (X : C), (sq.op.map (yoneda.obj X)).IsPullback

theorem CategoryTheory.Square.IsPullback.iff_of_equiv (sq₁ : Square (Type v)) (sq₂ : Square (Type u)) (e₁ : sq₁.X₁ ≃ sq₂.X₁) (e₂ : sq₁.X₂ ≃ sq₂.X₂) (e₃ : sq₁.X₃ ≃ sq₂.X₃) (e₄ : sq₁.X₄ ≃ sq₂.X₄) (comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁) (comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁) (comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂) (comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃) : sq₁.IsPullback ↔ sq₂.IsPullback

theorem CategoryTheory.Square.IsPullback.of_equiv {sq₁ : Square (Type v)} {sq₂ : Square (Type u)} (e₁ : sq₁.X₁ ≃ sq₂.X₁) (e₂ : sq₁.X₂ ≃ sq₂.X₂) (e₃ : sq₁.X₃ ≃ sq₂.X₃) (e₄ : sq₁.X₄ ≃ sq₂.X₄) (comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁) (comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁) (comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂) (comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃) (h₁ : sq₁.IsPullback) : sq₂.IsPullback