Sum Types

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

Permutations

instance NominalSets.Sum.instPermActionSum {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : PermAction 𝔸 (X ⊕ Y)

Equations

• NominalSets.Sum.instPermActionSum = { perm := fun (π : NominalSets.Perm 𝔸) => Sum.map (NominalSets.perm π) (NominalSets.perm π), perm_one := ⋯, perm_mul := ⋯ }

theorem NominalSets.Sum.perm_def {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (a✝ : X ⊕ Y) : perm π a✝ = Sum.map (perm π) (perm π) a✝

@[simp]

theorem NominalSets.Sum.perm_inl {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (x : X) : perm π (Sum.inl x) = Sum.inl (perm π x)

@[simp]

theorem NominalSets.Sum.perm_inr {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (π : Perm 𝔸) (x : Y) : perm π (Sum.inr x) = Sum.inr (perm π x)

@[simp]

theorem NominalSets.Sum.perm_elim {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] (π : Perm 𝔸) (f : X → Z) (g : Y → Z) (x : X ⊕ Y) : perm π (Sum.elim f g x) = Sum.elim (perm π f) (perm π g) (perm π x)

instance NominalSets.Sum.instDiscretePermActionSum {𝔸 : 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.Sum.isSupportOf_inl {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (A : Finset 𝔸) (x : X) : IsSupportOf A (Sum.inl x) ↔ IsSupportOf A x

@[simp]

theorem NominalSets.Sum.isSupportOf_inr {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (A : Finset 𝔸) (x : Y) : IsSupportOf A (Sum.inr x) ↔ IsSupportOf A x

@[simp]

theorem NominalSets.Sum.isSupported_inl {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (x : X) : IsSupported 𝔸 (Sum.inl x) ↔ IsSupported 𝔸 x

@[simp]

theorem NominalSets.Sum.isSupported_inr {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (x : Y) : IsSupported 𝔸 (Sum.inr x) ↔ IsSupported 𝔸 x

instance NominalSets.Sum.instNominalSum {𝔸 : 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.Sum.supp_inl {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [Nominal 𝔸 X] [Nominal 𝔸 Y] (x : X) : supp 𝔸 (Sum.inl x) = supp 𝔸 x

@[simp]

theorem NominalSets.Sum.supp_inr {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [Nominal 𝔸 X] [Nominal 𝔸 Y] (x : Y) : supp 𝔸 (Sum.inr x) = supp 𝔸 x

@[simp]

theorem NominalSets.Sum.isSupportedF_inl {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : IsSupportedF 𝔸 Sum.inl

@[simp]

theorem NominalSets.Sum.isSupportedF_inr {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : IsSupportedF 𝔸 Sum.inr

theorem NominalSets.Sum.isSupportedF_elim {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {W : Type u_5} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] [PermAction 𝔸 W] {f : X → Y → W} (hf : IsSupportedF 𝔸 fun (x : X × Y) => match x with | (x, y) => f x y) {g : X → Z → W} (hg : IsSupportedF 𝔸 fun (x : X × Z) => match x with | (x, y) => g x y) {h : X → Y ⊕ Z} (hh : IsSupportedF 𝔸 h) : IsSupportedF 𝔸 fun (x : X) => Sum.elim (f x) (g x) (h x)

Equivariance

@[simp]

theorem NominalSets.Sum.equivariant_inl {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : Equivariant 𝔸 Sum.inl

@[simp]

theorem NominalSets.Sum.equivariant_inr {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] : Equivariant 𝔸 Sum.inr

theorem NominalSets.Sum.equivariant_elim {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {W : Type u_5} [PermAction 𝔸 X] [PermAction 𝔸 Y] [PermAction 𝔸 Z] [PermAction 𝔸 W] {f : X → Y → W} (hf : Equivariant 𝔸 fun (x : X × Y) => match x with | (x, y) => f x y) {g : X → Z → W} (hg : Equivariant 𝔸 fun (x : X × Z) => match x with | (x, y) => g x y) {h : X → Y ⊕ Z} (hh : Equivariant 𝔸 h) : Equivariant 𝔸 fun (x : X) => Sum.elim (f x) (g x) (h x)