sigmaEquivSigmaPi — Mathlib

English

There exists a natural equivalence between the type of pairs (a, b) consisting of a composition a of n and a composition b of a.length, and the type of pairs (c, d) where c is a composition of n and d assigns to each index i < c.length a composition of c.blocksFun i. This equivalence formalizes a change of variables used in proving the associativity of composition of formal multilinear series.

Русский

Существует естественное эквивалентное отображение между множеством пар (a, b), где a — композиция n, b — композиция a.length, и множеством пар (c, d), где c — композиция n, а d назначает для каждого индекса i < c.length композицию c.blocksFun i. Это эквивалентность реализует смену переменных в доказательстве ассоциативности композиции формальных многочленов.

LaTeX

$$$\\text{sigmaEquivSigmaPi}(n) : (\\sum a : \\mathrm{Composition}(n), \\mathrm{Composition}(a.length)) \\simeq \\sum c : \\mathrm{Composition}(n), \\forall i : \\mathrm{Fin}(c.length), \\mathrm{Composition}(c.blocksFun(i))$$$

Lean4

/-- Natural equivalence between `(Σ (a : Composition n), Composition a.length)` and
`(Σ (c : Composition n), Π (i : Fin c.length), Composition (c.blocksFun i))`, that shows up as a
change of variables in the proof that composition of formal multilinear series is associative.

Consider a composition `a` of `n` and a composition `b` of `a.length`. Then `b` indicates how to
group together some blocks of `a`, giving altogether `b.length` blocks of blocks. These blocks of
blocks can be called `d₀, ..., d_{a.length - 1}`, and one obtains a composition `c` of `n` by
saying that each `dᵢ` is one single block. The map `⟨a, b⟩ → ⟨c, (d₀, ..., d_{a.length - 1})⟩` is
the direct map in the equiv.

Conversely, if one starts from `c` and the `dᵢ`s, one can join the `dᵢ`s to obtain a composition
`a` of `n`, and register the lengths of the `dᵢ`s in a composition `b` of `a.length`. This is the
inverse map of the equiv.
-/
def sigmaEquivSigmaPi (n : ℕ) :
    (Σ a : Composition n, Composition a.length) ≃ Σ c : Composition n, ∀ i : Fin c.length, Composition (c.blocksFun i)
    where
  toFun i := ⟨i.1.gather i.2, i.1.sigmaCompositionAux i.2⟩
  invFun
    i :=
    ⟨{  blocks := (ofFn fun j => (i.2 j).blocks).flatten
        blocks_pos := by
          simp only [and_imp, List.mem_flatten, exists_imp, forall_mem_ofFn_iff]
          exact fun {i} j hj => Composition.blocks_pos _ hj
        blocks_sum := by simp [sum_ofFn, Composition.blocks_sum, Composition.sum_blocksFun] },
      { blocks := ofFn fun j => (i.2 j).length
        blocks_pos := by
          intro k hk
          refine ((forall_mem_ofFn_iff (P := fun i => 0 < i)).2 fun j => ?_) k hk
          exact Composition.length_pos_of_pos _ (Composition.blocks_pos' _ _ _)
        blocks_sum := by dsimp only [Composition.length]; simp [sum_ofFn] }⟩
  left_inv := by
    -- the fact that we have a left inverse is essentially `join_splitWrtComposition`,
        -- but we need to massage it to take care of the dependent setting.

    rintro ⟨a, b⟩
    rw [sigma_composition_eq_iff]
    dsimp
    constructor
    · conv_rhs => rw [← flatten_splitWrtComposition a.blocks b, ← ofFn_get (splitWrtComposition a.blocks b)]
      have A : length (gather a b) = List.length (splitWrtComposition a.blocks b) := by
        simp only [length, gather, length_map, length_splitWrtComposition]
      congr! 2
      exact (Fin.heq_fun_iff A (α := List ℕ)).2 fun i => rfl
    · have B : Composition.length (Composition.gather a b) = List.length b.blocks := Composition.length_gather _ _
      conv_rhs => rw [← ofFn_getElem b.blocks]
      congr 1
      refine (Fin.heq_fun_iff B).2 fun i => ?_
      rw [sigmaCompositionAux, Composition.length, List.getElem_map_rev List.length,
        List.getElem_of_eq (map_length_splitWrtComposition _ _)]
  right_inv := by
    -- the fact that we have a right inverse is essentially `splitWrtComposition_join`,
        -- but we need to massage it to take care of the dependent setting.

    rintro ⟨c, d⟩
    have : map List.sum (ofFn fun i : Fin (Composition.length c) => (d i).blocks) = c.blocks := by
      simp [map_ofFn, Function.comp_def, Composition.blocks_sum, Composition.ofFn_blocksFun]
    rw [sigma_pi_composition_eq_iff]
    dsimp
    congr! 1
    · congr
      ext1
      dsimp [Composition.gather]
      rwa [splitWrtComposition_flatten]
      simp only [map_ofFn, Function.comp_def]
    · rw [Fin.heq_fun_iff]
      · intro i
        dsimp [Composition.sigmaCompositionAux]
        rw [getElem_of_eq (splitWrtComposition_flatten _ _ _)]
        · simp only [List.getElem_ofFn]
        · simp only [map_ofFn, Function.comp_def]
      · congr

Похожие утверждения