Documentation

Mathlib.Data.Sym.Sym2

The symmetric square #

This file defines the symmetric square, which is α × α modulo swapping. This is also known as the type of unordered pairs.

More generally, the symmetric square is the second symmetric power (see Data.Sym.Basic). The equivalence is Sym2.equivSym.

From the point of view that an unordered pair is equivalent to a multiset of cardinality two (see Sym2.equivMultiset), there is a Mem instance Sym2.Mem, which is a Prop-valued membership test. Given h : a ∈ z for z : Sym2 α, then Mem.other h is the other element of the pair, defined using Classical.choice. If α has decidable equality, then h.other' computably gives the other element.

The universal property of Sym2 is provided as Sym2.lift, which states that functions from Sym2 α are equivalent to symmetric two-argument functions from α.

Recall that an undirected graph (allowing self loops, but no multiple edges) is equivalent to a symmetric relation on the vertex type α. Given a symmetric relation on α, the corresponding edge set is constructed by Sym2.fromRel which is a special case of Sym2.lift.

Notation #

The element Sym2.mk (a, b) can be written as s(a, b) for short.

Tags #

symmetric square, unordered pairs, symmetric powers

inductive Sym2.Rel (α : Type u) :
α × αα × αProp

This is the relation capturing the notion of pairs equivalent up to permutations.

  • refl: ∀ {α : Type u} (x y : α), Sym2.Rel α (x, y) (x, y)
  • swap: ∀ {α : Type u} (x y : α), Sym2.Rel α (x, y) (y, x)
Instances For
    theorem Sym2.Rel.symm {α : Type u_1} {x : α × α} {y : α × α} :
    Sym2.Rel α x ySym2.Rel α y x
    theorem Sym2.Rel.trans {α : Type u_1} {x : α × α} {y : α × α} {z : α × α} (a : Sym2.Rel α x y) (b : Sym2.Rel α y z) :
    Sym2.Rel α x z
    def Sym2.Rel.setoid (α : Type u) :
    Setoid (α × α)

    One can use attribute [local instance] Sym2.Rel.setoid to temporarily make Quotient functionality work for α × α.

    Equations
    Instances For
      @[simp]
      theorem Sym2.rel_iff' {α : Type u_1} {p : α × α} {q : α × α} :
      Sym2.Rel α p q p = q p = q.swap
      theorem Sym2.rel_iff {α : Type u_1} {x : α} {y : α} {z : α} {w : α} :
      Sym2.Rel α (x, y) (z, w) x = z y = w x = w y = z
      @[reducible, inline]
      abbrev Sym2 (α : Type u) :

      Sym2 α is the symmetric square of α, which, in other words, is the type of unordered pairs.

      It is equivalent in a natural way to multisets of cardinality 2 (see Sym2.equivMultiset).

      Equations
      Instances For
        @[reducible, inline]
        abbrev Sym2.mk {α : Type u_4} (p : α × α) :
        Sym2 α

        Constructor for Sym2. This is the quotient map α × α → Sym2 α.

        Equations
        Instances For

          Pretty printer defined by notation3 command.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            s(x, y) is an unordered pair, which is to say a pair modulo the action of the symmetric group.

            It is equal to Sym2.mk (x, y).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Sym2.sound {α : Type u_1} {p : α × α} {p' : α × α} (h : Sym2.Rel α p p') :
              theorem Sym2.exact {α : Type u_1} {p : α × α} {p' : α × α} (h : Sym2.mk p = Sym2.mk p') :
              Sym2.Rel α p p'
              @[simp]
              theorem Sym2.eq {α : Type u_1} {p : α × α} {p' : α × α} :
              theorem Sym2.ind {α : Type u_1} {f : Sym2 αProp} (h : ∀ (x y : α), f s(x, y)) (i : Sym2 α) :
              f i
              theorem Sym2.inductionOn {α : Type u_1} {f : Sym2 αProp} (i : Sym2 α) (hf : ∀ (x y : α), f s(x, y)) :
              f i
              theorem Sym2.inductionOn₂ {α : Type u_1} {β : Type u_2} {f : Sym2 αSym2 βProp} (i : Sym2 α) (j : Sym2 β) (hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)) :
              f i j
              def Sym2.rec {α : Type u_1} {motive : Sym2 αSort u_4} (f : (p : α × α) → motive (Sym2.mk p)) (h : ∀ (p q : α × α) (h : Sym2.Rel α p q), f p = f q) (z : Sym2 α) :
              motive z

              Dependent recursion principal for Sym2. See Quot.rec.

              Equations
              Instances For
                @[reducible, inline]
                abbrev Sym2.recOnSubsingleton {α : Type u_1} {motive : Sym2 αSort u_4} [∀ (p : α × α), Subsingleton (motive (Sym2.mk p))] (z : Sym2 α) (f : (p : α × α) → motive (Sym2.mk p)) :
                motive z

                Dependent recursion principal for Sym2 when the target is a Subsingleton type. See Quot.recOnSubsingleton.

                Equations
                Instances For
                  theorem Sym2.exists {α : Type u_4} {f : Sym2 αProp} :
                  (∃ (x : Sym2 α), f x) ∃ (x : α) (y : α), f s(x, y)
                  theorem Sym2.forall {α : Type u_4} {f : Sym2 αProp} :
                  (∀ (x : Sym2 α), f x) ∀ (x y : α), f s(x, y)
                  theorem Sym2.eq_swap {α : Type u_1} {a : α} {b : α} :
                  s(a, b) = s(b, a)
                  @[simp]
                  theorem Sym2.mk_prod_swap_eq {α : Type u_1} {p : α × α} :
                  Sym2.mk p.swap = Sym2.mk p
                  theorem Sym2.congr_right {α : Type u_1} {a : α} {b : α} {c : α} :
                  s(a, b) = s(a, c) b = c
                  theorem Sym2.congr_left {α : Type u_1} {a : α} {b : α} {c : α} :
                  s(b, a) = s(c, a) b = c
                  theorem Sym2.eq_iff {α : Type u_1} {x : α} {y : α} {z : α} {w : α} :
                  s(x, y) = s(z, w) x = z y = w x = w y = z
                  theorem Sym2.mk_eq_mk_iff {α : Type u_1} {p : α × α} {q : α × α} :
                  Sym2.mk p = Sym2.mk q p = q p = q.swap
                  def Sym2.lift {α : Type u_1} {β : Type u_2} :
                  { f : ααβ // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ } (Sym2 αβ)

                  The universal property of Sym2; symmetric functions of two arguments are equivalent to functions from Sym2. Note that when β is Prop, it can sometimes be more convenient to use Sym2.fromRel instead.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem Sym2.lift_mk {α : Type u_1} {β : Type u_2} (f : { f : ααβ // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) (a₁ : α) (a₂ : α) :
                    Sym2.lift f s(a₁, a₂) = f a₁ a₂
                    @[simp]
                    theorem Sym2.coe_lift_symm_apply {α : Type u_1} {β : Type u_2} (F : Sym2 αβ) (a₁ : α) (a₂ : α) :
                    (Sym2.lift.symm F) a₁ a₂ = F s(a₁, a₂)
                    def Sym2.lift₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
                    { f : ααββγ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ } (Sym2 αSym2 βγ)

                    A two-argument version of Sym2.lift.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem Sym2.lift₂_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : { f : ααββγ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
                      Sym2.lift₂ f s(a₁, a₂) s(b₁, b₂) = f a₁ a₂ b₁ b₂
                      @[simp]
                      theorem Sym2.coe_lift₂_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (F : Sym2 αSym2 βγ) (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
                      (Sym2.lift₂.symm F) a₁ a₂ b₁ b₂ = F s(a₁, a₂) s(b₁, b₂)
                      def Sym2.map {α : Type u_1} {β : Type u_2} (f : αβ) :
                      Sym2 αSym2 β

                      The functor Sym2 is functorial, and this function constructs the induced maps.

                      Equations
                      Instances For
                        @[simp]
                        theorem Sym2.map_id {α : Type u_1} :
                        Sym2.map id = id
                        theorem Sym2.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : βγ} {f : αβ} :
                        theorem Sym2.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : βγ} {f : αβ} (x : Sym2 α) :
                        Sym2.map g (Sym2.map f x) = Sym2.map (g f) x
                        @[simp]
                        theorem Sym2.map_pair_eq {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) (y : α) :
                        Sym2.map f s(x, y) = s(f x, f y)
                        theorem Sym2.map.injective {α : Type u_1} {β : Type u_2} {f : αβ} (hinj : Function.Injective f) :
                        @[simp]
                        theorem Sym2.mkEmbedding_apply {α : Type u_1} (a : α) (b : α) :
                        (Sym2.mkEmbedding a) b = s(a, b)
                        def Sym2.mkEmbedding {α : Type u_1} (a : α) :
                        α Sym2 α

                        mk a as an embedding. This is the symmetric version of Function.Embedding.sectl.

                        Equations
                        Instances For
                          @[simp]
                          theorem Function.Embedding.sym2Map_apply {α : Type u_1} {β : Type u_2} (f : α β) :
                          ∀ (a : Sym2 α), f.sym2Map a = Sym2.map (⇑f) a
                          def Function.Embedding.sym2Map {α : Type u_1} {β : Type u_2} (f : α β) :
                          Sym2 α Sym2 β

                          Sym2.map as an embedding.

                          Equations
                          • f.sym2Map = { toFun := Sym2.map f, inj' := }
                          Instances For

                            Membership and set coercion #

                            def Sym2.Mem {α : Type u_1} (x : α) (z : Sym2 α) :

                            This is a predicate that determines whether a given term is a member of a term of the symmetric square. From this point of view, the symmetric square is the subtype of cardinality-two multisets on α.

                            Equations
                            Instances For
                              theorem Sym2.mem_iff' {α : Type u_1} {a : α} {b : α} {c : α} :
                              Sym2.Mem a s(b, c) a = b a = c
                              instance Sym2.instSetLike {α : Type u_1} :
                              SetLike (Sym2 α) α
                              Equations
                              • Sym2.instSetLike = { coe := fun (z : Sym2 α) => {x : α | Sym2.Mem x z}, coe_injective' := }
                              @[simp]
                              theorem Sym2.mem_iff_mem {α : Type u_1} {x : α} {z : Sym2 α} :
                              Sym2.Mem x z x z
                              theorem Sym2.mem_iff_exists {α : Type u_1} {x : α} {z : Sym2 α} :
                              x z ∃ (y : α), z = s(x, y)
                              theorem Sym2.ext_iff {α : Type u_1} {p : Sym2 α} {q : Sym2 α} :
                              p = q ∀ (x : α), x p x q
                              theorem Sym2.ext {α : Type u_1} {p : Sym2 α} {q : Sym2 α} (h : ∀ (x : α), x p x q) :
                              p = q
                              theorem Sym2.mem_mk_left {α : Type u_1} (x : α) (y : α) :
                              x s(x, y)
                              theorem Sym2.mem_mk_right {α : Type u_1} (x : α) (y : α) :
                              y s(x, y)
                              @[simp]
                              theorem Sym2.mem_iff {α : Type u_1} {a : α} {b : α} {c : α} :
                              a s(b, c) a = b a = c
                              theorem Sym2.out_fst_mem {α : Type u_1} (e : Sym2 α) :
                              (Quot.out e).1 e
                              theorem Sym2.out_snd_mem {α : Type u_1} (e : Sym2 α) :
                              (Quot.out e).2 e
                              theorem Sym2.ball {α : Type u_1} {p : αProp} {a : α} {b : α} :
                              (∀ cs(a, b), p c) p a p b
                              noncomputable def Sym2.Mem.other {α : Type u_1} {a : α} {z : Sym2 α} (h : a z) :
                              α

                              Given an element of the unordered pair, give the other element using Classical.choose. See also Mem.other' for the computable version.

                              Equations
                              Instances For
                                @[simp]
                                theorem Sym2.other_spec {α : Type u_1} {a : α} {z : Sym2 α} (h : a z) :
                                s(a, Sym2.Mem.other h) = z
                                theorem Sym2.other_mem {α : Type u_1} {a : α} {z : Sym2 α} (h : a z) :
                                theorem Sym2.mem_and_mem_iff {α : Type u_1} {x : α} {y : α} {z : Sym2 α} (hne : x y) :
                                x z y z z = s(x, y)
                                theorem Sym2.eq_of_ne_mem {α : Type u_1} {x : α} {y : α} {z : Sym2 α} {z' : Sym2 α} (h : x y) (h1 : x z) (h2 : y z) (h3 : x z') (h4 : y z') :
                                z = z'
                                instance Sym2.Mem.decidable {α : Type u_1} [DecidableEq α] (x : α) (z : Sym2 α) :
                                Equations
                                @[simp]
                                theorem Sym2.mem_map {α : Type u_1} {β : Type u_2} {f : αβ} {b : β} {z : Sym2 α} :
                                b Sym2.map f z az, f a = b
                                theorem Sym2.map_congr {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {s : Sym2 α} (h : xs, f x = g x) :
                                @[simp]
                                theorem Sym2.map_id' {α : Type u_1} :
                                (Sym2.map fun (x : α) => x) = id

                                Note: Sym2.map_id will not simplify Sym2.map id z due to Sym2.map_congr.

                                Diagonal #

                                def Sym2.diag {α : Type u_1} (x : α) :
                                Sym2 α

                                A type α is naturally included in the diagonal of α × α, and this function gives the image of this diagonal in Sym2 α.

                                Equations
                                Instances For
                                  theorem Sym2.diag_injective {α : Type u_1} :
                                  def Sym2.IsDiag {α : Type u_1} :
                                  Sym2 αProp

                                  A predicate for testing whether an element of Sym2 α is on the diagonal.

                                  Equations
                                  • Sym2.IsDiag = Sym2.lift Eq,
                                  Instances For
                                    theorem Sym2.mk_isDiag_iff {α : Type u_1} {x : α} {y : α} :
                                    s(x, y).IsDiag x = y
                                    @[simp]
                                    theorem Sym2.isDiag_iff_proj_eq {α : Type u_1} (z : α × α) :
                                    (Sym2.mk z).IsDiag z.1 = z.2
                                    theorem Sym2.IsDiag.map {α : Type u_1} {β : Type u_2} {e : Sym2 α} {f : αβ} :
                                    e.IsDiag(Sym2.map f e).IsDiag
                                    theorem Sym2.isDiag_map {α : Type u_1} {β : Type u_2} {e : Sym2 α} {f : αβ} (hf : Function.Injective f) :
                                    (Sym2.map f e).IsDiag e.IsDiag
                                    @[simp]
                                    theorem Sym2.diag_isDiag {α : Type u_1} (a : α) :
                                    (Sym2.diag a).IsDiag
                                    theorem Sym2.IsDiag.mem_range_diag {α : Type u_1} {z : Sym2 α} :
                                    z.IsDiagz Set.range Sym2.diag
                                    theorem Sym2.isDiag_iff_mem_range_diag {α : Type u_1} (z : Sym2 α) :
                                    z.IsDiag z Set.range Sym2.diag
                                    instance Sym2.IsDiag.decidablePred (α : Type u) [DecidableEq α] :
                                    DecidablePred Sym2.IsDiag
                                    Equations
                                    theorem Sym2.other_ne {α : Type u_1} {a : α} {z : Sym2 α} (hd : ¬z.IsDiag) (h : a z) :

                                    Declarations about symmetric relations #

                                    def Sym2.fromRel {α : Type u_1} {r : ααProp} (sym : Symmetric r) :
                                    Set (Sym2 α)

                                    Symmetric relations define a set on Sym2 α by taking all those pairs of elements that are related.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Sym2.fromRel_proj_prop {α : Type u_1} {r : ααProp} {sym : Symmetric r} {z : α × α} :
                                      Sym2.mk z Sym2.fromRel sym r z.1 z.2
                                      theorem Sym2.fromRel_prop {α : Type u_1} {r : ααProp} {sym : Symmetric r} {a : α} {b : α} :
                                      s(a, b) Sym2.fromRel sym r a b
                                      theorem Sym2.fromRel_bot {α : Type u_1} :
                                      theorem Sym2.fromRel_top {α : Type u_1} :
                                      Sym2.fromRel = Set.univ
                                      theorem Sym2.fromRel_ne {α : Type u_1} :
                                      Sym2.fromRel = {z : Sym2 α | ¬z.IsDiag}
                                      theorem Sym2.fromRel_irreflexive {α : Type u_1} {r : ααProp} {sym : Symmetric r} :
                                      Irreflexive r ∀ {z : Sym2 α}, z Sym2.fromRel sym¬z.IsDiag
                                      theorem Sym2.mem_fromRel_irrefl_other_ne {α : Type u_1} {r : ααProp} {sym : Symmetric r} (irrefl : Irreflexive r) {a : α} {z : Sym2 α} (hz : z Sym2.fromRel sym) (h : a z) :
                                      instance Sym2.fromRel.decidablePred {α : Type u_1} {r : ααProp} (sym : Symmetric r) [h : DecidableRel r] :
                                      DecidablePred fun (x : Sym2 α) => x Sym2.fromRel sym
                                      Equations
                                      def Sym2.ToRel {α : Type u_1} (s : Set (Sym2 α)) (x : α) (y : α) :

                                      The inverse to Sym2.fromRel. Given a set on Sym2 α, give a symmetric relation on α (see Sym2.toRel_symmetric).

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Sym2.toRel_prop {α : Type u_1} (s : Set (Sym2 α)) (x : α) (y : α) :
                                        Sym2.ToRel s x y s(x, y) s
                                        theorem Sym2.toRel_symmetric {α : Type u_1} (s : Set (Sym2 α)) :
                                        theorem Sym2.toRel_fromRel {α : Type u_1} {r : ααProp} (sym : Symmetric r) :
                                        theorem Sym2.fromRel_toRel {α : Type u_1} (s : Set (Sym2 α)) :

                                        Equivalence to the second symmetric power #

                                        def Sym2.sym2EquivSym' {α : Type u_1} :
                                        Sym2 α Sym.Sym' α 2

                                        The symmetric square is equivalent to length-2 vectors up to permutations.

                                        Equations
                                        • Sym2.sym2EquivSym' = { toFun := Quot.map (fun (x : α × α) => [x.1, x.2], ) , invFun := Quot.map Sym2.fromVector , left_inv := , right_inv := }
                                        Instances For
                                          def Sym2.equivSym (α : Type u_4) :
                                          Sym2 α Sym α 2

                                          The symmetric square is equivalent to the second symmetric power.

                                          Equations
                                          Instances For
                                            def Sym2.equivMultiset (α : Type u_4) :
                                            Sym2 α { s : Multiset α // Multiset.card s = 2 }

                                            The symmetric square is equivalent to multisets of cardinality two. (This is currently a synonym for equivSym, but it's provided in case the definition for Sym changes.)

                                            Equations
                                            Instances For

                                              Given [DecidableEq α] and [Fintype α], the following instance gives Fintype (Sym2 α).

                                              Equations
                                              instance Sym2.instDecidableRel' {α : Type u_1} [DecidableEq α] :
                                              DecidableRel HasEquiv.Equiv
                                              Equations
                                              • Sym2.instDecidableRel' = Sym2.instDecidableRel
                                              instance Sym2.instDecidableEq {α : Type u_1} [DecidableEq α] :
                                              Equations

                                              The other element of an element of the symmetric square #

                                              def Sym2.Mem.other' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a z) :
                                              α

                                              Get the other element of the unordered pair using the decidable equality. This is the computable version of Mem.other.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem Sym2.other_spec' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a z) :
                                                s(a, Sym2.Mem.other' h) = z
                                                @[simp]
                                                theorem Sym2.other_eq_other' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a z) :
                                                theorem Sym2.other_mem' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a z) :
                                                theorem Sym2.other_invol' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (ha : a z) (hb : Sym2.Mem.other' ha z) :
                                                theorem Sym2.other_invol {α : Type u_1} {a : α} {z : Sym2 α} (ha : a z) (hb : Sym2.Mem.other ha z) :
                                                theorem Sym2.filter_image_mk_isDiag {α : Type u_1} [DecidableEq α] (s : Finset α) :
                                                Finset.filter (fun (a : Sym2 α) => a.IsDiag) (Finset.image Sym2.mk (s ×ˢ s)) = Finset.image Sym2.mk s.diag
                                                theorem Sym2.filter_image_mk_not_isDiag {α : Type u_1} [DecidableEq α] (s : Finset α) :
                                                Finset.filter (fun (a : Sym2 α) => ¬a.IsDiag) (Finset.image Sym2.mk (s ×ˢ s)) = Finset.image Sym2.mk s.offDiag
                                                Equations
                                                • =
                                                instance Sym2.instUnique {α : Type u_1} [Unique α] :
                                                Equations
                                                instance Sym2.instIsEmpty {α : Type u_1} [IsEmpty α] :
                                                Equations
                                                • =
                                                instance Sym2.instNontrivial {α : Type u_1} [Nontrivial α] :
                                                Equations
                                                • =
                                                unsafe instance Sym2.instRepr {α : Type u_1} [Repr α] :
                                                Repr (Sym2 α)