refactor(algebra/hom/equiv): split files

Author: kim-em

src/algebra/big_operators/basic.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 -/
 
 import algebra.group.pi
-import algebra.hom.equiv
+import algebra.hom.equiv.basic
 import algebra.ring.opposite
 import data.finset.fold
 import data.fintype.basic

src/algebra/category/Semigroup/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Julian Kuelshammer
 -/
 import algebra.pempty_instances
-import algebra.hom.equiv
+import algebra.hom.equiv.basic
 import category_theory.concrete_category.bundled_hom
 import category_theory.functor.reflects_isomorphisms
 import category_theory.elementwise

src/algebra/divisibility.lean

@@ -6,6 +6,7 @@ Neil Strickland, Aaron Anderson
 -/
 
 import algebra.hom.group
+import algebra.hom.units
 import algebra.group_with_zero.basic
 
 /-!

src/algebra/group/opposite.lean

@@ -5,7 +5,7 @@ Authors: Kenny Lau
 -/
 import algebra.group.inj_surj
 import algebra.group.commute
-import algebra.hom.equiv
+import algebra.hom.equiv.basic
 import algebra.opposites
 import data.int.cast.defs
 

src/algebra/group/prod.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
 -/
+import algebra.hom.equiv.units
 import algebra.group.opposite
 
 /-!

src/algebra/group/ulift.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import data.int.cast.defs
-import algebra.hom.equiv
+import algebra.hom.equiv.basic
+import algebra.group_with_zero.basic
 
 /-!
 # `ulift` instances for groups and monoids

src/algebra/group/with_one.lean

@@ -3,7 +3,8 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
 -/
-import algebra.hom.equiv
+import algebra.hom.equiv.basic
+import algebra.group_with_zero.units
 import algebra.ring.basic
 import logic.equiv.defs
 import logic.equiv.option

src/algebra/hom/commute.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2018 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hughes,
+  Johannes Hölzl, Yury Kudryashov
+-/
+import algebra.hom.group
+import algebra.group.commute
+
+/-!
+# Multiplicative homomorphisms respect semiconjugation and commutation.
+-/
+
+section commute
+
+variables {F M N : Type*} [has_mul M] [has_mul N] {a x y : M}
+
+@[simp, to_additive]
+protected lemma semiconj_by.map [mul_hom_class F M N] (h : semiconj_by a x y) (f : F) :
+  semiconj_by (f a) (f x) (f y) :=
+by simpa only [semiconj_by, map_mul] using congr_arg f h
+
+@[simp, to_additive]
+protected lemma commute.map [mul_hom_class F M N] (h : commute x y) (f : F) :
+  commute (f x) (f y) :=
+h.map f
+
+end commute

src/algebra/hom/equiv.lean src/algebra/hom/equiv/basic.leansrc/algebra/hom/equiv.lean renamed to src/algebra/hom/equiv/basic.lean

@@ -3,8 +3,9 @@ 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.type_tags
-import algebra.group_with_zero.units
+import algebra.hom.group
+import data.fun_like.equiv
+import logic.equiv.basic
 import data.pi.algebra
 
 /-!
@@ -524,74 +525,6 @@ def monoid_hom.to_mul_equiv [mul_one_class M] [mul_one_class N] (f : M →* N) (
   right_inv := monoid_hom.congr_fun h₂,
   map_mul' := f.map_mul }
 
-/-- A group is isomorphic to its group of units. -/
-@[to_additive "An additive group is isomorphic to its group of additive units"]
-def to_units [group G] : G ≃* Gˣ :=
-{ to_fun := λ x, ⟨x, x⁻¹, mul_inv_self _, inv_mul_self _⟩,
-  inv_fun := coe,
-  left_inv := λ x, rfl,
-  right_inv := λ u, units.ext rfl,
-  map_mul' := λ x y, units.ext rfl }
-
-@[simp, to_additive] lemma coe_to_units [group G] (g : G) :
-  (to_units g : G) = g := rfl
-
-namespace units
-
-variables [monoid M] [monoid N] [monoid P]
-
-/-- A multiplicative equivalence of monoids defines a multiplicative equivalence
-of their groups of units. -/
-def map_equiv (h : M ≃* N) : Mˣ ≃* Nˣ :=
-{ inv_fun := map h.symm.to_monoid_hom,
-  left_inv := λ u, ext $ h.left_inv u,
-  right_inv := λ u, ext $ h.right_inv u,
-  .. map h.to_monoid_hom }
-
-@[simp]
-lemma map_equiv_symm (h : M ≃* N) : (map_equiv h).symm = map_equiv h.symm :=
-rfl
-
-@[simp]
-lemma coe_map_equiv (h : M ≃* N) (x : Mˣ) : (map_equiv h x : N) = h x :=
-rfl
-
-/-- Left multiplication by a unit of a monoid is a permutation of the underlying type. -/
-@[to_additive "Left addition of an additive unit is a permutation of the underlying type.",
-  simps apply {fully_applied := ff}]
-def mul_left (u : Mˣ) : equiv.perm M :=
-{ to_fun    := λx, u * x,
-  inv_fun   := λx, ↑u⁻¹ * x,
-  left_inv  := u.inv_mul_cancel_left,
-  right_inv := u.mul_inv_cancel_left }
-
-@[simp, to_additive]
-lemma mul_left_symm (u : Mˣ) : u.mul_left.symm = u⁻¹.mul_left :=
-equiv.ext $ λ x, rfl
-
-@[to_additive]
-lemma mul_left_bijective (a : Mˣ) : function.bijective ((*) a : M → M) :=
-(mul_left a).bijective
-
-/-- Right multiplication by a unit of a monoid is a permutation of the underlying type. -/
-@[to_additive "Right addition of an additive unit is a permutation of the underlying type.",
-  simps apply {fully_applied := ff}]
-def mul_right (u : Mˣ) : equiv.perm M :=
-{ to_fun    := λx, x * u,
-  inv_fun   := λx, x * ↑u⁻¹,
-  left_inv  := λ x, mul_inv_cancel_right x u,
-  right_inv := λ x, inv_mul_cancel_right x u }
-
-@[simp, to_additive]
-lemma mul_right_symm (u : Mˣ) : u.mul_right.symm = u⁻¹.mul_right :=
-equiv.ext $ λ x, rfl
-
-@[to_additive]
-lemma mul_right_bijective (a : Mˣ) : function.bijective ((* a) : M → M) :=
-(mul_right a).bijective
-
-end units
-
 namespace equiv
 
 section has_involutive_neg
@@ -610,173 +543,4 @@ lemma inv_symm : (equiv.inv G).symm = equiv.inv G := rfl
 
 end has_involutive_neg
 
-section group
-variables [group G]
-
-/-- Left multiplication in a `group` is a permutation of the underlying type. -/
-@[to_additive "Left addition in an `add_group` is a permutation of the underlying type."]
-protected def mul_left (a : G) : perm G := (to_units a).mul_left
-
-@[simp, to_additive]
-lemma coe_mul_left (a : G) : ⇑(equiv.mul_left a) = (*) a := rfl
-
-/-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
-@[simp, nolint simp_nf,
-  to_additive "Extra simp lemma that `dsimp` can use. `simp` will never use this."]
-lemma mul_left_symm_apply (a : G) : ((equiv.mul_left a).symm : G → G) = (*) a⁻¹ := rfl
-
-@[simp, to_additive]
-lemma mul_left_symm (a : G) : (equiv.mul_left a).symm = equiv.mul_left a⁻¹ :=
-ext $ λ x, rfl
-
-@[to_additive]
-lemma _root_.group.mul_left_bijective (a : G) : function.bijective ((*) a) :=
-(equiv.mul_left a).bijective
-
-/-- Right multiplication in a `group` is a permutation of the underlying type. -/
-@[to_additive "Right addition in an `add_group` is a permutation of the underlying type."]
-protected def mul_right (a : G) : perm G := (to_units a).mul_right
-
-@[simp, to_additive]
-lemma coe_mul_right (a : G) : ⇑(equiv.mul_right a) = λ x, x * a := rfl
-
-@[simp, to_additive]
-lemma mul_right_symm (a : G) : (equiv.mul_right a).symm = equiv.mul_right a⁻¹ :=
-ext $ λ x, rfl
-
-/-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
-@[simp, nolint simp_nf,
-  to_additive "Extra simp lemma that `dsimp` can use. `simp` will never use this."]
-lemma mul_right_symm_apply (a : G) : ((equiv.mul_right a).symm : G → G) = λ x, x * a⁻¹ := rfl
-
-@[to_additive]
-lemma _root_.group.mul_right_bijective (a : G) : function.bijective (* a) :=
-(equiv.mul_right a).bijective
-
-/-- A version of `equiv.mul_left a b⁻¹` that is defeq to `a / b`. -/
-@[to_additive /-" A version of `equiv.add_left a (-b)` that is defeq to `a - b`. "-/, simps]
-protected def div_left (a : G) : G ≃ G :=
-{ to_fun := λ b, a / b,
-  inv_fun := λ b, b⁻¹ * a,
-  left_inv := λ b, by simp [div_eq_mul_inv],
-  right_inv := λ b, by simp [div_eq_mul_inv] }
-
-@[to_additive]
-lemma div_left_eq_inv_trans_mul_left (a : G) :
-  equiv.div_left a = (equiv.inv G).trans (equiv.mul_left a) :=
-ext $ λ _, div_eq_mul_inv _ _
-
-/-- A version of `equiv.mul_right a⁻¹ b` that is defeq to `b / a`. -/
-@[to_additive /-" A version of `equiv.add_right (-a) b` that is defeq to `b - a`. "-/, simps]
-protected def div_right (a : G) : G ≃ G :=
-{ to_fun := λ b, b / a,
-  inv_fun := λ b, b * a,
-  left_inv := λ b, by simp [div_eq_mul_inv],
-  right_inv := λ b, by simp [div_eq_mul_inv] }
-
-@[to_additive]
-lemma div_right_eq_mul_right_inv (a : G) : equiv.div_right a = equiv.mul_right a⁻¹ :=
-ext $ λ _, div_eq_mul_inv _ _
-
-end group
-
-section group_with_zero
-variables [group_with_zero G]
-
-/-- Left multiplication by a nonzero element in a `group_with_zero` is a permutation of the
-underlying type. -/
-@[simps {fully_applied := ff}]
-protected def mul_left₀ (a : G) (ha : a ≠ 0) : perm G :=
-(units.mk0 a ha).mul_left
-
-lemma _root_.mul_left_bijective₀ (a : G) (ha : a ≠ 0) :
-  function.bijective ((*) a : G → G) :=
-(equiv.mul_left₀ a ha).bijective
-
-/-- Right multiplication by a nonzero element in a `group_with_zero` is a permutation of the
-underlying type. -/
-@[simps {fully_applied := ff}]
-protected def mul_right₀ (a : G) (ha : a ≠ 0) : perm G :=
-(units.mk0 a ha).mul_right
-
-lemma _root_.mul_right_bijective₀ (a : G) (ha : a ≠ 0) :
-  function.bijective ((* a) : G → G) :=
-(equiv.mul_right₀ a ha).bijective
-
-end group_with_zero
-
 end equiv
-
-/-- In a `division_comm_monoid`, `equiv.inv` is a `mul_equiv`. There is a variant of this
-`mul_equiv.inv' G : G ≃* Gᵐᵒᵖ` for the non-commutative case. -/
-@[to_additive "When the `add_group` is commutative, `equiv.neg` is an `add_equiv`.", simps apply]
-def mul_equiv.inv (G : Type*) [division_comm_monoid G] : G ≃* G :=
-{ to_fun   := has_inv.inv,
-  inv_fun  := has_inv.inv,
-  map_mul' := mul_inv,
-  ..equiv.inv G }
-
-@[simp] lemma mul_equiv.inv_symm (G : Type*) [division_comm_monoid G] :
-  (mul_equiv.inv G).symm = mul_equiv.inv G := rfl
-
-section type_tags
-
-/-- Reinterpret `G ≃+ H` as `multiplicative G ≃* multiplicative H`. -/
-def add_equiv.to_multiplicative [add_zero_class G] [add_zero_class H] :
-  (G ≃+ H) ≃ (multiplicative G ≃* multiplicative H) :=
-{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative,
-                  f.symm.to_add_monoid_hom.to_multiplicative, f.3, f.4, f.5⟩,
-  inv_fun := λ f, ⟨f.to_monoid_hom, f.symm.to_monoid_hom, f.3, f.4, f.5⟩,
-  left_inv := λ x, by { ext, refl, },
-  right_inv := λ x, by { ext, refl, }, }
-
-/-- Reinterpret `G ≃* H` as `additive G ≃+ additive H`. -/
-def mul_equiv.to_additive [mul_one_class G] [mul_one_class H] :
-  (G ≃* H) ≃ (additive G ≃+ additive H) :=
-{ to_fun := λ f, ⟨f.to_monoid_hom.to_additive, f.symm.to_monoid_hom.to_additive, f.3, f.4, f.5⟩,
-  inv_fun := λ f, ⟨f.to_add_monoid_hom, f.symm.to_add_monoid_hom, f.3, f.4, f.5⟩,
-  left_inv := λ x, by { ext, refl, },
-  right_inv := λ x, by { ext, refl, }, }
-
-/-- Reinterpret `additive G ≃+ H` as `G ≃* multiplicative H`. -/
-def add_equiv.to_multiplicative' [mul_one_class G] [add_zero_class H] :
-  (additive G ≃+ H) ≃ (G ≃* multiplicative H) :=
-{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative',
-                  f.symm.to_add_monoid_hom.to_multiplicative'', f.3, f.4, f.5⟩,
-  inv_fun := λ f, ⟨f.to_monoid_hom, f.symm.to_monoid_hom, f.3, f.4, f.5⟩,
-  left_inv := λ x, by { ext, refl, },
-  right_inv := λ x, by { ext, refl, }, }
-
-/-- Reinterpret `G ≃* multiplicative H` as `additive G ≃+ H` as. -/
-def mul_equiv.to_additive' [mul_one_class G] [add_zero_class H] :
-  (G ≃* multiplicative H) ≃ (additive G ≃+ H) :=
-add_equiv.to_multiplicative'.symm
-
-/-- Reinterpret `G ≃+ additive H` as `multiplicative G ≃* H`. -/
-def add_equiv.to_multiplicative'' [add_zero_class G] [mul_one_class H] :
-  (G ≃+ additive H) ≃ (multiplicative G ≃* H) :=
-{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative'',
-                  f.symm.to_add_monoid_hom.to_multiplicative', f.3, f.4, f.5⟩,
-  inv_fun := λ f, ⟨f.to_monoid_hom, f.symm.to_monoid_hom, f.3, f.4, f.5⟩,
-  left_inv := λ x, by { ext, refl, },
-  right_inv := λ x, by { ext, refl, }, }
-
-/-- Reinterpret `multiplicative G ≃* H` as `G ≃+ additive H` as. -/
-def mul_equiv.to_additive'' [add_zero_class G] [mul_one_class H] :
-  (multiplicative G ≃* H) ≃ (G ≃+ additive H) :=
-add_equiv.to_multiplicative''.symm
-
-end type_tags
-
-section
-variables (G) (H)
-
-/-- `additive (multiplicative G)` is just `G`. -/
-def add_equiv.additive_multiplicative [add_zero_class G] : additive (multiplicative G) ≃+ G :=
-mul_equiv.to_additive'' (mul_equiv.refl (multiplicative G))
-
-/-- `multiplicative (additive H)` is just `H`. -/
-def mul_equiv.multiplicative_additive [mul_one_class H] : multiplicative (additive H) ≃* H :=
-add_equiv.to_multiplicative'' (add_equiv.refl (additive H))
-
-end