Lax Lean Archive

Proof of `Homomorphism counts into a categorical product`

groundedproofs/Lax871432Proofs/Results.lean · lax-871432

What this proof establishes

no assumptions

lem✓Lax871432.CategoricalProductCounts

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

  • page 3 of this submission's paper

Description

eq:producteq:product. Composing with the two projections is a bijection from the homomorphisms into G1×gG2G₁ ×g G₂ onto pairs of homomorphisms into G1G₁ and into G2G₂: the categorical product is the product in the category of graphs and graph homomorphisms.