refactor(algebra/group_ring_action): split out subobject actions (#17786

) This moves: * Instances for `submonoid` and `subgroup` to a new `algebra.group_ring_action.subobjects` module * Instances for `subsemiring` and `subring` inline with the other smul instances * `invariant_subring` to its own file The argument goes that `mul_semiring_action` is just `mul_distrib_mul_action` + `ring`, so should be available as early as possible in the import hierarchy where both are already available. Cutting out subobject dependencies makes this easier.
leanprover-community · Dec 2, 2022 · afad8e4 · afad8e4
1 parent 70d50ec
commit afad8e4
Show file tree

Hide file tree

Showing 15 changed files with 82 additions and 60 deletions.
diff --git a/src/algebra/group_ring_action.lean → src/algebra/group_ring_action/basic.lean b/src/algebra/group_ring_action.lean → src/algebra/group_ring_action/basic.lean
@@ -5,8 +5,8 @@ Authors: Kenny Lau
 -/
 
 import algebra.ring.equiv
+import algebra.field.defs
 import group_theory.group_action.group
-import ring_theory.subring.basic
 
 /-!
 # Group action on rings
@@ -28,7 +28,6 @@ group action, invariant subring
 -/
 
 universes u v
-open_locale big_operators
 
 /-- Typeclass for multiplicative actions by monoids on semirings.
 
@@ -78,35 +77,6 @@ See note [reducible non-instances]. -/
 
 end
 
-section
-variables {M G R}
-
-/-- A stronger version of `submonoid.distrib_mul_action`. -/
-instance submonoid.mul_semiring_action [mul_semiring_action M R] (H : submonoid M) :
-  mul_semiring_action H R :=
-{ smul := (•),
-  .. H.mul_distrib_mul_action,
-  .. H.distrib_mul_action }
-
-/-- A stronger version of `subgroup.distrib_mul_action`. -/
-instance subgroup.mul_semiring_action [mul_semiring_action G R] (H : subgroup G) :
-  mul_semiring_action H R :=
-H.to_submonoid.mul_semiring_action
-
-/-- A stronger version of `subsemiring.distrib_mul_action`. -/
-instance subsemiring.mul_semiring_action {R'} [semiring R'] [mul_semiring_action R' R]
-  (H : subsemiring R') :
-  mul_semiring_action H R :=
-H.to_submonoid.mul_semiring_action
-
-/-- A stronger version of `subring.distrib_mul_action`. -/
-instance subring.mul_semiring_action {R'} [ring R'] [mul_semiring_action R' R]
-  (H : subring R') :
-  mul_semiring_action H R :=
-H.to_subsemiring.mul_semiring_action
-
-end
-
 section simp_lemmas
 
 variables {M G A R F}
@@ -121,25 +91,3 @@ map_inv₀ (mul_semiring_action.to_ring_hom M F x) _
 end simp_lemmas
 
 end semiring
-
-section ring
-
-variables (M : Type u) [monoid M] {R : Type v} [ring R] [mul_semiring_action M R]
-variables (S : subring R)
-open mul_action
-
-/-- A typeclass for subrings invariant under a `mul_semiring_action`. -/
-class is_invariant_subring : Prop :=
-(smul_mem : ∀ (m : M) {x : R}, x ∈ S → m • x ∈ S)
-
-instance is_invariant_subring.to_mul_semiring_action [is_invariant_subring M S] :
-  mul_semiring_action M S :=
-{ smul := λ m x, ⟨m • x, is_invariant_subring.smul_mem m x.2⟩,
-  one_smul := λ s, subtype.eq $ one_smul M s,
-  mul_smul := λ m₁ m₂ s, subtype.eq $ mul_smul m₁ m₂ s,
-  smul_add := λ m s₁ s₂, subtype.eq $ smul_add m s₁ s₂,
-  smul_zero := λ m, subtype.eq $ smul_zero m,
-  smul_one := λ m, subtype.eq $ smul_one m,
-  smul_mul := λ m s₁ s₂, subtype.eq $ smul_mul' m s₁ s₂ }
-
-end ring
diff --git a/src/algebra/group_ring_action/invariant.lean b/src/algebra/group_ring_action/invariant.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import ring_theory.subring.pointwise
+
+/-! # Subrings invariant under an action -/
+section ring
+
+variables (M R : Type*) [monoid M] [ring R] [mul_semiring_action M R]
+variables (S : subring R)
+open mul_action
+variables {R}
+
+/-- A typeclass for subrings invariant under a `mul_semiring_action`. -/
+class is_invariant_subring : Prop :=
+(smul_mem : ∀ (m : M) {x : R}, x ∈ S → m • x ∈ S)
+
+instance is_invariant_subring.to_mul_semiring_action [is_invariant_subring M S] :
+  mul_semiring_action M S :=
+{ smul := λ m x, ⟨m • x, is_invariant_subring.smul_mem m x.2⟩,
+  one_smul := λ s, subtype.eq $ one_smul M s,
+  mul_smul := λ m₁ m₂ s, subtype.eq $ mul_smul m₁ m₂ s,
+  smul_add := λ m s₁ s₂, subtype.eq $ smul_add m s₁ s₂,
+  smul_zero := λ m, subtype.eq $ smul_zero m,
+  smul_one := λ m, subtype.eq $ smul_one m,
+  smul_mul := λ m s₁ s₂, subtype.eq $ smul_mul' m s₁ s₂ }
+
+end ring
diff --git a/src/algebra/group_ring_action/subobjects.lean b/src/algebra/group_ring_action/subobjects.lean
@@ -0,0 +1,32 @@
+/-
+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.group_ring_action.basic
+import group_theory.subgroup.basic
+
+/-!
+# Instances of `mul_semiring_action` for subobjects
+
+These are defined in this file as `semiring`s are not available yet where `submonoid` and `subgroup`
+are defined.
+
+Instances for `subsemiring` and `subring` are provided next to the other scalar actions instances
+for those subobjects.
+
+-/
+variables {M G R : Type*}
+variables [monoid M] [group G] [semiring R]
+
+/-- A stronger version of `submonoid.distrib_mul_action`. -/
+instance submonoid.mul_semiring_action [mul_semiring_action M R] (H : submonoid M) :
+  mul_semiring_action H R :=
+{ smul := (•),
+  .. H.mul_distrib_mul_action,
+  .. H.distrib_mul_action }
+
+/-- A stronger version of `subgroup.distrib_mul_action`. -/
+instance subgroup.mul_semiring_action [mul_semiring_action G R] (H : subgroup G) :
+  mul_semiring_action H R :=
+H.to_submonoid.mul_semiring_action
diff --git a/src/algebra/hom/group_action.lean b/src/algebra/hom/group_action.lean
@@ -3,8 +3,9 @@ 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
+import algebra.group_ring_action.invariant
 import group_theory.group_action.defs
+import group_theory.subgroup.basic
 
 /-!
 # Equivariant homomorphisms

diff --git a/src/algebra/polynomial/group_ring_action.lean b/src/algebra/polynomial/group_ring_action.lean
@@ -3,7 +3,7 @@ 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
+import algebra.group_ring_action.basic
 import algebra.hom.group_action
 import data.polynomial.algebra_map
 import data.polynomial.monic

diff --git a/src/algebra/punit_instances.lean b/src/algebra/punit_instances.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau
 
 import algebra.module.basic
 import algebra.gcd_monoid.basic
-import algebra.group_ring_action
+import algebra.group_ring_action.basic
 import group_theory.group_action.defs
 
 /-!

diff --git a/src/algebra/ring/aut.lean b/src/algebra/ring/aut.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
-import algebra.group_ring_action
+import algebra.group_ring_action.basic
 import algebra.hom.aut
 import algebra.ring.equiv
 

diff --git a/src/algebra/star/basic.lean b/src/algebra/star/basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import algebra.big_operators.basic
 import algebra.ring.aut
 import algebra.ring.comp_typeclasses
 import data.rat.cast

diff --git a/src/algebra/star/prod.lean b/src/algebra/star/prod.lean
@@ -5,6 +5,7 @@ Authors: Eric Wieser
 -/
 import algebra.star.basic
 import algebra.ring.prod
+import algebra.module.prod
 
 /-!
 # `star` on product types

diff --git a/src/algebra/star/unitary.lean b/src/algebra/star/unitary.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Frédéric Dupuis
 -/
 import algebra.star.basic
+import group_theory.submonoid.operations
 
 /-!
 # Unitary elements of a star monoid

diff --git a/src/group_theory/group_action/conj_act.lean b/src/group_theory/group_action/conj_act.lean
@@ -5,7 +5,7 @@ Authors: Chris Hughes
 -/
 import group_theory.group_action.basic
 import group_theory.subgroup.basic
-import algebra.group_ring_action
+import algebra.group_ring_action.basic
 /-!
 # Conjugation action of a group on itself
 

diff --git a/src/ring_theory/subring/basic.lean b/src/ring_theory/subring/basic.lean
@@ -1142,6 +1142,10 @@ S.to_subsemiring.mul_action_with_zero
 instance [add_comm_monoid α] [module R α] (S : subring R) : module S α :=
 S.to_subsemiring.module
 
+/-- The action by a subsemiring is the action by the underlying ring. -/
+instance [semiring α] [mul_semiring_action R α] (S : subring R) : mul_semiring_action S α :=
+S.to_submonoid.mul_semiring_action
+
 /-- The center of a semiring acts commutatively on that semiring. -/
 instance center.smul_comm_class_left : smul_comm_class (center R) R R :=
 subsemiring.center.smul_comm_class_left

diff --git a/src/ring_theory/subring/pointwise.lean b/src/ring_theory/subring/pointwise.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import ring_theory.subring.basic
-import algebra.group_ring_action
 import group_theory.subgroup.pointwise
 import ring_theory.subsemiring.pointwise
 import data.set.pointwise.basic

diff --git a/src/ring_theory/subsemiring/basic.lean b/src/ring_theory/subsemiring/basic.lean
@@ -8,6 +8,7 @@ import algebra.module.basic
 import algebra.ring.equiv
 import algebra.ring.prod
 import algebra.order.ring.inj_surj
+import algebra.group_ring_action.subobjects
 import data.set.finite
 import group_theory.submonoid.centralizer
 import group_theory.submonoid.membership
@@ -1082,6 +1083,10 @@ mul_action_with_zero.comp_hom _ S.subtype.to_monoid_with_zero_hom
 instance [add_comm_monoid α] [module R' α] (S : subsemiring R') : module S α :=
 { smul := (•), .. module.comp_hom _ S.subtype }
 
+/-- The action by a subsemiring is the action by the underlying semiring. -/
+instance [semiring α] [mul_semiring_action R' α] (S : subsemiring R') : mul_semiring_action S α :=
+S.to_submonoid.mul_semiring_action
+
 /-- The center of a semiring acts commutatively on that semiring. -/
 instance center.smul_comm_class_left : smul_comm_class (center R') R' R' :=
 submonoid.center.smul_comm_class_left

diff --git a/src/ring_theory/subsemiring/pointwise.lean b/src/ring_theory/subsemiring/pointwise.lean
@@ -3,7 +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.group_ring_action
+import algebra.group_ring_action.basic
 import ring_theory.subsemiring.basic
 import group_theory.submonoid.pointwise
 import data.set.pointwise.basic