Pushouts in Type

We describe the pushout of two maps f : S ⟶ X₁ and g : S ⟶ X₂ in the category of types as the quotient of X₁ ⊕ X₂ by the equivalence relation generated by a relation. We also study the particular case when f is injective (in the file CategoryTheory.Types.Monomorphisms, it is deduced that monomorphisms are stable under cobase change in the category of types).

instance CategoryTheory.Limits.Types.instHasPushoutsType : HasPushouts (Type u)

inductive CategoryTheory.Limits.Types.Pushout.Rel {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : X₁ ⊕ X₂ → X₁ ⊕ X₂ → Prop

The pushout of two maps f : S ⟶ X₁ and g : S ⟶ X₂ is the quotient by the equivalence relation on X₁ ⊕ X₂ generated by this relation.

• inl_inr {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S) : Rel f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inr ((ConcreteCategory.hom g) s))

def CategoryTheory.Limits.Types.Pushout {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : Type u

Construction of the pushout in the category of types, as a quotient of X₁ ⊕ X₂.

Equations

• CategoryTheory.Limits.Types.Pushout f g = Quot (CategoryTheory.Limits.Types.Pushout.Rel f g)

inductive CategoryTheory.Limits.Types.Pushout.Rel' {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : X₁ ⊕ X₂ → X₁ ⊕ X₂ → Prop

In case f : S ⟶ X₁ is a monomorphism, this relation is the equivalence relation generated by Pushout.Rel f g.

• refl {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x : X₁ ⊕ X₂) : Rel' f g x x
• inl_inl {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x₀ y₀ : S) (h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀) : Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inl ((ConcreteCategory.hom f) y₀))
• inl_inr {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S) : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inr ((ConcreteCategory.hom g) s))
• inr_inl {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S) : Rel' f g (Sum.inr ((ConcreteCategory.hom g) s)) (Sum.inl ((ConcreteCategory.hom f) s))

def CategoryTheory.Limits.Types.Pushout' {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : Type u

The quotient of X₁ ⊕ X₂ by the relation PushoutRel' f g.

Equations

• CategoryTheory.Limits.Types.Pushout' f g = Quot (CategoryTheory.Limits.Types.Pushout.Rel' f g)

def CategoryTheory.Limits.Types.Pushout.inl {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : X₁ ⟶ Pushout f g

The left inclusion in the constructed pushout Pushout f g.

Equations

• CategoryTheory.Limits.Types.Pushout.inl f g = TypeCat.ofHom fun (x : X₁) => Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inl x)

def CategoryTheory.Limits.Types.Pushout.inr {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : X₂ ⟶ Pushout f g

The right inclusion in the constructed pushout Pushout f g.

Equations

• CategoryTheory.Limits.Types.Pushout.inr f g = TypeCat.ofHom fun (x : X₂) => Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inr x)

theorem CategoryTheory.Limits.Types.Pushout.condition {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : CategoryStruct.comp f (inl f g) = CategoryStruct.comp g (inr f g)

def CategoryTheory.Limits.Types.Pushout.cocone {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : PushoutCocone f g

The constructed pushout cocone in the category of types.

Equations

• CategoryTheory.Limits.Types.Pushout.cocone f g = CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.Types.Pushout.inl f g) (CategoryTheory.Limits.Types.Pushout.inr f g) ⋯

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.cocone_ι_app {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (j : WalkingSpan) : (cocone f g).ι.app j = Option.rec (CategoryStruct.comp f (TypeCat.ofHom fun (x : X₁) => Quot.mk (Rel f g) (Sum.inl x))) (fun (val : WalkingPair) => WalkingPair.rec (TypeCat.ofHom fun (x : X₁) => Quot.mk (Rel f g) (Sum.inl x)) (TypeCat.ofHom fun (x : X₂) => Quot.mk (Rel f g) (Sum.inr x)) val) j

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.cocone_pt {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : (cocone f g).pt = Pushout f g

def CategoryTheory.Limits.Types.Pushout.isColimitCocone {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : IsColimit (cocone f g)

The cocone cocone f g is colimit.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inl_iff {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₁ y₁ : X₁) : Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔ x₁ = y₁ ∨ ∃ (x₀ : S) (y₀ : S) (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀), x₁ = (ConcreteCategory.hom f) x₀ ∧ y₁ = (ConcreteCategory.hom f) y₀

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inr_iff {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₁ : X₁) (x₂ : X₂) : Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ (s : S), x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.inr_rel'_inr_iff {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₂ y₂ : X₂) : Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂

theorem CategoryTheory.Limits.Types.Pushout.Rel'.symm {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {x y : X₁ ⊕ X₂} (h : Rel' f g x y) : Rel' f g y x

theorem CategoryTheory.Limits.Types.Pushout.equivalence_rel' {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [Mono f] : _root_.Equivalence (Rel' f g)

def CategoryTheory.Limits.Types.Pushout.equivPushout' {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : Pushout f g ≃ Pushout' f g

The obvious equivalence Pushout f g ≃ Pushout' f g.

Equations

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

theorem CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [Mono f] (a b : X₁ ⊕ X₂) : Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Rel' f g a b

theorem CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [Mono f] (x₁ : X₁) (x₂ : X₂) : (ConcreteCategory.hom (inl f g)) x₁ = (ConcreteCategory.hom (inr f g)) x₂ ↔ ∃ (s : S), (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

instance CategoryTheory.Limits.Types.Pushout.mono_inr {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [Mono f] : Mono (inr f g)

theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c c' : PushoutCocone f g} (e : c ≅ c') (x₁ : X₁) (x₂ : X₂) (h : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂) : (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂

theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c c' : PushoutCocone f g} (e : c ≅ c') (x₁ : X₁) (x₂ : X₂) : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂ ↔ (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂

theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : PushoutCocone f g} (hc : IsColimit c) (h₁ : Function.Injective ⇑(ConcreteCategory.hom f)) (x₁ : X₁) (x₂ : X₂) : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂ ↔ ∃ (s : S), (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

theorem CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : PushoutCocone f g} (hc : IsColimit c) [Mono f] : Mono c.inr

theorem CategoryTheory.Limits.Types.pushoutCocone_inr_injective_of_isColimit {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : PushoutCocone f g} (hc : IsColimit c) (h₁ : Function.Injective ⇑(ConcreteCategory.hom f)) : Function.Injective ⇑(ConcreteCategory.hom c.inr)

instance CategoryTheory.Limits.Types.mono_inl {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} [Mono g] : Mono (Pushout.inl f g)

instance CategoryTheory.Limits.Types.instMonoPushoutInr {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} [Mono f] : Mono (pushout.inr f g)

instance CategoryTheory.Limits.Types.instMonoPushoutInl {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} [Mono g] : Mono (pushout.inl f g)

theorem CategoryTheory.Limits.Types.eq_or_eq_of_isPushout {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} (h : IsPushout t l r b) (x₄ : X₄) : (∃ (x₂ : (fun (X : Type u) => X) X₂), (ConcreteCategory.hom r) x₂ = x₄) ∨ ∃ (x₃ : (fun (X : Type u) => X) X₃), (ConcreteCategory.hom b) x₃ = x₄

theorem CategoryTheory.Limits.Types.eq_or_eq_of_isPushout' {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} (h : IsPushout t l r b) (x₄ : X₄) : (∃ (x₂ : (fun (X : Type u) => X) X₂), (ConcreteCategory.hom r) x₂ = x₄) ∨ ∃ (x₃ : (fun (X : Type u) => X) X₃), (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

theorem CategoryTheory.Limits.Types.isPullback_of_isPushout {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} (h : IsPushout t l r b) (ht : Function.Injective ⇑(ConcreteCategory.hom t)) : IsPullback t l r b

A pushout square in Type where the top map is injective is a pullback square. This is also essentially the lemma isPullback_of_isPushout_of_mono_left from the file CategoryTheory.Adhesive.Basic in the case of the adhesive category of types.

theorem CategoryTheory.Limits.Types.mono_of_isPushout_of_isPullback {X₁ X₂ X₃ X₄ X₅ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} {k : X₄ ⟶ X₅} (h₁ : IsPushout t l r b) {r' : X₂ ⟶ X₅} {b' : X₃ ⟶ X₅} (h₂ : IsPullback t l r' b') (facr : CategoryStruct.comp r k = r') (facb : CategoryStruct.comp b k = b') [hr' : Mono r'] (H : ∀ (x₃ y₃ : X₃), x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃) : Mono k

Consider a pushout square involving types X₁, X₂, X₃ and X₄:

     t
 X₁  ⟶  X₂
l|     |r  \
 v   b  v   \ r'
 X₃  ⟶  X₄   \
  \       k\  |
   \ b'     v v
    \______> X₅

Let k : X₄ ⟶ X₅, r' : X₂ ⟶ X₅ and b' : X₃ ⟶ X₅ be such that r ≫ k = r' and b ≫ k = b'. Assume that the outer square is a pullback, that r' is a monomorphism and that b' is injective on the complement of the range of l, then k : X₄ ⟶ X₅ is a monomorphism.

theorem CategoryTheory.Limits.Types.isPushout_of_isPullback_of_mono {X₁ X₂ X₃ X₄ X₅ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} {k : X₄ ⟶ X₅} {r' : X₂ ⟶ X₅} {b' : X₃ ⟶ X₅} (h₁ : IsPullback t l r' b') (facr : CategoryStruct.comp r k = r') (facb : CategoryStruct.comp b k = b') [Mono r'] [Mono k] (h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ) (H : ∀ (x₃ y₃ : X₃), x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃) : IsPushout t l r b

Consider a diagram where the outer square involving types X₁, X₂, X₃ and X₅ is a pullback, where the two bottom and right triangles commute:

     t
 X₁  ⟶  X₂
l|     |r  \
 v   b  v   \ r'
 X₃  ⟶  X₄   \
  \       k\  |
   \ b'     v v
    \______> X₅

Assume that r' and k are monomorphisms, that r and b are jointly surjective, and that b' is injective on the complement of the range of l, then the top-left square is a pushout.

theorem CategoryTheory.Limits.Types.isPushout_of_isPullback_of_mono' {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} (h₁ : IsPullback t l r b) [Mono r] (h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ) (H : ∀ (x₃ y₃ : X₃), x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃ → x₃ = y₃) : IsPushout t l r b

Consider a pullback square of types where the right map is a monomorphism. If the right and bottom map are jointly surjective, and the bottom map is injective on the complement on the range of the left map, then the square is a pushout square.