feat(Combinatorics/SimpleGraph/Copy): add indLabelledCopyCount and indCopyCount

Fills in the two TODO sections in `Mathlib/Combinatorics/SimpleGraph/Copy.lean`:

- `indLabelledCopyCount`: number of induced labelled copies of `H` in `G` (i.e. `|H ↪g G|`),
  the induced analogue of `labelledCopyCount`
- `indCopyCount`: number of induced unlabelled copies of `H` in `G` (i.e. number of induced
  subgraphs of `G` isomorphic to `H`), the induced analogue of `copyCount`

Supporting additions:
- `Copy.range_embeddingToSubgraph`: range of `f ↦ f.toCopy.toSubgraph` over embeddings equals
  `{B' | B'.IsInduced ∧ Nonempty (H ≃g B'.coe)}`, the induced analogue of `Copy.range_toSubgraph`
- `Subgraph.coe_isIndContained`: induced analogue of `Subgraph.coe_isContained`
- `Subgraph.IsInduced.toEmbedding`: canonical embedding `G'.coe ↪g G` for an induced subgraph,
  the embedding analogue of `Subgraph.hom`
- `Subgraph.IsInduced.map`: mapping an induced subgraph through an embedding stays induced
- `Embedding.comp_toHom`: `(f'.comp f).toHom = f'.toHom.comp f.toHom` (@[simp])

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -45,6 +45,10 @@ Containment:
 Induced containment:
 * Induced copies of `G` inside `H` are already defined as `G ↪g H`.
 * `SimpleGraph.IsIndContained G H` : `G` is contained as an induced subgraph in `H`.
+* `SimpleGraph.indLabelledCopyCount G H`: Number of induced labelled copies of `H` in `G`, i.e.
+  number of graph embeddings `H ↪g G`.
+* `SimpleGraph.indCopyCount G H`: Number of induced unlabelled copies of `H` in `G`, i.e. number
+  of induced subgraphs of `G` isomorphic to `H`.
 
 ## Notation
 
@@ -55,7 +59,6 @@ The following notation is declared in scope `SimpleGraph`:
 ## TODO
 
 * Relate `⊥ ⊴ H` to there being an independent set in `H`.
-* Count induced copies of a graph inside another.
 * Make `copyCount`/`labelledCopyCount` computable (not necessarily efficiently).
 -/
 
@@ -187,6 +190,19 @@ noncomputable def isoToSubgraph (f : Copy A B) : A ≃g f.toSubgraph.coe :=
     refine ⟨⟨H'.hom.comp e.toHom, Subgraph.hom_injective.comp e.injective⟩, ?_⟩
     simp [toSubgraph, Subgraph.map_comp]
 
+/-- The range of `f ↦ f.toCopy.toSubgraph` over embeddings is exactly the induced subgraphs
+isomorphic to `A`. Induced analogue of `Copy.range_toSubgraph`. -/
+lemma range_embeddingToSubgraph :
+    Set.range (fun f : A ↪g B => f.toCopy.toSubgraph) =
+    {B' : B.Subgraph | B'.IsInduced ∧ Nonempty (A ≃g B'.coe)} := by
+  ext G'
+  simp only [Set.mem_range, Set.mem_setOf_eq]
+  constructor
+  · rintro ⟨f, rfl⟩
+    exact ⟨Subgraph.IsInduced.top.map f, ⟨f.toCopy.isoToSubgraph⟩⟩
+  · rintro ⟨hInd, ⟨e⟩⟩
+    exact ⟨hInd.toEmbedding.comp e.toEmbedding, by simp [toSubgraph, Subgraph.map_comp]⟩
+
 lemma toSubgraph_surjOn :
     Set.SurjOn (toSubgraph (A := A)) .univ {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} :=
   fun H' hH' ↦ by simpa
@@ -409,11 +425,8 @@ protected lemma Iso.isIndContained (e : G ≃g H) : G ⊴ H := e.toEmbedding.isI
 /-- If `G` is isomorphic to `H`, then `H` is inducingly contained in `G`. -/
 protected lemma Iso.isIndContained' (e : G ≃g H) : H ⊴ G := e.symm.isIndContained
 
-protected lemma Subgraph.IsInduced.isIndContained {G' : G.Subgraph} (hG' : G'.IsInduced) :
-    G'.coe ⊴ G :=
-  ⟨{ toFun := (↑)
-     inj' := Subtype.coe_injective
-     map_rel_iff' := hG'.adj.symm }⟩
+lemma Subgraph.coe_isIndContained {G' : G.Subgraph} (hG' : G'.IsInduced) : G'.coe ⊴ G :=
+  ⟨hG'.toEmbedding⟩
 
 @[refl] lemma IsIndContained.refl (G : SimpleGraph V) : G ⊴ G := ⟨Embedding.refl⟩
 lemma IsIndContained.rfl : G ⊴ G := .refl _
@@ -440,7 +453,7 @@ lemma isIndContained_iff_exists_iso_subgraph :
     refine ⟨Subgraph.map f.toHom ⊤, f.toCopy.isoToSubgraph, ?_⟩
     simp [Subgraph.IsInduced, Relation.map_apply_apply, f.injective]
   · rintro ⟨H', e, hH'⟩
-    exact e.isIndContained.trans hH'.isIndContained
+    exact e.isIndContained.trans (Subgraph.coe_isIndContained hH')
 
 alias ⟨IsIndContained.exists_iso_subgraph, IsIndContained.of_exists_iso_subgraph⟩ :=
   isIndContained_iff_exists_iso_subgraph
@@ -543,9 +556,92 @@ end CopyCount
 
 /-!
 #### Induced copies
+-/
 
-TODO
+section IndLabelledCopyCount
+variable [Fintype V] [Fintype W]
+
+/-- `G.indLabelledCopyCount H` is the number of induced labelled copies of `H` in `G`,
+i.e., the number of graph embeddings from `H` to `G`.
+
+This is the induced analogue of `SimpleGraph.labelledCopyCount`. -/
+noncomputable def indLabelledCopyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
+  classical exact Fintype.card (H ↪g G)
+
+@[simp] lemma indLabelledCopyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
+    G.indLabelledCopyCount H = 1 := by
+  convert Fintype.card_unique
+  exact { default := RelEmbedding.ofIsEmpty H.Adj G.Adj
+          uniq := fun f => RelEmbedding.ext fun a => isEmptyElim a }
+
+@[simp] lemma indLabelledCopyCount_eq_zero : G.indLabelledCopyCount H = 0 ↔ ¬(H ⊴ G) := by
+  simp [indLabelledCopyCount, Fintype.card_eq_zero_iff, IsIndContained]
+
+@[simp] lemma indLabelledCopyCount_pos : 0 < G.indLabelledCopyCount H ↔ H ⊴ G := by
+  simp [Nat.pos_iff_ne_zero, indLabelledCopyCount_eq_zero]
+
+/-- Every induced labelled copy is a (non-induced) labelled copy. -/
+lemma indLabelledCopyCount_le_labelledCopyCount :
+    G.indLabelledCopyCount H ≤ G.labelledCopyCount H := by
+  classical
+  simp only [indLabelledCopyCount, labelledCopyCount]
+  exact Fintype.card_le_of_injective Embedding.toCopy fun f g h =>
+    RelEmbedding.ext fun w => DFunLike.congr_fun h w
+
+end IndLabelledCopyCount
+
+section IndCopyCount
+variable [Fintype V]
 
+/-- `G.indCopyCount H` is the number of induced unlabelled copies of `H` in `G`,
+i.e., the number of induced subgraphs of `G` isomorphic to `H`.
+
+This is the induced analogue of `SimpleGraph.copyCount`. -/
+noncomputable def indCopyCount (G : SimpleGraph V) (H : SimpleGraph W) : ℕ := by
+  classical exact #{G' : G.Subgraph | G'.IsInduced ∧ Nonempty (H ≃g G'.coe)}
+
+lemma indCopyCount_eq_card_image_embeddingToSubgraph
+    [Fintype W] [DecidableEq G.Subgraph] :
+    G.indCopyCount H = #((Finset.univ : Finset (H ↪g G)).image (·.toCopy.toSubgraph)) := by
+  rw [indCopyCount]
+  congr
+  refine Finset.coe_injective ?_
+  simpa using Copy.range_embeddingToSubgraph.symm
+
+@[simp] lemma indCopyCount_pos : 0 < G.indCopyCount H ↔ H ⊴ G := by
+  rw [isIndContained_iff_exists_iso_subgraph]
+  classical
+  simp only [indCopyCount, card_pos, filter_nonempty_iff, mem_univ, true_and]
+  exact ⟨fun ⟨G', hInd, hn⟩ => ⟨G', hn.some, hInd⟩,
+         fun ⟨G', e, hInd⟩ => ⟨G', hInd, ⟨e⟩⟩⟩
+
+@[simp] lemma indCopyCount_eq_zero : G.indCopyCount H = 0 ↔ ¬(H ⊴ G) := by
+  rw [← indCopyCount_pos]; omega
+
+/-- Every induced unlabelled copy corresponds to at least one induced labelled copy. -/
+lemma indCopyCount_le_indLabelledCopyCount [Fintype W] :
+    G.indCopyCount H ≤ G.indLabelledCopyCount H := by
+  classical
+  rw [indCopyCount_eq_card_image_embeddingToSubgraph, indLabelledCopyCount]
+  exact card_image_le
+
+@[simp] lemma indCopyCount_of_isEmpty [IsEmpty W] (G : SimpleGraph V) (H : SimpleGraph W) :
+    G.indCopyCount H = 1 := by
+  cases nonempty_fintype W
+  exact (indCopyCount_le_indLabelledCopyCount.trans_eq <|
+      indLabelledCopyCount_of_isEmpty ..).antisymm <|
+    indCopyCount_pos.2 <| .of_isEmpty
+
+/-- Every induced unlabelled copy is a (non-induced) unlabelled copy. -/
+lemma indCopyCount_le_copyCount : G.indCopyCount H ≤ G.copyCount H := by
+  classical
+  simp only [indCopyCount, copyCount]
+  exact Finset.card_le_card fun G' hG' => by
+    simp only [mem_filter, mem_univ, true_and] at hG' ⊢; exact hG'.2
+
+end IndCopyCount
+
+/-!
 ### Killing a subgraph
 
 An important aspect of graph containment is that we can remove not too many edges from a graph `H`

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -529,6 +529,9 @@ abbrev comp (f' : G' ↪g G'') (f : G ↪g G') : G ↪g G'' :=
 theorem coe_comp (f' : G' ↪g G'') (f : G ↪g G') : ⇑(f'.comp f) = f' ∘ f :=
   rfl
 
+@[simp] lemma comp_toHom (f' : G' ↪g G'') (f : G ↪g G') :
+    (f'.comp f).toHom = f'.toHom.comp f.toHom := rfl
+
 /-- Graph embeddings from `G` to `H` are the same thing as graph embeddings from `Gᶜ` to `Hᶜ`. -/
 def complEquiv : G ↪g H ≃ Gᶜ ↪g Hᶜ where
   toFun f := ⟨f.toEmbedding, by simp⟩

Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

@@ -669,6 +669,15 @@ theorem map_sup (f : G →g G') (H₁ H₂ : G.Subgraph) : (H₁ ⊔ H₂).map f
 @[simp] lemma edgeSet_map (f : G →g G') (H : G.Subgraph) :
     (H.map f).edgeSet = Sym2.map f '' H.edgeSet := Sym2.fromRel_relationMap ..
 
+lemma IsInduced.map {H : G.Subgraph} (hH : H.IsInduced) (e : G ↪g G') :
+    (H.map e.toHom).IsInduced := by
+  intro v hv w hw hAdj
+  rw [map_verts] at hv hw
+  obtain ⟨a, ha, rfl⟩ := hv
+  obtain ⟨b, hb, rfl⟩ := hw
+  simp only [map_adj, Relation.map_apply]
+  exact ⟨a, b, hH ha hb (e.map_adj_iff.mp hAdj), rfl, rfl⟩
+
 end map
 
 /-- Graph homomorphisms induce a contravariant function on subgraphs. -/
@@ -747,6 +756,15 @@ theorem hom_injective {x : Subgraph G} : Function.Injective x.hom :=
 @[simp] lemma map_hom_top (G' : G.Subgraph) : Subgraph.map G'.hom ⊤ = G' := by
   aesop (add unfold safe Relation.Map, unsafe G'.edge_vert, unsafe Adj.symm)
 
+/-- The canonical embedding of an induced subgraph into the ambient graph.
+Unlike `Subgraph.hom`, this is an embedding rather than a homomorphism, since induced subgraphs
+reflect adjacency. -/
+def IsInduced.toEmbedding {G' : G.Subgraph} (hG' : G'.IsInduced) : G'.coe ↪g G :=
+  { toFun := (↑), inj' := Subtype.coe_injective, map_rel_iff' := hG'.adj.symm }
+
+@[simp] lemma IsInduced.toHom_toEmbedding {G' : G.Subgraph} (hG' : G'.IsInduced) :
+    hG'.toEmbedding.toHom = G'.hom := rfl
+
 /-- There is an induced injective homomorphism of a subgraph of `G` as
 a spanning subgraph into `G`. -/
 @[simps]