Nominal sets

DefinitionSubgroup of finitely supported permutations of atoms#✓fully proved

The subgroup of finitely supported permutations of Atom: permutations that fix all atoms outside some finite set.

Cslib.Nominal.finPermSubgroup · 19 lines

def finPermSubgroup (Atom : Type*) [DecidableEq Atom] : Subgroup (Equiv.Perm Atom) where
  carrier := {π | ∃ S : Finset Atom, ∀ a, a ∉ S → π a = a}
  one_mem' := ⟨∅, fun _ _ => rfl⟩
  mul_mem' := by
    intro π σ hπ hσ
    obtain ⟨Sπ, hSπ⟩ := hπ
    obtain ⟨Sσ, hSσ⟩ := hσ
    refine ⟨Sπ ∪ Sσ, fun a ha => ?_⟩
    have haπ : a ∉ Sπ := fun h => ha (Finset.mem_union_left Sσ h)
    have haσ : a ∉ Sσ := fun h => ha (Finset.mem_union_right Sπ h)
    rw [Equiv.Perm.mul_apply, hSσ a haσ, hSπ a haπ]
  inv_mem' := by
    intro π hπ
    obtain ⟨S, hS⟩ := hπ
    refine ⟨S, fun a ha => ?_⟩
    have h : π a = a := hS a ha
    have h' : π⁻¹ (π a) = π⁻¹ a := congrArg (⇑π⁻¹) h
    rw [Equiv.Perm.coe_inv, Equiv.symm_apply_apply] at h'
    exact h'.symm

Used by 45

Used byAtom abstraction of a nominal set · Abstraction of an element at a bound atom · Equality of abstractions is α-equivalence · Abstractions with the same bound atom have equal bodies · α-equivalence relation on atom–element pairs · Reflexivity of α-equivalence · Symmetry of α-equivalence · Transitivity of α-equivalence · Setoid of α-equivalence · Permutation action on abstractions · Existence of fresh atoms · Existence of a least finite support · Group of finitely supported permutations · Freshness of an atom for an element · Freshness is non-membership in the least support · Permutation image of a support · Intersection of two supports is a support · Equivariant elements of a nominal set · Membership in the least support · Enlarging a support · Nominal set · A pair is supported by the union of its components' supports · Permutation action on abstractions computed on representatives · Permutations agreeing on the support act equally · Permutations moving only fresh atoms fix the element · Least finite support of an element · Support of an atom abstraction · Support of an atom · Equivariant elements have empty support · Equivariance of the least support · Minimality of the least support · Least support is a support · Supporting set of atoms for an element · Equivariant elements are supported by the empty set · Abstractions are supported by the body's support minus the atom · Transposition of two atoms · Symmetry of transpositions · Conjugation of a transposition · A transposition is its own inverse · A transposition squares to the identity · Transposition of an atom with itself is the identity · Action of a transposition · Swapping two fresh atoms fixes the element · Transposition fixes atoms other than the swapped pair · Transposition of atoms outside a support fixes the element

AbbreviationGroup of finitely supported permutations#✓fully proved

The group of finitely supported permutations of Atom.

abbrev FinPerm (Atom : Type*) [DecidableEq Atom] : Type _ := ↥(finPermSubgroup Atom)

Uses 1 · Used by 44

Statement usesSubgroup of finitely supported permutations of atoms

Used byAtom abstraction of a nominal set · Abstraction of an element at a bound atom · Equality of abstractions is α-equivalence · Abstractions with the same bound atom have equal bodies · α-equivalence relation on atom–element pairs · Reflexivity of α-equivalence · Symmetry of α-equivalence · Transitivity of α-equivalence · Setoid of α-equivalence · Permutation action on abstractions · Existence of fresh atoms · Existence of a least finite support · Freshness of an atom for an element · Freshness is non-membership in the least support · Permutation image of a support · Intersection of two supports is a support · Equivariant elements of a nominal set · Membership in the least support · Enlarging a support · Nominal set · A pair is supported by the union of its components' supports · Permutation action on abstractions computed on representatives · Permutations agreeing on the support act equally · Permutations moving only fresh atoms fix the element · Least finite support of an element · Support of an atom abstraction · Support of an atom · Equivariant elements have empty support · Equivariance of the least support · Minimality of the least support · Least support is a support · Supporting set of atoms for an element · Equivariant elements are supported by the empty set · Abstractions are supported by the body's support minus the atom · Transposition of two atoms · Symmetry of transpositions · Conjugation of a transposition · A transposition is its own inverse · A transposition squares to the identity · Transposition of an atom with itself is the identity · Action of a transposition · Swapping two fresh atoms fixes the element · Transposition fixes atoms other than the swapped pair · Transposition of atoms outside a support fixes the element

DefinitionTransposition of two atoms#✓fully proved

The transposition of two atoms, as a finite permutation.

def swap (a b : Atom) : FinPerm Atom :=
  ⟨Equiv.swap a b, ⟨{a, b}, fun x hx => by
    by_contra h
    exact h (Equiv.swap_apply_of_ne_of_ne
      (fun h₁ => hx (Finset.mem_insert.mpr (Or.inl h₁)))
      (fun h₂ => hx (Finset.mem_insert.mpr (Or.inr (Finset.mem_singleton.mpr h₂)))))⟩⟩

Uses 2 · Used by 19

Statement usesGroup of finitely supported permutations · Subgroup of finitely supported permutations of atoms

Used byAbstractions with the same bound atom have equal bodies · α-equivalence relation on atom–element pairs · Reflexivity of α-equivalence · Symmetry of α-equivalence · Transitivity of α-equivalence · Permutation action on abstractions · Permutations moving only fresh atoms fix the element · Support of an atom abstraction · Support of an atom · Abstractions are supported by the body's support minus the atom · Symmetry of transpositions · Conjugation of a transposition · A transposition is its own inverse · A transposition squares to the identity · Transposition of an atom with itself is the identity · Action of a transposition · Swapping two fresh atoms fixes the element · Transposition fixes atoms other than the swapped pair · Transposition of atoms outside a support fixes the element

TheoremAction of a transposition#✓fully proved

Applying a transposition is applying the underlying Equiv.swap.

theorem swap_smul (a b c : Atom) :
    (swap a b : FinPerm Atom) • c = Equiv.swap a b c

Uses 3 · Used by 8

Statement usesGroup of finitely supported permutations · Subgroup of finitely supported permutations of atoms · Transposition of two atoms

Used bySymmetry of α-equivalence · Transitivity of α-equivalence · Permutations moving only fresh atoms fix the element · Support of an atom abstraction · Support of an atom · Abstractions are supported by the body's support minus the atom · Swapping two fresh atoms fixes the element · Transposition fixes atoms other than the swapped pair

TheoremA transposition squares to the identity#✓fully proved

A transposition is an involution, stated for the FinPerm group.

theorem swap_mul_self (a b : Atom) : (swap a b : FinPerm Atom) * swap a b = 1

Uses 3 · Used by 4

Statement usesGroup of finitely supported permutations · Subgroup of finitely supported permutations of atoms · Transposition of two atoms

Used bySymmetry of α-equivalence · Transitivity of α-equivalence · Permutations moving only fresh atoms fix the element · A transposition is its own inverse

TheoremA transposition is its own inverse#✓fully proved

A transposition is its own inverse.

theorem swap_inv (a b : Atom) : (swap a b : FinPerm Atom)⁻¹ = swap a b

Uses 4 · Used by 1

Statement usesGroup of finitely supported permutations · Subgroup of finitely supported permutations of atoms · Transposition of two atoms

Proof usesA transposition squares to the identity

Used bySwapping two fresh atoms fixes the element

TheoremTransposition of an atom with itself is the identity#✓fully proved

A transposition of an atom with itself is the identity.

theorem swap_self (a : Atom) : (swap a a : FinPerm Atom) = 1

Uses 3 · Used by 1

Statement usesGroup of finitely supported permutations · Subgroup of finitely supported permutations of atoms · Transposition of two atoms

Used bySwapping two fresh atoms fixes the element

TheoremSymmetry of transpositions#✓fully proved

Transpositions are symmetric.

theorem swap_comm (a b : Atom) : (swap a b : FinPerm Atom) = swap b a

Uses 3 · Used by 3

Statement usesGroup of finitely supported permutations · Transposition of two atoms

Proof usesSubgroup of finitely supported permutations of atoms

Used bySymmetry of α-equivalence · Transitivity of α-equivalence · Swapping two fresh atoms fixes the element

TheoremConjugation of a transposition#✓fully proved

Conjugation of a transposition: σ * swap b c * σ⁻¹ = swap (σ b) (σ c).

theorem swap_conj (σ : FinPerm Atom) (b c : Atom) :
    σ * swap b c * σ⁻¹ = swap (σ • b) (σ • c)

Uses 3 · Used by 2

Statement usesGroup of finitely supported permutations · Subgroup of finitely supported permutations of atoms · Transposition of two atoms

Used byPermutation action on abstractions · Swapping two fresh atoms fixes the element

TheoremTransposition fixes atoms other than the swapped pair#✓fully proved

A transposition fixes every atom distinct from its two swapped atoms.

theorem swap_smul_of_ne_of_ne {a b c : Atom} (h1 : c ≠ a) (h2 : c ≠ b) :
    (swap a b : FinPerm Atom) • c = c

Uses 4 · Used by 6

Statement usesGroup of finitely supported permutations · Subgroup of finitely supported permutations of atoms · Transposition of two atoms

Proof usesAction of a transposition

Used byTransitivity of α-equivalence · Permutations moving only fresh atoms fix the element · Support of an atom abstraction · Support of an atom · Abstractions are supported by the body's support minus the atom · Transposition of atoms outside a support fixes the element

DefinitionSupporting set of atoms for an element#✓fully proved

S supports x when every finite permutation fixing S pointwise fixes x.

def Supports {X : Type*} [MulAction (FinPerm Atom) X] (S : Finset Atom) (x : X) : Prop :=
  ∀ π : FinPerm Atom, (∀ a ∈ S, π • a = a) → π • x = x

Uses 2 · Used by 20

Statement usesGroup of finitely supported permutations · Subgroup of finitely supported permutations of atoms

Used byExistence of fresh atoms · Existence of a least finite support · Freshness of an atom for an element · Freshness is non-membership in the least support · Permutation image of a support · Intersection of two supports is a support · Membership in the least support · Enlarging a support · Nominal set · A pair is supported by the union of its components' supports · Least finite support of an element · Support of an atom abstraction · Support of an atom · Equivariant elements have empty support · Equivariance of the least support · Minimality of the least support · Least support is a support · Equivariant elements are supported by the empty set · Swapping two fresh atoms fixes the element · Transposition of atoms outside a support fixes the element

TheoremEnlarging a support#✓fully proved

A support can be enlarged: fixing a larger set pointwise is a stronger hypothesis.

theorem Supports.mono {X : Type*} [MulAction (FinPerm Atom) X] {S T : Finset Atom}
    {x : X} (h : S ⊆ T) (hs : Supports S x) : Supports T x

Uses 3

Statement usesGroup of finitely supported permutations · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms

ClassNominal set#✓fully proved

A type with an action of finite permutations in which every element has a finite support: a nominal set.

class NominalSet (Atom : Type*) [DecidableEq Atom] (X : Type*) [MulAction (FinPerm Atom) X] : Prop where
  finiteSupport : ∀ x : X, ∃ S : Finset Atom, Supports S x

Uses 3 · Used by 22

Statement usesGroup of finitely supported permutations · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms

Used byAtom abstraction of a nominal set · Abstraction of an element at a bound atom · Equality of abstractions is α-equivalence · Abstractions with the same bound atom have equal bodies · Reflexivity of α-equivalence · Symmetry of α-equivalence · Transitivity of α-equivalence · Setoid of α-equivalence · Permutation action on abstractions · Existence of fresh atoms · Freshness is non-membership in the least support · Membership in the least support · Permutation action on abstractions computed on representatives · Permutations agreeing on the support act equally · Least finite support of an element · Support of an atom abstraction · Support of an atom · Equivariant elements have empty support · Equivariance of the least support · Minimality of the least support · Least support is a support · Abstractions are supported by the body's support minus the atom

TheoremA pair is supported by the union of its components' supports#✓fully proved

A pair is supported by the union of supports of its components.

theorem Supports.prod {X Y : Type*} [MulAction (FinPerm Atom) X]
    [MulAction (FinPerm Atom) Y] {S T : Finset Atom} {x : X} {y : Y}
    (hx : Supports S x) (hy : Supports T y) : Supports (S ∪ T) (x, y)

Uses 3

Statement usesGroup of finitely supported permutations · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms

DefinitionFreshness of an atom for an element#✓fully proved

a is fresh for x, written a # x in the nominal literature, when some finite support of x does not contain a.

def Fresh {X : Type*} [MulAction (FinPerm Atom) X] (a : Atom) (x : X) : Prop :=
  ∃ S : Finset Atom, Supports S x ∧ a ∉ S

Uses 3 · Used by 12

Statement usesGroup of finitely supported permutations · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms

Used byAbstractions with the same bound atom have equal bodies · α-equivalence relation on atom–element pairs · Reflexivity of α-equivalence · Symmetry of α-equivalence · Transitivity of α-equivalence · Permutation action on abstractions · Existence of fresh atoms · Freshness is non-membership in the least support · Intersection of two supports is a support · Permutations moving only fresh atoms fix the element · Abstractions are supported by the body's support minus the atom · Swapping two fresh atoms fixes the element

TheoremExistence of fresh atoms#✓fully proved

Every element has a fresh atom: choose one outside any of its supports.

theorem exists_fresh {X : Type*} [MulAction (FinPerm Atom) X] [NominalSet Atom X]
    (x : X) : ∃ a : Atom, Fresh a x

Uses 5

Statement usesGroup of finitely supported permutations · Freshness of an atom for an element · Nominal set · Subgroup of finitely supported permutations of atoms

Proof usesSupporting set of atoms for an element

TheoremTransposition of atoms outside a support fixes the element#✓fully proved

A transposition of two atoms both outside a support of x fixes x.

theorem swap_smul_of_supports_not_mem {X : Type*} [MulAction (FinPerm Atom) X]
    {S : Finset Atom} {x : X} (hS : Supports S x) {a b : Atom} (ha : a ∉ S)
    (hb : b ∉ S) : (swap a b : FinPerm Atom) • x = x

Uses 5 · Used by 1

Statement usesGroup of finitely supported permutations · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms · Transposition of two atoms

Proof usesTransposition fixes atoms other than the swapped pair

Used bySwapping two fresh atoms fixes the element

TheoremSwapping two fresh atoms fixes the element#✓fully proved

Swapping two fresh atoms fixes x. The proof uses a third atom c fresh for both witnessing supports, and the conjugation identity swap a b = swap a c * swap b c * swap a c.

theorem swap_smul_of_fresh_fresh {X : Type*} [MulAction (FinPerm Atom) X]
    {x : X} {a b : Atom} (ha : Fresh a x) (hb : Fresh b x) :
    (swap a b : FinPerm Atom) • x = x

Uses 11 · Used by 1

Statement usesGroup of finitely supported permutations · Freshness of an atom for an element · Subgroup of finitely supported permutations of atoms · Transposition of two atoms

Proof usesSupporting set of atoms for an element · Symmetry of transpositions · Conjugation of a transposition · A transposition is its own inverse · Transposition of an atom with itself is the identity · Action of a transposition · Transposition of atoms outside a support fixes the element

Used byPermutations moving only fresh atoms fix the element

TheoremPermutations moving only fresh atoms fix the element#✓fully proved

A permutation that fixes every atom outside a finite set F of fresh atoms fixes x, by induction on F. If π a = a we apply the induction hypothesis to π; otherwise we factor π = swap a b * π' with b = π a, where π' fixes a and has support inside F \ {a}, and swap a b fixes x since a and b are fresh.

theorem smul_eq_of_fresh {X : Type*} [MulAction (FinPerm Atom) X] {x : X}
    (F : Finset Atom) (hF : ∀ a ∈ F, Fresh a x) :
    ∀ π : FinPerm Atom, (∀ a ∉ F, π • a = a) → π • x = x

Uses 8 · Used by 1

Statement usesGroup of finitely supported permutations · Freshness of an atom for an element · Subgroup of finitely supported permutations of atoms

Proof usesTransposition of two atoms · A transposition squares to the identity · Action of a transposition · Swapping two fresh atoms fixes the element · Transposition fixes atoms other than the swapped pair

Used byIntersection of two supports is a support

TheoremIntersection of two supports is a support#✓fully proved

The intersection of two supports is a support: a permutation fixing the intersection fixes x, since every atom it can move (outside some finite support of the permutation, and outside the intersection) is fresh for x.

theorem Supports.inter {X : Type*} [MulAction (FinPerm Atom) X]
    {S₁ S₂ : Finset Atom} {x : X} (h₁ : Supports S₁ x) (h₂ : Supports S₂ x) :
    Supports (S₁ ∩ S₂) x

Uses 5 · Used by 1

Statement usesGroup of finitely supported permutations · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms

Proof usesFreshness of an atom for an element · Permutations moving only fresh atoms fix the element

Used byExistence of a least finite support

TheoremPermutation image of a support#✓fully proved

A permutation moves a support of x to a support of π • x.

theorem Supports.image {X : Type*} [MulAction (FinPerm Atom) X] {S : Finset Atom}
    {x : X} (hS : Supports S x) (π : FinPerm Atom) :
    Supports (S.image (π • ·)) (π • x)

Uses 3 · Used by 1

Statement usesGroup of finitely supported permutations · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms

Used byEquivariance of the least support

TheoremExistence of a least finite support#✓fully proved

A least finite support exists: among the supports of x, one is contained in every support. The proof is by strong induction on a chosen support S₀: either every element of S₀ lies in every support (so S₀ itself is least), or some a ∈ S₀ is missing from a support Sₐ, and the induction hypothesis applies to the strictly smaller support Sₐ ∩ S₀.

theorem exists_least_support {X : Type*} [MulAction (FinPerm Atom) X] (x : X)
    (S₀ : Finset Atom) (hS₀ : Supports S₀ x) :
    ∃ S : Finset Atom, Supports S x ∧ S ⊆ S₀ ∧
      ∀ T : Finset Atom, Supports T x → S ⊆ T

Uses 4 · Used by 3

Statement usesGroup of finitely supported permutations · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms

Proof usesIntersection of two supports is a support

Used byLeast finite support of an element · Minimality of the least support · Least support is a support

DefinitionLeast finite support of an element#✓fully proved

The least finite support of x: a support contained in every support of x.

noncomputable def supp {X : Type*} [MulAction (FinPerm Atom) X] [NominalSet Atom X]
    (x : X) : Finset Atom :=
  Classical.choose (exists_least_support x _
    (Classical.choose_spec (show ∃ S : Finset Atom, Supports S x from NominalSet.finiteSupport x)))

Uses 5 · Used by 13

Statement usesGroup of finitely supported permutations · Nominal set · Supporting set of atoms for an element · Existence of a least finite support · Subgroup of finitely supported permutations of atoms

Used bySymmetry of α-equivalence · Transitivity of α-equivalence · Permutation action on abstractions · Freshness is non-membership in the least support · Membership in the least support · Permutations agreeing on the support act equally · Support of an atom abstraction · Support of an atom · Equivariant elements have empty support · Equivariance of the least support · Minimality of the least support · Least support is a support · Abstractions are supported by the body's support minus the atom

TheoremLeast support is a support#✓fully proved

The least support is a support.

theorem supp_supports {X : Type*} [MulAction (FinPerm Atom) X] [NominalSet Atom X]
    (x : X) : Supports (supp (Atom := Atom) x) x

Uses 6 · Used by 4

Statement usesGroup of finitely supported permutations · Nominal set · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms · Least finite support of an element

Proof usesExistence of a least finite support

Used byMembership in the least support · Permutations agreeing on the support act equally · Equivariance of the least support · Abstractions are supported by the body's support minus the atom

TheoremMinimality of the least support#✓fully proved

The least support is contained in every support: minimality.

theorem supp_subset {X : Type*} [MulAction (FinPerm Atom) X] [NominalSet Atom X]
    (x : X) {S : Finset Atom} (hS : Supports S x) : supp (Atom := Atom) x ⊆ S

Uses 6 · Used by 6

Statement usesGroup of finitely supported permutations · Nominal set · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms · Least finite support of an element

Proof usesExistence of a least finite support

Used byFreshness is non-membership in the least support · Membership in the least support · Support of an atom abstraction · Support of an atom · Equivariant elements have empty support · Equivariance of the least support

TheoremMembership in the least support#✓fully proved

Membership in the least support: a ∈ supp (Atom := Atom) x iff a lies in every support of x.

theorem mem_supp_iff {X : Type*} [MulAction (FinPerm Atom) X] [NominalSet Atom X]
    (x : X) (a : Atom) : a ∈ supp (Atom := Atom) x ↔ ∀ S : Finset Atom, Supports S x → a ∈ S

Uses 7 · Used by 3

Statement usesGroup of finitely supported permutations · Nominal set · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms · Least finite support of an element

Proof usesMinimality of the least support · Least support is a support

Used byFreshness is non-membership in the least support · Support of an atom abstraction · Support of an atom

TheoremFreshness is non-membership in the least support#✓fully proved

Freshness is exactly non-membership in the least support.

theorem fresh_iff_not_mem_supp {X : Type*} [MulAction (FinPerm Atom) X]
    [NominalSet Atom X] (x : X) (a : Atom) : Fresh a x ↔ a ∉ supp (Atom := Atom) x

Uses 8 · Used by 4

Statement usesGroup of finitely supported permutations · Freshness of an atom for an element · Nominal set · Subgroup of finitely supported permutations of atoms · Least finite support of an element

Proof usesSupporting set of atoms for an element · Membership in the least support · Minimality of the least support

Used bySymmetry of α-equivalence · Transitivity of α-equivalence · Permutation action on abstractions · Abstractions are supported by the body's support minus the atom

TheoremEquivariance of the least support#✓fully proved

Support is equivariant: permuting x permutes its support.

theorem supp_smul {X : Type*} [MulAction (FinPerm Atom) X] [NominalSet Atom X]
    (x : X) (π : FinPerm Atom) :
    supp (Atom := Atom) (π • x) = (supp (Atom := Atom) x).image (π • ·)

Uses 8 · Used by 4

Statement usesGroup of finitely supported permutations · Nominal set · Subgroup of finitely supported permutations of atoms · Least finite support of an element

Proof usesSupporting set of atoms for an element · Permutation image of a support · Minimality of the least support · Least support is a support

Used bySymmetry of α-equivalence · Transitivity of α-equivalence · Permutation action on abstractions · Support of an atom abstraction

TheoremSupport of an atom#✓fully proved

The support of an atom is its singleton.

theorem supp_atom (a : Atom) : supp (Atom := Atom) (a : Atom) = {a}

Uses 10

Statement usesGroup of finitely supported permutations · Nominal set · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms · Least finite support of an element

Proof usesMembership in the least support · Minimality of the least support · Transposition of two atoms · Action of a transposition · Transposition fixes atoms other than the swapped pair

TheoremPermutations agreeing on the support act equally#✓fully proved

Two permutations that agree on the support of x act equally on x: their ratio fixes the support pointwise, hence fixes x.

theorem smul_eq_of_agree_on_supp {X : Type*} [MulAction (FinPerm Atom) X]
    [NominalSet Atom X] {x : X} {π σ : FinPerm Atom}
    (h : ∀ a ∈ supp (Atom := Atom) x, π • a = σ • a) : π • x = σ • x

Uses 5 · Used by 2

Statement usesGroup of finitely supported permutations · Nominal set · Subgroup of finitely supported permutations of atoms · Least finite support of an element

Proof usesLeast support is a support

Used byTransitivity of α-equivalence · Abstractions are supported by the body's support minus the atom

DefinitionEquivariant elements of a nominal set#✓fully proved

An element fixed by every permutation has the empty set as a support.

def IsEquivariant {X : Type*} [MulAction (FinPerm Atom) X] (x : X) : Prop :=
  ∀ π : FinPerm Atom, π • x = x

Uses 2 · Used by 2

Statement usesGroup of finitely supported permutations · Subgroup of finitely supported permutations of atoms

Used byEquivariant elements have empty support · Equivariant elements are supported by the empty set

TheoremEquivariant elements are supported by the empty set#✓fully proved

An equivariant element is supported by the empty set.

theorem supports_empty_of_equivariant {X : Type*} [MulAction (FinPerm Atom) X]
    {x : X} (h : IsEquivariant (Atom := Atom) x) : Supports (∅ : Finset Atom) x

Uses 4 · Used by 1

Statement usesGroup of finitely supported permutations · Equivariant elements of a nominal set · Supporting set of atoms for an element · Subgroup of finitely supported permutations of atoms

Used byEquivariant elements have empty support

TheoremEquivariant elements have empty support#✓fully proved

An equivariant element has empty support.

theorem supp_eq_empty_of_equivariant {X : Type*} [MulAction (FinPerm Atom) X]
    [NominalSet Atom X] {x : X} (h : IsEquivariant (Atom := Atom) x) : supp (Atom := Atom) x = (∅ : Finset Atom)

Uses 8

Statement usesGroup of finitely supported permutations · Equivariant elements of a nominal set · Nominal set · Subgroup of finitely supported permutations of atoms · Least finite support of an element

Proof usesSupporting set of atoms for an element · Minimality of the least support · Equivariant elements are supported by the empty set

Definitionα-equivalence relation on atom–element pairs#✓fully proved

α-equivalence relation on atom–element pairs. α-equivalence: equal pairs, or a renaming of the bound atom by a fresh transposition.

def AbsRel (a b : Atom) (x y : X) : Prop :=
  (a = b ∧ x = y) ∨
    (a ≠ b ∧ Fresh a y ∧ (swap a b : FinPerm Atom) • x = y)

Uses 4 · Used by 6

Statement usesGroup of finitely supported permutations · Freshness of an atom for an element · Subgroup of finitely supported permutations of atoms · Transposition of two atoms

Used byEquality of abstractions is α-equivalence · Abstractions with the same bound atom have equal bodies · Reflexivity of α-equivalence · Symmetry of α-equivalence · Transitivity of α-equivalence · Setoid of α-equivalence

TheoremReflexivity of α-equivalence#✓fully proved

Reflexivity of α-equivalence. α-equivalence is reflexive.

theorem absRel_refl (a : Atom) (x : X) : AbsRel a a x x

Uses 6 · Used by 1

Statement usesα-equivalence relation on atom–element pairs · Group of finitely supported permutations · Nominal set · Subgroup of finitely supported permutations of atoms

Proof usesFreshness of an atom for an element · Transposition of two atoms

Used bySetoid of α-equivalence

TheoremSymmetry of α-equivalence#✓fully proved

Symmetry of α-equivalence. α-equivalence is symmetric. Symmetry uses equivariance of support (supp_smul).

theorem absRel_symm {a b : Atom} {x y : X} (h : AbsRel a b x y) : AbsRel b a y x

Uses 12 · Used by 1

Statement usesα-equivalence relation on atom–element pairs · Group of finitely supported permutations · Nominal set · Subgroup of finitely supported permutations of atoms

Proof usesFreshness of an atom for an element · Freshness is non-membership in the least support · Least finite support of an element · Equivariance of the least support · Transposition of two atoms · Symmetry of transpositions · A transposition squares to the identity · Action of a transposition

Used bySetoid of α-equivalence

TheoremTransitivity of α-equivalence#✓fully proved

Transitivity of α-equivalence. α-equivalence is transitive. Transitivity uses the fact that two permutations agreeing on supp y act equally on y (smul_eq_of_agree_on_supp).

theorem absRel_trans {a b d : Atom} {x y z : X} (h₁ : AbsRel a b x y)
    (h₂ : AbsRel b d y z) : AbsRel a d x z

Uses 14 · Used by 1

Statement usesα-equivalence relation on atom–element pairs · Group of finitely supported permutations · Nominal set · Subgroup of finitely supported permutations of atoms

Proof usesFreshness of an atom for an element · Freshness is non-membership in the least support · Permutations agreeing on the support act equally · Least finite support of an element · Equivariance of the least support · Transposition of two atoms · Symmetry of transpositions · A transposition squares to the identity · Action of a transposition · Transposition fixes atoms other than the swapped pair

Used bySetoid of α-equivalence

DefinitionSetoid of α-equivalence#✓fully proved

The setoid of α-equivalence.

def absSetoid : Setoid (Atom × X) where
  r := fun p q => AbsRel p.1 q.1 p.2 q.2
  iseqv := ⟨fun p => absRel_refl p.1 p.2, fun h => absRel_symm h,
    fun h₁ h₂ => absRel_trans h₁ h₂⟩

Uses 7 · Used by 7

Statement usesα-equivalence relation on atom–element pairs · Group of finitely supported permutations · Nominal set · Reflexivity of α-equivalence · Symmetry of α-equivalence · Transitivity of α-equivalence · Subgroup of finitely supported permutations of atoms

Used byAtom abstraction of a nominal set · Abstraction of an element at a bound atom · Equality of abstractions is α-equivalence · Permutation action on abstractions · Permutation action on abstractions computed on representatives · Support of an atom abstraction · Abstractions are supported by the body's support minus the atom

DefinitionAtom abstraction of a nominal set#✓fully proved

Atom abstraction: [a]x, the quotient of Atom × X by α-equivalence.

def Abs (Atom : Type*) [Infinite Atom] [DecidableEq Atom] (X : Type*)
    [MulAction (FinPerm Atom) X] [NominalSet Atom X] : Type _ :=
  Quotient (@absSetoid Atom _ _ X _ _)

Uses 4 · Used by 7

Statement usesGroup of finitely supported permutations · Nominal set · Setoid of α-equivalence · Subgroup of finitely supported permutations of atoms

Used byAbstraction of an element at a bound atom · Equality of abstractions is α-equivalence · Abstractions with the same bound atom have equal bodies · Permutation action on abstractions · Permutation action on abstractions computed on representatives · Support of an atom abstraction · Abstractions are supported by the body's support minus the atom

DefinitionAbstraction of an element at a bound atom#✓fully proved

The abstraction [a]x.

def abs (a : Atom) (x : X) : Abs Atom X := Quotient.mk _ (a, x)

Uses 5 · Used by 5

Statement usesAtom abstraction of a nominal set · Group of finitely supported permutations · Nominal set · Setoid of α-equivalence · Subgroup of finitely supported permutations of atoms

Used byEquality of abstractions is α-equivalence · Abstractions with the same bound atom have equal bodies · Permutation action on abstractions computed on representatives · Support of an atom abstraction · Abstractions are supported by the body's support minus the atom

TheoremEquality of abstractions is α-equivalence#✓fully proved

Equality of abstractions is α-equivalence.

theorem abs_eq_iff {a b : Atom} {x y : X} :
    abs a x = abs b y ↔ AbsRel a b x y

Uses 7 · Used by 1

Statement usesAtom abstraction of a nominal set · α-equivalence relation on atom–element pairs · Group of finitely supported permutations · Nominal set · Abstraction of an element at a bound atom · Subgroup of finitely supported permutations of atoms

Proof usesSetoid of α-equivalence

Used byAbstractions with the same bound atom have equal bodies

TheoremAbstractions with the same bound atom have equal bodies#✓fully proved

An abstraction with the same bound atom determines its body.

theorem abs_eq_of_same_atom {a : Atom} {x y : X} (h : abs a x = abs a y) : x = y

Uses 9 · Used by 1

Statement usesAtom abstraction of a nominal set · Group of finitely supported permutations · Nominal set · Abstraction of an element at a bound atom · Subgroup of finitely supported permutations of atoms

Proof usesα-equivalence relation on atom–element pairs · Freshness of an atom for an element · Equality of abstractions is α-equivalence · Transposition of two atoms

Used bySupport of an atom abstraction

DefinitionPermutation action on abstractions#✓fully proved

The action of a permutation on abstractions, applied to a representative.

Cslib.Nominal.absSmul · 32 lines

def absSmul (π : FinPerm Atom) : Abs Atom X → Abs Atom X :=
  Quotient.lift (fun p : Atom × X => Quotient.mk _ (π • p.1, π • p.2)) (by
    intro p q h
    apply Quotient.sound
    rcases h with ⟨hab, hxy⟩ | ⟨hab, haf, hswap⟩
    · exact Or.inl ⟨congrArg (π • ·) hab, congrArg (π • ·) hxy⟩
    · refine Or.inr ⟨?_, ?_, ?_⟩
      · intro hEq
        exact hab ((MulAction.injective π) hEq)
      · -- `π • a` is fresh for `π • y`.
        have ha_not : p.1 ∉ supp (Atom := Atom) q.2 := by
          -- `p.1 = a`, `q.2 = y`: freshness of `a` for `y`.
          exact (fresh_iff_not_mem_supp (Atom := Atom) q.2 p.1).mp haf
        have hnot : (π • p.1) ∉ supp (Atom := Atom) (π • q.2) := by
          intro hmem
          rw [supp_smul] at hmem
          obtain ⟨c, hc, hEq⟩ := Finset.mem_image.mp hmem
          have hc_eq : c = p.1 := MulAction.injective π hEq
          exact ha_not (hc_eq ▸ hc)
        exact (fresh_iff_not_mem_supp (Atom := Atom) (π • q.2) (π • p.1)).mpr hnot
      · -- `swap (π•a) (π•b) • (π•x) = π•y` by conjugation.
        have hconj : (swap (π • p.1) (π • q.1) : FinPerm Atom) =
            π * swap p.1 q.1 * π⁻¹ := (swap_conj π p.1 q.1).symm
        show (swap (π • p.1) (π • q.1) : FinPerm Atom) • (π • p.2) = π • q.2
        calc (swap (π • p.1) (π • q.1) : FinPerm Atom) • (π • p.2)
            = (π * swap p.1 q.1 * π⁻¹) • (π • p.2) := by rw [hconj]
          _ = π • ((swap p.1 q.1) • (π⁻¹ • (π • p.2))) := by rw [mul_smul, mul_smul]
          _ = π • ((swap p.1 q.1) • p.2) := by
              have h_inv : π⁻¹ • (π • p.2) = p.2 := by
                rw [← mul_smul, inv_mul_cancel, one_smul]
              rw [h_inv]
          _ = π • q.2 := by rw [hswap])

Uses 11 · Used by 3

Statement usesAtom abstraction of a nominal set · Group of finitely supported permutations · Freshness of an atom for an element · Nominal set · Setoid of α-equivalence · Subgroup of finitely supported permutations of atoms · Freshness is non-membership in the least support · Least finite support of an element · Equivariance of the least support · Transposition of two atoms · Conjugation of a transposition

Used byPermutation action on abstractions computed on representatives · Support of an atom abstraction · Abstractions are supported by the body's support minus the atom

TheoremPermutation action on abstractions computed on representatives#✓fully proved

A permutation applied to an abstraction, on representatives.

theorem smul_abs (π : FinPerm Atom) (a : Atom) (x : X) :
    π • abs a x = abs (π • a) (π • x)

Uses 7 · Used by 2

Statement usesAtom abstraction of a nominal set · Group of finitely supported permutations · Nominal set · Abstraction of an element at a bound atom · Setoid of α-equivalence · Permutation action on abstractions · Subgroup of finitely supported permutations of atoms

Used bySupport of an atom abstraction · Abstractions are supported by the body's support minus the atom

TheoremAbstractions are supported by the body's support minus the atom#✓fully proved

The action of a permutation on an abstraction fixes it when the permutation fixes supp x \ {a} pointwise.

theorem supports_erase_abs {a : Atom} {x : X} (π : FinPerm Atom)
    (hπ : ∀ c ∈ (supp (Atom := Atom) x).erase a, π • c = c) :
    π • abs a x = abs a x

Uses 16 · Used by 1

Statement usesAtom abstraction of a nominal set · Group of finitely supported permutations · Nominal set · Abstraction of an element at a bound atom · Setoid of α-equivalence · Permutation action on abstractions · Subgroup of finitely supported permutations of atoms · Least finite support of an element

Proof usesFreshness of an atom for an element · Freshness is non-membership in the least support · Permutation action on abstractions computed on representatives · Permutations agreeing on the support act equally · Least support is a support · Transposition of two atoms · Action of a transposition · Transposition fixes atoms other than the swapped pair

Used bySupport of an atom abstraction

TheoremSupport of an atom abstraction#✓fully proved

The support of an abstraction is the body's support minus the bound atom.

theorem supp_abs (a : Atom) (x : X) :
    supp (Atom := Atom) (abs a x) = (supp (Atom := Atom) x).erase a

Uses 18

Statement usesAtom abstraction of a nominal set · Group of finitely supported permutations · Nominal set · Supporting set of atoms for an element · Abstraction of an element at a bound atom · Setoid of α-equivalence · Permutation action on abstractions · Subgroup of finitely supported permutations of atoms · Least finite support of an element · Abstractions are supported by the body's support minus the atom

Proof usesAbstractions with the same bound atom have equal bodies · Membership in the least support · Permutation action on abstractions computed on representatives · Equivariance of the least support · Minimality of the least support · Transposition of two atoms · Action of a transposition · Transposition fixes atoms other than the swapped pair

46 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.