Pushout-products in adhesive categories #
This file proves that the pushout-product of monomorphisms in an adhesive cartesian monoidal category is a monomorphism.
theorem CategoryTheory.Functor.PushoutObjObj.mono_ι_of_isPullback {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {X₂ Y₂ : C₂} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂} [Adhesive C₃] (sq : F.PushoutObjObj f₁ f₂) (h : IsPullback ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂)) [Mono ((F.obj Y₁).map f₂)] [Mono ((F.map f₁).app Y₂)] :
The induced pushout map (Leibniz pushout) of an F.PushoutObjObj is a monomorphism if its
naturality square is a pullback and the morphisms being pulled back are monomorphisms.
instance CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.instMonoHomObjArrowFunctorPushoutProduct {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [CartesianMonoidalCategory C] [Adhesive C] {X Y : Arrow C} [Mono X.hom] [Mono Y.hom] :
Mono ((pushoutProduct.obj X).obj Y).hom
The pushout-product of two monomorphisms in an adhesive cartesian monoidal category is a monomorphism.