Product Types

This file formalizes definitions and results about permutations and supports for product types.

Permutations

instance NominalSets.Prod.instPermActionProd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : PermAction 𝔸 (X × Y)

Equations

• NominalSets.Prod.instPermActionProd = { perm := fun (π : NominalSets.Perm 𝔸) (x : X × Y) => (NominalSets.perm π x.1, NominalSets.perm π x.2), perm_one := ⋯, perm_mul := ⋯ }

theorem NominalSets.Prod.perm_def {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (x : X × Y) : perm π x = (perm π x.1, perm π x.2)

@[simp]

theorem NominalSets.Prod.perm_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (x : X) (y : Y) : perm π (x, y) = (perm π x, perm π y)

@[simp]

theorem NominalSets.Prod.perm_fst {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (x : X × Y) : (perm π x).1 = perm π x.1

@[simp]

theorem NominalSets.Prod.perm_snd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (x : X × Y) : (perm π x).2 = perm π x.2

instance NominalSets.Prod.instDiscretePermActionProd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [DiscretePermAction 𝔸 X] [DiscretePermAction 𝔸 Y] : DiscretePermAction 𝔸 (X × Y)

Supports

@[simp]

theorem NominalSets.Prod.isSupportOf_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (A : Finset 𝔸) (x : X) (y : Y) : IsSupportOf A (x, y) ↔ IsSupportOf A x ∧ IsSupportOf A y

@[simp]

theorem NominalSets.Prod.isSupported_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (x : X) (y : Y) : IsSupported 𝔸 (x, y) ↔ IsSupported 𝔸 x ∧ IsSupported 𝔸 y

instance NominalSets.Prod.instNominalProd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [Nominal 𝔸 X] [Nominal 𝔸 Y] : Nominal 𝔸 (X × Y)

@[simp]

theorem NominalSets.Prod.supp_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [DecidableEq 𝔸] [Nominal 𝔸 X] [Nominal 𝔸 Y] (x : X) (y : Y) : supp 𝔸 (x, y) = supp 𝔸 x ∪ supp 𝔸 y

@[simp]

theorem NominalSets.Prod.isSupportedF_fst {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : IsSupportedF 𝔸 Prod.fst

@[simp]

theorem NominalSets.Prod.isSupportedF_snd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : IsSupportedF 𝔸 Prod.snd

theorem NominalSets.Prod.isSupportedF_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : X → Y} (hf : IsSupportedF 𝔸 f) {g : X → Z} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 fun (x : X) => (f x, g x)

Equivariance

@[simp]

theorem NominalSets.Prod.equivariant_fst {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : Equivariant 𝔸 Prod.fst

@[simp]

theorem NominalSets.Prod.equivariant_snd {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : Equivariant 𝔸 Prod.snd

theorem NominalSets.Prod.equivariant_mk {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] {f : X → Y} (hf : Equivariant 𝔸 f) {g : X → Z} (hg : Equivariant 𝔸 g) : Equivariant 𝔸 fun (x : X) => (f x, g x)