chore(order/hom): rearrange definitions of order_{hom,iso,embedding} (

#10752) We symmetrize the locations of `rel_{hom,iso,embedding}` and `order_{hom,iso,embedding}` by putting the `rel_` definitions in `order/rel_iso.lean` and the `order_` definitions in `order/hom/basic.lean`. (`order_hom.lean` needed to be split up to fix an import loop.) Requested by @YaelDillies. ## Moved definitions * `order_hom`, `order_iso`, `order_embedding` are now in `order/hom/basic.lean` * `order_hom.has_sup` ... `order_hom.complete_lattice` are now in `order/hom/lattice.lean` ## Other changes Some import cleanup.
leanprover-community · Dec 13, 2021 · 7181b3a · 7181b3a
1 parent b351ca9
commit 7181b3a
Show file tree

Hide file tree

Showing 16 changed files with 808 additions and 773 deletions.
diff --git a/src/algebra/lie/solvable.lean b/src/algebra/lie/solvable.lean
@@ -3,9 +3,9 @@ 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.lie.ideal_operations
 import algebra.lie.abelian
-import order.order_hom
+import algebra.lie.ideal_operations
+import order.hom.basic
 
 /-!
 # Solvable Lie algebras

diff --git a/src/algebra/order/monoid.lean b/src/algebra/order/monoid.lean
@@ -9,7 +9,7 @@ import algebra.group.prod
 import algebra.order.monoid_lemmas
 import order.bounded_order
 import order.min_max
-import order.rel_iso
+import order.hom.basic
 
 /-!
 # Ordered monoids

diff --git a/src/combinatorics/set_family/shadow.lean b/src/combinatorics/set_family/shadow.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Alena Gusakov, Yaël Dillies
 -/
 import data.finset.lattice
+import logic.function.iterate
 
 /-!
 # Shadows

diff --git a/src/data/finset/option.lean b/src/data/finset/option.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Mario Carneiro, Sean Leather
 -/
 import data.finset.basic
-import order.order_hom
+import order.hom.basic
 
 /-!
 # Finite sets in `option α`

diff --git a/src/data/nat/fib.lean b/src/data/nat/fib.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 -/
 import data.nat.gcd
+import logic.function.iterate
 import tactic.ring
 
 /-!

diff --git a/src/linear_algebra/eigenspace.lean b/src/linear_algebra/eigenspace.lean
@@ -5,10 +5,10 @@ Authors: Alexander Bentkamp
 -/
 
 import field_theory.is_alg_closed.basic
+import linear_algebra.charpoly.basic
 import linear_algebra.finsupp
 import linear_algebra.matrix.to_lin
-import order.order_hom
-import linear_algebra.charpoly.basic
+import order.hom.basic
 
 /-!
 # Eigenvectors and eigenvalues

diff --git a/src/order/category/Preorder.lean b/src/order/category/Preorder.lean
@@ -5,7 +5,7 @@ Authors: Johan Commelin
 -/
 import category_theory.concrete_category.bundled_hom
 import algebra.punit_instances
-import order.order_hom
+import order.hom.basic
 
 /-! # Category of preorders -/
 

diff --git a/src/order/closure.lean b/src/order/closure.lean
@@ -6,7 +6,7 @@ Authors: Bhavik Mehta, Yaël Dillies
 import data.set.lattice
 import data.set_like.basic
 import order.galois_connection
-import order.order_hom
+import order.hom.basic
 import tactic.monotonicity
 
 /-!

diff --git a/src/order/fixed_points.lean b/src/order/fixed_points.lean
@@ -3,8 +3,8 @@ 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, Kenny Lau, Yury Kudryashov
 -/
-import order.order_hom
 import dynamics.fixed_points.basic
+import order.hom.lattice
 
 /-!
 # Fixed point construction on complete lattices