From e7bab9a85e92cf46c02cb4725a7be2f04691e3a7 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Sun, 8 Jan 2023 05:18:21 +0000
Subject: [PATCH] chore(algebra/group_ring_action/invariant): streamline
 imports (#18092)

The only file importing `algebra/group_ring_action/invariant` was `algebra/hom/group_action`.  This means that the material needing both files can safely be moved from `hom/group_action` to `group_ring_action/invariant`, while only decreasing the imports of anything else in the hierarchy.

This is worth doing since `group_ring_action/invariant` has another relatively heavy import (`ring_theory/subring/pointwise`).  After this rearrangement, `hom/group_action` should be ready to port.
---
 src/algebra/algebra/basic.lean               |  1 +
 src/algebra/group_ring_action/invariant.lean | 18 +++++++++++++++
 src/algebra/hom/group_action.lean            | 23 ++++----------------
 src/algebra/module/linear_map.lean           |  1 +
 src/field_theory/fixed.lean                  |  1 +
 src/ring_theory/ideal/quotient.lean          |  1 +
 6 files changed, 26 insertions(+), 19 deletions(-)

diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
index a20c4ffa7eb78..b478de90292dc 100644
--- a/src/algebra/algebra/basic.lean
+++ b/src/algebra/algebra/basic.lean
@@ -10,6 +10,7 @@ import algebra.ring.aut
 import algebra.ring.ulift
 import algebra.char_zero.lemmas
 import linear_algebra.span
+import ring_theory.subring.basic
 import tactic.abel
 
 /-!
diff --git a/src/algebra/group_ring_action/invariant.lean b/src/algebra/group_ring_action/invariant.lean
index 3e10bde74ee2b..f0f9a7d16a4a6 100644
--- a/src/algebra/group_ring_action/invariant.lean
+++ b/src/algebra/group_ring_action/invariant.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
+import algebra.hom.group_action
 import ring_theory.subring.pointwise
 
 /-! # Subrings invariant under an action -/
@@ -28,3 +29,20 @@ instance is_invariant_subring.to_mul_semiring_action [is_invariant_subring M S]
   smul_mul := λ m s₁ s₂, subtype.eq $ smul_mul' m s₁ s₂ }
 
 end ring
+
+section
+variables (M : Type*) [monoid M]
+variables {R' : Type*} [ring R'] [mul_semiring_action M R']
+variables (U : subring R') [is_invariant_subring M U]
+
+/-- The canonical inclusion from an invariant subring. -/
+def is_invariant_subring.subtype_hom : U →+*[M] R' :=
+{ map_smul' := λ m s, rfl, ..U.subtype }
+
+@[simp] theorem is_invariant_subring.coe_subtype_hom :
+  (is_invariant_subring.subtype_hom M U : U → R') = coe := rfl
+
+@[simp] theorem is_invariant_subring.coe_subtype_hom' :
+  (is_invariant_subring.subtype_hom M U : U →+* R') = U.subtype := rfl
+
+end
diff --git a/src/algebra/hom/group_action.lean b/src/algebra/hom/group_action.lean
index 4bc204da1c7d4..a2e4343592e30 100644
--- a/src/algebra/hom/group_action.lean
+++ b/src/algebra/hom/group_action.lean
@@ -3,9 +3,8 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import algebra.group_ring_action.invariant
-import group_theory.group_action.defs
-import group_theory.subgroup.basic
+import algebra.group_ring_action.basic
+import algebra.module.basic
 
 /-!
 # Equivariant homomorphisms
@@ -35,6 +34,8 @@ The above types have corresponding classes:
 
 -/
 
+assert_not_exists submonoid
+
 variables (M' : Type*)
 variables (X : Type*) [has_smul M' X]
 variables (Y : Type*) [has_smul M' Y]
@@ -50,7 +51,6 @@ variables (R' : Type*) [ring R'] [mul_semiring_action M R']
 variables (S : Type*) [semiring S] [mul_semiring_action M S]
 variables (S' : Type*) [ring S'] [mul_semiring_action M S']
 variables (T : Type*) [semiring T] [mul_semiring_action M T]
-variables (G : Type*) [group G] (H : subgroup G)
 
 set_option old_structure_cmd true
 
@@ -340,18 +340,3 @@ ext $ λ x, by rw [comp_apply, id_apply]
 ext $ λ x, by rw [comp_apply, id_apply]
 
 end mul_semiring_action_hom
-
-section
-variables (M) {R'} (U : subring R') [is_invariant_subring M U]
-
-/-- The canonical inclusion from an invariant subring. -/
-def is_invariant_subring.subtype_hom : U →+*[M] R' :=
-{ map_smul' := λ m s, rfl, ..U.subtype }
-
-@[simp] theorem is_invariant_subring.coe_subtype_hom :
-  (is_invariant_subring.subtype_hom M U : U → R') = coe := rfl
-
-@[simp] theorem is_invariant_subring.coe_subtype_hom' :
-  (is_invariant_subring.subtype_hom M U : U →+* R') = U.subtype := rfl
-
-end
diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean
index 96457fd912eb8..affad643cf562 100644
--- a/src/algebra/module/linear_map.lean
+++ b/src/algebra/module/linear_map.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne Baanen,
   Frédéric Dupuis, Heather Macbeth
 -/
+import algebra.big_operators.basic
 import algebra.hom.group_action
 import algebra.module.pi
 import algebra.star.basic
diff --git a/src/field_theory/fixed.lean b/src/field_theory/fixed.lean
index 599e38b164127..f8192a0368438 100644
--- a/src/field_theory/fixed.lean
+++ b/src/field_theory/fixed.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
+import algebra.group_ring_action.invariant
 import algebra.polynomial.group_ring_action
 import field_theory.normal
 import field_theory.separable
diff --git a/src/ring_theory/ideal/quotient.lean b/src/ring_theory/ideal/quotient.lean
index a1b0740ec5350..ce7a83a3f0eae 100644
--- a/src/ring_theory/ideal/quotient.lean
+++ b/src/ring_theory/ideal/quotient.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Chris Hughes, Mario Carneiro, Anne Baanen
 -/
 import algebra.ring.fin
+import algebra.ring.prod
 import linear_algebra.quotient
 import ring_theory.congruence
 import ring_theory.ideal.basic