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∈ 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
Equations
- Sym2.Rel.setoid α = { r := Sym2.Rel α, iseqv := (_ : Equivalence (Sym2.Rel α)) }
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 α)
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.
Membership and set coercion #
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 = Quotient.mk (Sym2.Rel.setoid α) (x, y)
Given an element of the unordered pair, give the other element using Classical.choose
.
See also Mem.other'
for the computable version.
Equations
Equations
- One or more equations did not get rendered due to their size.
Note: Sym2.map_id
will not simplify Sym2.map id z
due to Sym2.map_congr
.
Diagonal #
A type α
is naturally included in the diagonal of α × α× α
, and this function gives the image
of this diagonal in Sym2 α
.
Equations
- Sym2.diag x = Quotient.mk (Sym2.Rel.setoid α) (x, x)
Equations
- Sym2.IsDiag.decidablePred α z = Quotient.recOnSubsingleton z fun a => Eq.mpr (_ : Decidable (Sym2.IsDiag (Quotient.mk (Sym2.Rel.setoid α) a)) = Decidable (a.fst = a.snd)) inferInstance
Declarations about symmetric relations #
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) })
Equations
- Sym2.fromRel.decidablePred sym z = Quotient.recOnSubsingleton z fun x => h x.fst x.snd
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 = (Quotient.mk (Sym2.Rel.setoid α) (x, y) ∈ s)
Equivalence to the second symmetric power #
The symmetric square is equivalent to the second symmetric power.
Equations
- Sym2.equivSym α = Equiv.trans Sym2.sym2EquivSym' (Equiv.symm Sym.symEquivSym')
Given [DecidableEq α]
and [Fintype α]
, the following instance gives Fintype (Sym2 α)
.
Equations
- Sym2.instDecidableRelProdRel α x y = decidable_of_bool (Sym2.relBool x y) (_ : Sym2.relBool x y = true ↔ Sym2.Rel α x y)
An algorithm for deciding equality in Sym2 α
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Sym2.instDecidableEqSym2 α a b = decidable_of_bool (Sym2.eqBool a b) (_ : Sym2.eqBool a b = true ↔ a = b)
The other element of an element of the symmetric square #
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.
Equations
- Sym2.instUniqueSym2 = Unique.mk' (Sym2 α)