feat(Combinatorics/SimpleGraph/Inversion): Möbius inversion between copy counts and induced copy counts

Adds the bijection `Copy.equivSigmaEmbedding`, the labelled forward count
identity `copyCount_eq_sum_embeddingCount`, and its Möbius inverse
`embeddingCount_eq_sum_signed_copyCount` over ℤ. The Möbius direction reduces
via the order-equivalence `iccEquivPowersetEdgeFinsetSdiff` between `Icc G K`
and the powerset of the edge difference to `Finset.sum_powerset_neg_one_pow_card`.

Supporting `Copy.inducedShape` (the pullback `H.comap f.toEmbedding`) and the
per-fiber bijection `Copy.fiberInducedShapeEquiv` are kept inline in this file
rather than split out, since neither has a standalone consumer outside this
Möbius decomposition.

Co-authored-by: Malte Jackisch <45597826+MaltyBlanket@users.noreply.github.com>

Author: FordUniver

Mathlib.lean

@@ -3620,6 +3620,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Hasse
 public import Mathlib.Combinatorics.SimpleGraph.IncMatrix
 public import Mathlib.Combinatorics.SimpleGraph.InducedCopy
 public import Mathlib.Combinatorics.SimpleGraph.Init
+public import Mathlib.Combinatorics.SimpleGraph.Inversion
 public import Mathlib.Combinatorics.SimpleGraph.LapMatrix
 public import Mathlib.Combinatorics.SimpleGraph.LineGraph
 public import Mathlib.Combinatorics.SimpleGraph.Maps

Mathlib/Combinatorics/SimpleGraph/Inversion.lean

@@ -0,0 +1,298 @@
+/-
+Copyright (c) 2026 Christoph Spiegel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christoph Spiegel
+-/
+module
+
+public import Mathlib.Algebra.BigOperators.Field
+public import Mathlib.Combinatorics.SimpleGraph.Automorphism
+public import Mathlib.Combinatorics.SimpleGraph.Finite
+public import Mathlib.Data.Nat.Choose.Sum
+public import Mathlib.Data.Rat.Cast.Defs
+
+/-!
+# Möbius inversion between copy counts and induced copy counts
+
+For a guest graph `G : SimpleGraph V` and a host graph `H : SimpleGraph W` with finite
+vertex types, this file establishes the standard summation identity expressing the copy
+count `H.copyCount G` as a sum over supergraphs of `G` (on the same vertex type `V`) of
+induced copy counts `H.embeddingCount G'`, together with its Möbius inverse expressing
+`H.embeddingCount G` as a signed sum of `H.copyCount G'`.
+
+Following the convention from `Mathlib/Combinatorics/SimpleGraph/Copy.lean` and
+`Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean`, counting operations are host-first
+(`H.copyCount G`, `H.embeddingCount G`); types are guest-first (`Copy G H`, `Embedding G H`).
+
+## Main declarations
+
+* `SimpleGraph.Copy.inducedShape` — for `f : Copy G H`, the supergraph of `G` on `V`
+  recording the induced adjacency on the image, transported back via `f.toEmbedding`.
+* `SimpleGraph.Copy.fiberInducedShapeEquiv` — the per-fiber bijection between copies with a
+  prescribed induced shape and graph embeddings of that shape.
+* `SimpleGraph.Copy.equivSigmaEmbedding` — the load-bearing bijection
+  `Copy G H ≃ Σ G' ∈ Icc G ⊤, Embedding G'.val H`.
+* `SimpleGraph.iccEquivPowersetEdgeFinsetSdiff` — for `G ≤ K`, the equivalence
+  `Finset.Icc G K ≃ (K.edgeFinset \ G.edgeFinset).powerset` used to reduce the inner
+  alternating sum to `Finset.sum_powerset_neg_one_pow_card`.
+
+## Main results
+
+* `SimpleGraph.copyCount_eq_sum_embeddingCount` — forward identity:
+  `H.copyCount G = ∑ G' ∈ Icc G ⊤, H.embeddingCount G'`.
+* `SimpleGraph.embeddingCount_eq_sum_signed_copyCount` — Möbius inverse over `ℤ`:
+  `(H.embeddingCount G : ℤ) = ∑ G' ∈ Icc G ⊤,
+    (-1) ^ #(G'.edgeFinset \ G.edgeFinset) * (H.copyCount G' : ℤ)`.
+
+## Implementation notes
+
+The forward bijection `Copy.equivSigmaEmbedding` is the only "real" content; the Möbius
+direction reduces to it via the classical alternating-sum identity
+`Finset.sum_powerset_neg_one_pow_card`, reindexed through the order-isomorphism
+`G' ∈ Icc G ⊤ ↔ S ⊆ E(⊤) \ E(G)`.
+
+The Möbius identity is stated in `ℤ` (rather than `ℕ`) because the signs are essential.
+
+The `LocallyFiniteOrder (SimpleGraph V)` instance consumed by `Finset.Icc G ⊤` comes from
+`SimpleGraph.Finite.instLocallyFiniteOrder`, which requires `[DecidableLE (SimpleGraph V)]`.
+The declarations below routinely invoke `Classical.decRel _` since the bijection is already
+noncomputable.
+-/
+
+public section
+
+open Finset Function
+
+namespace SimpleGraph
+
+variable {V W : Type*}
+
+/-! ### Induced shape of a copy
+
+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 pullback of the host graph along the underlying injection of a copy. -/
+def inducedShape (f : Copy G H) : SimpleGraph V :=
+  H.comap f.toEmbedding
+
+@[simp] lemma inducedShape_adj (f : Copy G H) {a b : V} :
+    f.inducedShape.Adj a b ↔ H.Adj (f a) (f b) := Iff.rfl
+
+lemma le_inducedShape (f : Copy G H) : G ≤ f.inducedShape :=
+  fun _ _ => f.toHom.map_adj
+
+/-- 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
+  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 `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
+
+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
+
+variable {G : SimpleGraph V} {H : SimpleGraph W}
+
+/-- The load-bearing equivalence: a copy of `G` in `H` is the same data as a choice of
+supergraph `G' ∈ Icc G ⊤` (the induced shape) together with a graph embedding
+`G' ↪g H`. This expresses every copy uniquely as an induced copy of some shape `G'`
+between `G` and the complete graph.
+
+The proof goes via the canonical fiber decomposition `Equiv.sigmaFiberEquiv` for the map
+`Copy.inducedShape`. The index `K : SimpleGraph V` is restricted to `Icc G ⊤`, which is
+exactly the set of shapes with nonempty fiber. The per-fiber bijection is
+`Copy.fiberInducedShapeEquiv`. -/
+noncomputable def Copy.equivSigmaEmbedding (G : SimpleGraph V) (H : SimpleGraph W)
+    [Fintype V] [DecidableEq V] [DecidableLE (SimpleGraph V)] :
+    Copy G H ≃ Σ G' : ↥(Finset.Icc G ⊤), Embedding G'.val H :=
+  (Equiv.sigmaFiberEquiv (Copy.inducedShape : Copy G H → SimpleGraph V)).symm.trans <|
+  { toFun := fun ⟨K, f⟩ =>
+      let hGK : G ≤ K := f.prop ▸ f.val.le_inducedShape
+      ⟨⟨K, Finset.mem_Icc.mpr ⟨hGK, le_top⟩⟩,
+       Copy.fiberInducedShapeEquiv hGK f⟩
+    invFun := fun ⟨⟨K, hK⟩, e⟩ =>
+      ⟨K, (Copy.fiberInducedShapeEquiv (Finset.mem_Icc.mp hK).1).symm e⟩
+    left_inv := by
+      rintro ⟨K, f⟩
+      simp
+    right_inv := by
+      rintro ⟨⟨K, hK⟩, e⟩
+      simp only [Equiv.apply_symm_apply] }
+
+/-- Forward identity: every copy of `G` in `H` is an induced copy of some unique
+supergraph `G' ∈ Icc G ⊤` of `G`. -/
+theorem copyCount_eq_sum_embeddingCount [Fintype V] [DecidableEq V]
+    [DecidableLE (SimpleGraph V)] [Finite W] (G : SimpleGraph V) (H : SimpleGraph W) :
+    H.copyCount G = ∑ G' ∈ Finset.Icc G ⊤, H.embeddingCount G' := by
+  rw [copyCount_eq_nat_card, Nat.card_congr (Copy.equivSigmaEmbedding G H), Nat.card_sigma,
+    ← Finset.sum_attach (Finset.Icc G ⊤) (fun G' => H.embeddingCount G')]
+  refine Finset.sum_congr rfl fun G' _ => ?_
+  exact (embeddingCount_eq_nat_card _ _).symm
+
+end Forward
+
+/-! ### Möbius (signed-sum) inverse
+
+The Möbius inverse to the forward identity, expressing `H.embeddingCount G` as a signed
+sum of `H.copyCount G'` over supergraphs `G' ∈ Icc G ⊤`. The proof reduces, via the
+order-isomorphism `iccEquivPowersetEdgeFinsetSdiff` below, to the alternating-sum
+identity `Finset.sum_powerset_neg_one_pow_card`.
+-/
+
+section Mobius
+
+open Classical in
+/-- Order-isomorphism between the closed interval `Finset.Icc G K` of graphs and the
+powerset of the edge difference `K.edgeFinset \ G.edgeFinset`, valid when `G ≤ K`.
+
+The forward map sends a graph `G'` with `G ≤ G' ≤ K` to its "extra edges over `G`",
+namely `G'.edgeFinset \ G.edgeFinset`. The inverse sends a subset `S` of "missing edges
+of `G` inside `K`" to the graph whose edge set is `G.edgeFinset ∪ S`, constructed via
+`fromEdgeSet`. -/
+noncomputable def iccEquivPowersetEdgeFinsetSdiff [Fintype V] [DecidableEq V]
+    [DecidableLE (SimpleGraph V)] {G K : SimpleGraph V} (hGK : G ≤ K) :
+    ↥(Finset.Icc G K) ≃ ↥(K.edgeFinset \ G.edgeFinset).powerset where
+  toFun G' :=
+    ⟨G'.val.edgeFinset \ G.edgeFinset, by
+      have h₁ : G ≤ G'.val := (Finset.mem_Icc.mp G'.prop).1
+      have h₂ : G'.val ≤ K := (Finset.mem_Icc.mp G'.prop).2
+      simp only [Finset.mem_powerset]
+      exact Finset.sdiff_subset_sdiff (edgeFinset_mono h₂) (Finset.Subset.refl _)⟩
+  invFun S :=
+    ⟨fromEdgeSet ((G.edgeFinset : Set (Sym2 V)) ∪ S.val), by
+      have hSK : S.val ⊆ K.edgeFinset \ G.edgeFinset := Finset.mem_powerset.mp S.prop
+      refine Finset.mem_Icc.mpr ⟨?_, ?_⟩
+      · -- `G ≤ fromEdgeSet (G.edgeFinset ∪ S)`
+        intro a b hab
+        refine (fromEdgeSet_adj _).mpr ⟨Or.inl ?_, hab.ne⟩
+        rw [mem_coe, mem_edgeFinset]; exact hab
+      · -- `fromEdgeSet (G.edgeFinset ∪ S) ≤ K`
+        rw [fromEdgeSet_le]
+        intro e he
+        rw [Set.mem_diff] at he
+        obtain ⟨heGS, _⟩ := he
+        rcases heGS with heG | heS
+        · rw [mem_coe, mem_edgeFinset] at heG
+          exact edgeSet_subset_edgeSet.mpr hGK heG
+        · have : e ∈ K.edgeFinset := (Finset.mem_sdiff.mp (hSK heS)).1
+          rwa [mem_edgeFinset] at this⟩
+  left_inv := by
+    rintro ⟨G', hG'⟩
+    have hGG' : G ≤ G' := (Finset.mem_Icc.mp hG').1
+    apply Subtype.ext
+    ext a b
+    simp only [fromEdgeSet_adj, Set.mem_union, mem_coe, mem_edgeFinset, Finset.coe_sdiff,
+      Set.mem_diff]
+    constructor
+    · rintro ⟨h | ⟨h, _⟩, _⟩
+      · exact hGG' h
+      · exact h
+    · intro h
+      refine ⟨?_, h.ne⟩
+      by_cases hG : G.Adj a b
+      · exact Or.inl hG
+      · exact Or.inr ⟨h, hG⟩
+  right_inv := by
+    rintro ⟨S, hS⟩
+    have hSK : S ⊆ K.edgeFinset \ G.edgeFinset := Finset.mem_powerset.mp hS
+    apply Subtype.ext
+    ext e
+    simp only [Finset.mem_sdiff, mem_edgeFinset, edgeSet_fromEdgeSet, Set.mem_diff,
+      Set.mem_union, mem_coe]
+    constructor
+    · rintro ⟨⟨hGS, _⟩, heG⟩
+      cases hGS with
+      | inl h => exact absurd h heG
+      | inr h => exact h
+    · intro heS
+      have heK : e ∈ K.edgeFinset := (Finset.mem_sdiff.mp (hSK heS)).1
+      have heNotDiag : e ∉ Sym2.diagSet := fun hd =>
+        K.not_isDiag_of_mem_edgeSet (mem_edgeFinset.mp heK) hd
+      have heNotG : e ∉ G.edgeSet := fun heG =>
+        (Finset.mem_sdiff.mp (hSK heS)).2 (mem_edgeFinset.mpr heG)
+      exact ⟨⟨Or.inr heS, heNotDiag⟩, heNotG⟩
+
+open Classical in
+/-- The Möbius (signed-sum) inverse to `copyCount_eq_sum_embeddingCount`: the induced
+copy count is recovered as an alternating sum of copy counts indexed by supergraphs
+`G' ∈ Icc G ⊤`, with sign `(-1) ^ #(G'.edgeFinset \ G.edgeFinset)`. -/
+theorem embeddingCount_eq_sum_signed_copyCount [Fintype V] [DecidableEq V]
+    [DecidableLE (SimpleGraph V)] [Finite W] (G : SimpleGraph V) (H : SimpleGraph W) :
+    (H.embeddingCount G : ℤ) =
+      ∑ G' ∈ Finset.Icc G ⊤,
+        (-1 : ℤ) ^ #(G'.edgeFinset \ G.edgeFinset) * (H.copyCount G' : ℤ) := by
+  -- (1) The inner alternating sum collapses to `if L = G then 1 else 0`.
+  have hinner : ∀ L : SimpleGraph V, G ≤ L →
+      ∑ K' ∈ Finset.Icc G L, (-1 : ℤ) ^ #(K'.edgeFinset \ G.edgeFinset)
+        = if L = G then 1 else 0 := by
+    intro L hGL
+    have key : ∑ K' ∈ Finset.Icc G L, (-1 : ℤ) ^ #(K'.edgeFinset \ G.edgeFinset)
+        = ∑ S ∈ (L.edgeFinset \ G.edgeFinset).powerset, (-1 : ℤ) ^ #S := by
+      rw [← Finset.sum_attach (Finset.Icc G L)
+            (fun K' => (-1 : ℤ) ^ #(K'.edgeFinset \ G.edgeFinset)),
+          ← Finset.sum_attach (L.edgeFinset \ G.edgeFinset).powerset
+            (fun S => (-1 : ℤ) ^ #S)]
+      exact Finset.sum_equiv (iccEquivPowersetEdgeFinsetSdiff hGL)
+        (fun _ => by simp) (fun _ _ => rfl)
+    rw [key, Finset.sum_powerset_neg_one_pow_card]
+    by_cases hLG : L = G
+    · subst hLG; simp
+    · have hne : L.edgeFinset \ G.edgeFinset ≠ ∅ := by
+        intro hempty
+        apply hLG
+        have hsub : L ≤ G := by
+          simpa [Finset.sdiff_eq_empty_iff_subset, edgeFinset_subset_edgeFinset] using hempty
+        exact le_antisymm hsub hGL
+      rw [if_neg hne, if_neg hLG]
+  -- (2) Substitute the forward identity into the right-hand side.
+  simp_rw [fun K' : SimpleGraph V => copyCount_eq_sum_embeddingCount K' H,
+    Nat.cast_sum, Finset.mul_sum]
+  -- (3) Swap the order of summation: pairs (K', L) with G ≤ K' ≤ L ≤ ⊤.
+  rw [Finset.sum_comm' (s := Finset.Icc G (⊤ : SimpleGraph V))
+      (t := fun K' => Finset.Icc K' ⊤)
+      (s' := fun L => Finset.Icc G L) (t' := Finset.Icc G (⊤ : SimpleGraph V))
+      (h := fun K' L => by
+        simp only [Finset.mem_Icc]; constructor
+        · rintro ⟨⟨hGK', _⟩, hKL, _⟩
+          exact ⟨⟨hGK', hKL⟩, ⟨hGK'.trans hKL, le_top⟩⟩
+        · rintro ⟨⟨hGK', hKL⟩, _⟩
+          exact ⟨⟨hGK', le_top⟩, ⟨hKL, le_top⟩⟩)]
+  -- (4) Pull `embeddingCount L` out of the inner sum and apply `hinner`.
+  simp_rw [mul_comm ((-1 : ℤ) ^ _) ((H.embeddingCount _ : ℤ)), ← Finset.mul_sum]
+  -- (5) Apply `hinner` to each inner sum.
+  rw [Finset.sum_congr rfl fun L hL => by
+    rw [hinner L (Finset.mem_Icc.mp hL).1]]
+  -- (6) Collapse using `sum_ite_eq'`: only the `L = G` term survives.
+  simp_rw [mul_ite, mul_one, mul_zero]
+  rw [Finset.sum_ite_eq' (Finset.Icc G ⊤) G (fun L => (H.embeddingCount L : ℤ))]
+  rw [if_pos (Finset.mem_Icc.mpr ⟨le_refl _, le_top⟩)]
+
+end Mobius
+
+end SimpleGraph