Finitely-Supported Renamings

This file provides basic lemmas about finitely-supported renamings.

@[simp]

theorem RenamingSets.Ren.mk_coe {𝔸 : Type u_1} (σ : 𝔸 → 𝔸) (hσ : ∃ (A : Finset 𝔸), ∀ a ∉ A, σ a = a) : ⇑{ toFun := σ, exists_support' := hσ } = σ

@[simp]

theorem RenamingSets.Ren.coe_mk {𝔸 : Type u_1} (σ : Ren 𝔸) : { toFun := ⇑σ, exists_support' := ⋯ } = σ

theorem RenamingSets.Ren.exists_support {𝔸 : Type u_1} (ρ : Ren 𝔸) : ∃ (A : Finset 𝔸), ∀ a ∉ A, ρ a = a

theorem RenamingSets.Ren.ext {𝔸 : Type u_1} {ρ₁ ρ₂ : Ren 𝔸} (h : ∀ (a : 𝔸), ρ₁ a = ρ₂ a) : ρ₁ = ρ₂

theorem RenamingSets.Ren.ext_iff {𝔸 : Type u_1} {ρ₁ ρ₂ : Ren 𝔸} : ρ₁ = ρ₂ ↔ ∀ (a : 𝔸), ρ₁ a = ρ₂ a

instance RenamingSets.Ren.instMonoid {𝔸 : Type u_1} : Monoid (Ren 𝔸)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RenamingSets.Ren.mem_supp {𝔸 : Type u_1} (a : 𝔸) (ρ : Ren 𝔸) : a ∈ ρ.supp ↔ ρ a ≠ a

@[simp]

theorem RenamingSets.Ren.swap_swap {𝔸 : Type u_1} [DecidableEq 𝔸] (a b : 𝔸) : swap a b * swap a b = 1

@[simp]

theorem RenamingSets.Ren.swap_swap_r {𝔸 : Type u_1} [DecidableEq 𝔸] (a b : 𝔸) (σ : Ren 𝔸) : swap a b * (swap a b * σ) = σ