structure RenamingSets.PartialHom {𝔸 : Type u_3} [DecidableEq 𝔸] (A : Finset 𝔸) (X : Type u_1) [RenameAction 𝔸 X] [RenamingSet 𝔸 X] (Y : Type u_2) [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] : Type (max u_1 u_2)

PartialHom A X Y is the type of partial morphisms which are defined everywhere except for those elements whose support intersects A.

• toFun : { x : X // supp 𝔸 x ∩ A = ∅ } → Y

  The underlying function.

• supported' ⦃σ : Ren 𝔸⦄ : (∀ a ∈ A, σ a = a) → ∀ ⦃x : X⦄ (hx₁ : supp 𝔸 x ∩ A = ∅) (hx₂ : supp 𝔸 (RenamingSets.rename σ x) ∩ A = ∅), RenamingSets.rename σ (self.toFun ⟨x, hx₁⟩) = self.toFun ⟨RenamingSets.rename σ x, hx₂⟩

  The function has a finite support.

instance RenamingSets.PartialHom.instFunLikeSubtypeEqFinsetInterSuppEmptyCollection {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] {A : Finset 𝔸} : FunLike (PartialHom A X Y) { x : X // supp 𝔸 x ∩ A = ∅ } Y

Equations

• RenamingSets.PartialHom.instFunLikeSubtypeEqFinsetInterSuppEmptyCollection = { coe := RenamingSets.PartialHom.toFun, coe_injective' := ⋯ }

theorem RenamingSets.PartialHom.supported {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] {A : Finset 𝔸} (f : PartialHom A X Y) ⦃σ : Ren 𝔸⦄ : (∀ a ∈ A, σ a = a) → ∀ ⦃x : X⦄ (hx₁ : supp 𝔸 x ∩ A = ∅) (hx₂ : supp 𝔸 (RenamingSets.rename σ x) ∩ A = ∅), RenamingSets.rename σ (f ⟨x, hx₁⟩) = f ⟨RenamingSets.rename σ x, hx₂⟩

theorem RenamingSets.PartialHom.supp_subset {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] [Infinite 𝔸] {A : Finset 𝔸} (f : PartialHom A X Y) (x : { x : X // supp 𝔸 x ∩ A = ∅ }) : supp 𝔸 (f x) ⊆ A ∪ supp 𝔸 ↑x

@[irreducible]

noncomputable def RenamingSets.PartialHom.extend {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] {A : Finset 𝔸} (f : PartialHom A X Y) (x : X) : Y

Any PartialHom has a unique, finitely-supported total extension.

Equations

• f.extend x = RenamingSets.rename (RenamingSets.Ren.unfresh (RenamingSets.supp 𝔸 x) A) (f ⟨RenamingSets.rename (RenamingSets.Ren.fresh (RenamingSets.supp 𝔸 x) A) x, ⋯⟩)

theorem RenamingSets.PartialHom.extend_def {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] [Infinite 𝔸] {A : Finset 𝔸} {x : X} (σ σ' : Ren 𝔸) (hσ₁ : ∀ a ∈ supp 𝔸 x, σ a ∉ A) (hσ₂ : ∀ a ∈ supp 𝔸 x, σ' (σ a) = a) (hσ₃ : ∀ a ∈ A, σ' a = a) (f : PartialHom A X Y) : f.extend x = RenamingSets.rename σ' (f ⟨RenamingSets.rename σ x, ⋯⟩)

@[simp]

theorem RenamingSets.PartialHom.extend_eq {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] [Infinite 𝔸] {A : Finset 𝔸} (f : PartialHom A X Y) (x : X) (hx : supp 𝔸 x ∩ A = ∅) : f.extend x = f ⟨x, hx⟩

@[simp]

theorem RenamingSets.PartialHom.isSupportOfF_extend {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] [Infinite 𝔸] {A : Finset 𝔸} (f : PartialHom A X Y) : IsSupportOfF A f.extend

@[simp]

theorem RenamingSets.PartialHom.isSupportOfF_extend' {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] [Infinite 𝔸] {A B : Finset 𝔸} (f : PartialHom A X Y) (h : A ⊆ B) : IsSupportOfF B f.extend

@[simp]

theorem RenamingSets.PartialHom.isSupportedF_extend {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] [Infinite 𝔸] {A : Finset 𝔸} (f : PartialHom A X Y) : IsSupportedF 𝔸 f.extend

def RenamingSets.PartialHom.rename {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] [Infinite 𝔸] (σ : Ren 𝔸) {A : Finset 𝔸} {f : X → Y} (hf : IsSupportOfF A f) : PartialHom (A ∪ σ.supp ∪ Finset.image (⇑σ) A) X Y

Every finitely-supported function gives rise to a partial renaming function.

Equations

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

@[simp]

theorem RenamingSets.PartialHom.rename_toFun {𝔸 : Type u_3} [DecidableEq 𝔸] {X : Type u_1} {Y : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] [Infinite 𝔸] (σ : Ren 𝔸) {A : Finset 𝔸} {f : X → Y} (hf : IsSupportOfF A f) (x : { x : X // supp 𝔸 x ∩ (A ∪ σ.supp ∪ Finset.image (⇑σ) A) = ∅ }) : (rename σ hf) x = RenamingSets.rename σ (f ↑x)