Finitely-Supported Renamings

This file defines finitely-supported renamings and related operations. A finitely-supported renaming on 𝔸 is a function σ : 𝔸 → 𝔸 such that σ a ≠ a for only finitely many a : 𝔸.

structure RenamingSets.Ren (𝔸 : Type u_1) : Type u_1

The type of finitely supported renamings.

• toFun : 𝔸 → 𝔸

  The underlying function.

• exists_support' : ∃ (A : Finset 𝔸), ∀ a ∉ A, self.toFun a = a

  The underlying function is the identity everywhere except for finitely many elements.

instance RenamingSets.Ren.instFunLike {𝔸 : Type u_1} : FunLike (Ren 𝔸) 𝔸 𝔸

Equations

• RenamingSets.Ren.instFunLike = { coe := RenamingSets.Ren.toFun, coe_injective' := ⋯ }

def RenamingSets.Ren.Simps.coe {𝔸 : Type u_1} (f : Ren 𝔸) : 𝔸 → 𝔸

A simps projection for function coercion.

Equations

• RenamingSets.Ren.Simps.coe f = ⇑f

instance RenamingSets.Ren.instOne {𝔸 : Type u_1} : One (Ren 𝔸)

Equations

• RenamingSets.Ren.instOne = { one := { toFun := fun (a : 𝔸) => a, exists_support' := ⋯ } }

@[simp]

theorem RenamingSets.Ren.one_coe {𝔸 : Type u_1} (a : 𝔸) : 1 a = a

instance RenamingSets.Ren.instMul {𝔸 : Type u_1} : Mul (Ren 𝔸)

Equations

• RenamingSets.Ren.instMul = { mul := fun (ρ₁ ρ₂ : RenamingSets.Ren 𝔸) => { toFun := fun (a : 𝔸) => ρ₁ (ρ₂ a), exists_support' := ⋯ } }

@[simp]

theorem RenamingSets.Ren.mul_coe {𝔸 : Type u_1} (ρ₁ ρ₂ : Ren 𝔸) (a : 𝔸) : (ρ₁ * ρ₂) a = ρ₁ (ρ₂ a)

def RenamingSets.Ren.restrict {𝔸 : Type u_1} [DecidableEq 𝔸] (A : Finset 𝔸) (f : 𝔸 → 𝔸) : Ren 𝔸

Constructs a renaming by restricting a function to a finite set.

Equations

• RenamingSets.Ren.restrict A f = { toFun := fun (a : 𝔸) => if a ∈ A then f a else a, exists_support' := ⋯ }

@[simp]

theorem RenamingSets.Ren.restrict_coe {𝔸 : Type u_1} [DecidableEq 𝔸] (A : Finset 𝔸) (f : 𝔸 → 𝔸) (a : 𝔸) : (restrict A f) a = if a ∈ A then f a else a

@[reducible, inline]

abbrev RenamingSets.Ren.assign {𝔸 : Type u_1} [DecidableEq 𝔸] (a b : 𝔸) : Ren 𝔸

assign a b is the renaming which re-assigns b to a.

Equations

• RenamingSets.Ren.assign a b = RenamingSets.Ren.restrict {a} fun (x : 𝔸) => b

def RenamingSets.Ren.swap {𝔸 : Type u_1} [DecidableEq 𝔸] (a b : 𝔸) : Ren 𝔸

The renaming which swaps two variables.

Equations

• RenamingSets.Ren.swap a b = { toFun := fun (c : 𝔸) => if c = a then b else if c = b then a else c, exists_support' := ⋯ }

@[simp]

theorem RenamingSets.Ren.swap_coe {𝔸 : Type u_1} [DecidableEq 𝔸] (a b c : 𝔸) : (swap a b) c = if c = a then b else if c = b then a else c

noncomputable def RenamingSets.Ren.supp {𝔸 : Type u_1} (ρ : Ren 𝔸) : Finset 𝔸

The support of a renaming ρ is the set of all elements on which ρ is not the identity.

Equations

• ρ.supp = {a ∈ ⋯.choose | ρ a ≠ a}