chore: to_additive various results on groups, group actions (#20498)

Mathlib/GroupTheory/GroupAction/Basic.lean

@@ -17,6 +17,13 @@ This file primarily concerns itself with orbits, stabilizers, and other objects
 actions. Despite this file being called `basic`, low-level helper lemmas for algebraic manipulation
 of `•` belong elsewhere.
 
+## Main definitions
+
+* `MulAction.orbit`
+* `MulAction.fixedPoints`
+* `MulAction.fixedBy`
+* `MulAction.stabilizer`
+
 -/
 
 
@@ -266,6 +273,8 @@ namespace MulAction
 variable {G : Type*} [Group G] {α : Type*} [MulAction G α]
 
 /-- To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions.-/
+@[to_additive
+  "To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions."]
 theorem le_stabilizer_iff_smul_le (s : Set α) (H : Subgroup G) :
     H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s := by
   constructor

Mathlib/GroupTheory/GroupAction/Blocks.lean

@@ -16,6 +16,8 @@ Given `SMul G X`, an action of a type `G` on a type `X`, we define
 
 - the predicate `IsBlock G B` states that `B : Set X` is a block,
   which means that the sets `g • B`, for `g ∈ G`, are equal or disjoint.
+  Under `Group G` and `MulAction G X`, this is equivalent to the classical
+  definition `MulAction.IsBlock.def_one`
 
 - a bunch of lemmas that give examples of “trivial” blocks : ⊥, ⊤, singletons,
   and non trivial blocks: orbit of the group, orbit of a normal subgroup…
@@ -25,14 +27,14 @@ The non-existence of nontrivial blocks is the definition of primitive actions.
 ## Results for actions on finite sets
 
 - `IsBlock.ncard_block_mul_ncard_orbit_eq` : The cardinality of a block
-multiplied by the number of its translates is the cardinal of the ambient type
+  multiplied by the number of its translates is the cardinal of the ambient type
 
 - `IsBlock.eq_univ_of_card_lt` : a too large block is equal to `Set.univ`
 
 - `IsBlock.subsingleton_of_card_lt` : a too small block is a subsingleton
 
 - `IsBlock.of_subset` : the intersections of the translates of a finite subset
-that contain a given point is a block
+  that contain a given point is a block
 
 ## References
 
@@ -63,7 +65,7 @@ theorem orbit.pairwiseDisjoint :
   exact (orbit.eq_or_disjoint x y).resolve_right h
 
 /-- Orbits of an element form a partition -/
-@[to_additive]
+@[to_additive "Orbits of an element of a partition"]
 theorem IsPartition.of_orbits :
     Setoid.IsPartition (Set.range fun a : X => orbit G a) := by
   apply orbit.pairwiseDisjoint.isPartition_of_exists_of_ne_empty
@@ -143,8 +145,11 @@ lemma IsBlock.disjoint_smul_set_smul (hB : IsBlock G B) (hgs : ¬ g • B ⊆ s
 lemma IsBlock.disjoint_smul_smul_set (hB : IsBlock G B) (hgs : ¬ g • B ⊆ s • B) :
     Disjoint (s • B) (g • B) := (hB.disjoint_smul_set_smul hgs).symm
 
+@[to_additive]
 alias ⟨IsBlock.smul_eq_smul_of_nonempty, _⟩ := isBlock_iff_smul_eq_smul_of_nonempty
+@[to_additive]
 alias ⟨IsBlock.pairwiseDisjoint_range_smul, _⟩ := isBlock_iff_pairwiseDisjoint_range_smul
+@[to_additive]
 alias ⟨IsBlock.smul_eq_smul_or_disjoint, _⟩ := isBlock_iff_smul_eq_smul_or_disjoint
 
 /-- A fixed block is a block. -/
@@ -277,13 +282,15 @@ protected lemma IsBlock.orbit (a : X) : IsBlock G (orbit G a) := (IsFixedBlock.o
 lemma isBlock_top : IsBlock (⊤ : Subgroup G) B ↔ IsBlock G B :=
   Subgroup.topEquiv.toEquiv.forall_congr fun _ ↦ Subgroup.topEquiv.toEquiv.forall_congr_left
 
+@[to_additive]
 lemma IsBlock.preimage {H Y : Type*} [Group H] [MulAction H Y]
     {φ : H → G} (j : Y →ₑ[φ] X) (hB : IsBlock G B) :
     IsBlock H (j ⁻¹' B) := by
   rintro g₁ g₂ hg
   rw [← Group.preimage_smul_setₛₗ, ← Group.preimage_smul_setₛₗ] at hg ⊢
   exact (hB <| ne_of_apply_ne _ hg).preimage _
 
+@[to_additive]
 theorem IsBlock.image {H Y : Type*} [Group H] [MulAction H Y]
     {φ : G →* H} (j : X →ₑ[φ] Y)
     (hφ : Function.Surjective φ) (hj : Function.Injective j)
@@ -292,18 +299,40 @@ theorem IsBlock.image {H Y : Type*} [Group H] [MulAction H Y]
   simp only [IsBlock, hφ.forall, ← image_smul_setₛₗ]
   exact fun g₁ g₂ hg ↦ disjoint_image_of_injective hj <| hB <| ne_of_apply_ne _ hg
 
+@[to_additive]
 theorem IsBlock.subtype_val_preimage {C : SubMulAction G X} (hB : IsBlock G B) :
     IsBlock G (Subtype.val ⁻¹' B : Set C) :=
   hB.preimage C.inclusion
 
+@[to_additive]
 theorem isBlock_subtypeVal {C : SubMulAction G X} {B : Set C} :
     IsBlock G (Subtype.val '' B : Set X) ↔ IsBlock G B := by
   refine forall₂_congr fun g₁ g₂ ↦ ?_
   rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set, ← image_smul_set, ne_eq,
     Set.image_eq_image C.inclusion_injective, disjoint_image_iff C.inclusion_injective]
 
+theorem _root_.AddAction.IsBlock.of_addsubgroup_of_conjugate
+    {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] {B : Set X}
+    {H : AddSubgroup G} (hB : AddAction.IsBlock H B) (g : G) :
+    AddAction.IsBlock (H.map (AddAut.conj g).toAddMonoidHom) (g +ᵥ B) := by
+  rw [AddAction.isBlock_iff_vadd_eq_or_disjoint]
+  intro h'
+  obtain ⟨h, hH, hh⟩ := AddSubgroup.mem_map.mp (SetLike.coe_mem h')
+  simp only [AddEquiv.coe_toAddMonoidHom, AddAut.conj_apply] at hh
+  suffices h' +ᵥ (g +ᵥ B) = g +ᵥ (h +ᵥ B) by
+    simp only [this]
+    apply (hB.vadd_eq_or_disjoint ⟨h, hH⟩).imp
+    · intro hB'; congr
+    · exact Set.disjoint_image_of_injective (AddAction.injective g)
+  suffices (h' : G) +ᵥ (g +ᵥ B) = g +ᵥ (h +ᵥ B) by
+    exact this
+  rw [← hh, vadd_vadd, vadd_vadd]
+  erw [AddAut.conj_apply]
+  simp
+
+@[to_additive existing AddAction.IsBlock.of_addsubgroup_of_conjugate]
 theorem IsBlock.of_subgroup_of_conjugate {H : Subgroup G} (hB : IsBlock H B) (g : G) :
-    IsBlock (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H) (g • B) := by
+    IsBlock (H.map (MulAut.conj g).toMonoidHom) (g • B) := by
   rw [isBlock_iff_smul_eq_or_disjoint]
   intro h'
   obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h')
@@ -318,6 +347,18 @@ theorem IsBlock.of_subgroup_of_conjugate {H : Subgroup G} (hB : IsBlock H B) (g
   rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right]
 
 /-- A translate of a block is a block -/
+theorem _root_.AddAction.IsBlock.translate
+    {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] (B : Set X)
+    (g : G) (hB : AddAction.IsBlock G B) :
+    AddAction.IsBlock G (g +ᵥ B) := by
+  rw [← AddAction.isBlock_top] at hB ⊢
+  rw [← AddSubgroup.map_comap_eq_self_of_surjective (G := G) ?_ ⊤]
+  · apply AddAction.IsBlock.of_addsubgroup_of_conjugate
+    rwa [AddSubgroup.comap_top]
+  · exact (AddAut.conj g).surjective
+
+/-- A translate of a block is a block -/
+@[to_additive existing]
 theorem IsBlock.translate (g : G) (hB : IsBlock G B) :
     IsBlock G (g • B) := by
   rw [← isBlock_top] at hB ⊢
@@ -329,9 +370,12 @@ theorem IsBlock.translate (g : G) (hB : IsBlock G B) :
 variable (G) in
 /-- For `SMul G X`, a block system of `X` is a partition of `X` into blocks
   for the action of `G` -/
+@[to_additive "For `VAdd G X`, a block system of `X` is a partition of `X` into blocks
+ for the additive action of `G`"]
 def IsBlockSystem (ℬ : Set (Set X)) := Setoid.IsPartition ℬ ∧ ∀ ⦃B⦄, B ∈ ℬ → IsBlock G B
 
-/-- Translates of a block form a block system. -/
+/-- Translates of a block form a block system -/
+@[to_additive "Translates of a block form a block system"]
 theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X]
     (hB : IsBlock G B) (hBe : B.Nonempty) :
     IsBlockSystem G (Set.range fun g : G => g • B) := by
@@ -352,6 +396,7 @@ theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X]
 
 section Normal
 
+@[to_additive]
 lemma smul_orbit_eq_orbit_smul (N : Subgroup G) [nN : N.Normal] (a : X) (g : G) :
     g • orbit N a = orbit N (g • a) := by
   simp only [orbit, Set.image_smul, Set.smul_set_range]
@@ -368,6 +413,7 @@ lemma smul_orbit_eq_orbit_smul (N : Subgroup G) [nN : N.Normal] (a : X) (g : G)
     simp only [← mul_assoc, ← smul_smul, smul_inv_smul, inv_inv]
 
 /-- An orbit of a normal subgroup is a block -/
+@[to_additive "An orbit of a normal subgroup is a block"]
 theorem IsBlock.orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) :
     IsBlock G (orbit N a) := by
   rw [isBlock_iff_smul_eq_or_disjoint]
@@ -376,6 +422,7 @@ theorem IsBlock.orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) :
   apply orbit.eq_or_disjoint
 
 /-- The orbits of a normal subgroup form a block system -/
+@[to_additive "The orbits of a normal subgroup form a block system"]
 theorem IsBlockSystem.of_normal {N : Subgroup G} [N.Normal] :
     IsBlockSystem G (Set.range fun a : X => orbit N a) := by
   constructor
@@ -436,6 +483,7 @@ section Stabilizer
   (Wielandt, th. 7.5) -/
 
 /-- The orbit of `a` under a subgroup containing the stabilizer of `a` is a block -/
+@[to_additive "The orbit of `a` under a subgroup containing the stabilizer of `a` is a block"]
 theorem IsBlock.of_orbit {H : Subgroup G} {a : X} (hH : stabilizer G a ≤ H) :
     IsBlock G (MulAction.orbit H a) := by
   rw [isBlock_iff_smul_eq_of_nonempty]
@@ -447,11 +495,14 @@ theorem IsBlock.of_orbit {H : Subgroup G} {a : X} (hH : stabilizer G a ≤ H) :
   simpa only [mem_stabilizer_iff, InvMemClass.coe_inv, mul_smul, inv_smul_eq_iff]
 
 /-- If `B` is a block containing `a`, then the stabilizer of `B` contains the stabilizer of `a` -/
+@[to_additive
+  "If `B` is a block containing `a`, then the stabilizer of `B` contains the stabilizer of `a`"]
 theorem IsBlock.stabilizer_le (hB : IsBlock G B) {a : X} (ha : a ∈ B) :
     stabilizer G a ≤ stabilizer G B :=
   fun g hg ↦ hB.smul_eq_of_nonempty ⟨a, by rwa [← hg, smul_mem_smul_set_iff], ha⟩
 
 /-- A block containing `a` is the orbit of `a` under its stabilizer -/
+@[to_additive "A block containing `a` is the orbit of `a` under its stabilizer"]
 theorem IsBlock.orbit_stabilizer_eq [IsPretransitive G X] (hB : IsBlock G B) {a : X} (ha : a ∈ B) :
     MulAction.orbit (stabilizer G B) a = B := by
   ext x
@@ -466,6 +517,9 @@ theorem IsBlock.orbit_stabilizer_eq [IsPretransitive G X] (hB : IsBlock G B) {a
 
 /-- A subgroup containing the stabilizer of `a`
   is the stabilizer of the orbit of `a` under that subgroup -/
+@[to_additive
+  "A subgroup containing the stabilizer of `a`
+  is the stabilizer of the orbit of `a` under that subgroup"]
 theorem stabilizer_orbit_eq {a : X} {H : Subgroup G} (hH : stabilizer G a ≤ H) :
     stabilizer G (orbit H a) = H := by
   ext g
@@ -482,6 +536,9 @@ variable (G)
 
 /-- Order equivalence between blocks in `X` containing a point `a`
  and subgroups of `G` containing the stabilizer of `a` (Wielandt, th. 7.5)-/
+@[to_additive
+  "Order equivalence between blocks in `X` containing a point `a`
+ and subgroups of `G` containing the stabilizer of `a` (Wielandt, th. 7.5)"]
 def block_stabilizerOrderIso [htGX : IsPretransitive G X] (a : X) :
     { B : Set X // a ∈ B ∧ IsBlock G B } ≃o Set.Ici (stabilizer G a) where
   toFun := fun ⟨B, ha, hB⟩ => ⟨stabilizer G B, hB.stabilizer_le ha⟩
@@ -512,6 +569,7 @@ namespace IsBlock
 
 variable [IsPretransitive G X] {B : Set X}
 
+@[to_additive]
 theorem ncard_block_eq_relindex (hB : IsBlock G B) {x : X} (hx : x ∈ B) :
     B.ncard = (stabilizer G x).relindex (stabilizer G B) := by
   have key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (stabilizer G B) x := by
@@ -520,18 +578,23 @@ theorem ncard_block_eq_relindex (hB : IsBlock G B) {x : X} (hx : x ∈ B) :
 
 /-- The cardinality of the ambient space is the product of the cardinality of a block
   by the cardinality of the set of translates of that block -/
+@[to_additive
+  "The cardinality of the ambient space is the product of the cardinality of a block
+  by the cardinality of the set of translates of that block"]
 theorem ncard_block_mul_ncard_orbit_eq (hB : IsBlock G B) (hB_ne : B.Nonempty) :
     Set.ncard B * Set.ncard (orbit G B) = Nat.card X := by
   obtain ⟨x, hx⟩ := hB_ne
   rw [ncard_block_eq_relindex hB hx, ← index_stabilizer,
       Subgroup.relindex_mul_index (hB.stabilizer_le hx), index_stabilizer_of_transitive]
 
 /-- The cardinality of a block divides the cardinality of the ambient type -/
+@[to_additive "The cardinality of a block divides the cardinality of the ambient type"]
 theorem ncard_dvd_card (hB : IsBlock G B) (hB_ne : B.Nonempty) :
     Set.ncard B ∣ Nat.card X :=
   Dvd.intro _ (hB.ncard_block_mul_ncard_orbit_eq hB_ne)
 
 /-- A too large block is equal to `univ` -/
+@[to_additive "A too large block is equal to `univ`"]
 theorem eq_univ_of_card_lt [hX : Finite X] (hB : IsBlock G B) (hB' : Nat.card X < Set.ncard B * 2) :
     B = Set.univ := by
   rcases Set.eq_empty_or_nonempty B with rfl | hB_ne
@@ -547,6 +610,7 @@ theorem eq_univ_of_card_lt [hX : Finite X] (hB : IsBlock G B) (hB' : Nat.card X
 @[deprecated (since := "2024-10-29")] alias eq_univ_card_lt := eq_univ_of_card_lt
 
 /-- If a block has too many translates, then it is a (sub)singleton  -/
+@[to_additive "If a block has too many translates, then it is a (sub)singleton"]
 theorem subsingleton_of_card_lt [Finite X] (hB : IsBlock G B)
     (hB' : Nat.card X < 2 * Set.ncard (orbit G B)) :
     B.Subsingleton := by
@@ -568,7 +632,10 @@ theorem subsingleton_of_card_lt [Finite X] (hB : IsBlock G B)
    are just `k + ℕ`, for `k ≤ 0`, and the corresponding intersection is `ℕ`, which is not a block.
    (Remark by Thomas Browning) -/
 /-- The intersection of the translates of a *finite* subset which contain a given point
-is a block (Wielandt, th. 7.3 )-/
+is a block (Wielandt, th. 7.3)-/
+@[to_additive
+  "The intersection of the translates of a *finite* subset which contain a given point
+  is a block (Wielandt, th. 7.3)"]
 theorem of_subset (a : X) (hfB : B.Finite) :
     IsBlock G (⋂ (k : G) (_ : a ∈ k • B), k • B) := by
   let B' := ⋂ (k : G) (_ : a ∈ k • B), k • B

Mathlib/GroupTheory/GroupAction/Pointwise.lean

@@ -29,6 +29,7 @@ import Mathlib.GroupTheory.GroupAction.Hom
 
 open Set Pointwise
 
+@[to_additive]
 theorem MulAction.smul_bijective_of_is_unit
     {M : Type*} [Monoid M] {α : Type*} [MulAction M α] {m : M} (hm : IsUnit m) :
     Function.Bijective (fun (a : α) ↦ m • a) := by
@@ -54,11 +55,13 @@ variable [FunLike F M N] [MulActionSemiHomClass F σ M N]
 -- "Left-hand side does not simplify, when using the simp lemma on itself."
 -- For now we will have to manually add `image_smul_setₛₗ _` to the `simp` argument list.
 -- TODO: when https://github.com/leanprover/lean4/issues/3107 is fixed, mark this as `@[simp]`.
+@[to_additive]
 theorem image_smul_setₛₗ :
     h '' (c • s) = σ c • h '' s := by
   simp only [← image_smul, image_image, map_smulₛₗ h]
 
 /-- Translation of preimage is contained in preimage of translation -/
+@[to_additive]
 theorem smul_preimage_set_leₛₗ :
     c • h ⁻¹' t ⊆ h ⁻¹' (σ c • t) := by
   rintro x ⟨y, hy, rfl⟩
@@ -67,6 +70,7 @@ theorem smul_preimage_set_leₛₗ :
 variable {c}
 
 /-- General version of `preimage_smul_setₛₗ` -/
+@[to_additive]
 theorem preimage_smul_setₛₗ'
     (hc : Function.Surjective (fun (m : M) ↦ c • m))
     (hc' : Function.Injective (fun (n : N) ↦ σ c • n)) :
@@ -82,6 +86,7 @@ theorem preimage_smul_setₛₗ'
   · exact smul_preimage_set_leₛₗ M N σ h c t
 
 /-- `preimage_smul_setₛₗ` when both scalars act by unit -/
+@[to_additive]
 theorem preimage_smul_setₛₗ_of_units (hc : IsUnit c) (hc' : IsUnit (σ c)) :
     h ⁻¹' (σ c • t) = c • h ⁻¹' t := by
   apply preimage_smul_setₛₗ'
@@ -90,13 +95,15 @@ theorem preimage_smul_setₛₗ_of_units (hc : IsUnit c) (hc' : IsUnit (σ c)) :
 
 
 /-- `preimage_smul_setₛₗ` in the context of a `MonoidHom` -/
+@[to_additive]
 theorem MonoidHom.preimage_smul_setₛₗ (σ : R →* S)
     {F : Type*} [FunLike F M N] [MulActionSemiHomClass F ⇑σ M N] (h : F)
     {c : R} (hc : IsUnit c) (t : Set N) :
     h ⁻¹' (σ c • t) = c • h ⁻¹' t :=
   preimage_smul_setₛₗ_of_units M N σ h t hc (IsUnit.map σ hc)
 
 /-- `preimage_smul_setₛₗ` in the context of a `MonoidHomClass` -/
+@[to_additive]
 theorem preimage_smul_setₛₗ
     {G : Type*} [FunLike G R S] [MonoidHomClass G R S] (σ : G)
     {F : Type*} [FunLike F M N] [MulActionSemiHomClass F σ M N] (h : F)
@@ -105,6 +112,7 @@ theorem preimage_smul_setₛₗ
  MonoidHom.preimage_smul_setₛₗ M N (σ : R →* S) h hc t
 
 /-- `preimage_smul_setₛₗ` in the context of a groups -/
+@[to_additive]
 theorem Group.preimage_smul_setₛₗ
     {R S : Type*} [Group R] [Group S] (σ : R → S)
     [MulAction R M] [MulAction S N]
@@ -121,21 +129,25 @@ variable (R)
 variable [FunLike F M₁ M₂] [MulActionHomClass F R M₁ M₂]
     (c : R) (s : Set M₁) (t : Set M₂)
 
-@[simp] -- This can be safely removed as a `@[simp]` lemma if `image_smul_setₛₗ` is readded.
+-- This can be safely removed as a `@[simp]` lemma if `image_smul_setₛₗ` is readded.
+@[to_additive (attr := simp)]
 theorem image_smul_set :
     h '' (c • s) = c • h '' s :=
   image_smul_setₛₗ _ _ _ h c s
 
+@[to_additive]
 theorem smul_preimage_set_le :
     c • h ⁻¹' t ⊆ h ⁻¹' (c • t) :=
   smul_preimage_set_leₛₗ _ _ _ h c t
 
 variable {c}
 
+@[to_additive]
 theorem preimage_smul_set (hc : IsUnit c) :
     h ⁻¹' (c • t) = c • h ⁻¹' t :=
   preimage_smul_setₛₗ_of_units _ _ _ h t hc hc
 
+@[to_additive]
 theorem Group.preimage_smul_set
     {R : Type*} [Group R] (M₁ M₂ : Type*)
     [MulAction R M₁] [MulAction R M₂]