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.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 : α), (x, y) (x, y)
• swap : ∀ {α : Type u} (x y : α), (x, y) (y, x)

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

theorem sym2.rel.symm {α : Type u_1} {x y : α × α} :
x y y x
theorem sym2.rel.trans {α : Type u_1} {x y z : α × α} :
x y y z x z
theorem sym2.rel.is_equivalence {α : Type u_1} :
@[protected, instance]
def sym2.rel.setoid (α : Type u) :
setoid × α)
Equations
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.equiv_multiset).

Equations
@[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.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)
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
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
@[simp]
theorem sym2.lift_mk {α : Type u_1} {β : Type u_2} (f : {f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁}) (a₁ a₂ : α) :
(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.map {α : Type u_1} {β : Type u_2} (f : α → β) :
sym2 αsym2 β

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

Equations
@[simp]
theorem sym2.map_id {α : Type u_1} :
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 f x) = sym2.map (g f) x
@[simp]
theorem sym2.map_pair_eq {α : Type u_1} {β : Type u_2} (f : α → β) (x y : α) :
(x, y) = (f x, f y)
theorem sym2.map.injective {α : Type u_1} {β : Type u_2} {f : α → β} (hinj : function.injective f) :

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
@[protected, instance]
def sym2.has_mem {α : Type u_1} :
(sym2 α)
Equations
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 α) :
theorem sym2.out_snd_mem {α : Type u_1} (e : sym2 α) :
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
@[simp]
theorem sym2.other_spec {α : Type u_1} {a : α} {z : sym2 α} (h : a z) :
(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 = (x, y)
@[protected, ext]
theorem sym2.ext {α : Type u_1} (z z' : sym2 α) (h : ∀ (x : α), x z x z') :
z = z'
@[protected, instance]
def sym2.mem.decidable {α : Type u_1} [decidable_eq α] (x : α) (z : sym2 α) :
Equations
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
theorem sym2.diag_injective {α : Type u_1} :
def sym2.is_diag {α : Type u_1} :
sym2 α → Prop

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

Equations
theorem sym2.mk_is_diag_iff {α : Type u_1} {x y : α} :
@[simp]
theorem sym2.is_diag_iff_proj_eq {α : Type u_1} (z : α × α) :
z.fst = z.snd
@[simp]
theorem sym2.diag_is_diag {α : Type u_1} (a : α) :
theorem sym2.is_diag.mem_range_diag {α : Type u_1} {z : sym2 α} :
z.is_diag
theorem sym2.is_diag_iff_mem_range_diag {α : Type u_1} (z : sym2 α) :
@[protected, instance]
def sym2.is_diag.decidable_pred (α : Type u) [decidable_eq α] :
Equations
theorem sym2.other_ne {α : Type u_1} {a : α} {z : sym2 α} (hd : ¬z.is_diag) (h : a z) :

def sym2.from_rel {α : 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
@[simp]
theorem sym2.from_rel_proj_prop {α : Type u_1} {r : α → α → Prop} {sym : symmetric r} {z : α × α} :
@[simp]
theorem sym2.from_rel_prop {α : Type u_1} {r : α → α → Prop} {sym : symmetric r} {a b : α} :
(a, b) r a b
theorem sym2.from_rel_irreflexive {α : Type u_1} {r : α → α → Prop} {sym : symmetric r} :
∀ {z : sym2 α}, z ¬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 ) (h : a z) :
@[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
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
@[simp]
theorem sym2.to_rel_prop {α : Type u_1} (s : set (sym2 α)) (x y : α) :
x y (x, y) s
theorem sym2.to_rel_symmetric {α : Type u_1} (s : set (sym2 α)) :
theorem sym2.to_rel_from_rel {α : Type u_1} {r : α → α → Prop} (sym : symmetric r) :
theorem sym2.from_rel_to_rel {α : Type u_1} (s : set (sym2 α)) :

Equivalence to the second symmetric power #

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

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

Equations
def sym2.equiv_sym (α : Type u_1) :
sym2 α sym α 2

The symmetric square is equivalent to the second symmetric power.

Equations
def sym2.equiv_multiset (α : Type u_1) :
sym2 α {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
def sym2.rel_bool {α : Type u_1} [decidable_eq α] (x y : α × α) :

An algorithm for computing sym2.rel.

Equations
theorem sym2.rel_bool_spec {α : Type u_1} [decidable_eq α] (x y : α × α) :
y) x y
@[protected, instance]
def sym2.rel.decidable_rel (α : Type u_1) [decidable_eq α] :

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

Equations
• = λ (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
@[simp]
theorem sym2.other_spec' {α : Type u_1} [decidable_eq α] {a : α} {z : sym2 α} (h : a z) :
(a, = z
@[simp]
theorem sym2.other_eq_other' {α : Type u_1} [decidable_eq α] {a : α} {z : sym2 α} (h : a z) :
theorem sym2.other_mem' {α : Type u_1} [decidable_eq α] {a : α} {z : sym2 α} (h : a z) :
theorem sym2.other_invol' {α : Type u_1} [decidable_eq α] {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_quotient_mk_is_diag {α : Type u_1} [decidable_eq α] (s : finset α) :
theorem sym2.filter_image_quotient_mk_not_is_diag {α : Type u_1} [decidable_eq α] (s : finset α) :
finset.filter (λ (a : sym2 α), ¬a.is_diag) (s.product s)) =
@[protected, instance]
def sym2.subsingleton {α : Type u_1} [subsingleton α] :
@[protected, instance]
def sym2.unique {α : Type u_1} [unique α] :
Equations
@[protected, instance]
def sym2.is_empty {α : Type u_1} [is_empty α] :
@[protected, instance]
def sym2.nontrivial {α : Type u_1} [nontrivial α] :