diff options
| -rw-r--r-- | Nominal/Instances.lean | 116 |
1 files 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 |