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
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 α)
Instances For
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.
Instances For
A two-argument version of Sym2.lift
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 α
.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Given an element of the unordered pair, give the other element using Classical.choose
.
See also Mem.other'
for the computable version.
Equations
Instances For
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 #
Equations
- Sym2.IsDiag.decidablePred α z = Quotient.recOnSubsingleton z fun (a : α × α) => Eq.mpr (_ : Decidable (Sym2.IsDiag ⟦a⟧) = Decidable (a.1 = a.2)) 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) })
Instances For
Equations
- Sym2.fromRel.decidablePred sym z = Quotient.recOnSubsingleton z fun (x : α × α) => h x.1 x.2
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)
Instances For
Equivalence to the second symmetric power #
The symmetric square is equivalent to the second symmetric power.
Equations
- Sym2.equivSym α = Sym2.sym2EquivSym'.trans Sym.symEquivSym'.symm
Instances For
Given [DecidableEq α]
and [Fintype α]
, the following instance gives Fintype (Sym2 α)
.
Equations
- Sym2.instDecidableRel' = Sym2.instDecidableRel
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.
Instances For
Equations
- (_ : Subsingleton (Sym2 α)) = (_ : Subsingleton (Sym2 α))
Equations
- Sym2.instUniqueSym2 = Unique.mk' (Sym2 α)
Equations
- (_ : Nontrivial (Sym2 α)) = (_ : Nontrivial (Sym2 α))