chore(algebra/opposites): split group actions and division_ring into …

…their own files (#10383)

This splits out `group_theory.group_action.opposite` and `algebra.field.opposite` from `algebra.opposites`.
The motivation is to make opposite actions available slightly earlier in the import graph.
We probably want to split out `ring` at some point too, but that's likely a more annoying change so I've left it for future work.

These lemmas are just moved, and some `_root_` prefixes eliminated by removing the surrounding `namespace`.

src/algebra/char_p/invertible.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import algebra.invertible
-import algebra.field
+import algebra.field.basic
 import algebra.char_p.basic
 
 /-!

src/algebra/continued_fractions/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 -/
 import data.seq.seq
-import algebra.field
+import algebra.field.basic
 /-!
 # Basic Definitions/Theorems for Continued Fractions
 

src/algebra/euclidean_domain.lean

@@ -5,7 +5,7 @@ Authors: Louis Carlin, Mario Carneiro
 -/
 
 import data.int.basic
-import algebra.field
+import algebra.field.basic
 
 /-!
 # Euclidean domains

src/algebra/field/opposite.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+import algebra.field.basic
+import algebra.opposites
+
+/-!
+# Field structure on the multiplicative opposite
+-/
+
+variables (α : Type*)
+
+namespace mul_opposite
+
+instance [division_ring α] : division_ring αᵐᵒᵖ :=
+{ .. mul_opposite.group_with_zero α, .. mul_opposite.ring α }
+
+instance [field α] : field αᵐᵒᵖ :=
+{ .. mul_opposite.division_ring α, .. mul_opposite.comm_ring α }
+
+end mul_opposite

src/algebra/module/opposites.lean

@@ -3,14 +3,14 @@ Copyright (c) 2020 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import algebra.opposites
+import group_theory.group_action.opposite
 import data.equiv.module
 
 /-!
 # Module operations on `Mᵐᵒᵖ`
 
-This file contains definitions that could not be placed into `algebra.opposites` due to import
-cycles.
+This file contains definitions that build on top of the group action definitions in
+`group_theory.group_action.opposite`.
 -/
 
 namespace mul_opposite

src/algebra/opposites.lean

@@ -3,15 +3,14 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import algebra.field
 import algebra.group.commute
-import group_theory.group_action.defs
+import algebra.ring.basic
 import data.equiv.mul_add
 
 /-!
 # Multiplicative opposite and algebraic operations on it
 
-In this file we define `mul_oppposite α = αᵐᵒᵖ` to be the multiplicative opposite of `α`. It
+In this file we define `mul_opposite α = αᵐᵒᵖ` to be the multiplicative opposite of `α`. It
 inherits all additive algebraic structures on `α`, and reverses the order of multipliers in
 multiplicative structures, i.e., `op (x * y) = op x * op y`, where `mul_opposite.op` is the
 canonical map from `α` to `αᵐᵒᵖ`.
@@ -294,89 +293,6 @@ instance [group_with_zero α] : group_with_zero αᵐᵒᵖ :=
   .. mul_opposite.monoid_with_zero α, .. mul_opposite.div_inv_monoid α,
   .. mul_opposite.nontrivial α }
 
-instance [division_ring α] : division_ring αᵐᵒᵖ :=
-{ .. mul_opposite.group_with_zero α, .. mul_opposite.ring α }
-
-instance [field α] : field αᵐᵒᵖ :=
-{ .. mul_opposite.division_ring α, .. mul_opposite.comm_ring α }
-
-instance (R : Type*) [monoid R] [mul_action R α] : mul_action R αᵐᵒᵖ :=
-{ one_smul := λ x, unop_injective $ one_smul R (unop x),
-  mul_smul := λ r₁ r₂ x, unop_injective $ mul_smul r₁ r₂ (unop x),
-  .. mul_opposite.has_scalar α R }
-
-instance (R : Type*) [monoid R] [add_monoid α] [distrib_mul_action R α] :
-  distrib_mul_action R αᵐᵒᵖ :=
-{ smul_add := λ r x₁ x₂, unop_injective $ smul_add r (unop x₁) (unop x₂),
-  smul_zero := λ r, unop_injective $ smul_zero r,
-  .. mul_opposite.mul_action α R }
-
-instance (R : Type*) [monoid R] [monoid α] [mul_distrib_mul_action R α] :
-  mul_distrib_mul_action R αᵐᵒᵖ :=
-{ smul_mul := λ r x₁ x₂, unop_injective $ smul_mul' r (unop x₂) (unop x₁),
-  smul_one := λ r, unop_injective $ smul_one r,
-  .. mul_opposite.mul_action α R }
-
-instance {M N} [has_scalar M N] [has_scalar M α] [has_scalar N α] [is_scalar_tower M N α] :
-  is_scalar_tower M N αᵐᵒᵖ :=
-⟨λ x y z, unop_injective $ smul_assoc _ _ _⟩
-
-instance {M N} [has_scalar M α] [has_scalar N α] [smul_comm_class M N α] :
-  smul_comm_class M N αᵐᵒᵖ :=
-⟨λ x y z, unop_injective $ smul_comm _ _ _⟩
-
-/-- Like `has_mul.to_has_scalar`, but multiplies on the right.
-
-See also `monoid.to_opposite_mul_action` and `monoid_with_zero.to_opposite_mul_action`. -/
-instance _root_.has_mul.to_has_opposite_scalar [has_mul α] : has_scalar αᵐᵒᵖ α :=
-{ smul := λ c x, x * c.unop }
-
-@[simp] lemma op_smul_eq_mul [has_mul α] {a a' : α} : op a • a' = a' * a := rfl
-
--- TODO: add an additive version once we have additive opposites
-/-- The right regular action of a group on itself is transitive. -/
-instance _root_.mul_action.opposite_regular.is_pretransitive {G : Type*} [group G] :
-  mul_action.is_pretransitive Gᵐᵒᵖ G :=
-⟨λ x y, ⟨op (x⁻¹ * y), mul_inv_cancel_left _ _⟩⟩
-
-instance _root_.semigroup.opposite_smul_comm_class [semigroup α] :
-  smul_comm_class αᵐᵒᵖ α α :=
-{ smul_comm := λ x y z, (mul_assoc _ _ _) }
-
-instance _root_.semigroup.opposite_smul_comm_class' [semigroup α] :
-  smul_comm_class α αᵐᵒᵖ α :=
-{ smul_comm := λ x y z, (mul_assoc _ _ _).symm }
-
-/-- Like `monoid.to_mul_action`, but multiplies on the right. -/
-instance _root_.monoid.to_opposite_mul_action [monoid α] : mul_action αᵐᵒᵖ α :=
-{ smul := (•),
-  one_smul := mul_one,
-  mul_smul := λ x y r, (mul_assoc _ _ _).symm }
-
-instance _root_.is_scalar_tower.opposite_mid {M N} [monoid N] [has_scalar M N]
-  [smul_comm_class M N N] :
-  is_scalar_tower M Nᵐᵒᵖ N :=
-⟨λ x y z, mul_smul_comm _ _ _⟩
-
-instance _root_.smul_comm_class.opposite_mid {M N} [monoid N] [has_scalar M N]
-  [is_scalar_tower M N N] :
-  smul_comm_class M Nᵐᵒᵖ N :=
-⟨λ x y z, by { induction y using mul_opposite.rec, simp [smul_mul_assoc] }⟩
-
--- The above instance does not create an unwanted diamond, the two paths to
--- `mul_action αᵐᵒᵖ αᵐᵒᵖ` are defeq.
-example [monoid α] : monoid.to_mul_action αᵐᵒᵖ = mul_opposite.mul_action α αᵐᵒᵖ := rfl
-
-/-- `monoid.to_opposite_mul_action` is faithful on cancellative monoids. -/
-instance _root_.left_cancel_monoid.to_has_faithful_opposite_scalar [left_cancel_monoid α] :
-  has_faithful_scalar αᵐᵒᵖ α :=
-⟨λ x y h, unop_injective $ mul_left_cancel (h 1)⟩
-
-/-- `monoid.to_opposite_mul_action` is faithful on nontrivial cancellative monoids with zero. -/
-instance _root_.cancel_monoid_with_zero.to_has_faithful_opposite_scalar
-  [cancel_monoid_with_zero α] [nontrivial α] : has_faithful_scalar αᵐᵒᵖ α :=
-⟨λ x y h, unop_injective $ mul_left_cancel₀ one_ne_zero (h 1)⟩
-
 variable {α}
 
 lemma semiconj_by.op [has_mul α] {a x y : α} (h : semiconj_by a x y) :

src/algebra/order/field.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
-import algebra.field
+import algebra.field.basic
 import algebra.group_power.order
 import algebra.order.ring
 import tactic.monotonicity.basic

src/algebra/periodic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Benjamin Davidson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Benjamin Davidson
 -/
+import algebra.field.opposite
 import algebra.module.basic
 import algebra.order.archimedean
 import data.int.parity

src/algebra/smul_with_zero.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import algebra.group_power.basic
-import algebra.opposites
+import group_theory.group_action.opposite
 
 /-!
 # Introduce `smul_with_zero`

src/algebra/star/basic.lean

@@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import tactic.apply_fun
+import algebra.field.opposite
 import algebra.field_power
 import data.equiv.ring_aut
 import group_theory.group_action.units
+import group_theory.group_action.opposite
 import algebra.ring.comp_typeclasses
 
 /-!

src/data/equiv/ring.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
 import data.equiv.mul_add
-import algebra.field
+import algebra.field.basic
 import algebra.opposites
 import algebra.big_operators.basic
 

src/data/equiv/transfer_instance.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import algebra.algebra.basic
-import algebra.field
+import algebra.field.basic
 import algebra.group.type_tags
 import ring_theory.ideal.local_ring
 import data.equiv.basic

src/group_theory/group_action/opposite.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2020 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import algebra.opposites
+import group_theory.group_action.defs
+
+/-!
+# Scalar actions on and by `Mᵐᵒᵖ`
+
+This file defines the actions on the opposite type `has_scalar R Mᵐᵒᵖ`, and actions by the opposite
+type, `has_scalar Rᵐᵒᵖ M`.
+
+Note that `mul_opposite.has_scalar` is provided in an earlier file as it is needed to provide the
+`add_monoid.nsmul` and `add_comm_group.gsmul` fields.
+-/
+
+variables (α : Type*)
+
+/-! ### Actions _on_ the opposite type
+
+Actions on the opposite type just act on the underlying type.
+-/
+
+namespace mul_opposite
+
+instance (R : Type*) [monoid R] [mul_action R α] : mul_action R αᵐᵒᵖ :=
+{ one_smul := λ x, unop_injective $ one_smul R (unop x),
+  mul_smul := λ r₁ r₂ x, unop_injective $ mul_smul r₁ r₂ (unop x),
+  .. mul_opposite.has_scalar α R }
+
+instance (R : Type*) [monoid R] [add_monoid α] [distrib_mul_action R α] :
+  distrib_mul_action R αᵐᵒᵖ :=
+{ smul_add := λ r x₁ x₂, unop_injective $ smul_add r (unop x₁) (unop x₂),
+  smul_zero := λ r, unop_injective $ smul_zero r,
+  .. mul_opposite.mul_action α R }
+
+instance (R : Type*) [monoid R] [monoid α] [mul_distrib_mul_action R α] :
+  mul_distrib_mul_action R αᵐᵒᵖ :=
+{ smul_mul := λ r x₁ x₂, unop_injective $ smul_mul' r (unop x₂) (unop x₁),
+  smul_one := λ r, unop_injective $ smul_one r,
+  .. mul_opposite.mul_action α R }
+
+instance {M N} [has_scalar M N] [has_scalar M α] [has_scalar N α] [is_scalar_tower M N α] :
+  is_scalar_tower M N αᵐᵒᵖ :=
+⟨λ x y z, unop_injective $ smul_assoc _ _ _⟩
+
+instance {M N} [has_scalar M α] [has_scalar N α] [smul_comm_class M N α] :
+  smul_comm_class M N αᵐᵒᵖ :=
+⟨λ x y z, unop_injective $ smul_comm _ _ _⟩
+
+end mul_opposite
+
+/-! ### Actions _by_ the opposite type (right actions)
+
+In `has_mul.to_has_scalar` in another file, we define the left action `a₁ • a₂ = a₁ * a₂`. For the
+multiplicative opposite, we define `mul_opposite.op a₁ • a₂ = a₂ * a₁`, with the multiplication
+reversed.
+-/
+
+open mul_opposite
+
+/-- Like `has_mul.to_has_scalar`, but multiplies on the right.
+
+See also `monoid.to_opposite_mul_action` and `monoid_with_zero.to_opposite_mul_action_with_zero`. -/
+instance has_mul.to_has_opposite_scalar [has_mul α] : has_scalar αᵐᵒᵖ α :=
+{ smul := λ c x, x * c.unop }
+
+@[simp] lemma op_smul_eq_mul [has_mul α] {a a' : α} : op a • a' = a' * a := rfl
+
+-- TODO: add an additive version once we have additive opposites
+/-- The right regular action of a group on itself is transitive. -/
+instance mul_action.opposite_regular.is_pretransitive {G : Type*} [group G] :
+  mul_action.is_pretransitive Gᵐᵒᵖ G :=
+⟨λ x y, ⟨op (x⁻¹ * y), mul_inv_cancel_left _ _⟩⟩
+
+instance semigroup.opposite_smul_comm_class [semigroup α] :
+  smul_comm_class αᵐᵒᵖ α α :=
+{ smul_comm := λ x y z, (mul_assoc _ _ _) }
+
+instance semigroup.opposite_smul_comm_class' [semigroup α] :
+  smul_comm_class α αᵐᵒᵖ α :=
+{ smul_comm := λ x y z, (mul_assoc _ _ _).symm }
+
+/-- Like `monoid.to_mul_action`, but multiplies on the right. -/
+instance monoid.to_opposite_mul_action [monoid α] : mul_action αᵐᵒᵖ α :=
+{ smul := (•),
+  one_smul := mul_one,
+  mul_smul := λ x y r, (mul_assoc _ _ _).symm }
+
+instance is_scalar_tower.opposite_mid {M N} [monoid N] [has_scalar M N]
+  [smul_comm_class M N N] :
+  is_scalar_tower M Nᵐᵒᵖ N :=
+⟨λ x y z, mul_smul_comm _ _ _⟩
+
+instance smul_comm_class.opposite_mid {M N} [monoid N] [has_scalar M N]
+  [is_scalar_tower M N N] :
+  smul_comm_class M Nᵐᵒᵖ N :=
+⟨λ x y z, by { induction y using mul_opposite.rec, simp [smul_mul_assoc] }⟩
+
+-- The above instance does not create an unwanted diamond, the two paths to
+-- `mul_action αᵐᵒᵖ αᵐᵒᵖ` are defeq.
+example [monoid α] : monoid.to_mul_action αᵐᵒᵖ = mul_opposite.mul_action α αᵐᵒᵖ := rfl
+
+/-- `monoid.to_opposite_mul_action` is faithful on cancellative monoids. -/
+instance left_cancel_monoid.to_has_faithful_opposite_scalar [left_cancel_monoid α] :
+  has_faithful_scalar αᵐᵒᵖ α :=
+⟨λ x y h, unop_injective $ mul_left_cancel (h 1)⟩
+
+/-- `monoid.to_opposite_mul_action` is faithful on nontrivial cancellative monoids with zero. -/
+instance cancel_monoid_with_zero.to_has_faithful_opposite_scalar
+  [cancel_monoid_with_zero α] [nontrivial α] : has_faithful_scalar αᵐᵒᵖ α :=
+⟨λ x y h, unop_injective $ mul_left_cancel₀ one_ne_zero (h 1)⟩

src/group_theory/group_action/prod.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Eric Wieser
 -/
 import algebra.group.prod
+import group_theory.group_action.defs
 
 /-!
 # Prod instances for additive and multiplicative actions

src/group_theory/submonoid/operations.lean

@@ -9,6 +9,7 @@ import group_theory.submonoid.basic
 import data.equiv.mul_add
 import algebra.group.prod
 import algebra.group.inj_surj
+import group_theory.group_action.defs
 
 /-!
 # Operations on `submonoid`s

src/number_theory/number_field.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ashvni Narayanan, Anne Baanen
 -/
 
-import algebra.field
+import algebra.field.basic
 import data.rat.basic
 import ring_theory.algebraic
 import ring_theory.dedekind_domain

src/number_theory/pythagorean_triples.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Paul van Wamelen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul van Wamelen
 -/
-import algebra.field
+import algebra.field.basic
 import ring_theory.int.basic
 import algebra.group_with_zero.power
 import tactic.ring