chore(GroupTheory/GroupAction/SubMulAction/Combination.lean): rename Nat.Combination to Set.powersetCard (leanprover-community#34581)

Following suggestion by @ocfnash  and @alreadydone , rename `Nat.Combination` as `Set.powersetCard`,
in analogy to `Finset.powerset` and `Finset.powersetCard`.

Some later improvements are given in leanprover-community#34307

Author: AntoineChambert-Loir

Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean

@@ -16,30 +16,30 @@ public import Mathlib.GroupTheory.GroupAction.Basic
 Combinations in a type are finite subsets of given cardinality.
 This file provides some API for handling them, especially in the context of a group action.
 
-* `Nat.Combination α n` is the set of all `Finset α` with cardinality `n`.
+* `Set.powersetCard α n` is the set of all `Finset α` with cardinality `n`.
 
-* `Nat.Combination.card` proves that the `Nat.card`-cardinality
+* `Set.powersetCard.card` proves that the `Nat.card`-cardinality
 of this set is equal to `(Nat.card α).choose n`.
 
-* `Nat.Combination.subMulAction`:
-When a group `G` acts on `α`, the `SubMulAction` of `G` on `n.Combination α`.
+* `Set.powersetCard.subMulAction`:
+When a group `G` acts on `α`, the `SubMulAction` of `G` on `Set.powersetCard α n`.
 
-This induces a `MulAction G (n.Combination α)` instance. Then:
+This induces a `MulAction G (Set.powersetCard α n)` instance. Then:
 
-* `EmbeddingToCombination.map`: the equivariant map from `Fin n ↪ α` to `n.Combination α`.
+* `EmbeddingToCombination.map`: the equivariant map from `Fin n ↪ α` to `Set.powersetCard α n`.
 
-* `Nat.Combination.isPretransitive_of_isMultiplyPretransitive`
+* `Set.powersetCard.isPretransitive_of_isMultiplyPretransitive`
 shows the pretransitivity of that action if the action of `G` on `α` is `n`-pretransitive.
 
-* `Nat.Combination.isPretransitive` shows that `Equiv.Perm α`
-acts pretransitively on `n.Combination α`, for all `n`.
+* `Set.powersetCard.isPretransitive` shows that `Equiv.Perm α`
+acts pretransitively on `Set.powersetCard α n`, for all `n`.
 
-* `Nat.Combination.compl`: Given an equality `m + n = Fintype.card α`,
+* `Set.powersetCard.compl`: Given an equality `m + n = Fintype.card α`,
 the complement of an `n`-combination, as an `m`-combination.
 This map is an equivariant map with respect to a group action on `α`.
 
 * `Nat.toCombination_one_equivariant`:
-The obvious map from `α` to `1.Combination α`, as an equivariant map.
+The obvious map from `α` to `Set.powersetCard α 1`, as an equivariant map.
 
 -/
 
@@ -48,34 +48,34 @@ The obvious map from `α` to `1.Combination α`, as an equivariant map.
 variable (G : Type*) [Group G] (α : Type*) [MulAction G α]
 
 /-- The type of combinations of `n` elements of a type `α` -/
-def Nat.Combination (n : ℕ) := {s : Finset α | s.card = n}
+def Set.powersetCard (n : ℕ) := {s : Finset α | s.card = n}
 
-variable {α} {n : ℕ} {s t : n.Combination α}
+variable {α} {n : ℕ} {s t : Set.powersetCard α n}
 
-namespace Nat.Combination
+namespace Set.powersetCard
 
 open scoped Pointwise
 
-open MulAction Finset
+open MulAction Finset Set
 
 @[simp]
 theorem mem_iff {s : Finset α} :
-    s ∈ n.Combination α ↔ s.card = n := by
-  rw [Combination, Set.mem_setOf_eq]
+    s ∈ Set.powersetCard α n ↔ s.card = n := by
+  rw [Set.powersetCard, Set.mem_setOf_eq]
 
-instance : SetLike (n.Combination α) α := SetLike.instSubtype
+instance : SetLike (Set.powersetCard α n) α := SetLike.instSubtype
 
 @[simp]
-theorem coe_coe {s : n.Combination α} :
+theorem coe_coe {s : Set.powersetCard α n} :
     ((s : Finset α) : Set α) = s := rfl
 
-theorem mem_coe_iff {s : Nat.Combination α n} {a : α} : a ∈ (s : Finset α) ↔ a ∈ s := .rfl
+theorem mem_coe_iff {s : Set.powersetCard α n} {a : α} : a ∈ (s : Finset α) ↔ a ∈ s := .rfl
 
 theorem eq_iff_subset : s = t ↔ (s : Finset α) ⊆ (t : Finset α) := by
   rw [Finset.subset_iff_eq_of_card_le (t.prop.trans_le s.prop.ge), Subtype.ext_iff]
 
 theorem exists_mem_notMem (hn : 1 ≤ n) (hα : n < ENat.card α) {a b : α} (hab : a ≠ b) :
-    ∃ s : n.Combination α, a ∈ s ∧ b ∉ s := by
+    ∃ s : Set.powersetCard α n, a ∈ s ∧ b ∉ s := by
   have ha' : n ≤ Set.encard {b}ᶜ := by
     rwa [← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α), Set.encard_singleton,
       add_comm, ENat.lt_add_one_iff' (ENat.coe_ne_top n)] at hα
@@ -87,26 +87,26 @@ theorem exists_mem_notMem (hn : 1 ≤ n) (hα : n < ENat.card α) {a b : α} (ha
       by simpa using has, by simpa using has'⟩
 
 variable (α n) in
-/-- `Nat.Combination α n` as a `SubMulAction` of `Finset α`. -/
-@[to_additive /--`Nat.Combination α n` as a `SubAddAction` of `Finsetα`.-/]
+/-- `Set.powersetCard α n` as a `SubMulAction` of `Finset α`. -/
+@[to_additive /--`Set.powersetCard α n` as a `SubAddAction` of `Finsetα`.-/]
 def subMulAction [DecidableEq α] : SubMulAction G (Finset α) where
-  carrier := n.Combination α
+  carrier := Set.powersetCard α n
   smul_mem' g s := (Finset.card_smul_finset g s).trans
 
 @[to_additive]
-instance [DecidableEq α] : MulAction G (n.Combination α) :=
+instance [DecidableEq α] : MulAction G (Set.powersetCard α n) :=
   (subMulAction G α n).mulAction
 
 variable {G}
 
 @[to_additive (attr := simp)]
-theorem coe_smul [DecidableEq α] {n : ℕ} {g : G} {s : n.Combination α} :
-    ((g • s : n.Combination α) : Finset α) = g • s :=
+theorem coe_smul [DecidableEq α] {n : ℕ} {g : G} {s : Set.powersetCard α n} :
+    ((g • s : Set.powersetCard α n) : Finset α) = g • s :=
   SubMulAction.val_smul (p := subMulAction G α n) g s
 
 theorem addAction_faithful {G : Type*} [AddGroup G] {α : Type*} [AddAction G α] {n : ℕ}
     [DecidableEq α] (hn : 1 ≤ n) (hα : n < ENat.card α) {g : G} :
-    AddAction.toPerm g = (1 : Equiv.Perm (n.Combination α))
+    AddAction.toPerm g = (1 : Equiv.Perm (Set.powersetCard α n))
       ↔ AddAction.toPerm g = (1 : Equiv.Perm α) := by
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · contrapose h with h
@@ -123,11 +123,11 @@ theorem addAction_faithful {G : Type*} [AddGroup G] {α : Type*} [AddAction G α
     simp [Subtype.ext_iff, Finset.ext_iff, mem_vadd_finset, h]
 
 /-- If an additive group `G` acts faithfully on `α`,
-then it acts faithfully on `n.Combination α`,
+then it acts faithfully on `Set.powersetCard α n`,
 provided `1 ≤ n < ENat.card α`. -/
 theorem faithfulVAdd {G : Type*} [AddGroup G] {α : Type*} [AddAction G α] {n : ℕ}
     [DecidableEq α] (hn : 1 ≤ n) (hα : n < ENat.card α) [FaithfulVAdd G α] :
-    FaithfulVAdd G (n.Combination α) := by
+    FaithfulVAdd G (Set.powersetCard α n) := by
   rw [faithfulVAdd_iff]
   intro g hg
   apply AddAction.toPerm_injective (α := G) (β := α)
@@ -136,7 +136,7 @@ theorem faithfulVAdd {G : Type*} [AddGroup G] {α : Type*} [AddAction G α] {n :
 
 theorem mulAction_faithful {G : Type*} [Group G] {α : Type*} [MulAction G α] {n : ℕ}
     [DecidableEq α] (hn : 1 ≤ n) (hα : n < ENat.card α) {g : G} :
-    MulAction.toPerm g = (1 : Equiv.Perm (n.Combination α))
+    MulAction.toPerm g = (1 : Equiv.Perm (Set.powersetCard α n))
       ↔ MulAction.toPerm g = (1 : Equiv.Perm α) := by
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · contrapose h with h
@@ -153,10 +153,10 @@ theorem mulAction_faithful {G : Type*} [Group G] {α : Type*} [MulAction G α] {
     simp [Subtype.ext_iff, Finset.ext_iff, mem_smul_finset, h]
 
 /-- If a group `G` acts faithfully on `α`,
-then it acts faithfull on `n.Combination α`,
+then it acts faithfull on `Set.powersetCard α n`,
 provided `1 ≤ n < ENat.card α`. -/
 theorem faithfulSMul [DecidableEq α] (hn : 1 ≤ n) (hα : n < ENat.card α) [FaithfulSMul G α] :
-    FaithfulSMul G (n.Combination α) := by
+    FaithfulSMul G (Set.powersetCard α n) := by
   rw [faithfulSMul_iff]
   intro g hg
   apply MulAction.toPerm_injective (α := G) (β := α)
@@ -172,7 +172,7 @@ variable (n) in
 @[to_additive /-- The equivariant map from embeddings of `Fin n`
   (aka arrangements) to combinations. -/]
 def mulActionHom_of_embedding [DecidableEq α] :
-    (Fin n ↪ α) →[G] n.Combination α where
+    (Fin n ↪ α) →[G] Set.powersetCard α n where
   toFun f := ⟨Finset.univ.map f, by rw [mem_iff, Finset.card_map, Finset.card_fin]⟩
   map_smul' g f := by
     rw [← Subtype.coe_inj, Subtype.coe_mk, coe_smul,
@@ -194,39 +194,39 @@ theorem mulActionHom_of_embedding_surjective [DecidableEq α] :
   exact ⟨f, Subtype.ext hf⟩
 
 protected theorem card :
-    Nat.card (n.Combination α) = (Nat.card α).choose n := by
+    Nat.card (powersetCard α n) = (Nat.card α).choose n := by
   classical
   cases fintypeOrInfinite α
-  · suffices n.Combination α = Finset.powersetCard n (Finset.univ : Finset α) by
+  · suffices powersetCard α n = Finset.powersetCard n (Finset.univ : Finset α) by
       simp [this]
     ext; simp
   · rcases n with _ | n
-    · simp [Combination]
-    · rcases finite_or_infinite (Combination α (n + 1)) with hc | hc
-      · refine (Infinite.false (α := (Combination α (n + 1) → Combination α (n + 1))) ?_).elim
-        have : FaithfulSMul (Equiv.Perm α) (Combination α (n + 1)) :=
-          Nat.Combination.faithfulSMul (le_add_left 1 n) (by simp)
-        exact (Infinite.false (α := (Combination α (n + 1) → Combination α (n + 1)))
+    · simp [powersetCard]
+    · rcases finite_or_infinite (powersetCard α (n + 1)) with hc | hc
+      · refine (Infinite.false (α := (powersetCard α (n + 1) → powersetCard α (n + 1))) ?_).elim
+        have : FaithfulSMul (Equiv.Perm α) (powersetCard α (n + 1)) :=
+          faithfulSMul (Nat.le_add_left 1 n) (by simp)
+        exact (Infinite.false (α := (powersetCard α (n + 1) → powersetCard α (n + 1)))
           (Infinite.of_injective _ (smul_left_injective' (M := Equiv.Perm α)))).elim
       · simp
 
 variable {α} in
-/-- If `0 < n < ENat.card α`, then `n.Combination α` is nontrivial. -/
+/-- If `0 < n < ENat.card α`, then `Set.powersetCard α n` is nontrivial. -/
 theorem nontrivial (h1 : 0 < n) (h2 : n < ENat.card α) :
-    Nontrivial (n.Combination α) := by
+    Nontrivial (Set.powersetCard α n) := by
   classical
   have h : Nontrivial α :=
-    (ENat.one_lt_card_iff_nontrivial α).mp (lt_of_le_of_lt (one_le_cast.mpr h1) h2)
-  have : FaithfulSMul (Equiv.Perm α) (Combination α n) := Nat.Combination.faithfulSMul h1 h2
-  have h := (smul_left_injective' (M := Equiv.Perm α) (α := Combination α n)).nontrivial
+    (ENat.one_lt_card_iff_nontrivial α).mp (lt_of_le_of_lt (Nat.one_le_cast.mpr h1) h2)
+  have : FaithfulSMul (Equiv.Perm α) (powersetCard α n) := faithfulSMul h1 h2
+  have h := (smul_left_injective' (M := Equiv.Perm α) (α := Set.powersetCard α n)).nontrivial
   contrapose! h
   infer_instance
 
 variable {α} in
-/-- A variant of `Nat.Combination.nontrivial` that uses `Nat.card`. -/
+/-- A variant of `Set.powersetCard.nontrivial` that uses `Nat.card`. -/
 theorem nontrivial' (h1 : 0 < n) (h2 : n < Nat.card α) :
-    Nontrivial (n.Combination α) := by
-  have : Finite α := finite_of_card_ne_zero (ne_zero_of_lt h2)
+    Nontrivial (Set.powersetCard α n) := by
+  have : Finite α := Nat.finite_of_card_ne_zero (ne_zero_of_lt h2)
   apply nontrivial h1
   simp [ENat.card_eq_coe_natCard α, h2]
 
@@ -236,10 +236,10 @@ variable [DecidableEq α]
 
 @[to_additive isPretransitive_of_isMultiplyPretransitive']
 theorem isPretransitive_of_isMultiplyPretransitive (h : IsMultiplyPretransitive G α n) :
-    IsPretransitive G (n.Combination α) :=
+    IsPretransitive G (Set.powersetCard α n) :=
   IsPretransitive.of_surjective_map (mulActionHom_of_embedding_surjective G α) h
 
-theorem isPretransitive : IsPretransitive (Equiv.Perm α) (n.Combination α) :=
+theorem isPretransitive : IsPretransitive (Equiv.Perm α) (Set.powersetCard α n) :=
   isPretransitive_of_isMultiplyPretransitive _ _
     (Equiv.Perm.isMultiplyPretransitive α n)
 
@@ -251,20 +251,20 @@ variable [DecidableEq α] [Fintype α] {m : ℕ} (hm : m + n = Fintype.card α)
 include hm
 
 /-- The complement of a combination, as an equivariant map. -/
-def compl : n.Combination α →[G] m.Combination α where
+def compl : Set.powersetCard α n →[G] Set.powersetCard α m where
   toFun s := ⟨(sᶜ : Finset α), by
       rw [mem_iff, Finset.card_compl]
       have := mem_iff.mp s.2
       omega⟩
   map_smul' g s := by ext; simp [← Finset.inv_smul_mem_iff]
 
 variable {hm} in
-theorem coe_compl {s : n.Combination α} :
+theorem coe_compl {s : Set.powersetCard α n} :
     (compl G α hm s : Finset α) = (s : Finset α)ᶜ :=
   rfl
 
 variable {hm} in
-theorem mem_compl {s : n.Combination α} {a : α} :
+theorem mem_compl {s : Set.powersetCard α n} {a : α} :
     a ∈ compl G α hm s ↔ a ∉ s :=
   Finset.mem_compl
 
@@ -284,7 +284,7 @@ end
 /-- The obvious map from a type to its 1-combinations, as an equivariant map. -/
 @[to_additive /-- The obvious map from a type to its 1-combinations, as an equivariant map. -/]
 def mulActionHom_singleton [DecidableEq α] :
-    α →[G] Nat.Combination α 1 where
+    α →[G] Set.powersetCard α 1 where
   toFun x := ⟨{x}, Finset.card_singleton x⟩
   map_smul' _ _ := rfl
 
@@ -295,4 +295,4 @@ theorem mulActionHom_singleton_bijective [DecidableEq α] :
   obtain ⟨a, rfl⟩ := Finset.card_eq_one.mp hs
   exact ⟨a, rfl⟩
 
-end Nat.Combination
+end Set.powersetCard