mathlib3 documentation

data.sym.sym2

The symmetric square #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.equiv_sym.

From the point of view that an unordered pair is equivalent to a multiset of cardinality two (see sym2.equiv_multiset), there is a has_mem instance sym2.mem, which is a Prop-valued membership test. Given h : a ∈ z for z : sym2 α, then h.other 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.from_rel 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

refl : ∀ {α : Type u} (x y : α), sym2.rel α (x, y) (x, y)
swap : ∀ {α : Type u} (x y : α), sym2.rel α (x, y) (y, x)

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

Instances for sym2.rel

sym2.rel.decidable_rel

@[symm]

theorem sym2.rel.symm {α : Type u_1} {x y : α × α} :

sym2.rel α x y → sym2.rel α y x

@[trans]

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 α)

@[protected, instance]

def sym2.rel.setoid (α : Type u) :

setoid (α × α)

Equations

sym2.rel.setoid α = {r := sym2.rel α, iseqv := _}

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

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.equiv_multiset).

Equations

sym2 α = quotient (sym2.rel.setoid α)

@[protected]

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

f i

@[protected]

theorem sym2.induction_on {α : Type u_1} {f : sym2 α → Prop} (i : sym2 α) (hf : ∀ (x y : α), f ⟦(x, y)⟧) :

f i

@[protected]

theorem sym2.induction_on₂ {α : 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

@[protected]

theorem sym2.exists {α : Type u_1} {f : sym2 α → Prop} :

(∃ (x : sym2 α), f x) ↔ ∃ (x y : α), f ⟦(x, y)⟧

@[protected]

theorem sym2.forall {α : Type u_1} {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 : α × α} :

⟦p.swap ⟧ = ⟦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 = 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.from_rel instead.

Equations

sym2.lift = {to_fun := λ (f : {f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁}), quotient.lift (function.uncurry ↑f) _, inv_fun := λ (F : sym2 α → β), ⟨function.curry (F ∘ quotient.mk), _⟩, left_inv := _, right_inv := _}

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

sym2.lift₂ = {to_fun := λ (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₁}), quotient.lift₂ (λ (a : α × α) (b : β × β), f.val a.fst a.snd b.fst b.snd) _, inv_fun := λ (F : sym2 α → sym2 β → γ), ⟨λ (a₁ a₂ : α) (b₁ b₂ : β), F ⟦(a₁, a₂)⟧ ⟦(b₁, b₂)⟧, _⟩, left_inv := _, right_inv := _}

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

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

@[protected]

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

@[protected, instance]

def sym2.set_like {α : Type u_1} :

set_like (sym2 α) α

Equations

sym2.set_like = {coe := λ (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 = ⟦(x, y)⟧

@[ext]

theorem sym2.ext {α : Type u_1} {p 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).fst ∈ e

theorem sym2.out_snd_mem {α : Type u_1} (e : sym2 α) :

(quotient.out e).snd ∈ e

theorem sym2.ball {α : Type u_1} {p : α → Prop} {a b : α} :

(∀ (c : α), 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.some. See also mem.other' for the computable version.

Equations

sym2.mem.other h = classical.some 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 z' : sym2 α} (h : x ≠ y) (h1 : x ∈ z) (h2 : y ∈ z) (h3 : x ∈ z') (h4 : y ∈ z') :

z = z'

@[protected, instance]

def sym2.mem.decidable {α : Type u_1} [decidable_eq α] (x : α) (z : sym2 α) :

decidable (x ∈ z)

Equations

sym2.mem.decidable x z = quotient.rec_on_subsingleton z (λ (_x : α × α), sym2.mem.decidable._match_1 x _x)
sym2.mem.decidable._match_1 x (y₁, y₂) = decidable_of_iff' (x = y₁ ∨ x = y₂) sym2.mem_iff

@[simp]

theorem sym2.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {z : sym2 α} :

b ∈ sym2.map f z ↔ ∃ (a : α), a ∈ z ∧ f a = b

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

sym2.map f s = sym2.map g s

@[simp]

theorem sym2.map_id' {α : Type u_1} :

sym2.map (λ (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 : α) :

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.is_diag {α : Type u_1} :

sym2 α → Prop

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

Equations

sym2.is_diag = ⇑sym2.lift ⟨eq α, _⟩

Instances for sym2.is_diag

sym2.is_diag.decidable_pred

theorem sym2.mk_is_diag_iff {α : Type u_1} {x y : α} :

sym2.is_diag ⟦(x, y)⟧ ↔ x = y

@[simp]

theorem sym2.is_diag_iff_proj_eq {α : Type u_1} (z : α × α) :

sym2.is_diag ⟦z⟧ ↔ z.fst = z.snd

@[simp]

theorem sym2.diag_is_diag {α : Type u_1} (a : α) :

(sym2.diag a).is_diag

theorem sym2.is_diag.mem_range_diag {α : Type u_1} {z : sym2 α} :

z.is_diag → z ∈ set.range sym2.diag

theorem sym2.is_diag_iff_mem_range_diag {α : Type u_1} (z : sym2 α) :

z.is_diag ↔ z ∈ set.range sym2.diag

@[protected, instance]

def sym2.is_diag.decidable_pred (α : Type u) [decidable_eq α] :

decidable_pred sym2.is_diag

Equations

sym2.is_diag.decidable_pred α = λ (z : sym2 α), quotient.rec_on_subsingleton z (λ (a : α × α), _.mpr (_inst_1 a.fst a.snd))

theorem sym2.other_ne {α : Type u_1} {a : α} {z : sym2 α} (hd : ¬z.is_diag) (h : a ∈ z) :

sym2.mem.other h ≠ a

Declarations about symmetric relations #

def sym2.from_rel {α : Type u_1} {r : α → α → Prop} (sym : symmetric r) :

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

Equations

sym2.from_rel sym = set_of (⇑sym2.lift ⟨r, _⟩)

@[simp]

theorem sym2.from_rel_proj_prop {α : Type u_1} {r : α → α → Prop} {sym : symmetric r} {z : α × α} :

⟦z⟧ ∈ sym2.from_rel sym ↔ r z.fst z.snd

@[simp]

theorem sym2.from_rel_prop {α : Type u_1} {r : α → α → Prop} {sym : symmetric r} {a b : α} :

⟦(a, b)⟧ ∈ sym2.from_rel sym ↔ r a b

theorem sym2.from_rel_bot {α : Type u_1} :

sym2.from_rel _ = ∅

theorem sym2.from_rel_top {α : Type u_1} :

sym2.from_rel _ = set.univ

theorem sym2.from_rel_irreflexive {α : Type u_1} {r : α → α → Prop} {sym : symmetric r} :

irreflexive r ↔ ∀ {z : sym2 α}, z ∈ sym2.from_rel sym → ¬z.is_diag

theorem sym2.mem_from_rel_irrefl_other_ne {α : Type u_1} {r : α → α → Prop} {sym : symmetric r} (irrefl : irreflexive r) {a : α} {z : sym2 α} (hz : z ∈ sym2.from_rel sym) (h : a ∈ z) :

sym2.mem.other h ≠ a

@[protected, instance]

def sym2.from_rel.decidable_pred {α : Type u_1} {r : α → α → Prop} (sym : symmetric r) [h : decidable_rel r] :

decidable_pred (λ (_x : sym2 α), _x ∈ sym2.from_rel sym)

Equations

sym2.from_rel.decidable_pred sym = λ (z : sym2 α), quotient.rec_on_subsingleton z (λ (x : α × α), h x.fst x.snd)

def sym2.to_rel {α : Type u_1} (s : set (sym2 α)) (x y : α) :

Prop

The inverse to sym2.from_rel. Given a set on sym2 α, give a symmetric relation on α (see sym2.to_rel_symmetric).

Equations

sym2.to_rel s x y = (⟦(x, y)⟧ ∈ s)

@[simp]

theorem sym2.to_rel_prop {α : Type u_1} (s : set (sym2 α)) (x y : α) :

sym2.to_rel s x y ↔ ⟦(x, y)⟧ ∈ s

theorem sym2.to_rel_symmetric {α : Type u_1} (s : set (sym2 α)) :

symmetric (sym2.to_rel s)

theorem sym2.to_rel_from_rel {α : Type u_1} {r : α → α → Prop} (sym : symmetric r) :

sym2.to_rel (sym2.from_rel sym) = r

theorem sym2.from_rel_to_rel {α : Type u_1} (s : set (sym2 α)) :

sym2.from_rel _ = s

Equivalence to the second symmetric power #

def sym2.sym2_equiv_sym' {α : Type u_1} :

sym2 α ≃ sym.sym' α 2

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

Equations

sym2.sym2_equiv_sym' = {to_fun := quotient.map (λ (x : α × α), ⟨[x.fst, x.snd], _⟩) sym2.sym2_equiv_sym'._proof_2, inv_fun := quotient.map from_vector sym2.sym2_equiv_sym'._proof_3, left_inv := _, right_inv := _}

def sym2.equiv_sym (α : Type u_1) :

sym2 α ≃ sym α 2

The symmetric square is equivalent to the second symmetric power.

Equations

sym2.equiv_sym α = sym2.sym2_equiv_sym'.trans sym.sym_equiv_sym'.symm

def sym2.equiv_multiset (α : Type u_1) :

sym2 α ≃ {s // ⇑multiset.card s = 2}

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

Equations

sym2.equiv_multiset α = sym2.equiv_sym α

def sym2.rel_bool {α : Type u_1} [decidable_eq α] (x y : α × α) :

An algorithm for computing sym2.rel.

Equations

sym2.rel_bool x y = ite (x.fst = y.fst) (decidable.to_bool (x.snd = y.snd)) (ite (x.fst = y.snd) (decidable.to_bool (x.snd = y.fst)) bool.ff)

theorem sym2.rel_bool_spec {α : Type u_1} [decidable_eq α] (x y : α × α) :

↥(sym2.rel_bool x y) ↔ sym2.rel α x y

@[protected, instance]

def sym2.rel.decidable_rel (α : Type u_1) [decidable_eq α] :

decidable_rel (sym2.rel α)

Given [decidable_eq α] and [fintype α], the following instance gives fintype (sym2 α).

Equations

sym2.rel.decidable_rel α = λ (x y : α × α), decidable_of_bool (sym2.rel_bool x y) _

The other element of an element of the symmetric square #

def sym2.mem.other' {α : Type u_1} [decidable_eq α] {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.mem.other' h = quot.rec (λ (x : α × α) (h' : a ∈ quot.mk setoid.r x), pair_other a x) sym2.mem.other'._proof_1 z h

@[simp]

theorem sym2.other_spec' {α : Type u_1} [decidable_eq α] {a : α} {z : sym2 α} (h : a ∈ z) :

⟦(a, sym2.mem.other' h)⟧ = z

@[simp]

theorem sym2.other_eq_other' {α : Type u_1} [decidable_eq α] {a : α} {z : sym2 α} (h : a ∈ z) :

sym2.mem.other h = sym2.mem.other' h

theorem sym2.other_mem' {α : Type u_1} [decidable_eq α] {a : α} {z : sym2 α} (h : a ∈ z) :

sym2.mem.other' h ∈ z

theorem sym2.other_invol' {α : Type u_1} [decidable_eq α] {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_is_diag {α : Type u_1} [decidable_eq α] (s : finset α) :

finset.filter sym2.is_diag (finset.image quotient.mk (s ×ˢ s)) = finset.image quotient.mk s.diag

theorem sym2.filter_image_quotient_mk_not_is_diag {α : Type u_1} [decidable_eq α] (s : finset α) :

finset.filter (λ (a : sym2 α), ¬a.is_diag) (finset.image quotient.mk (s ×ˢ s)) = finset.image quotient.mk s.off_diag

@[protected, instance]

def sym2.subsingleton {α : Type u_1} [subsingleton α] :

subsingleton (sym2 α)

@[protected, instance]

def sym2.unique {α : Type u_1} [unique α] :

unique (sym2 α)

Equations

sym2.unique = unique.mk' (sym2 α)

@[protected, instance]

def sym2.is_empty {α : Type u_1} [is_empty α] :

is_empty (sym2 α)

@[protected, instance]

def sym2.nontrivial {α : Type u_1} [nontrivial α] :

nontrivial (sym2 α)