[Merged by Bors] - chore(algebra/group_ring_action): docstring, move monoid.End to algebra/group/hom

src/algebra/group/hom.lean

@@ -179,7 +179,70 @@ omit mP
 @[simp, to_additive] lemma comp_id (f : M →* N) : f.comp (id M) = f := ext $ λ x, rfl
 @[simp, to_additive] lemma id_comp (f : M →* N) : (id N).comp f = f := ext $ λ x, rfl
 
-variables [mM] [mN]
+end monoid_hom
+
+section End
+
+namespace monoid
+
+variables (M) [monoid M]
+
+/-- The monoid of endomorphisms. -/
+protected def End := M →* M
+
+namespace End
+
+instance : monoid (monoid.End M) :=
+{ mul := monoid_hom.comp,
+  one := monoid_hom.id M,
+  mul_assoc := λ _ _ _, monoid_hom.comp_assoc _ _ _,
+  mul_one := monoid_hom.comp_id,
+  one_mul := monoid_hom.id_comp }
+
+instance : inhabited (monoid.End M) := ⟨1⟩
+
+instance : has_coe_to_fun (monoid.End M) := ⟨_, monoid_hom.to_fun⟩
+
+end End
+
+@[simp] lemma coe_one : ((1 : monoid.End M) : M → M) = id := rfl
+@[simp] lemma coe_mul (f g) : ((f * g : monoid.End M) : M → M) = f ∘ g := rfl
+
+end monoid
+
+namespace add_monoid
+
+variables (A : Type*) [add_monoid A]
+
+/-- The monoid of endomorphisms. -/
+protected def End := A →+ A
+
+namespace End
+
+instance : monoid (add_monoid.End A) :=
+{ mul := add_monoid_hom.comp,
+  one := add_monoid_hom.id A,
+  mul_assoc := λ _ _ _, add_monoid_hom.comp_assoc _ _ _,
+  mul_one := add_monoid_hom.comp_id,
+  one_mul := add_monoid_hom.id_comp }
+
+instance : inhabited (add_monoid.End A) := ⟨1⟩
+
+instance : has_coe_to_fun (add_monoid.End A) := ⟨_, add_monoid_hom.to_fun⟩
+
+end End
+
+@[simp] lemma coe_one : ((1 : add_monoid.End A) : A → A) = id := rfl
+@[simp] lemma coe_mul (f g) : ((f * g : add_monoid.End A) : A → A) = f ∘ g := rfl
+
+end add_monoid
+
+end End
+
+namespace monoid_hom
+variables [mM : monoid M] [mN : monoid N] [mP : monoid P]
+variables [group G] [comm_group H]
+include mM mN
 
 /-- `1` is the monoid homomorphism sending all elements to `1`. -/
 @[to_additive]

src/algebra/group_ring_action.lean

@@ -2,14 +2,31 @@
 Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
-
-Group action on rings.
 -/
 
 import group_theory.group_action
 import data.equiv.ring
 import data.polynomial.monic
 
+/-!
+# Group action on rings
+
+This file defines the typeclass of monoid acting on semirings `mul_semiring_action M R`,
+and the corresponding typeclass of invariant subrings.
+
+Note that `algebra` does not satisfy the axioms of `mul_semiring_action`.
+
+## Implementation notes
+
+There is no separate typeclass for group acting on rings, group acting on fields, etc.
+They are all grouped under `mul_semiring_action`.
+
+## Tags
+
+group action, invariant subring
+
+-/
+
 universes u v
 open_locale big_operators
 
@@ -49,32 +66,6 @@ def distrib_mul_action.to_add_equiv [distrib_mul_action G A] (x : G) : A ≃+ A
 { .. distrib_mul_action.to_add_monoid_hom G A x,
   .. mul_action.to_perm G A x }
 
-/-- The monoid of endomorphisms. -/
-def monoid.End := M →* M
-
-instance monoid.End.monoid : monoid (monoid.End M) :=
-{ mul := monoid_hom.comp,
-  one := monoid_hom.id M,
-  mul_assoc := λ _ _ _, monoid_hom.comp_assoc _ _ _,
-  mul_one := monoid_hom.comp_id,
-  one_mul := monoid_hom.id_comp }
-
-instance monoid.End.inhabited : inhabited (monoid.End M) :=
-⟨1⟩
-
-/-- The monoid of endomorphisms. -/
-def add_monoid.End := A →+ A
-
-instance add_monoid.End.monoid : monoid (add_monoid.End A) :=
-{ mul := add_monoid_hom.comp,
-  one := add_monoid_hom.id A,
-  mul_assoc := λ _ _ _, add_monoid_hom.comp_assoc _ _ _,
-  mul_one := add_monoid_hom.comp_id,
-  one_mul := add_monoid_hom.id_comp }
-
-instance add_monoid.End.inhabited : inhabited (add_monoid.End A) :=
-⟨1⟩
-
 /-- Each element of the group defines an additive monoid homomorphism. -/
 def distrib_mul_action.hom_add_monoid_hom [distrib_mul_action M A] : M →* add_monoid.End A :=
 { to_fun := distrib_mul_action.to_add_monoid_hom M A,