Partial permutation

This files defines permutations on a set.

A partial permutation on α is a domain Set α and two functions α → α that map domain to domain and are inverse to each other on domain.

Main declarations

• PartialPerm α: The type of partial permutations on α.

structure PartialPerm (α : Type u_1) : Type u_1

A partial permutation of a subset domain of α. The (global) maps toFun : α → α and invFun : α → α map domain to itself, and are inverse to each other there. The values of toFun and invFun outside of domain are irrelevant.

• toFun : α → α
• invFun : α → α
• domain : Set α
• toFun_domain' : ∀ ⦃x : α⦄, x ∈ self.domain → self.toFun x ∈ self.domain
• invFun_domain' : ∀ ⦃x : α⦄, x ∈ self.domain → self.invFun x ∈ self.domain
• left_inv' : ∀ ⦃x : α⦄, x ∈ self.domain → self.invFun (self.toFun x) = x
• right_inv' : ∀ ⦃x : α⦄, x ∈ self.domain → self.toFun (self.invFun x) = x

theorem PartialPerm.toFun_domain' {α : Type u_1} (self : PartialPerm α) ⦃x : α⦄ : x ∈ self.domain → self.toFun x ∈ self.domain

theorem PartialPerm.invFun_domain' {α : Type u_1} (self : PartialPerm α) ⦃x : α⦄ : x ∈ self.domain → self.invFun x ∈ self.domain

theorem PartialPerm.left_inv' {α : Type u_1} (self : PartialPerm α) ⦃x : α⦄ : x ∈ self.domain → self.invFun (self.toFun x) = x

theorem PartialPerm.right_inv' {α : Type u_1} (self : PartialPerm α) ⦃x : α⦄ : x ∈ self.domain → self.toFun (self.invFun x) = x

def Equiv.Perm.toPartialPerm {α : Type u_1} (π : Equiv.Perm α) : PartialPerm α

A Perm gives rise to a PartialPerm defined on the entire type.

Equations

• π.toPartialPerm = { toFun := ⇑π, invFun := ⇑(Equiv.symm π), domain := Set.univ, toFun_domain' := ⋯, invFun_domain' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }

def PartialPerm.symm {α : Type u_1} (π : PartialPerm α) : PartialPerm α

The inverse of a partial permutation.

Equations

• π.symm = { toFun := π.invFun, invFun := π.toFun, domain := π.domain, toFun_domain' := ⋯, invFun_domain' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }

instance PartialPerm.instCoeFunForall {α : Type u_1} : CoeFun (PartialPerm α) fun (x : PartialPerm α) => α → α

Equations

• PartialPerm.instCoeFunForall = { coe := PartialPerm.toFun }

@[simp]

theorem PartialPerm.coe_mk {α : Type u_1} (f : α → α) (g : α → α) (s : Set α) (ml : ∀ ⦃x : α⦄, x ∈ s → f x ∈ s) (mr : ∀ ⦃x : α⦄, x ∈ s → g x ∈ s) (il : ∀ ⦃x : α⦄, x ∈ s → g (f x) = x) (ir : ∀ ⦃x : α⦄, x ∈ s → f (g x) = x) : { toFun := f, invFun := g, domain := s, toFun_domain' := ml, invFun_domain' := mr, left_inv' := il, right_inv' := ir }.toFun = f

@[simp]

theorem PartialPerm.coe_symm_mk {α : Type u_1} (f : α → α) (g : α → α) (s : Set α) (ml : ∀ ⦃x : α⦄, x ∈ s → f x ∈ s) (mr : ∀ ⦃x : α⦄, x ∈ s → g x ∈ s) (il : ∀ ⦃x : α⦄, x ∈ s → g (f x) = x) (ir : ∀ ⦃x : α⦄, x ∈ s → f (g x) = x) : { toFun := f, invFun := g, domain := s, toFun_domain' := ml, invFun_domain' := mr, left_inv' := il, right_inv' := ir }.symm.toFun = g

@[simp]

theorem PartialPerm.toFun_as_coe {α : Type u_1} (π : PartialPerm α) : π.toFun = π.toFun

@[simp]

theorem PartialPerm.invFun_as_coe {α : Type u_1} (π : PartialPerm α) : π.invFun = π.symm.toFun

@[simp]

theorem PartialPerm.map_domain {α : Type u_1} (π : PartialPerm α) {x : α} (h : x ∈ π.domain) : π.toFun x ∈ π.domain

@[simp]

theorem PartialPerm.iterate_domain {α : Type u_1} (π : PartialPerm α) {x : α} (h : x ∈ π.domain) {n : ℕ} : π.toFun^[n] x ∈ π.domain

@[simp]

theorem PartialPerm.left_inv {α : Type u_1} (π : PartialPerm α) {x : α} (h : x ∈ π.domain) : π.symm.toFun (π.toFun x) = x

@[simp]

theorem PartialPerm.right_inv {α : Type u_1} (π : PartialPerm α) {x : α} (h : x ∈ π.domain) : π.toFun (π.symm.toFun x) = x

@[simp]

theorem PartialPerm.symm_domain {α : Type u_1} (π : PartialPerm α) : π.symm.domain = π.domain

@[simp]

theorem PartialPerm.symm_symm {α : Type u_1} (π : PartialPerm α) : π.symm.symm = π

theorem PartialPerm.eq_symm_apply {α : Type u_1} (π : PartialPerm α) {x : α} {y : α} (hx : x ∈ π.domain) (hy : y ∈ π.domain) : x = π.symm.toFun y ↔ π.toFun x = y

theorem PartialPerm.mapsTo {α : Type u_1} (π : PartialPerm α) : Set.MapsTo π.toFun π.domain π.domain

theorem PartialPerm.leftInvOn {α : Type u_1} (π : PartialPerm α) : Set.LeftInvOn π.symm.toFun π.toFun π.domain

theorem PartialPerm.rightInvOn {α : Type u_1} (π : PartialPerm α) : Set.RightInvOn π.symm.toFun π.toFun π.domain

theorem PartialPerm.invOn {α : Type u_1} (π : PartialPerm α) : Set.InvOn π.symm.toFun π.toFun π.domain π.domain

theorem PartialPerm.injOn {α : Type u_1} (π : PartialPerm α) : Set.InjOn π.toFun π.domain

theorem PartialPerm.bijOn {α : Type u_1} (π : PartialPerm α) : Set.BijOn π.toFun π.domain π.domain

theorem PartialPerm.surjOn {α : Type u_1} (π : PartialPerm α) : Set.SurjOn π.toFun π.domain π.domain

@[simp]

theorem PartialPerm.copy_domain {α : Type u_1} (π : PartialPerm α) (f : α → α) (hf : π.toFun = f) (g : α → α) (hg : π.symm.toFun = g) (s : Set α) (hs : π.domain = s) : (π.copy f hf g hg s hs).domain = s

@[simp]

theorem PartialPerm.copy_toFun {α : Type u_1} (π : PartialPerm α) (f : α → α) (hf : π.toFun = f) (g : α → α) (hg : π.symm.toFun = g) (s : Set α) (hs : π.domain = s) : (π.copy f hf g hg s hs).toFun = f

@[simp]

theorem PartialPerm.copy_invFun {α : Type u_1} (π : PartialPerm α) (f : α → α) (hf : π.toFun = f) (g : α → α) (hg : π.symm.toFun = g) (s : Set α) (hs : π.domain = s) : (π.copy f hf g hg s hs).invFun = g

def PartialPerm.copy {α : Type u_1} (π : PartialPerm α) (f : α → α) (hf : π.toFun = f) (g : α → α) (hg : π.symm.toFun = g) (s : Set α) (hs : π.domain = s) : PartialPerm α

Create a copy of a PartialPerm providing better definitional equalities.

Equations

• π.copy f hf g hg s hs = { toFun := f, invFun := g, domain := s, toFun_domain' := ⋯, invFun_domain' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }

theorem PartialPerm.copy_eq {α : Type u_1} (π : PartialPerm α) (f : α → α) (hf : π.toFun = f) (g : α → α) (hg : π.symm.toFun = g) (s : Set α) (hs : π.domain = s) : π.copy f hf g hg s hs = π

def PartialPerm.toPerm {α : Type u_1} (π : PartialPerm α) : Equiv.Perm ↑π.domain

Associating to a partial_perm a permutation of the domain.

Equations

• π.toPerm = { toFun := fun (x : ↑π.domain) => ⟨π.toFun ↑x, ⋯⟩, invFun := fun (y : ↑π.domain) => ⟨π.symm.toFun ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PartialPerm.image_domain {α : Type u_1} (π : PartialPerm α) : π.toFun '' π.domain = π.domain

theorem PartialPerm.forall_mem_domain {α : Type u_1} (π : PartialPerm α) {p : α → Prop} : (∀ y ∈ π.domain, p y) ↔ ∀ x ∈ π.domain, p (π.toFun x)

theorem PartialPerm.exists_mem_domain {α : Type u_1} (π : PartialPerm α) {p : α → Prop} : (∃ y ∈ π.domain, p y) ↔ ∃ x ∈ π.domain, p (π.toFun x)

def PartialPerm.IsStable {α : Type u_1} (π : PartialPerm α) (s : Set α) : Prop

A set s is stable under a partial equivalence π if it preserved by it.

Equations

• π.IsStable s = ∀ ⦃x : α⦄, x ∈ π.domain → (π.toFun x ∈ s ↔ x ∈ s)

theorem PartialPerm.IsStable.apply_mem_iff {α : Type u_1} {π : PartialPerm α} {s : Set α} {x : α} (h : π.IsStable s) (hx : x ∈ π.domain) : π.toFun x ∈ s ↔ x ∈ s

theorem PartialPerm.IsStable.symm_apply_mem_iff {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) ⦃y : α⦄ : y ∈ π.domain → (π.symm.toFun y ∈ s ↔ y ∈ s)

theorem PartialPerm.IsStable.symm {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : π.symm.IsStable s

@[simp]

theorem PartialPerm.IsStable.symm_iff {α : Type u_1} {π : PartialPerm α} {s : Set α} : π.symm.IsStable s ↔ π.IsStable s

theorem PartialPerm.IsStable.mapsTo {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : Set.MapsTo π.toFun (π.domain ∩ s) (π.domain ∩ s)

theorem PartialPerm.IsStable.symm_mapsTo {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : Set.MapsTo π.symm.toFun (π.domain ∩ s) (π.domain ∩ s)

@[simp]

theorem PartialPerm.IsStable.restr_toFun {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : h.restr.toFun = π.toFun

@[simp]

theorem PartialPerm.IsStable.restr_invFun {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : h.restr.invFun = π.symm.toFun

@[simp]

theorem PartialPerm.IsStable.restr_domain {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : h.restr.domain = π.domain ∩ s

def PartialPerm.IsStable.restr {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : PartialPerm α

Restrict a PartialPerm to a stable subset.

Equations

• h.restr = { toFun := π.toFun, invFun := π.symm.toFun, domain := π.domain ∩ s, toFun_domain' := ⋯, invFun_domain' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }

theorem PartialPerm.IsStable.image_eq {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : π.toFun '' (π.domain ∩ s) = π.domain ∩ s

theorem PartialPerm.IsStable.symm_image_eq {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : π.symm.toFun '' (π.domain ∩ s) = π.domain ∩ s

theorem PartialPerm.IsStable.iff_preimage_eq {α : Type u_1} {π : PartialPerm α} {s : Set α} : π.IsStable s ↔ π.domain ∩ π.toFun ⁻¹' s = π.domain ∩ s

theorem PartialPerm.IsStable.of_preimage_eq {α : Type u_1} {π : PartialPerm α} {s : Set α} : π.domain ∩ π.toFun ⁻¹' s = π.domain ∩ s → π.IsStable s

Alias of the reverse direction of PartialPerm.IsStable.iff_preimage_eq.

theorem PartialPerm.IsStable.preimage_eq {α : Type u_1} {π : PartialPerm α} {s : Set α} : π.IsStable s → π.domain ∩ π.toFun ⁻¹' s = π.domain ∩ s

Alias of the forward direction of PartialPerm.IsStable.iff_preimage_eq.

theorem PartialPerm.IsStable.iff_symm_preimage_eq {α : Type u_1} {π : PartialPerm α} {s : Set α} : π.IsStable s ↔ π.domain ∩ π.symm.toFun ⁻¹' s = π.domain ∩ s

theorem PartialPerm.IsStable.symm_preimage_eq {α : Type u_1} {π : PartialPerm α} {s : Set α} : π.IsStable s → π.domain ∩ π.symm.toFun ⁻¹' s = π.domain ∩ s

Alias of the forward direction of PartialPerm.IsStable.iff_symm_preimage_eq.

theorem PartialPerm.IsStable.of_symm_preimage_eq {α : Type u_1} {π : PartialPerm α} {s : Set α} : π.domain ∩ π.symm.toFun ⁻¹' s = π.domain ∩ s → π.IsStable s

Alias of the reverse direction of PartialPerm.IsStable.iff_symm_preimage_eq.

theorem PartialPerm.IsStable.compl {α : Type u_1} {π : PartialPerm α} {s : Set α} (h : π.IsStable s) : π.IsStable sᶜ

theorem PartialPerm.IsStable.inter {α : Type u_1} {π : PartialPerm α} {s : Set α} {s' : Set α} (h : π.IsStable s) (h' : π.IsStable s') : π.IsStable (s ∩ s')

theorem PartialPerm.IsStable.union {α : Type u_1} {π : PartialPerm α} {s : Set α} {s' : Set α} (h : π.IsStable s) (h' : π.IsStable s') : π.IsStable (s ∪ s')

theorem PartialPerm.IsStable.diff {α : Type u_1} {π : PartialPerm α} {s : Set α} {s' : Set α} (h : π.IsStable s) (h' : π.IsStable s') : π.IsStable (s \ s')

theorem PartialPerm.IsStable.leftInvOn_piecewise {α : Type u_1} {π : PartialPerm α} {s : Set α} {π' : PartialPerm α} [(i : α) → Decidable (i ∈ s)] (h : π.IsStable s) (h' : π'.IsStable s) : Set.LeftInvOn (s.piecewise π.symm.toFun π'.symm.toFun) (s.piecewise π.toFun π'.toFun) (s.ite π.domain π'.domain)

theorem PartialPerm.IsStable.inter_eq_of_inter_eq_of_eqOn {α : Type u_1} {π : PartialPerm α} {s : Set α} {π' : PartialPerm α} (h : π.IsStable s) (h' : π'.IsStable s) (hs : π.domain ∩ s = π'.domain ∩ s) (Heq : Set.EqOn π.toFun π'.toFun (π.domain ∩ s)) : π.domain ∩ s = π'.domain ∩ s

theorem PartialPerm.IsStable.symm_eqOn_of_inter_eq_of_eqOn {α : Type u_1} {π : PartialPerm α} {s : Set α} {π' : PartialPerm α} (h : π.IsStable s) (hs : π.domain ∩ s = π'.domain ∩ s) (Heq : Set.EqOn π.toFun π'.toFun (π.domain ∩ s)) : Set.EqOn π.symm.toFun π'.symm.toFun (π.domain ∩ s)

theorem PartialPerm.image_domain_inter_eq' {α : Type u_1} (π : PartialPerm α) (s : Set α) : π.toFun '' (π.domain ∩ s) = π.domain ∩ π.symm.toFun ⁻¹' s

theorem PartialPerm.image_domain_inter_eq {α : Type u_1} (π : PartialPerm α) (s : Set α) : π.toFun '' (π.domain ∩ s) = π.domain ∩ π.symm.toFun ⁻¹' (π.domain ∩ s)

theorem PartialPerm.image_eq_domain_inter_inv_preimage {α : Type u_1} (π : PartialPerm α) {s : Set α} (h : s ⊆ π.domain) : π.toFun '' s = π.domain ∩ π.symm.toFun ⁻¹' s

theorem PartialPerm.symm_image_eq_domain_inter_preimage {α : Type u_1} (π : PartialPerm α) {s : Set α} (h : s ⊆ π.domain) : π.symm.toFun '' s = π.domain ∩ π.toFun ⁻¹' s

theorem PartialPerm.symm_image_domain_inter_eq {α : Type u_1} (π : PartialPerm α) (s : Set α) : π.symm.toFun '' (π.domain ∩ s) = π.domain ∩ π.toFun ⁻¹' (π.domain ∩ s)

theorem PartialPerm.symm_image_domain_inter_eq' {α : Type u_1} (π : PartialPerm α) (s : Set α) : π.symm.toFun '' (π.domain ∩ s) = π.domain ∩ π.toFun ⁻¹' s

theorem PartialPerm.domain_inter_preimage_inv_preimage {α : Type u_1} (π : PartialPerm α) (s : Set α) : π.domain ∩ π.toFun ⁻¹' (π.symm.toFun ⁻¹' s) = π.domain ∩ s

theorem PartialPerm.domain_inter_preimage_domain_inter {α : Type u_1} (π : PartialPerm α) (s : Set α) : π.domain ∩ π.toFun ⁻¹' (π.domain ∩ s) = π.domain ∩ π.toFun ⁻¹' s

theorem PartialPerm.domain_inter_inv_preimage_preimage {α : Type u_1} (π : PartialPerm α) (s : Set α) : π.domain ∩ π.symm.toFun ⁻¹' (π.toFun ⁻¹' s) = π.domain ∩ s

theorem PartialPerm.symm_image_image_of_subset_domain {α : Type u_1} (π : PartialPerm α) {s : Set α} (h : s ⊆ π.domain) : π.symm.toFun '' (π.toFun '' s) = s

theorem PartialPerm.image_symm_image_of_subset_domain {α : Type u_1} (π : PartialPerm α) {s : Set α} (h : s ⊆ π.domain) : π.toFun '' (π.symm.toFun '' s) = s

theorem PartialPerm.domain_subset_preimage_domain {α : Type u_1} {π : PartialPerm α} : π.domain ⊆ π.toFun ⁻¹' π.domain

theorem PartialPerm.symm_image_domain {α : Type u_1} {π : PartialPerm α} : π.symm.toFun '' π.domain = π.domain

theorem PartialPerm.ext {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : ∀ (x : α), π.toFun x = π'.toFun x) (hsymm : ∀ (x : α), π.symm.toFun x = π'.symm.toFun x) (hs : π.domain = π'.domain) : π = π'

Two partial permutations that have the same domain, same toFun and same invFun, coincide.

def PartialPerm.refl (α : Type u_1) : PartialPerm α

The identity partial permutation.

Equations

• PartialPerm.refl α = Equiv.Perm.toPartialPerm (Equiv.refl α)

@[simp]

theorem PartialPerm.refl_domain {α : Type u_1} : (PartialPerm.refl α).domain = Set.univ

@[simp]

theorem PartialPerm.coe_refl {α : Type u_1} : (PartialPerm.refl α).toFun = id

@[simp]

theorem PartialPerm.symm_refl {α : Type u_1} : (PartialPerm.refl α).symm = PartialPerm.refl α

instance PartialPerm.instInhabited {α : Type u_1} : Inhabited (PartialPerm α)

Equations

• PartialPerm.instInhabited = { default := PartialPerm.refl α }

@[simp]

theorem PartialPerm.trans_domain {α : Type u_1} (π : PartialPerm α) (π' : PartialPerm α) (h : π.domain = π'.domain) : (π.trans π' h).domain = π.domain

@[simp]

theorem PartialPerm.trans_invFun {α : Type u_1} (π : PartialPerm α) (π' : PartialPerm α) (h : π.domain = π'.domain) : ∀ (a : α), (π.trans π' h).invFun a = (π.symm.toFun ∘ π'.symm.toFun) a

@[simp]

theorem PartialPerm.trans_toFun {α : Type u_1} (π : PartialPerm α) (π' : PartialPerm α) (h : π.domain = π'.domain) : ∀ (a : α), (π.trans π' h).toFun a = (π'.toFun ∘ π.toFun) a

def PartialPerm.trans {α : Type u_1} (π : PartialPerm α) (π' : PartialPerm α) (h : π.domain = π'.domain) : PartialPerm α

Composing two partial permutations if the domain of the first coincides with the domain of the second.

Equations

• π.trans π' h = { toFun := π'.toFun ∘ π.toFun, invFun := π.symm.toFun ∘ π'.symm.toFun, domain := π.domain, toFun_domain' := ⋯, invFun_domain' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }

def PartialPerm.ofSet {α : Type u_1} (s : Set α) : PartialPerm α

The identity partial PERMUTATION on a set s

Equations

• PartialPerm.ofSet s = { toFun := id, invFun := id, domain := s, toFun_domain' := ⋯, invFun_domain' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }

@[simp]

theorem PartialPerm.ofSet_domain {α : Type u_1} (s : Set α) : (PartialPerm.ofSet s).domain = s

@[simp]

theorem PartialPerm.coe_ofSet {α : Type u_1} (s : Set α) : (PartialPerm.ofSet s).toFun = id

@[simp]

theorem PartialPerm.ofSet_symm {α : Type u_1} (s : Set α) : (PartialPerm.ofSet s).symm = PartialPerm.ofSet s

@[simp]

theorem PartialPerm.ofSet_trans_ofSet {α : Type u_1} (s : Set α) : (PartialPerm.ofSet s).trans (PartialPerm.ofSet s) ⋯ = PartialPerm.ofSet s

@[simp]

theorem PartialPerm.ofSet_univ {α : Type u_1} : PartialPerm.ofSet Set.univ = PartialPerm.refl α

def PartialPerm.toPartialEquiv {α : Type u_1} (π : PartialPerm α) : PartialEquiv α α

Reinterpret a partial permutation as a partial equivalence.

Equations

• π.toPartialEquiv = { toFun := π.toFun, invFun := π.symm.toFun, source := π.domain, target := π.domain, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }

@[simp]

theorem PartialPerm.coe_toPartialEquiv {α : Type u_1} (π : PartialPerm α) : ↑π.toPartialEquiv = π.toFun

@[simp]

theorem PartialPerm.coe_toPartialEquiv_symm {α : Type u_1} (π : PartialPerm α) : ↑π.toPartialEquiv.symm = π.symm.toFun

@[simp]

theorem PartialPerm.toPartialEquiv_source {α : Type u_1} (π : PartialPerm α) : π.toPartialEquiv.source = π.domain

@[simp]

theorem PartialPerm.toPartialEquiv_target {α : Type u_1} (π : PartialPerm α) : π.toPartialEquiv.target = π.domain

@[simp]

theorem PartialPerm.toPartialEquiv_refl {α : Type u_1} : (PartialPerm.refl α).toPartialEquiv = PartialEquiv.refl α

@[simp]

theorem PartialPerm.toPartialEquiv_symm {α : Type u_1} (π : PartialPerm α) : π.symm.toPartialEquiv = π.toPartialEquiv.symm

@[simp]

theorem PartialPerm.toPartialEquiv_trans {α : Type u_1} (π : PartialPerm α) (π' : PartialPerm α) (h : π.domain = π'.domain) : (π.trans π' h).toPartialEquiv = π.toPartialEquiv.trans π'.toPartialEquiv

def PartialPerm.EqOnDomain {α : Type u_1} (π : PartialPerm α) (π' : PartialPerm α) : Prop

EqOnDomain π π' means that π and π' have the same domain, and coincide there. Then π and π' should really be considered the same partial permutation.

Equations

• π.EqOnDomain π' = (π.domain = π'.domain ∧ Set.EqOn π.toFun π'.toFun π.domain)

instance PartialPerm.eqOnDomainSetoid {α : Type u_1} : Setoid (PartialPerm α)

eq_on_domain is an equivalence relation

Equations

• PartialPerm.eqOnDomainSetoid = { r := PartialPerm.EqOnDomain, iseqv := ⋯ }

theorem PartialPerm.eq_on_domain_refl {α : Type u_1} {π : PartialPerm α} : π ≈ π

theorem PartialPerm.EqOnDomain.domain_eq {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≈ π') : π.domain = π'.domain

Two equivalent partial permutations have the same domain

theorem PartialPerm.EqOnDomain.symm_domain_eq {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≈ π') : π.symm.domain = π'.symm.domain

theorem PartialPerm.EqOnDomain.eqOn {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≈ π') : Set.EqOn π.toFun π'.toFun π.domain

Two equivalent partial permutations coincide on the domain

theorem PartialPerm.EqOnDomain.symm' {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≈ π') : π.symm ≈ π'.symm

If two partial permutations are equivalent, so are their inverses.

theorem PartialPerm.EqOnDomain.symm_eqOn {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≈ π') : Set.EqOn π.symm.toFun π'.symm.toFun π.domain

Two equivalent partial permutations have coinciding inverses on the domain

theorem PartialPerm.EqOnDomain.domain_inter_preimage_eq {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (hπ : π ≈ π') (s : Set α) : π.domain ∩ π.toFun ⁻¹' s = π'.domain ∩ π'.toFun ⁻¹' s

Preimages are respected by equivalence.

theorem PartialPerm.EqOnDomain.eq {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≈ π') (hπ : π.domain = Set.univ) : π = π'

Two equivalent partial permutations are equal when the domain and domain are univ.

instance PartialPerm.instPreorder {α : Type u_1} : Preorder (PartialPerm α)

We define a preorder on partial permutations by saying π ≤ π' if the domain of π is contained in the domain of π', and the permutations agree on the domain of π.

Equations

• PartialPerm.instPreorder = Preorder.mk ⋯ ⋯ ⋯

theorem PartialPerm.domain_mono {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≤ π') : π.domain ⊆ π'.domain

theorem PartialPerm.eqOn_domain_of_le {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≤ π') : Set.EqOn π.toFun π'.toFun π.domain

theorem PartialPerm.le_of_eq_on_domain {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≈ π') : π ≤ π'

theorem PartialPerm.apply_eq_of_le {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} (h : π ≤ π') {x : α} (hx : x ∈ π.domain) : π'.toFun x = π.toFun x

def PartialPerm.piecewise {α : Type u_1} (π : PartialPerm α) (π' : PartialPerm α) [(j : α) → Decidable (j ∈ π.domain)] (h : Disjoint π.domain π'.domain) : PartialPerm α

Construct a partial permutation from two partial permutations with disjoint domains.

Equations

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

@[simp]

theorem PartialPerm.piecewise_domain {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} [(j : α) → Decidable (j ∈ π.domain)] {h : Disjoint π.domain π'.domain} : (π.piecewise π' h).domain = π.domain ∪ π'.domain

theorem PartialPerm.mem_piecewise_domain_left {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} [(j : α) → Decidable (j ∈ π.domain)] {h : Disjoint π.domain π'.domain} {x : α} (hx : x ∈ π.domain) : x ∈ (π.piecewise π' h).domain

theorem PartialPerm.mem_piecewise_domain_right {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} [(j : α) → Decidable (j ∈ π.domain)] {h : Disjoint π.domain π'.domain} {x : α} (hx : x ∈ π'.domain) : x ∈ (π.piecewise π' h).domain

theorem PartialPerm.piecewise_apply_eq_left {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} [(j : α) → Decidable (j ∈ π.domain)] {h : Disjoint π.domain π'.domain} {x : α} (hx : x ∈ π.domain) : (π.piecewise π' h).toFun x = π.toFun x

theorem PartialPerm.piecewise_apply_eq_right {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} [(j : α) → Decidable (j ∈ π.domain)] {h : Disjoint π.domain π'.domain} {x : α} (hx : x ∈ π'.domain) : (π.piecewise π' h).toFun x = π'.toFun x

theorem PartialPerm.le_piecewise_left {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} [(j : α) → Decidable (j ∈ π.domain)] {h : Disjoint π.domain π'.domain} : π ≤ π.piecewise π' h

theorem PartialPerm.le_piecewise_right {α : Type u_1} {π : PartialPerm α} {π' : PartialPerm α} [(j : α) → Decidable (j ∈ π.domain)] {h : Disjoint π.domain π'.domain} : π' ≤ π.piecewise π' h

@[simp]

theorem Set.BijOn.toPartialPerm_invFun {α : Type u_1} [Nonempty α] (f : α → α) (s : Set α) (hf : Set.BijOn f s s) : (Set.BijOn.toPartialPerm f s hf).invFun = Function.invFunOn f s

@[simp]

theorem Set.BijOn.toPartialPerm_domain {α : Type u_1} [Nonempty α] (f : α → α) (s : Set α) (hf : Set.BijOn f s s) : (Set.BijOn.toPartialPerm f s hf).domain = s

@[simp]

theorem Set.BijOn.toPartialPerm_toFun {α : Type u_1} [Nonempty α] (f : α → α) (s : Set α) (hf : Set.BijOn f s s) : (Set.BijOn.toPartialPerm f s hf).toFun = f

noncomputable def Set.BijOn.toPartialPerm {α : Type u_1} [Nonempty α] (f : α → α) (s : Set α) (hf : Set.BijOn f s s) : PartialPerm α

A bijection between two sets s : Set α and t : Set α provides a partial permutation on α.

Equations

• Set.BijOn.toPartialPerm f s hf = { toFun := f, invFun := Function.invFunOn f s, domain := s, toFun_domain' := ⋯, invFun_domain' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }

Perm.toPartialPerm

A Perm can be be interpreted as a PartialPerm. We set up simp lemmas to reduce most properties of the PartialPerm to that of the Perm.

@[simp]

theorem Equiv.Perm.toPartialPerm_one {α : Type u_1} : Equiv.Perm.toPartialPerm (Equiv.refl α) = PartialPerm.refl α

@[simp]

theorem Equiv.Perm.toPartialPerm_inv {α : Type u_1} (π : Equiv.Perm α) : π⁻¹.toPartialPerm = π.toPartialPerm.symm

@[simp]

theorem Equiv.Perm.toPartialPerm_mul {α : Type u_1} (π : Equiv.Perm α) (π' : Equiv.Perm α) : (π * π').toPartialPerm = π'.toPartialPerm.trans π.toPartialPerm ⋯

@[simp]

theorem Equiv.Perm.toPartialEquiv_toPartialPerm {α : Type u_1} (π : Equiv.Perm α) : π.toPartialPerm.toPartialEquiv = Equiv.toPartialEquiv π