chore: remove Cardinal imports from GroupTheory.GroupAction.Quotient (#28529)

Author: Ruben-VandeVelde

Mathlib/Algebra/Polynomial/GroupRingAction.lean

@@ -6,6 +6,7 @@ Authors: Kenny Lau
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Monic
 import Mathlib.Algebra.Ring.Action.Basic
+import Mathlib.GroupTheory.Coset.Card
 import Mathlib.GroupTheory.GroupAction.Hom
 import Mathlib.GroupTheory.GroupAction.Quotient
 

Mathlib/Analysis/Convex/Topology.lean

@@ -23,7 +23,7 @@ We prove the following facts:
 * `Set.Finite.isClosed_convexHull` : convex hull of a finite set is closed.
 -/
 
-assert_not_exists Norm
+assert_not_exists Cardinal Norm
 
 open Metric Bornology Set Pointwise Convex
 

Mathlib/Analysis/Normed/Module/Convex.lean

@@ -24,6 +24,8 @@ We prove the following facts:
   is bounded.
 -/
 
+-- TODO assert_not_exists Cardinal
+
 variable {E : Type*}
 
 open Metric Set

Mathlib/Analysis/NormedSpace/Connected.lean

@@ -25,6 +25,7 @@ Statements with connectedness instead of path-connectedness are also given.
 -/
 
 assert_not_exists Subgroup.index Nat.divisors
+-- TODO assert_not_exists Cardinal
 
 open Convex Set Metric
 

Mathlib/GroupTheory/GroupAction/CardCommute.lean

@@ -4,17 +4,63 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Thomas Browning
 -/
 import Mathlib.Algebra.Group.ConjFinite
+import Mathlib.GroupTheory.Coset.Card
 import Mathlib.GroupTheory.GroupAction.Quotient
 
 /-!
-# A consequence of Burnside's lemma
+# Properties of group actions involving quotient groups
 
-See `Mathlib/GroupTheory/GroupAction/Quotient.lean` for Burnside's lemma itself.
-This lemma is separate because it requires `Nat.card`
-and hence transitively the development of cardinals.
+This file proves cardinality properties of group actions which use the quotient group construction,
+notably
+* the class formula `MulAction.card_eq_sum_card_group_div_card_stabilizer'`
+* `card_comm_eq_card_conjClasses_mul_card`
+
+as well as their analogues for additive groups.
+
+See `Mathlib/GroupTheory/GroupAction/Quotient.lean` for the construction of isomorphisms used to
+prove these cardinality properties.
+These lemmas are separate because they require the development of cardinals.
 -/
 
-variable {α : Type*}
+variable {α β : Type*}
+
+open Function
+
+namespace MulAction
+
+variable (α β)
+variable [Group α] [MulAction α β]
+
+local notation "Ω" => Quotient <| orbitRel α β
+
+/-- **Class formula** for a finite group acting on a finite type. See
+`MulAction.card_eq_sum_card_group_div_card_stabilizer` for a specialized version using
+`Quotient.out`. -/
+@[to_additive
+      /-- **Class formula** for a finite group acting on a finite type. See
+      `AddAction.card_eq_sum_card_addGroup_div_card_stabilizer` for a specialized version using
+      `Quotient.out`. -/]
+theorem card_eq_sum_card_group_div_card_stabilizer' [Fintype α] [Fintype β] [Fintype Ω]
+    [∀ b : β, Fintype <| stabilizer α b] {φ : Ω → β} (hφ : LeftInverse Quotient.mk'' φ) :
+    Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) := by
+  classical
+    have : ∀ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) =
+        Fintype.card (α ⧸ stabilizer α (φ ω)) := by
+      intro ω
+      rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),
+        Fintype.card_prod, Nat.mul_div_cancel]
+      exact Fintype.card_pos_iff.mpr (by infer_instance)
+    simp_rw [this, ← Fintype.card_sigma,
+      Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
+
+/-- **Class formula** for a finite group acting on a finite type. -/
+@[to_additive /-- **Class formula** for a finite group acting on a finite type. -/]
+theorem card_eq_sum_card_group_div_card_stabilizer [Fintype α] [Fintype β] [Fintype Ω]
+    [∀ b : β, Fintype <| stabilizer α b] :
+    Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α ω.out) :=
+  card_eq_sum_card_group_div_card_stabilizer' α β Quotient.out_eq'
+
+end MulAction
 
 instance instInfiniteProdSubtypeCommute [Mul α] [Infinite α] :
     Infinite { p : α × α // Commute p.1 p.2 } :=

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -5,9 +5,10 @@ Authors: Chris Hughes, Thomas Browning
 -/
 import Mathlib.Algebra.Group.Subgroup.Actions
 import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
+import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Dynamics.PeriodicPts.Defs
 import Mathlib.GroupTheory.Commutator.Basic
-import Mathlib.GroupTheory.Coset.Card
+import Mathlib.GroupTheory.Coset.Basic
 import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.ConjAct
 import Mathlib.GroupTheory.GroupAction.Hom
@@ -17,12 +18,14 @@ import Mathlib.GroupTheory.GroupAction.Hom
 
 This file proves properties of group actions which use the quotient group construction, notably
 * the orbit-stabilizer theorem `MulAction.card_orbit_mul_card_stabilizer_eq_card_group`
-* the class formula `MulAction.card_eq_sum_card_group_div_card_stabilizer'`
+* the class formula `MulAction.selfEquivSigmaOrbitsQuotientStabilizer'`
 * Burnside's lemma `MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group`,
 
 as well as their analogues for additive groups.
 -/
 
+assert_not_exists Cardinal
+
 universe u v w
 
 variable {α : Type u} {β : Type v} {γ : Type w}
@@ -211,26 +214,6 @@ noncomputable def selfEquivSigmaOrbitsQuotientStabilizer' {φ : Ω → β}
         (Equiv.setCongr <| orbitRel.Quotient.orbit_eq_orbit_out _ hφ).trans <|
           orbitEquivQuotientStabilizer α (φ ω)
 
-/-- **Class formula** for a finite group acting on a finite type. See
-`MulAction.card_eq_sum_card_group_div_card_stabilizer` for a specialized version using
-`Quotient.out`. -/
-@[to_additive
-      /-- **Class formula** for a finite group acting on a finite type. See
-      `AddAction.card_eq_sum_card_addGroup_div_card_stabilizer` for a specialized version using
-      `Quotient.out`. -/]
-theorem card_eq_sum_card_group_div_card_stabilizer' [Fintype α] [Fintype β] [Fintype Ω]
-    [∀ b : β, Fintype <| stabilizer α b] {φ : Ω → β} (hφ : LeftInverse Quotient.mk'' φ) :
-    Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) := by
-  classical
-    have : ∀ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) =
-        Fintype.card (α ⧸ stabilizer α (φ ω)) := by
-      intro ω
-      rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),
-        Fintype.card_prod, Nat.mul_div_cancel]
-      exact Fintype.card_pos_iff.mpr (by infer_instance)
-    simp_rw [this, ← Fintype.card_sigma,
-      Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
-
 /-- **Class formula**. This is a special case of
 `MulAction.self_equiv_sigma_orbits_quotient_stabilizer'` with `φ = Quotient.out`. -/
 @[to_additive
@@ -239,13 +222,6 @@ theorem card_eq_sum_card_group_div_card_stabilizer' [Fintype α] [Fintype β] [F
 noncomputable def selfEquivSigmaOrbitsQuotientStabilizer : β ≃ Σ ω : Ω, α ⧸ stabilizer α ω.out :=
   selfEquivSigmaOrbitsQuotientStabilizer' α β Quotient.out_eq'
 
-/-- **Class formula** for a finite group acting on a finite type. -/
-@[to_additive /-- **Class formula** for a finite group acting on a finite type. -/]
-theorem card_eq_sum_card_group_div_card_stabilizer [Fintype α] [Fintype β] [Fintype Ω]
-    [∀ b : β, Fintype <| stabilizer α b] :
-    Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α ω.out) :=
-  card_eq_sum_card_group_div_card_stabilizer' α β Quotient.out_eq'
-
 /-- **Burnside's lemma** : a (noncomputable) bijection between the disjoint union of all
 `{x ∈ X | g • x = x}` for `g ∈ G` and the product `G × X/G`, where `G` is a group acting on `X` and
 `X/G` denotes the quotient of `X` by the relation `orbitRel G X`. -/

Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.Group.Subgroup.Finite
+import Mathlib.GroupTheory.Coset.Card
 import Mathlib.GroupTheory.GroupAction.Quotient
 import Mathlib.GroupTheory.Perm.Basic
 import Mathlib.LinearAlgebra.Alternating.Basic

Mathlib/Topology/Algebra/Group/Quotient.lean

@@ -15,6 +15,8 @@ In this file we define topology on `G ⧸ N`, where `N` is a subgroup of `G`,
 and prove basic properties of this topology.
 -/
 
+assert_not_exists Cardinal
+
 open Topology
 open scoped Pointwise
 

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -18,7 +18,7 @@ import Mathlib.LinearAlgebra.Quotient.Defs
 We use the class `ContinuousSMul` for topological (semi) modules and topological vector spaces.
 -/
 
-assert_not_exists TrivialStar
+assert_not_exists Cardinal TrivialStar
 
 open LinearMap (ker range)
 open Topology Filter Pointwise

Mathlib/Topology/CWComplex/Classical/Basic.lean

@@ -5,6 +5,7 @@ Authors: Floris van Doorn, Hannah Scholz
 -/
 
 import Mathlib.Analysis.NormedSpace.Real
+import Mathlib.Data.ENat.Basic
 import Mathlib.Logic.Equiv.PartialEquiv
 import Mathlib.Topology.MetricSpace.ProperSpace.Real