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 symmetric square has a setoid instance, so ⟦(a, b)⟧ denotes a term of the symmetric square.

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)

theorem Sym2.Rel.symm {α : Type u_1} {x : α × α} {y : α × α} : Sym2.Rel α x y → Sym2.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} : Equivalence (Sym2.Rel α)

instance Sym2.Rel.setoid (α : Type u) : Setoid (α × α)

Equations

• Sym2.Rel.setoid α = { r := Sym2.Rel α, iseqv := (_ : Equivalence (Sym2.Rel α)) }

@[simp]

theorem Sym2.rel_iff {α : Type u_1} {x : α} {y : α} {z : α} {w : α} : (x, y) ≈ (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

@[reducible]

def Sym2 (α : Type u) : 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

• Sym2 α = Quotient (Sym2.Rel.setoid α)

theorem Sym2.ind {α : Type u_1} {f : Sym2 α → Prop} (h : ∀ (x y : α), f ⟦(x, y)⟧) (i : Sym2 α) : f i

theorem Sym2.inductionOn {α : Type u_1} {f : Sym2 α → Prop} (i : Sym2 α) (hf : ∀ (x y : α), f ⟦(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 ⟦(a₁, a₂)⟧ ⟦(b₁, b₂)⟧) : f i j

theorem Sym2.exists {α : Type u_4} {f : Sym2 α → Prop} : (∃ (x : Sym2 α), f x) ↔ ∃ (x : α) (y : α), f ⟦(x, y)⟧

theorem Sym2.forall {α : Type u_4} {f : Sym2 α → Prop} : (∀ (x : Sym2 α), f x) ↔ ∀ (x y : α), f ⟦(x, y)⟧

theorem Sym2.eq_swap {α : Type u_1} {a : α} {b : α} : ⟦(a, b)⟧ = ⟦(b, a)⟧

@[simp]

theorem Sym2.mk''_prod_swap_eq {α : Type u_1} {p : α × α} : ⟦Prod.swap p⟧ = ⟦p⟧

theorem Sym2.congr_right {α : Type u_1} {a : α} {b : α} {c : α} : ⟦(a, b)⟧ = ⟦(a, c)⟧ ↔ b = c

theorem Sym2.congr_left {α : Type u_1} {a : α} {b : α} {c : α} : ⟦(b, a)⟧ = ⟦(c, a)⟧ ↔ b = c

theorem Sym2.eq_iff {α : Type u_1} {x : α} {y : α} {z : α} {w : α} : ⟦(x, y)⟧ = ⟦(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 ∨ p = Prod.swap q

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.

@[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 ⟦(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 ⟦(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.

@[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 ⟦(a₁, a₂)⟧ ⟦(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 ⟦(a₁, a₂)⟧ ⟦(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

• Sym2.map f = Quotient.map (Prod.map f f) (_ : ∀ ⦃a b : α × α⦄, a ≈ b → Prod.map f f a ≈ Prod.map f f b)

@[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) = Sym2.map g ∘ Sym2.map 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 ⟦(x, y)⟧ = ⟦(f x, f y)⟧

theorem Sym2.map.injective {α : Type u_1} {β : Type u_2} {f : α → β} (hinj : Function.Injective f) : Function.Injective (Sym2.map f)

Membership and set coercion

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

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

• Sym2.Mem x z = ∃ (y : α), z = ⟦(x, y)⟧

theorem Sym2.mem_iff' {α : Type u_1} {a : α} {b : α} {c : α} : Sym2.Mem a ⟦(b, c)⟧ ↔ a = b ∨ a = c

instance Sym2.instSetLikeSym2 {α : Type u_1} : SetLike (Sym2 α) α

Equations

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

@[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 = ⟦(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 ∈ ⟦(x, y)⟧

theorem Sym2.mem_mk''_right {α : Type u_1} (x : α) (y : α) : y ∈ ⟦(x, y)⟧

@[simp]

theorem Sym2.mem_iff {α : Type u_1} {a : α} {b : α} {c : α} : a ∈ ⟦(b, c)⟧ ↔ a = b ∨ a = c

theorem Sym2.out_fst_mem {α : Type u_1} (e : Sym2 α) : (Quotient.out e).1 ∈ e

theorem Sym2.out_snd_mem {α : Type u_1} (e : Sym2 α) : (Quotient.out e).2 ∈ e

theorem Sym2.ball {α : Type u_1} {p : α → Prop} {a : α} {b : α} : (∀ c ∈ ⟦(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

• Sym2.Mem.other h = Classical.choose h

@[simp]

theorem Sym2.other_spec {α : Type u_1} {a : α} {z : Sym2 α} (h : a ∈ z) : ⟦(a, Sym2.Mem.other h)⟧ = z

theorem Sym2.other_mem {α : Type u_1} {a : α} {z : Sym2 α} (h : a ∈ z) : Sym2.Mem.other h ∈ z

theorem Sym2.mem_and_mem_iff {α : Type u_1} {x : α} {y : α} {z : Sym2 α} (hne : x ≠ y) : x ∈ z ∧ y ∈ z ↔ z = ⟦(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 α) : Decidable (x ∈ z)

Equations

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

@[simp]

theorem Sym2.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {z : Sym2 α} : b ∈ Sym2.map f z ↔ ∃ a ∈ z, f a = b

theorem Sym2.map_congr {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} {s : Sym2 α} (h : ∀ x ∈ s, f x = g x) : Sym2.map f s = Sym2.map g s

@[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

• Sym2.diag x = ⟦(x, x)⟧

theorem Sym2.diag_injective {α : Type u_1} : Function.Injective Sym2.diag

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 { val := Eq, property := (_ : ∀ (x x_1 : α), (x = x_1) = (x_1 = x)) }

theorem Sym2.mk''_isDiag_iff {α : Type u_1} {x : α} {y : α} : Sym2.IsDiag ⟦(x, y)⟧ ↔ x = y

@[simp]

theorem Sym2.isDiag_iff_proj_eq {α : Type u_1} (z : α × α) : Sym2.IsDiag ⟦z⟧ ↔ z.1 = z.2

theorem Sym2.IsDiag.map {α : Type u_1} {β : Type u_2} {e : Sym2 α} {f : α → β} : Sym2.IsDiag e → Sym2.IsDiag (Sym2.map f e)

theorem Sym2.isDiag_map {α : Type u_1} {β : Type u_2} {e : Sym2 α} {f : α → β} (hf : Function.Injective f) : Sym2.IsDiag (Sym2.map f e) ↔ Sym2.IsDiag e

@[simp]

theorem Sym2.diag_isDiag {α : Type u_1} (a : α) : Sym2.IsDiag (Sym2.diag a)

theorem Sym2.IsDiag.mem_range_diag {α : Type u_1} {z : Sym2 α} : Sym2.IsDiag z → z ∈ Set.range Sym2.diag

theorem Sym2.isDiag_iff_mem_range_diag {α : Type u_1} (z : Sym2 α) : Sym2.IsDiag z ↔ z ∈ Set.range Sym2.diag

instance Sym2.IsDiag.decidablePred (α : Type u) [DecidableEq α] : DecidablePred Sym2.IsDiag

Equations

• Sym2.IsDiag.decidablePred α z = Quotient.recOnSubsingleton z fun (a : α × α) => Eq.mpr (_ : Decidable (Sym2.IsDiag ⟦a⟧) = Decidable (a.1 = a.2)) inferInstance

theorem Sym2.other_ne {α : Type u_1} {a : α} {z : Sym2 α} (hd : ¬Sym2.IsDiag z) (h : a ∈ z) : Sym2.Mem.other h ≠ a

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

• Sym2.fromRel sym = setOf (Sym2.lift { val := r, property := (_ : ∀ (x x_1 : α), r x x_1 = r x_1 x) })

@[simp]

theorem Sym2.fromRel_proj_prop {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} {z : α × α} : ⟦z⟧ ∈ Sym2.fromRel sym ↔ r z.1 z.2

theorem Sym2.fromRel_prop {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} {a : α} {b : α} : ⟦(a, b)⟧ ∈ Sym2.fromRel sym ↔ r a b

theorem Sym2.fromRel_bot {α : Type u_1} : Sym2.fromRel (_ : ∀ (x y : α), ⊥ x y → ⊥ x y) = ∅

theorem Sym2.fromRel_top {α : Type u_1} : Sym2.fromRel (_ : ∀ (x y : α), ⊤ x y → ⊤ x y) = Set.univ

theorem Sym2.fromRel_ne {α : Type u_1} : Sym2.fromRel (_ : ∀ (x y : α), x ≠ y → y ≠ x) = {z : Sym2 α | ¬Sym2.IsDiag z}

theorem Sym2.fromRel_irreflexive {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} : Irreflexive r ↔ ∀ {z : Sym2 α}, z ∈ Sym2.fromRel sym → ¬Sym2.IsDiag z

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) : Sym2.Mem.other h ≠ a

instance Sym2.fromRel.decidablePred {α : Type u_1} {r : α → α → Prop} (sym : Symmetric r) [h : DecidableRel r] : DecidablePred fun (x : Sym2 α) => x ∈ Sym2.fromRel sym

Equations

• Sym2.fromRel.decidablePred sym z = Quotient.recOnSubsingleton z fun (x : α × α) => h x.1 x.2

def Sym2.ToRel {α : Type u_1} (s : Set (Sym2 α)) (x : α) (y : α) : Prop

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

Equations

• Sym2.ToRel s x y = (⟦(x, y)⟧ ∈ s)

@[simp]

theorem Sym2.toRel_prop {α : Type u_1} (s : Set (Sym2 α)) (x : α) (y : α) : Sym2.ToRel s x y ↔ ⟦(x, y)⟧ ∈ s

theorem Sym2.toRel_symmetric {α : Type u_1} (s : Set (Sym2 α)) : Symmetric (Sym2.ToRel s)

theorem Sym2.toRel_fromRel {α : Type u_1} {r : α → α → Prop} (sym : Symmetric r) : Sym2.ToRel (Sym2.fromRel sym) = r

theorem Sym2.fromRel_toRel {α : Type u_1} (s : Set (Sym2 α)) : Sym2.fromRel (_ : Symmetric (Sym2.ToRel s)) = s

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

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

def Sym2.equivSym (α : Type u_4) : Sym2 α ≃ Sym α 2

The symmetric square is equivalent to the second symmetric power.

Equations

• Sym2.equivSym α = Sym2.sym2EquivSym'.trans Sym.symEquivSym'.symm

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

• Sym2.equivMultiset α = Sym2.equivSym α

instance Sym2.instDecidableRel {α : Type u_1} [DecidableEq α] : DecidableRel (Sym2.Rel α)

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

Equations

• Sym2.instDecidableRel x✝ x = decidable_of_iff' (x✝.1 = x.1 ∧ x✝.2 = x.2 ∨ x✝.1 = x.2 ∧ x✝.2 = x.1) (_ : (x✝.1, x✝.2) ≈ (x.1, x.2) ↔ x✝.1 = x.1 ∧ x✝.2 = x.2 ∨ x✝.1 = x.2 ∧ x✝.2 = x.1)

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

Equations

• Sym2.instDecidableRel' = Sym2.instDecidableRel

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

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

@[simp]

theorem Sym2.other_spec' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : ⟦(a, Sym2.Mem.other' h)⟧ = z

@[simp]

theorem Sym2.other_eq_other' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : Sym2.Mem.other h = Sym2.Mem.other' h

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

theorem Sym2.other_invol' {α : Type u_1} [DecidableEq α] {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Sym2.Mem.other' ha ∈ z) : Sym2.Mem.other' hb = a

theorem Sym2.other_invol {α : Type u_1} {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Sym2.Mem.other ha ∈ z) : Sym2.Mem.other hb = a

theorem Sym2.filter_image_quotient_mk''_isDiag {α : Type u_1} [DecidableEq α] (s : Finset α) : Finset.filter Sym2.IsDiag (Finset.image Quotient.mk'' (s ×ˢ s)) = Finset.image Quotient.mk'' (Finset.diag s)

theorem Sym2.filter_image_quotient_mk''_not_isDiag {α : Type u_1} [DecidableEq α] (s : Finset α) : Finset.filter (fun (a : Sym2 α) => ¬Sym2.IsDiag a) (Finset.image Quotient.mk'' (s ×ˢ s)) = Finset.image Quotient.mk'' (Finset.offDiag s)

instance Sym2.instSubsingletonSym2 {α : Type u_1} [Subsingleton α] : Subsingleton (Sym2 α)

Equations

• (_ : Subsingleton (Sym2 α)) = (_ : Subsingleton (Sym2 α))

instance Sym2.instUniqueSym2 {α : Type u_1} [Unique α] : Unique (Sym2 α)

Equations

• Sym2.instUniqueSym2 = Unique.mk' (Sym2 α)

instance Sym2.instIsEmptySym2 {α : Type u_1} [IsEmpty α] : IsEmpty (Sym2 α)

Equations

• (_ : IsEmpty (Sym2 α)) = (_ : IsEmpty (Sym2 α))

instance Sym2.instNontrivialSym2 {α : Type u_1} [Nontrivial α] : Nontrivial (Sym2 α)

Equations

• (_ : Nontrivial (Sym2 α)) = (_ : Nontrivial (Sym2 α))