Documentation

Mathlib.Data.Sym.Basic

Symmetric powers #

This file defines symmetric powers of a type. The nth symmetric power consists of homogeneous n-tuples modulo permutations by the symmetric group.

The special case of 2-tuples is called the symmetric square, which is addressed in more detail in Data.Sym.Sym2.

TODO: This was created as supporting material for Sym2; it needs a fleshed-out interface.

Tags #

symmetric powers

def Sym (α : Type u_1) (n : ) :
Type u_1

The nth symmetric power is n-tuples up to permutation. We define it as a subtype of Multiset since these are well developed in the library. We also give a definition Sym.sym' in terms of vectors, and we show these are equivalent in Sym.symEquivSym'.

Equations
Instances For
    def Sym.toMultiset {α : Type u_1} {n : } (s : Sym α n) :

    The canonical map to Multiset α that forgets that s has length n

    Equations
    • s = s
    Instances For
      instance Sym.hasCoe (α : Type u_1) (n : ) :
      CoeOut (Sym α n) (Multiset α)
      Equations
      instance instDecidableEqSym {α : Type u_1} {n : } [DecidableEq α] :
      Equations
      @[reducible, inline]
      abbrev Vector.Perm.isSetoid (α : Type u_1) (n : ) :
      Setoid (Vector α n)

      This is the List.Perm setoid lifted to Vector.

      See note [reducible non-instances].

      Equations
      Instances For
        theorem Sym.coe_injective {α : Type u_1} {n : } :
        Function.Injective Sym.toMultiset
        @[simp]
        theorem Sym.coe_inj {α : Type u_1} {n : } {s₁ : Sym α n} {s₂ : Sym α n} :
        s₁ = s₂ s₁ = s₂
        theorem Sym.ext {α : Type u_1} {n : } {s₁ : Sym α n} {s₂ : Sym α n} (h : s₁ = s₂) :
        s₁ = s₂
        @[simp]
        theorem Sym.val_eq_coe {α : Type u_1} {n : } (s : Sym α n) :
        s = s
        @[reducible, match_pattern, inline]
        abbrev Sym.mk {α : Type u_1} {n : } (m : Multiset α) (h : Multiset.card m = n) :
        Sym α n

        Construct an element of the nth symmetric power from a multiset of cardinality n.

        Equations
        Instances For
          @[match_pattern]
          def Sym.nil {α : Type u_1} :
          Sym α 0

          The unique element in Sym α 0.

          Equations
          • Sym.nil = 0,
          Instances For
            @[simp]
            theorem Sym.coe_nil {α : Type u_1} :
            Sym.nil = 0
            @[match_pattern]
            def Sym.cons {α : Type u_1} {n : } (a : α) (s : Sym α n) :
            Sym α n.succ

            Inserts an element into the term of Sym α n, increasing the length by one.

            Equations
            Instances For

              Inserts an element into the term of Sym α n, increasing the length by one.

              Equations
              Instances For
                @[simp]
                theorem Sym.cons_inj_right {α : Type u_1} {n : } (a : α) (s : Sym α n) (s' : Sym α n) :
                a ::ₛ s = a ::ₛ s' s = s'
                @[simp]
                theorem Sym.cons_inj_left {α : Type u_1} {n : } (a : α) (a' : α) (s : Sym α n) :
                a ::ₛ s = a' ::ₛ s a = a'
                theorem Sym.cons_swap {α : Type u_1} {n : } (a : α) (b : α) (s : Sym α n) :
                a ::ₛ b ::ₛ s = b ::ₛ a ::ₛ s
                theorem Sym.coe_cons {α : Type u_1} {n : } (s : Sym α n) (a : α) :
                (a ::ₛ s) = a ::ₘ s
                def Sym.ofVector {α : Type u_1} {n : } :
                Vector α nSym α n

                This is the quotient map that takes a list of n elements as an n-tuple and produces an nth symmetric power.

                Equations
                Instances For
                  instance Sym.instCoeVector {α : Type u_1} {n : } :
                  Coe (Vector α n) (Sym α n)

                  This is the quotient map that takes a list of n elements as an n-tuple and produces an nth symmetric power.

                  Equations
                  @[simp]
                  theorem Sym.ofVector_nil {α : Type u_1} :
                  Sym.ofVector Vector.nil = Sym.nil
                  @[simp]
                  theorem Sym.ofVector_cons {α : Type u_1} {n : } (a : α) (v : Vector α n) :
                  @[simp]
                  theorem Sym.card_coe {α : Type u_1} {n : } {s : Sym α n} :
                  Multiset.card s = n
                  instance Sym.instMembership {α : Type u_1} {n : } :
                  Membership α (Sym α n)

                  α ∈ s means that a appears as one of the factors in s.

                  Equations
                  • Sym.instMembership = { mem := fun (a : α) (s : Sym α n) => a s }
                  instance Sym.decidableMem {α : Type u_1} {n : } [DecidableEq α] (a : α) (s : Sym α n) :
                  Equations
                  @[simp]
                  theorem Sym.mem_mk {α : Type u_1} {n : } (a : α) (s : Multiset α) (h : Multiset.card s = n) :
                  a Sym.mk s h a s
                  @[simp]
                  theorem Sym.not_mem_nil {α : Type u_1} (a : α) :
                  aSym.nil
                  @[simp]
                  theorem Sym.mem_cons {α : Type u_1} {n : } {s : Sym α n} {a : α} {b : α} :
                  a b ::ₛ s a = b a s
                  @[simp]
                  theorem Sym.mem_coe {α : Type u_1} {n : } {s : Sym α n} {a : α} :
                  a s a s
                  theorem Sym.mem_cons_of_mem {α : Type u_1} {n : } {s : Sym α n} {a : α} {b : α} (h : a s) :
                  a b ::ₛ s
                  theorem Sym.mem_cons_self {α : Type u_1} {n : } (a : α) (s : Sym α n) :
                  a a ::ₛ s
                  theorem Sym.cons_of_coe_eq {α : Type u_1} {n : } (a : α) (v : Vector α n) :
                  theorem Sym.sound {α : Type u_1} {n : } {a : Vector α n} {b : Vector α n} (h : (a).Perm b) :
                  def Sym.erase {α : Type u_1} {n : } [DecidableEq α] (s : Sym α (n + 1)) (a : α) (h : a s) :
                  Sym α n

                  erase s a h is the sym that subtracts 1 from the multiplicity of a if a is present in the sym.

                  Equations
                  • s.erase a h = (s).erase a,
                  Instances For
                    @[simp]
                    theorem Sym.erase_mk {α : Type u_1} {n : } [DecidableEq α] (m : Multiset α) (hc : Multiset.card m = n + 1) (a : α) (h : a m) :
                    (Sym.mk m hc).erase a h = Sym.mk (m.erase a)
                    @[simp]
                    theorem Sym.coe_erase {α : Type u_1} {n : } [DecidableEq α] {s : Sym α n.succ} {a : α} (h : a s) :
                    (s.erase a h) = (s).erase a
                    @[simp]
                    theorem Sym.cons_erase {α : Type u_1} {n : } [DecidableEq α] {s : Sym α n.succ} {a : α} (h : a s) :
                    a ::ₛ s.erase a h = s
                    @[simp]
                    theorem Sym.erase_cons_head {α : Type u_1} {n : } [DecidableEq α] (s : Sym α n) (a : α) (h : optParam (a a ::ₛ s) ) :
                    (a ::ₛ s).erase a h = s
                    def Sym.Sym' (α : Type u_3) (n : ) :
                    Type u_3

                    Another definition of the nth symmetric power, using vectors modulo permutations. (See Sym.)

                    Equations
                    Instances For
                      def Sym.cons' {α : Type u_3} {n : } :
                      αSym.Sym' α nSym.Sym' α n.succ

                      This is cons but for the alternative Sym' definition.

                      Equations
                      Instances For

                        This is cons but for the alternative Sym' definition.

                        Equations
                        Instances For
                          def Sym.symEquivSym' {α : Type u_3} {n : } :
                          Sym α n Sym.Sym' α n

                          Multisets of cardinality n are equivalent to length-n vectors up to permutations.

                          Equations
                          Instances For
                            theorem Sym.cons_equiv_eq_equiv_cons (α : Type u_3) (n : ) (a : α) (s : Sym α n) :
                            Sym.cons' a (Sym.symEquivSym' s) = Sym.symEquivSym' (a ::ₛ s)
                            instance Sym.instZeroSym {α : Type u_1} :
                            Zero (Sym α 0)
                            Equations
                            • Sym.instZeroSym = { zero := 0, }
                            @[simp]
                            theorem Sym.toMultiset_zero {α : Type u_1} :
                            0 = 0
                            Equations
                            • Sym.instEmptyCollectionOfNatNat = { emptyCollection := 0 }
                            theorem Sym.eq_nil_of_card_zero {α : Type u_1} (s : Sym α 0) :
                            s = Sym.nil
                            instance Sym.uniqueZero {α : Type u_1} :
                            Unique (Sym α 0)
                            Equations
                            • Sym.uniqueZero = { default := Sym.nil, uniq := }
                            def Sym.replicate {α : Type u_1} (n : ) (a : α) :
                            Sym α n

                            replicate n a is the sym containing only a with multiplicity n.

                            Equations
                            Instances For
                              theorem Sym.replicate_succ {α : Type u_1} {a : α} {n : } :
                              theorem Sym.coe_replicate {α : Type u_1} {n : } {a : α} :
                              @[simp]
                              theorem Sym.mem_replicate {α : Type u_1} {n : } {a : α} {b : α} :
                              b Sym.replicate n a n 0 b = a
                              theorem Sym.eq_replicate_iff {α : Type u_1} {n : } {s : Sym α n} {a : α} :
                              s = Sym.replicate n a bs, b = a
                              theorem Sym.exists_mem {α : Type u_1} {n : } (s : Sym α n.succ) :
                              ∃ (a : α), a s
                              theorem Sym.exists_cons_of_mem {α : Type u_1} {n : } {s : Sym α (n + 1)} {a : α} (h : a s) :
                              ∃ (t : Sym α n), s = a ::ₛ t
                              theorem Sym.exists_eq_cons_of_succ {α : Type u_1} {n : } (s : Sym α n.succ) :
                              ∃ (a : α) (s' : Sym α n), s = a ::ₛ s'
                              theorem Sym.eq_replicate {α : Type u_1} {a : α} {n : } {s : Sym α n} :
                              s = Sym.replicate n a bs, b = a
                              theorem Sym.eq_replicate_of_subsingleton {α : Type u_1} [Subsingleton α] (a : α) {n : } (s : Sym α n) :
                              instance Sym.instSubsingleton {α : Type u_1} [Subsingleton α] (n : ) :
                              Equations
                              • =
                              instance Sym.inhabitedSym {α : Type u_1} [Inhabited α] (n : ) :
                              Inhabited (Sym α n)
                              Equations
                              instance Sym.inhabitedSym' {α : Type u_1} [Inhabited α] (n : ) :
                              Equations
                              instance Sym.instIsEmptySucc {α : Type u_1} (n : ) [IsEmpty α] :
                              IsEmpty (Sym α n.succ)
                              Equations
                              • =
                              instance Sym.instUnique {α : Type u_1} (n : ) [Unique α] :
                              Unique (Sym α n)
                              Equations
                              theorem Sym.replicate_right_inj {α : Type u_1} {a : α} {b : α} {n : } (h : n 0) :
                              instance Sym.instNontrivialHAddNatOfNat {α : Type u_1} (n : ) [Nontrivial α] :
                              Nontrivial (Sym α (n + 1))
                              Equations
                              • =
                              def Sym.map {α : Type u_1} {β : Type u_2} {n : } (f : αβ) (x : Sym α n) :
                              Sym β n

                              A function α → β induces a function Sym α n → Sym β n by applying it to every element of the underlying n-tuple.

                              Equations
                              Instances For
                                @[simp]
                                theorem Sym.mem_map {α : Type u_1} {β : Type u_2} {n : } {f : αβ} {b : β} {l : Sym α n} :
                                b Sym.map f l al, f a = b
                                @[simp]
                                theorem Sym.map_id' {α : Type u_3} {n : } (s : Sym α n) :
                                Sym.map (fun (x : α) => x) s = s

                                Note: Sym.map_id is not simp-normal, as simp ends up unfolding id with Sym.map_congr

                                theorem Sym.map_id {α : Type u_3} {n : } (s : Sym α n) :
                                Sym.map id s = s
                                @[simp]
                                theorem Sym.map_map {α : Type u_3} {β : Type u_4} {γ : Type u_5} {n : } (g : βγ) (f : αβ) (s : Sym α n) :
                                Sym.map g (Sym.map f s) = Sym.map (g f) s
                                @[simp]
                                theorem Sym.map_zero {α : Type u_1} {β : Type u_2} (f : αβ) :
                                Sym.map f 0 = 0
                                @[simp]
                                theorem Sym.map_cons {α : Type u_1} {β : Type u_2} {n : } (f : αβ) (a : α) (s : Sym α n) :
                                Sym.map f (a ::ₛ s) = f a ::ₛ Sym.map f s
                                theorem Sym.map_congr {α : Type u_1} {β : Type u_2} {n : } {f : αβ} {g : αβ} {s : Sym α n} (h : xs, f x = g x) :
                                Sym.map f s = Sym.map g s
                                @[simp]
                                theorem Sym.map_mk {α : Type u_1} {β : Type u_2} {n : } {f : αβ} {m : Multiset α} {hc : Multiset.card m = n} :
                                Sym.map f (Sym.mk m hc) = Sym.mk (Multiset.map f m)
                                @[simp]
                                theorem Sym.coe_map {α : Type u_1} {β : Type u_2} {n : } (s : Sym α n) (f : αβ) :
                                (Sym.map f s) = Multiset.map f s
                                theorem Sym.map_injective {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) (n : ) :
                                @[simp]
                                theorem Sym.equivCongr_apply {α : Type u_1} {β : Type u_2} {n : } (e : α β) (x : Sym α n) :
                                (Sym.equivCongr e) x = Sym.map (e) x
                                @[simp]
                                theorem Sym.equivCongr_symm_apply {α : Type u_1} {β : Type u_2} {n : } (e : α β) (x : Sym β n) :
                                (Sym.equivCongr e).symm x = Sym.map (e.symm) x
                                def Sym.equivCongr {α : Type u_1} {β : Type u_2} {n : } (e : α β) :
                                Sym α n Sym β n

                                Mapping an equivalence α ≃ β using Sym.map gives an equivalence between Sym α n and Sym β n.

                                Equations
                                Instances For
                                  def Sym.attach {α : Type u_1} {n : } (s : Sym α n) :
                                  Sym { x : α // x s } n

                                  "Attach" a proof that a ∈ s to each element a in s to produce an element of the symmetric power on {x // x ∈ s}.

                                  Equations
                                  • s.attach = (s).attach,
                                  Instances For
                                    @[simp]
                                    theorem Sym.attach_mk {α : Type u_1} {n : } {m : Multiset α} {hc : Multiset.card m = n} :
                                    (Sym.mk m hc).attach = Sym.mk m.attach
                                    @[simp]
                                    theorem Sym.coe_attach {α : Type u_1} {n : } (s : Sym α n) :
                                    s.attach = (s).attach
                                    theorem Sym.attach_map_coe {α : Type u_1} {n : } (s : Sym α n) :
                                    Sym.map Subtype.val s.attach = s
                                    @[simp]
                                    theorem Sym.mem_attach {α : Type u_1} {n : } (s : Sym α n) (x : { x : α // x s }) :
                                    x s.attach
                                    @[simp]
                                    theorem Sym.attach_nil {α : Type u_1} :
                                    Sym.nil.attach = Sym.nil
                                    @[simp]
                                    theorem Sym.attach_cons {α : Type u_1} {n : } (x : α) (s : Sym α n) :
                                    (x ::ₛ s).attach = x, ::ₛ Sym.map (fun (x_1 : { x : α // x s }) => x_1, ) s.attach
                                    def Sym.cast {α : Type u_1} {n : } {m : } (h : n = m) :
                                    Sym α n Sym α m

                                    Change the length of a Sym using an equality. The simp-normal form is for the cast to be pushed outward.

                                    Equations
                                    • Sym.cast h = { toFun := fun (s : Sym α n) => s, , invFun := fun (s : Sym α m) => s, , left_inv := , right_inv := }
                                    Instances For
                                      @[simp]
                                      theorem Sym.cast_rfl {α : Type u_1} {n : } {s : Sym α n} :
                                      (Sym.cast ) s = s
                                      @[simp]
                                      theorem Sym.cast_cast {α : Type u_1} {n : } {n' : } {s : Sym α n} {n'' : } (h : n = n') (h' : n' = n'') :
                                      (Sym.cast h') ((Sym.cast h) s) = (Sym.cast ) s
                                      @[simp]
                                      theorem Sym.coe_cast {α : Type u_1} {n : } {m : } {s : Sym α n} (h : n = m) :
                                      ((Sym.cast h) s) = s
                                      @[simp]
                                      theorem Sym.mem_cast {α : Type u_1} {n : } {m : } {s : Sym α n} {a : α} (h : n = m) :
                                      a (Sym.cast h) s a s
                                      def Sym.append {α : Type u_1} {n : } {n' : } (s : Sym α n) (s' : Sym α n') :
                                      Sym α (n + n')

                                      Append a pair of Sym terms.

                                      Equations
                                      • s.append s' = s + s',
                                      Instances For
                                        @[simp]
                                        theorem Sym.append_inj_right {α : Type u_1} {n : } {n' : } (s : Sym α n) {t : Sym α n'} {t' : Sym α n'} :
                                        s.append t = s.append t' t = t'
                                        @[simp]
                                        theorem Sym.append_inj_left {α : Type u_1} {n : } {n' : } {s : Sym α n} {s' : Sym α n} (t : Sym α n') :
                                        s.append t = s'.append t s = s'
                                        theorem Sym.append_comm {α : Type u_1} {n' : } (s : Sym α n') (s' : Sym α n') :
                                        s.append s' = (Sym.cast ) (s'.append s)
                                        @[simp]
                                        theorem Sym.coe_append {α : Type u_1} {n : } {n' : } (s : Sym α n) (s' : Sym α n') :
                                        (s.append s') = s + s'
                                        theorem Sym.mem_append_iff {α : Type u_1} {n : } {m : } {s : Sym α n} {a : α} {s' : Sym α m} :
                                        a s.append s' a s a s'
                                        def Sym.fill {α : Type u_1} {n : } (a : α) (i : Fin (n + 1)) (m : Sym α (n - i)) :
                                        Sym α n

                                        Fill a term m : Sym α (n - i) with i copies of a to obtain a term of Sym α n. This is a convenience wrapper for m.append (replicate i a) that adjusts the term using Sym.cast.

                                        Equations
                                        Instances For
                                          theorem Sym.coe_fill {α : Type u_1} {n : } {a : α} {i : Fin (n + 1)} {m : Sym α (n - i)} :
                                          (Sym.fill a i m) = m + (Sym.replicate (i) a)
                                          theorem Sym.mem_fill_iff {α : Type u_1} {n : } {a : α} {b : α} {i : Fin (n + 1)} {s : Sym α (n - i)} :
                                          a Sym.fill b i s i 0 a = b a s
                                          def Sym.filterNe {α : Type u_1} {n : } [DecidableEq α] (a : α) (m : Sym α n) :
                                          (i : Fin (n + 1)) × Sym α (n - i)

                                          Remove every a from a given Sym α n. Yields the number of copies i and a term of Sym α (n - i).

                                          Equations
                                          Instances For
                                            theorem Sym.sigma_sub_ext {α : Type u_1} {n : } {m₁ : (i : Fin (n + 1)) × Sym α (n - i)} {m₂ : (i : Fin (n + 1)) × Sym α (n - i)} (h : m₁.snd = m₂.snd) :
                                            m₁ = m₂
                                            theorem Sym.fill_filterNe {α : Type u_1} {n : } [DecidableEq α] (a : α) (m : Sym α n) :
                                            Sym.fill a (Sym.filterNe a m).fst (Sym.filterNe a m).snd = m
                                            theorem Sym.filter_ne_fill {α : Type u_1} {n : } [DecidableEq α] (a : α) (m : (i : Fin (n + 1)) × Sym α (n - i)) (h : am.snd) :
                                            Sym.filterNe a (Sym.fill a m.fst m.snd) = m
                                            theorem Sym.count_coe_fill_self_of_not_mem {α : Type u_1} {n : } [DecidableEq α] {a : α} {i : Fin (n + 1)} {s : Sym α (n - i)} (hx : as) :
                                            Multiset.count a (Sym.fill a i s) = i
                                            theorem Sym.count_coe_fill_of_ne {α : Type u_1} {n : } [DecidableEq α] {a : α} {x : α} {i : Fin (n + 1)} {s : Sym α (n - i)} (hx : x a) :

                                            Combinatorial equivalences #

                                            def SymOptionSuccEquiv.encode {α : Type u_1} {n : } [DecidableEq α] (s : Sym (Option α) n.succ) :
                                            Sym (Option α) n Sym α n.succ

                                            Function from the symmetric product over Option splitting on whether or not it contains a none.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem SymOptionSuccEquiv.encode_of_none_mem {α : Type u_1} {n : } [DecidableEq α] (s : Sym (Option α) n.succ) (h : none s) :
                                              @[simp]
                                              theorem SymOptionSuccEquiv.encode_of_not_none_mem {α : Type u_1} {n : } [DecidableEq α] (s : Sym (Option α) n.succ) (h : nones) :
                                              SymOptionSuccEquiv.encode s = Sum.inr (Sym.map (fun (o : { x : Option α // x s }) => (o).get ) s.attach)
                                              def SymOptionSuccEquiv.decode {α : Type u_1} {n : } :
                                              Sym (Option α) n Sym α n.succSym (Option α) n.succ

                                              Inverse of Sym_option_succ_equiv.decode.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem SymOptionSuccEquiv.decode_inl {α : Type u_1} {n : } (s : Sym (Option α) n) :
                                                @[simp]
                                                theorem SymOptionSuccEquiv.decode_inr {α : Type u_1} {n : } (s : Sym α n.succ) :
                                                SymOptionSuccEquiv.decode (Sum.inr s) = Sym.map (Function.Embedding.some) s
                                                def symOptionSuccEquiv {α : Type u_1} {n : } [DecidableEq α] :
                                                Sym (Option α) n.succ Sym (Option α) n Sym α n.succ

                                                The symmetric product over Option is a disjoint union over simpler symmetric products.

                                                Equations
                                                • symOptionSuccEquiv = { toFun := SymOptionSuccEquiv.encode, invFun := SymOptionSuccEquiv.decode, left_inv := , right_inv := }
                                                Instances For