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
theorem Sym2.Rel.is_equivalence {α : Type u_1} :
def Sym2.Rel.setoid (α : Type u) :
Setoid (α × α)

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

Equations
• = { r := , iseqv := }
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

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

Pretty printer defined by notation3 command.

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.Rel α p p'
@[simp]
theorem Sym2.eq {α : Type u_1} {p : α × α} {p' : α × α} :
= Sym2.mk p' Sym2.Rel α 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 ()) (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 ())] (z : Sym2 α) (f : (p : α × α) → motive ()) :
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 =
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 : α × α} :
= 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 : αβ} :
Sym2.map (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 : ) :
@[simp]
theorem Sym2.mkEmbedding_apply {α : Type u_1} (a : α) (b : α) :
() 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
• = { toFun := fun (b : α) => s(a, b), inj' := }
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 {α : 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 α) :
().1 e
theorem Sym2.out_snd_mem {α : Type u_1} (e : Sym2 α) :
().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, ) = 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} [] (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
• = s(x, x)
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 : α × α) :
().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 : ) :
(Sym2.map f e).IsDiag e.IsDiag
@[simp]
theorem Sym2.diag_isDiag {α : Type u_1} (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) [] :
DecidablePred Sym2.IsDiag
Equations
theorem Sym2.other_ne {α : Type u_1} {a : α} {z : Sym2 α} (hd : ¬z.IsDiag) (h : a z) :

def Sym2.fromRel {α : Type u_1} {r : ααProp} (sym : ) :
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 : } {z : α × α} :
Sym2.fromRel sym r z.1 z.2
theorem Sym2.fromRel_prop {α : Type u_1} {r : ααProp} {sym : } {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} :
= Set.univ
theorem Sym2.fromRel_ne {α : Type u_1} :
= {z : Sym2 α | ¬z.IsDiag}
theorem Sym2.fromRel_irreflexive {α : Type u_1} {r : ααProp} {sym : } :
∀ {z : Sym2 α}, z Sym2.fromRel sym¬z.IsDiag
theorem Sym2.mem_fromRel_irrefl_other_ne {α : Type u_1} {r : ααProp} {sym : } (irrefl : ) {a : α} {z : Sym2 α} (hz : z Sym2.fromRel sym) (h : a z) :
instance Sym2.fromRel.decidablePred {α : Type u_1} {r : ααProp} (sym : ) [h : ] :
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 : ) :
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
• = Sym2.sym2EquivSym'.trans Sym.symEquivSym'.symm
Instances For
def Sym2.equivMultiset (α : Type u_4) :
Sym2 α { s : // 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
instance Sym2.instDecidableRel {α : Type u_1} [] :

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

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

The other element of an element of the symmetric square #

def Sym2.Mem.other' {α : Type u_1} [] {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
• = Sym2.rec (motive := fun (x : Sym2 α) => a xα) (fun (s : α × α) (x : a ) => ) z h
Instances For
@[simp]
theorem Sym2.other_spec' {α : Type u_1} [] {a : α} {z : Sym2 α} (h : a z) :
s(a, ) = z
@[simp]
theorem Sym2.other_eq_other' {α : Type u_1} [] {a : α} {z : Sym2 α} (h : a z) :
theorem Sym2.other_mem' {α : Type u_1} [] {a : α} {z : Sym2 α} (h : a z) :
theorem Sym2.other_invol' {α : Type u_1} [] {a : α} {z : Sym2 α} (ha : a z) (hb : z) :
= a
theorem Sym2.other_invol {α : Type u_1} {a : α} {z : Sym2 α} (ha : a z) (hb : z) :
= a
theorem Sym2.filter_image_mk_isDiag {α : Type u_1} [] (s : ) :
Finset.filter Sym2.IsDiag (Finset.image Sym2.mk (s ×ˢ s)) = Finset.image Sym2.mk s.diag
theorem Sym2.filter_image_mk_not_isDiag {α : Type u_1} [] (s : ) :
Finset.filter (fun (a : Sym2 α) => ¬a.IsDiag) (Finset.image Sym2.mk (s ×ˢ s)) = Finset.image Sym2.mk s.offDiag
instance Sym2.instSubsingleton {α : Type u_1} [] :
Equations
• =
instance Sym2.instUnique {α : Type u_1} [] :
Equations
instance Sym2.instIsEmpty {α : Type u_1} [] :
Equations
• =
instance Sym2.instNontrivial {α : Type u_1} [] :
Equations
• =
unsafe instance Sym2.instRepr {α : Type u_1} [Repr α] :
Repr (Sym2 α)
Equations
• One or more equations did not get rendered due to their size.