Window lemma for pushouts

1. Proposition

Let 20231102-window_lemma_for_pushouts_760824120891fc757bc0445145b027d09b237baa.svg be a category and

20231102-window_lemma_for_pushouts_91bc1ed755b2b9b14a79070ff56342e515238e02.svg

be a commutative diagram, such that

20231102-window_lemma_for_pushouts_912927aa55351b10a21eec42e7d3c48a2fcf9393.svg

and

20231102-window_lemma_for_pushouts_542ba072b3a2a422688ddee8f53cf48d971a5bf5.svg

are pushouts

Then

20231102-window_lemma_for_pushouts_abb00f62818c83954b35b75ce364c8343a9cd08a.svg

is also a pushout

2. Proof

2.1. existence

Suppose there exists morphism

20231102-window_lemma_for_pushouts_09aa72ad36782b0b2687acee8bfc5f7e1d567a4d.svg

Then by commutativity

20231102-window_lemma_for_pushouts_1508fb015e10259f7d6226d375f2f4b1f7e04ea3.svg

It follows, that

20231102-window_lemma_for_pushouts_64764bc91f65ca2517cd494b3884e832727a84dc.svg

2.2. uniqueness

Date: nil

Author: Anton Zakrewski

Created: 2024-10-13 So 18:59