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). 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 a ∈ z for z : sym2 α, it does not appear to be
possible, in general, to computably give the other element in the
pair. For this, sym2.vmem a z is a Type-valued membership test
that gives a way to obtain the other element with sym2.vmem.other.
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.
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
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 α)
Declarations about membership
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.has_mem = {mem := sym2.mem α}
This is a type-valued version of the membership predicate mem that contains the other
element y of z such that z = ⟦(x, y)⟧. It is a subsingleton already,
so there is no need to apply trunc to the type.
Equations
- _ = _
The vmem version of mk_has_mem.
Equations
- sym2.mk_has_vmem x y = ⟨y, _⟩
Equations
- sym2.has_lift = {lift := _}
This is the mem-based version of other.
Equations
Declarations about symmetric relations
Symmetric relations define a set on sym2 α by taking all those pairs
of elements that are related.
Equations
- sym2.from_rel sym = λ (z : sym2 α), quotient.rec_on z (λ (z : α × α), r z.fst z.snd) _
Equations
- sym2.from_rel.decidable_as_set sym = λ (x : sym2 α), quotient.rec_on x (λ (x' : α × α), _.mpr (h x'.fst x'.snd)) _
Equations
- sym2.from_rel.decidable_pred sym = id (λ (a : sym2 α), sym2.from_rel.decidable_as_set sym a)
Equivalence to the second symmetric power
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 := _}
The symmetric square is equivalent to the second symmetric power.
Equations
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
Given [decidable_eq α] and [fintype α], the following instance gives fintype (sym2 α).
Equations
- sym2.decidable_rel α = λ (x y : α × α), decidable_of_bool (sym2.rel_bool x y) _