tighten inducedShape docstrings; add Embedding.inducedShape_toCopy

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Inversion.lean

@@ -79,35 +79,25 @@ noncomputable instance instLocallyFiniteOrder [Fintype V] [DecidableEq V] :
 
 /-! ### Induced shape of a copy
 
-For a copy `f : Copy G H` with `G : SimpleGraph V` the guest, 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`,
-and its fiber under `Copy.inducedShape` is canonically `Embedding G' H` for each
-supergraph `G' ∈ Icc G ⊤`. -/
+The pullback `H.comap f.toEmbedding` records the induced adjacency on the image of a copy
+`f : Copy G H`, transported back to `V`. It is always a supergraph of `G`, and pinning it
+down to a specific supergraph `G'` promotes the copy to an embedding `G' ↪g H`. -/
 
 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 : V ↪ W`. This is always a supergraph of `G`
-(by `Copy.le_inducedShape`); it records the induced subgraph of `H` on the image of `f`,
-transported back to the vertex type `V`. -/
-@[expose] def inducedShape (f : Copy G H) : SimpleGraph V :=
+/-- The pullback of the host graph along the underlying injection of a copy. -/
+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 `f : Copy G H` 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'`. -/
+/-- A copy with induced shape `G'` promotes to a graph embedding `G' ↪g H`. -/
 @[expose] def toEmbeddingOfInducedShapeEq (f : Copy G H) (h : f.inducedShape = G') :
     G' ↪g H where
   toFun := f
@@ -119,27 +109,20 @@ that is missing in `Copy` is recovered from `h : f.inducedShape = G'`. -/
 @[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
-isomorphic to the type of graph embeddings `G' ↪g H`. The underlying function of the copy
-is the same as the underlying function of the embedding; the only difference is the explicit
-recording of the iff-direction of adjacency, made possible by the inducedShape-equation. -/
+/-- The fiber of `inducedShape` over a supergraph `G' ≥ G` is canonically `Embedding G' H`. -/
 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
+  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
 
+@[simp] lemma Embedding.inducedShape_toCopy {G : SimpleGraph V} {H : SimpleGraph W}
+    (e : Embedding G H) : e.toCopy.inducedShape = G := by
+  ext a b; rw [Copy.inducedShape_adj]; exact e.map_rel_iff
+
 /-! ### Forward bijection and count identity -/
 
 section Forward