RenamingSets.Hom

structure RenamingSets.Hom (𝔸 : Type u_5) (X : Type u_6) (Y : Type u_7) [RenameAction 𝔸 X] [RenameAction 𝔸 Y] :

Type (max u_6 u_7)

Morphisms in the category of nominal renaming sets.

toFun : X → Y
The underlying function.
isSupportedF' : IsSupportedF 𝔸 self.toFun
The function has a finite support. Do not use this directly except when elements of the Hom type. Prefer isSupportedF instead.

Instances For

instance RenamingSets.Hom.instFunLike {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] :

FunLike (Hom 𝔸 X Y) X Y

Equations

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

source

def RenamingSets.Hom.Simps.coe {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (f : Hom 𝔸 X Y) :

X → Y

A simps projection for function application.

Equations

RenamingSets.Hom.Simps.coe f = ⇑f

Instances For

source

@[simp]

theorem RenamingSets.Hom.isSupportedF {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (f : Hom 𝔸 X Y) :

IsSupportedF 𝔸 ⇑f

source

@[simp]

theorem RenamingSets.Hom.coe_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (f : X → Y) (hf : IsSupportedF 𝔸 f) :

⇑{ toFun := f, isSupportedF' := hf } = f

source

@[simp]

theorem RenamingSets.Hom.mk_coe {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (f : Hom 𝔸 X Y) :

{ toFun := ⇑f, isSupportedF' := ⋯ } = f

source

theorem RenamingSets.Hom.ext {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] {f g : Hom 𝔸 X Y} (h : ⇑f = ⇑g) :

f = g

source

theorem RenamingSets.Hom.ext_iff {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] {f g : Hom 𝔸 X Y} :

f = g ↔ ⇑f = ⇑g

source

theorem RenamingSets.Hom.ext' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [DecidableEq 𝔸] [RenamingSet 𝔸 X] {f g : Hom 𝔸 X Y} (A : Finset 𝔸) (hA : ∀ (x : X), supp 𝔸 x ∩ A = ∅ → f x = g x) :

f = g

source

noncomputable instance RenamingSets.Hom.instRenameAction {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] :

RenameAction 𝔸 (Hom 𝔸 X Y)

Equations

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

source

theorem RenamingSets.Hom.rename_coe {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] (σ : Ren 𝔸) (f : Hom 𝔸 X Y) (a✝ : X) :

(rename σ f) a✝ = rename σ (⇑f) a✝

source

theorem RenamingSets.Hom.isSupportOf_iff_coe {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] (A : Finset 𝔸) (f : Hom 𝔸 X Y) :

IsSupportOf A f ↔ IsSupportOf A ⇑f

source

instance RenamingSets.Hom.instRenamingSet {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] :

RenamingSet 𝔸 (Hom 𝔸 X Y)

source

@[simp]

theorem RenamingSets.Hom.rename_apply {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] (σ : Ren 𝔸) (f : Hom 𝔸 X Y) (x : X) :

(rename σ f) (rename σ x) = rename σ (f x)

source

@[simp]

theorem RenamingSets.Hom.isSupportOfF_supp {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] (f : Hom 𝔸 X Y) :

IsSupportOfF (supp 𝔸 f) ⇑f

source

theorem RenamingSets.Hom.supp_min {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] {A : Finset 𝔸} {f : Hom 𝔸 X Y} (hf : IsSupportOfF A ⇑f) :

supp 𝔸 f ⊆ A

source

@[simp]

theorem RenamingSets.Hom.isSupportOf_iff_isSupportOfF {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] (A : Finset 𝔸) (f : Hom 𝔸 X Y) :

IsSupportOf A f ↔ IsSupportOfF A ⇑f

source

theorem RenamingSets.Hom.supp_subset {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] [DecidableEq 𝔸] (f : Hom 𝔸 X Y) (x : X) :

supp 𝔸 (f x) ⊆ supp 𝔸 f ∪ supp 𝔸 x

source

@[simp]

theorem RenamingSets.Hom.equivariant_apply {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] :

Equivariant 𝔸 fun (x : Hom 𝔸 X Y × X) => x.1 x.2

source

@[simp]

theorem RenamingSets.Hom.isSupportedF_apply {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] :

IsSupportedF 𝔸 fun (x : Hom 𝔸 X Y × X) => x.1 x.2

source

@[simp]

theorem RenamingSets.Hom.equivariant_apply' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] [Infinite 𝔸] [RenamingSet 𝔸 Y] [RenamingSet 𝔸 Z] {f : X → Hom 𝔸 Y Z} (hf : Equivariant 𝔸 f) {g : X → Y} (hg : Equivariant 𝔸 g) :

Equivariant 𝔸 fun (x : X) => (f x) (g x)

source

@[simp]

theorem RenamingSets.Hom.isSupportedF_apply' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] [Infinite 𝔸] [RenamingSet 𝔸 Y] [RenamingSet 𝔸 Z] {f : X → Hom 𝔸 Y Z} (hf : IsSupportedF 𝔸 f) {g : X → Y} (hg : IsSupportedF 𝔸 g) :

IsSupportedF 𝔸 fun (x : X) => (f x) (g x)

source

theorem RenamingSets.Hom.isSupportedF_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] [RenamingSet 𝔸 Z] (f : X → Y → Z) (hf : IsSupportedF 𝔸 fun (x : X × Y) => match x with | (x, y) => f x y) :

IsSupportedF 𝔸 fun (x : X) => { toFun := f x, isSupportedF' := ⋯ }

source

def RenamingSets.Hom.curry {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] [RenamingSet 𝔸 Z] (f : Hom 𝔸 (X × Y) Z) :

Hom 𝔸 X (Hom 𝔸 Y Z)

Currying for morphisms.

Equations

f.curry = { toFun := fun (x : X) => { toFun := fun (y : Y) => f (x, y), isSupportedF' := ⋯ }, isSupportedF' := ⋯ }

Instances For

source

@[simp]

theorem RenamingSets.Hom.curry_coe_coe {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] [RenamingSet 𝔸 Z] (f : Hom 𝔸 (X × Y) Z) (x : X) (y : Y) :

(f.curry x) y = f (x, y)

source

def RenamingSets.Hom.eval {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] :

Hom 𝔸 (Hom 𝔸 X Y × X) Y

The evaluation morphism.

Equations

RenamingSets.Hom.eval = { toFun := fun (x : RenamingSets.Hom 𝔸 X Y × X) => x.1 x.2, isSupportedF' := ⋯ }

Instances For

source

@[simp]

theorem RenamingSets.Hom.eval_coe {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [Infinite 𝔸] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] (x : Hom 𝔸 X Y × X) :

eval x = x.1 x.2