Commit 2026-03-22 12:35 a6c795e0

feat(Combinatorics/SimpleGraph/LineGraph): lift copies/isomorphisms to line-graph (#33292) Non-injective homomorphisms (G →g G') cannot be lifted to a homomorphism on line-graphs (G.lineGraph →g G'.lineGraph) because e.g. ∀ k > 1 there is a homomorphism from pathGraph k to G' iff G' has an edge, and ∀ n > 0, (pathGraph (n + 1)).lineGraph ≃ pathGraph n, but there is no homomorphism from pathGraph k to pathGraph 1 because it has no edges. So for G := pathGraph 3 and G' := pathGraph 2 there is a G →g G' but no G.lineGraph →g G'.lineGraph. But we can lift Copy/Embedding/Iso.