feat(Combinatorics/SimpleGraph/InducedCopy): Copy.inducedShape

For a copy `f : Copy G H`, the *induced shape* of `f` is the pullback
`H.comap f.toEmbedding`: a graph on `V` whose adjacency records the induced
adjacency of `H` restricted to the image of `f`.

Adds:
* `Copy.inducedShape`, `Copy.inducedShape_adj`, `Copy.le_inducedShape`.
* `Copy.toEmbeddingOfInducedShapeEq`: promotes a copy whose induced shape
  equals a prescribed supergraph `G' ≥ G` to an embedding `G' ↪g H`.
* `Copy.fiberInducedShapeEquiv`: the per-supergraph bijection
  `{f : Copy G H // f.inducedShape = G'} ≃ Embedding G' H`.

This material is the load-bearing fiber decomposition consumed by the
Möbius inversion `copyCount_eq_sum_embeddingCount` /
`embeddingCount_eq_sum_signed_copyCount` (downstream PR).

`Copy.toEmbeddingOfInducedShapeEq` is `@[expose]` for the same reason as
`Copy.toEmbeddingOfIsInduced`: its `_apply` simp lemma needs the body to
unfold across modules.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean

@@ -89,6 +89,71 @@ abbrev toSubgraph (f : Embedding G H) : H.Subgraph := f.toCopy.toSubgraph
 
 end Embedding
 
+/-!
+### Induced shape of a copy
+
+For a copy `f : Copy G H`, the *induced shape* of `f` is the pullback `H.comap f.toEmbedding`:
+a graph on `V` whose adjacency records the induced adjacency of `H` restricted to the image
+of `f`. It is always a supergraph of `G` (`Copy.le_inducedShape`), and a copy whose induced
+shape equals a prescribed supergraph `G' ≥ G` upgrades to a graph embedding `G' ↪g H`. The
+fibers of `Copy.inducedShape` over supergraphs `G' ≥ G` are canonically embeddings
+`G' ↪g H` (`Copy.fiberInducedShapeEquiv`).
+-/
+
+namespace Copy
+
+variable {G G' : SimpleGraph V} {H : SimpleGraph W}
+
+/-- The *induced shape* of a copy `f : Copy G H` is the pullback of the host graph along
+the underlying injection `f.toEmbedding`. This is always a supergraph of `G`
+(`Copy.le_inducedShape`); it records the induced subgraph of `H` on the image of `f`,
+transported back to the vertex type `V`. -/
+def inducedShape (f : Copy G H) : SimpleGraph V :=
+  H.comap f.toEmbedding
+
+/-- Adjacency in the induced shape unfolds to adjacency in `H` at the image vertices. -/
+@[simp] lemma inducedShape_adj (f : Copy G H) {a b : V} :
+    f.inducedShape.Adj a b ↔ H.Adj (f a) (f b) := Iff.rfl
+
+/-- A copy is dominated by its induced shape: every edge of `G` is mapped to an edge of
+`H`, hence appears as an edge of the pullback. -/
+lemma le_inducedShape (f : Copy G H) : G ≤ f.inducedShape :=
+  fun _ _ => f.toHom.map_adj
+
+/-- Promote a copy whose induced shape equals a specified supergraph `G'` to a graph
+embedding `G' ↪g H`. The underlying function is `f` itself; the adjacency-iff direction
+that is missing in `Copy` is recovered from `h : f.inducedShape = G'`. -/
+@[expose] def toEmbeddingOfInducedShapeEq (f : Copy G H) (h : f.inducedShape = G') : G' ↪g H where
+  toFun := f
+  inj' := f.injective
+  map_rel_iff' {a b} := by
+    change H.Adj (f a) (f b) ↔ G'.Adj a b
+    rw [← h, inducedShape_adj]
+
+@[simp] lemma toEmbeddingOfInducedShapeEq_apply (f : Copy G H) (h : f.inducedShape = G')
+    (v : V) : f.toEmbeddingOfInducedShapeEq h v = f v := rfl
+
+/-- The fiber of `Copy.inducedShape` over a fixed supergraph `G'` of `G` is canonically
+equivalent to the type of graph embeddings `G' ↪g H`. The underlying function of the copy
+matches the underlying function of the embedding; the only added datum is the
+adjacency-iff direction recovered from the inducedShape equation. -/
+def fiberInducedShapeEquiv (hGG' : G ≤ G') :
+    {f : Copy G H // f.inducedShape = G'} ≃ Embedding G' H where
+  toFun f := f.val.toEmbeddingOfInducedShapeEq f.prop
+  invFun e := ⟨e.toCopy.comp (Copy.ofLE G G' hGG'), by
+    ext a b
+    simp [inducedShape]⟩
+  left_inv f := by
+    apply Subtype.ext
+    ext v
+    simp
+  right_inv e := by
+    apply DFunLike.ext
+    intro v
+    simp
+
+end Copy
+
 /-!
 ### Induced containment