move(algebra/hom/*): Move group hom files together (#12647)

Move * `algebra.group.freiman` to `algebra.hom.freiman` * `algebra.group.hom` to `algebra.hom.basic` * `algebra.group.hom_instances` to `algebra.hom.instances` * `algebra.group.units_hom` to `algebra.hom.units` * `algebra.group_action_hom` to `algebra.hom.group_action` * `algebra.iterate_hom` to `algebra.hom.iterate` * `algebra.non_unital_alg_hom` to `algebra.hom.non_unital_alg`
leanprover-community · Mar 25, 2022 · 172f317 · 172f317
1 parent 351c32f
commit 172f317
Show file tree

Hide file tree

Showing 34 changed files with 43 additions and 43 deletions.
diff --git a/src/algebra/algebra/bilinear.lean b/src/algebra/algebra/bilinear.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import algebra.algebra.basic
+import algebra.hom.iterate
 import linear_algebra.tensor_product
-import algebra.iterate_hom
 
 /-!
 # Facts about algebras involving bilinear maps and tensor products

diff --git a/src/algebra/char_p/basic.lean b/src/algebra/char_p/basic.lean
@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Joey van Langen, Casper Putz
 -/
 
+import algebra.hom.iterate
 import data.int.modeq
-import algebra.iterate_hom
+import data.nat.choose.dvd
 import data.nat.choose.sum
 import group_theory.order_of_element
-import data.nat.choose.dvd
 import ring_theory.nilpotent
 /-!
 # Characteristic of semirings

diff --git a/src/algebra/free.lean b/src/algebra/free.lean
@@ -3,10 +3,10 @@ Copyright (c) 2019 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import data.equiv.basic
+import algebra.hom.group
 import control.applicative
 import control.traversable.basic
-import algebra.group.hom
+import data.equiv.basic
 
 /-!
 # Free constructions

diff --git a/src/algebra/group/conj.lean b/src/algebra/group/conj.lean
@@ -3,11 +3,11 @@ Copyright (c) 2018  Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Chris Hughes, Michael Howes
 -/
-import data.fintype.basic
-import algebra.group.hom
 import algebra.group.semiconj
-import data.equiv.mul_add_aut
 import algebra.group_with_zero.basic
+import algebra.hom.group
+import data.equiv.mul_add_aut
+import data.fintype.basic
 
 /-!
 # Conjugacy of group elements

diff --git a/src/algebra/group/default.lean b/src/algebra/group/default.lean
@@ -3,10 +3,10 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Michael Howes
 -/
-import algebra.group.type_tags
 import algebra.group.conj
+import algebra.group.type_tags
 import algebra.group.with_one
-import algebra.group.units_hom
+import algebra.hom.units
 
 /-!
 # Various multiplicative and additive structures.

diff --git a/src/algebra/group/ext.lean b/src/algebra/group/ext.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Bryan Gin-ge Chen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bryan Gin-ge Chen, Yury Kudryashov
 -/
-import algebra.group.hom
+import algebra.hom.group
 
 /-!
 # Extensionality lemmas for monoid and group structures

diff --git a/src/algebra/group/pi.lean b/src/algebra/group/pi.lean
@@ -3,11 +3,11 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
+import algebra.hom.group_instances
 import data.pi
 import data.set.function
 import data.set.pairwise
 import tactic.pi_instances
-import algebra.group.hom_instances
 
 /-!
 # Pi instances for groups and monoids

diff --git a/src/algebra/group/type_tags.lean b/src/algebra/group/type_tags.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import algebra.group.hom
+import algebra.hom.group
 import data.equiv.basic
 /-!
 # Type tags that turn additive structures into multiplicative, and vice versa

diff --git a/src/algebra/group_with_zero/basic.lean b/src/algebra/group_with_zero/basic.lean
@@ -3,10 +3,10 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import logic.nontrivial
-import algebra.group.units_hom
 import algebra.group.inj_surj
 import algebra.group_with_zero.defs
+import algebra.hom.units
+import logic.nontrivial
 
 /-!
 # Groups with an adjoined zero element

diff --git a/src/algebra/group/freiman.lean → src/algebra/hom/freiman.lean b/src/algebra/group/freiman.lean → src/algebra/hom/freiman.lean
diff --git a/src/algebra/group/hom.lean → src/algebra/hom/group.lean b/src/algebra/group/hom.lean → src/algebra/hom/group.lean
diff --git a/src/algebra/group_action_hom.lean → src/algebra/hom/group_action.lean b/src/algebra/group_action_hom.lean → src/algebra/hom/group_action.lean
diff --git a/src/algebra/group/hom_instances.lean → src/algebra/hom/group_instances.lean b/src/algebra/group/hom_instances.lean → src/algebra/hom/group_instances.lean
diff --git a/src/algebra/iterate_hom.lean → src/algebra/hom/iterate.lean b/src/algebra/iterate_hom.lean → src/algebra/hom/iterate.lean
diff --git a/src/algebra/non_unital_alg_hom.lean → src/algebra/hom/non_unital_alg.lean b/src/algebra/non_unital_alg_hom.lean → src/algebra/hom/non_unital_alg.lean
diff --git a/src/algebra/group/units_hom.lean → src/algebra/hom/units.lean b/src/algebra/group/units_hom.lean → src/algebra/hom/units.lean
@@ -3,7 +3,8 @@ Copyright (c) 2018 Johan Commelin All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Chris Hughes, Kevin Buzzard
 -/
-import algebra.group.hom
+import algebra.hom.group
+
 /-!
 # Lift monoid homomorphisms to group homomorphisms of their units subgroups.
 -/

diff --git a/src/algebra/lie/non_unital_non_assoc_algebra.lean b/src/algebra/lie/non_unital_non_assoc_algebra.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import algebra.hom.non_unital_alg
 import algebra.lie.basic
-import algebra.non_unital_alg_hom
 
 /-!
 # Lie algebras as non-unital, non-associative algebras

diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean
@@ -4,10 +4,10 @@ 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.group.hom
+import algebra.hom.group
+import algebra.hom.group_action
 import algebra.module.basic
 import algebra.module.pi
-import algebra.group_action_hom
 import algebra.ring.comp_typeclasses
 import algebra.star.basic
 

diff --git a/src/algebra/monoid_algebra/basic.lean b/src/algebra/monoid_algebra/basic.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury G. Kudryashov, Scott Morrison
 -/
 import algebra.big_operators.finsupp
+import algebra.hom.non_unital_alg
 import linear_algebra.finsupp
-import algebra.non_unital_alg_hom
 
 /-!
 # Monoid algebras

diff --git a/src/algebra/order/hom/monoid.lean b/src/algebra/order/hom/monoid.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import algebra.group.hom
+import algebra.hom.group
 import algebra.order.with_zero
 import order.hom.basic
 

diff --git a/src/algebra/polynomial/group_ring_action.lean b/src/algebra/polynomial/group_ring_action.lean
@@ -3,10 +3,10 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import data.polynomial.monic
-import data.polynomial.algebra_map
 import algebra.group_ring_action
-import algebra.group_action_hom
+import algebra.hom.group_action
+import data.polynomial.algebra_map
+import data.polynomial.monic
 
 
 /-!

diff --git a/src/algebra/regular/pow.lean b/src/algebra/regular/pow.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import algebra.group_power.basic
+import algebra.hom.iterate
 import algebra.regular.basic
-import algebra.iterate_hom
 
 /-!
 # Regular elements

diff --git a/src/category_theory/monoidal/discrete.lean b/src/category_theory/monoidal/discrete.lean
@@ -3,9 +3,9 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.monoidal.natural_transformation
+import algebra.hom.group
 import category_theory.discrete_category
-import algebra.group.hom
+import category_theory.monoidal.natural_transformation
 
 /-!
 # Monoids as discrete monoidal categories

diff --git a/src/category_theory/preadditive/default.lean b/src/category_theory/preadditive/default.lean
@@ -3,11 +3,11 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import algebra.group.hom
-import category_theory.limits.shapes.kernels
 import algebra.big_operators.basic
+import algebra.hom.group
 import algebra.module.basic
 import category_theory.endomorphism
+import category_theory.limits.shapes.kernels
 
 /-!
 # Preadditive categories

diff --git a/src/data/finsupp/basic.lean b/src/data/finsupp/basic.lean
@@ -3,9 +3,9 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Scott Morrison
 -/
-import data.finset.preimage
+import algebra.hom.group_action
 import algebra.indicator_function
-import algebra.group_action_hom
+import data.finset.preimage
 
 /-!
 # Type of functions with finite support

diff --git a/src/data/polynomial/derivative.lean b/src/data/polynomial/derivative.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
-import algebra.iterate_hom
+import algebra.hom.iterate
 import data.polynomial.eval
 
 /-!

diff --git a/src/deprecated/group.lean b/src/deprecated/group.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import algebra.group.type_tags
-import algebra.group.units_hom
+import algebra.hom.units
 import algebra.ring.basic
 import data.equiv.mul_add
 

diff --git a/src/dynamics/circle/rotation_number/translation_number.lean b/src/dynamics/circle/rotation_number/translation_number.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
-import algebra.iterate_hom
+import algebra.hom.iterate
 import analysis.specific_limits.basic
 import order.iterate
 import order.semiconj_Sup

diff --git a/src/field_theory/perfect_closure.lean b/src/field_theory/perfect_closure.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import algebra.char_p.basic
-import data.equiv.ring
 import algebra.group_with_zero.power
-import algebra.iterate_hom
+import algebra.hom.iterate
+import data.equiv.ring
 
 /-!
 # The perfect closure of a field

diff --git a/src/group_theory/group_action/defs.lean b/src/group_theory/group_action/defs.lean
@@ -3,9 +3,8 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Yury Kudryashov
 -/
-import algebra.group.defs
-import algebra.group.hom
 import algebra.group.type_tags
+import algebra.hom.group
 import algebra.opposites
 import logic.embedding
 

diff --git a/src/group_theory/group_action/sub_mul_action.lean b/src/group_theory/group_action/sub_mul_action.lean
@@ -3,7 +3,7 @@ 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.group_action_hom
+import algebra.hom.group_action
 import algebra.module.basic
 import data.set_like.basic
 import group_theory.group_action.basic

diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.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, Julian Kuelshammer
 -/
-import algebra.iterate_hom
+import algebra.hom.iterate
 import data.nat.modeq
 import data.set.pointwise
 import dynamics.periodic_pts

diff --git a/src/topology/algebra/group_completion.lean b/src/topology/algebra/group_completion.lean
@@ -3,9 +3,9 @@ Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl
 -/
-import algebra.group.hom_instances
-import topology.uniform_space.completion
+import algebra.hom.group_instances
 import topology.algebra.uniform_group
+import topology.uniform_space.completion
 
 /-!
 # Completion of topological groups:

diff --git a/test/simps.lean b/test/simps.lean
@@ -1,4 +1,4 @@
-import algebra.group.hom
+import algebra.hom.group
 import data.sum.basic
 import tactic.simps