From 32f51048343ee23e6382e5aff37308ec015fcdf3 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Wed, 22 Oct 2025 21:51:54 +0200
Subject: add product and coproduct instances

---
 Nominal/Instances.lean | 116 ++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 106 insertions(+), 10 deletions(-)

diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean
index bf1d372..decc0cb 100644
--- a/Nominal/Instances.lean
+++ b/Nominal/Instances.lean
@@ -1,5 +1,6 @@
 import Nominal.Permutations
 import Nominal.Support
+import Mathlib
 
 /-!
 # Instances
@@ -16,20 +17,19 @@ The set 𝔸 of atoms itself is a nominal set, where supp a = {a}.
 -/
 section Atoms
 
-private lemma NominalSet.supp_atoms' {a : 𝔸} : PermSet.HasSupport 𝔸 a {a} := by
+private lemma NominalSet.supp_atom' {a : 𝔸} : PermSet.HasSupport 𝔸 a {a} := by
   simp [PermSet.HasSupport, PermSet.fix, PermSet.fix']
 
 instance : NominalSet 𝔸 𝔸 where
   fin_supp := by
-    intro a
-    use {a}
-    exact ⟨NominalSet.supp_atoms' 𝔸, Set.finite_singleton a⟩
+    intro a; use {a}
+    exact ⟨NominalSet.supp_atom' 𝔸, Set.finite_singleton a⟩
 
-lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by
+lemma NominalSet.supp_atom [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by
   ext b; constructor
-  · apply support_subset_supp
-    · apply NominalSet.supp_atoms'
-    · apply Set.finite_singleton
+  · apply support_subset_supp 𝔸
+    · exact NominalSet.supp_atom' 𝔸
+    · exact Set.finite_singleton a
   · suffices a ∈ supp 𝔸 a by simp; intro h; rwa [h]
     intro S ⟨hsuppS, hfinS⟩
     by_contra ha
@@ -61,8 +61,7 @@ def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where
   mul_smul := by intro _ _ _; rfl
   is_discrete := by intro _ _; rfl
   fin_supp := by
-    intro x
-    use {}
+    intro x; use {}
     constructor
     · intro π hπ; simp [PermSet.fix']; rfl
     · exact Set.finite_empty
@@ -81,3 +80,100 @@ instance : DiscreteNominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit
 instance : DiscreteNominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool
 
 end Discrete
+
+/-!
+## Products
+
+Pairs of two nominal sets also form a nominal set, where supp (x, y) = supp x ∪ supp y.
+-/
+section Products
+
+instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X × Y) where
+
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] [Infinite 𝔸]
+
+private lemma NominalSet.supp_product' {x : X} {y : Y} : PermSet.HasSupport 𝔸 (x, y) (supp 𝔸 x ∪ supp 𝔸 y) := by
+  intro π hπ
+  obtain ⟨hπ₁, hπ₂⟩ := PermSet.fix_union 𝔸 hπ
+  exact Prod.mk_inj.mpr ⟨supp_is_support 𝔸 hπ₁, supp_is_support 𝔸 hπ₂⟩
+
+instance : NominalSet 𝔸 (X × Y) where
+  fin_supp := by
+    intro ⟨x, y⟩; use NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y
+    exact ⟨NominalSet.supp_product' 𝔸, Set.Finite.union (NominalSet.supp_finite 𝔸) (NominalSet.supp_finite 𝔸)⟩
+
+@[simp] lemma NominalSet.supp_product {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 x ∪ supp 𝔸 y := by
+  ext b; constructor
+  · apply support_subset_supp
+    · exact supp_product' 𝔸
+    · exact Set.Finite.union (supp_finite 𝔸) (supp_finite 𝔸)
+  · intro hb; cases hb with
+    | inl hx =>
+        intro S hS
+        suffices PermSet.HasSupport 𝔸 x S by apply hx; exact ⟨this, hS.out.right⟩
+        intro π hπ
+        suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.left
+        exact (hS.out.left hπ).out
+    | inr hy =>
+        intro S hS
+        suffices PermSet.HasSupport 𝔸 y S by apply hy; exact ⟨this, hS.out.right⟩
+        intro π hπ
+        suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.right
+        exact (hS.out.left hπ).out
+
+lemma NominalSet.supp_product_comm {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 (y, x) := by
+  simp; apply Set.union_comm
+
+end Products
+
+/-!
+## Coproducts
+
+Sums of two nominal sets also form a nominal set, where supp (inl x) = supp x and supp (inr y) = supp y.
+-/
+section Coproducts
+
+instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X ⊕ Y) where
+
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] [Infinite 𝔸]
+
+private lemma NominalSet.supp_coproduct₁' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (supp 𝔸 x) := by
+  intro π hπ
+  simp [PermSet.fix']
+  exact supp_is_support 𝔸 hπ
+
+private lemma NominalSet.supp_coproduct₂' {y : Y} : PermSet.HasSupport 𝔸 (.inr y : X ⊕ Y) (supp 𝔸 y) := by
+  intro π hπ
+  simp [PermSet.fix']
+  exact supp_is_support 𝔸 hπ
+
+instance : NominalSet 𝔸 (X ⊕ Y) where
+  fin_supp := by
+    intro xy
+    cases xy with
+    | inl x => use NominalSet.supp 𝔸 x; exact ⟨NominalSet.supp_coproduct₁' 𝔸, NominalSet.supp_finite 𝔸⟩
+    | inr y => use NominalSet.supp 𝔸 y; exact ⟨NominalSet.supp_coproduct₂' 𝔸, NominalSet.supp_finite 𝔸⟩
+
+@[simp] lemma NominalSet.supp_coproduct₁ {x : X} : supp 𝔸 (.inl x : X ⊕ Y) = supp 𝔸 x := by
+  ext b; constructor
+  · apply support_subset_supp
+    · exact supp_coproduct₁' 𝔸
+    · exact supp_finite 𝔸
+  · intro hb S hS
+    suffices PermSet.HasSupport 𝔸 x S by apply hb; exact ⟨this, hS.out.right⟩
+    intro π hπ
+    suffices π ∈ PermSet.fix' 𝔸 (.inl x : X ⊕ Y) by simp [PermSet.fix'] at this; exact this
+    exact (hS.out.left hπ).out
+
+@[simp] lemma NominalSet.supp_coproduct₂ {y : Y} : supp 𝔸 (.inr y : X ⊕ Y) = supp 𝔸 y := by
+  ext b; constructor
+  · apply support_subset_supp
+    · exact supp_coproduct₂' 𝔸
+    · exact supp_finite 𝔸
+  · intro hb S hS
+    suffices PermSet.HasSupport 𝔸 y S by apply hb; exact ⟨this, hS.out.right⟩
+    intro π hπ
+    suffices π ∈ PermSet.fix' 𝔸 (.inr y : X ⊕ Y) by simp [PermSet.fix'] at this; exact this
+    exact (hS.out.left hπ).out
+
+end Coproducts
-- 
cgit v1.3.1