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

@@ -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
 
 /-!

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

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

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

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

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