Lemmaprecheck passverified 2026-09-24 (gpt-6-sol)

Horizontally pasted commutative squares commute

Statement

Given two commutative squares sharing the edge $h$ , pasted horizontally,

the outer rectangle commutes: $h^{'} \circ (f^{'} \circ f) = (k^{'} \circ k) \circ g$ .

Facts & Assumptions

Given: Objects and morphisms of the two squares above.

Diagram: $f ⁣ : A \to B$ , $f^{'} ⁣ : B \to C$ , $g ⁣ : A \to A^{'}$ , $h ⁣ : B \to B^{'}$ , $h^{'} ⁣ : C \to C^{'}$ , $k ⁣ : A^{'} \to B^{'}$ , $k^{'} ⁣ : B^{'} \to C^{'}$ .

[C1]

$h \circ f = k \circ g$ (given: the left square commutes).

[C2]

$h^{'} \circ f^{'} = k^{'} \circ h$ (given: the right square commutes).

[A1]

Composition of morphisms in a category is associative.

Proof

technique · direct

1.1

$h^{'} \circ (f^{'} \circ f) = (h^{'} \circ f^{'}) \circ f = (k^{'} \circ h) \circ f$ , applying associativity and the right square $h^{'} \circ f^{'} = k^{'} \circ h$ .

A1C2

2.1

$(k^{'} \circ h) \circ f = k^{'} \circ (h \circ f) = k^{'} \circ (k \circ g)$ , applying associativity and the left square $h \circ f = k \circ g$ .

A1C1step 1.1

3.1

$k^{'} \circ (k \circ g) = (k^{'} \circ k) \circ g$ by associativity, so $h^{'} \circ (f^{'} \circ f) = (k^{'} \circ k) \circ g$ : the outer rectangle commutes.

A1step 1.1step 2.1∎

Depends on

Category, object, morphism, domain, codomain, identity, composition, and hom-collection

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Ch. 1 (standard reference, not scraped)