chore(data/equiv): split and move to logic/equiv (#12929)

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rearranging.20files.20in.20.60data.2F.60 This PR rearranges files in `data/equiv/` by 1) moving bundled isomorphisms to a relevant subfolder of `algebra/`; 2) moving `denumerable` and `encodable` to `logic/`; 3) moving the remainder of `data/equiv/` to `logic/equiv/`. The commits of this PR correspond to those steps. In particular, the following files were moved: * `data/equiv/module.lean` → `algebra/module/equiv.lean` * `data/equiv/mul_add.lean` → `algebra/hom/equiv.lean` * `data/equiv/mul_add_aut.lean` → `algebra/hom/aut.lean` * `data/equiv/ring.lean` → `algebra/ring/equiv.lean` * `data/equiv/ring_aut.lean` → `algebra/ring/aut.lean` * `data/equiv/denumerable.lean` → `logic/denumerable.lean` * `data/equiv/encodable/*.lean` → `logic/encodable/basic.lean logic/encodable/lattice.lean logic/encodable/small.lean` * `data/equiv/*.lean` to: `logic/equiv/basic.lean logic/equiv/fin.lean logic/equiv/functor.lean logic/equiv/local_equiv.lean logic/equiv/option.lean logic/equiv/transfer_instance.lean logic/equiv/embedding.lean logic/equiv/fintype.lean logic/equiv/list.lean logic/equiv/nat.lean logic/equiv/set.lean`
leanprover-community · Mar 26, 2022 · cc8c90d · cc8c90d
1 parent 434a938
commit cc8c90d
Show file tree

Hide file tree

Showing 118 changed files with 148 additions and 148 deletions.
diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import algebra.module.basic
+import algebra.ring.aut
 import linear_algebra.span
 import tactic.abel
-import data.equiv.ring_aut
 
 /-!
 # Algebras over commutative semirings

diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean
@@ -5,8 +5,8 @@ Authors: Johannes Hölzl
 -/
 
 import algebra.group.pi
+import algebra.hom.equiv
 import algebra.ring.opposite
-import data.equiv.mul_add
 import data.finset.fold
 import data.fintype.basic
 import data.set.pairwise

diff --git a/src/algebra/category/CommRing/basic.lean b/src/algebra/category/CommRing/basic.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison, Johannes Hölzl, Yury Kudryashov
 -/
 import algebra.category.Group.basic
 import category_theory.concrete_category.reflects_isomorphisms
-import data.equiv.ring
+import algebra.ring.equiv
 
 /-!
 # Category instances for semiring, ring, comm_semiring, and comm_ring.

diff --git a/src/algebra/field_power.lean b/src/algebra/field_power.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
 import algebra.group_with_zero.power
+import algebra.ring.equiv
 import tactic.linarith
-import data.equiv.ring
 
 /-!
 # Integer power operation on fields and division rings

diff --git a/src/algebra/free.lean b/src/algebra/free.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau
 import algebra.hom.group
 import control.applicative
 import control.traversable.basic
-import data.equiv.basic
+import logic.equiv.basic
 
 /-!
 # Free constructions

diff --git a/src/algebra/group/conj.lean b/src/algebra/group/conj.lean
@@ -5,8 +5,8 @@ Authors: Patrick Massot, Chris Hughes, Michael Howes
 -/
 import algebra.group.semiconj
 import algebra.group_with_zero.basic
+import algebra.hom.aut
 import algebra.hom.group
-import data.equiv.mul_add_aut
 import data.fintype.basic
 
 /-!

diff --git a/src/algebra/group/opposite.lean b/src/algebra/group/opposite.lean
@@ -5,8 +5,8 @@ Authors: Kenny Lau
 -/
 import algebra.group.inj_surj
 import algebra.group.commute
+import algebra.hom.equiv
 import algebra.opposites
-import data.equiv.mul_add
 
 /-!
 # Group structures on the multiplicative and additive opposites

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

diff --git a/src/algebra/group/ulift.lean b/src/algebra/group/ulift.lean
@@ -3,7 +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 data.equiv.mul_add
+import algebra.hom.equiv
 
 /-!
 # `ulift` instances for groups and monoids

diff --git a/src/algebra/group/with_one.lean b/src/algebra/group/with_one.lean
@@ -3,10 +3,10 @@ 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.ring.basic
-import data.equiv.basic
-import data.equiv.mul_add
-import data.equiv.option
+import logic.equiv.basic
+import logic.equiv.option
 
 /-!
 # Adjoining a zero/one to semigroups and related algebraic structures

diff --git a/src/algebra/group_ring_action.lean b/src/algebra/group_ring_action.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
-import data.equiv.ring
+import algebra.ring.equiv
 import group_theory.group_action.group
 import ring_theory.subring.basic
 

diff --git a/src/data/equiv/mul_add_aut.lean → src/algebra/hom/aut.lean b/src/data/equiv/mul_add_aut.lean → src/algebra/hom/aut.lean
diff --git a/src/data/equiv/mul_add.lean → src/algebra/hom/equiv.lean b/src/data/equiv/mul_add.lean → src/algebra/hom/equiv.lean
diff --git a/src/algebra/lie/basic.lean b/src/algebra/lie/basic.lean
@@ -3,10 +3,10 @@ Copyright (c) 2019 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import tactic.noncomm_ring
-import data.equiv.module
+import algebra.module.equiv
 import data.bracket
 import linear_algebra.basic
+import tactic.noncomm_ring
 
 /-!
 # Lie algebras

diff --git a/src/data/equiv/module.lean → src/algebra/module/equiv.lean b/src/data/equiv/module.lean → src/algebra/module/equiv.lean
diff --git a/src/algebra/module/opposites.lean b/src/algebra/module/opposites.lean
@@ -3,8 +3,8 @@ 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.module.equiv
 import group_theory.group_action.opposite
-import data.equiv.module
 
 /-!
 # Module operations on `Mᵐᵒᵖ`

diff --git a/src/algebra/module/submodule.lean b/src/algebra/module/submodule.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import algebra.module.linear_map
-import data.equiv.module
+import algebra.module.equiv
 import group_theory.group_action.sub_mul_action
 /-!
 

diff --git a/src/algebra/module/ulift.lean b/src/algebra/module/ulift.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.ring.ulift
-import data.equiv.module
+import algebra.module.equiv
 
 /-!
 # `ulift` instances for module and multiplicative actions

diff --git a/src/algebra/opposites.lean b/src/algebra/opposites.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import algebra.group.defs
-import data.equiv.basic
+import logic.equiv.basic
 import logic.nontrivial
 
 /-!

diff --git a/src/algebra/order/hom/ring.lean b/src/algebra/order/hom/ring.lean
@@ -5,7 +5,7 @@ Authors: Alex J. Best, Yaël Dillies
 -/
 import algebra.order.hom.monoid
 import algebra.order.ring
-import data.equiv.ring
+import algebra.ring.equiv
 
 /-!
 # Ordered ring homomorphisms

diff --git a/src/algebra/order/monoid.lean b/src/algebra/order/monoid.lean
@@ -6,8 +6,8 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 import algebra.group.with_one
 import algebra.group.type_tags
 import algebra.group.prod
+import algebra.hom.equiv
 import algebra.order.monoid_lemmas
-import data.equiv.mul_add
 import order.bounded_order
 import order.min_max
 import order.hom.basic

diff --git a/src/algebra/quandle.lean b/src/algebra/quandle.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
+import algebra.hom.equiv
 import data.zmod.basic
-import data.equiv.mul_add
 import tactic.group
 
 /-!

diff --git a/src/algebra/quaternion.lean b/src/algebra/quaternion.lean
@@ -3,10 +3,10 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import tactic.ring_exp
 import algebra.algebra.basic
+import algebra.ring.equiv
 import algebra.ring.opposite
-import data.equiv.ring
+import tactic.ring_exp
 
 /-!
 # Quaternions

diff --git a/src/data/equiv/ring_aut.lean → src/algebra/ring/aut.lean b/src/data/equiv/ring_aut.lean → src/algebra/ring/aut.lean
@@ -3,8 +3,8 @@ 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 data.equiv.mul_add_aut
-import data.equiv.ring
+import algebra.hom.aut
+import algebra.ring.equiv
 
 /-!
 # Ring automorphisms

diff --git a/src/algebra/ring/comp_typeclasses.lean b/src/algebra/ring/comp_typeclasses.lean
@@ -5,7 +5,7 @@ Authors: Frédéric Dupuis, Heather Macbeth
 -/
 
 import algebra.ring.basic
-import data.equiv.ring
+import algebra.ring.equiv
 
 /-!
 # Propositional typeclasses on several ring homs

diff --git a/src/data/equiv/ring.lean → src/algebra/ring/equiv.lean b/src/data/equiv/ring.lean → src/algebra/ring/equiv.lean
@@ -3,10 +3,10 @@ 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 data.equiv.mul_add
+import algebra.big_operators.basic
 import algebra.field.basic
+import algebra.hom.equiv
 import algebra.ring.opposite
-import algebra.big_operators.basic
 
 /-!
 # (Semi)ring equivs

diff --git a/src/algebra/ring/prod.lean b/src/algebra/ring/prod.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Chris Hughes, Mario Carneiro, Yury Kudryashov
 -/
 import algebra.group.prod
 import algebra.ring.basic
-import data.equiv.ring
+import algebra.ring.equiv
 
 /-!
 # Semiring, ring etc structures on `R × S`

diff --git a/src/algebra/ring/ulift.lean b/src/algebra/ring/ulift.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.group.ulift
-import data.equiv.ring
+import algebra.ring.equiv
 
 /-!
 # `ulift` instances for ring

diff --git a/src/algebra/star/basic.lean b/src/algebra/star/basic.lean
@@ -6,7 +6,7 @@ Authors: Scott Morrison
 import tactic.apply_fun
 import algebra.field.opposite
 import algebra.field_power
-import data.equiv.ring_aut
+import algebra.ring.aut
 import group_theory.group_action.units
 import group_theory.group_action.opposite
 import algebra.ring.comp_typeclasses

diff --git a/src/algebra/star/module.lean b/src/algebra/star/module.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser, Frédéric Dupuis
 -/
 import algebra.star.self_adjoint
-import data.equiv.module
+import algebra.module.equiv
 import linear_algebra.prod
 
 /-!

diff --git a/src/algebraic_geometry/Spec.lean b/src/algebraic_geometry/Spec.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison, Justus Springer
 -/
 import algebraic_geometry.locally_ringed_space
 import algebraic_geometry.structure_sheaf
-import data.equiv.transfer_instance
+import logic.equiv.transfer_instance
 import ring_theory.localization.localization_localization
 import topology.sheaves.sheaf_condition.sites
 import topology.sheaves.functors

diff --git a/src/algebraic_geometry/locally_ringed_space.lean b/src/algebraic_geometry/locally_ringed_space.lean
@@ -6,7 +6,7 @@ Authors: Johan Commelin
 
 import algebraic_geometry.ringed_space
 import algebraic_geometry.stalks
-import data.equiv.transfer_instance
+import logic.equiv.transfer_instance
 
 /-!
 # The category of locally ringed spaces

diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel, Yury Kudryashov
 -/
 import analysis.calculus.formal_multilinear_series
 import analysis.specific_limits.normed
-import data.equiv.fin
+import logic.equiv.fin
 
 /-!
 # Analytic functions

diff --git a/src/category_theory/endomorphism.lean b/src/category_theory/endomorphism.lean
@@ -3,9 +3,9 @@ Copyright (c) 2019 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Scott Morrison, Simon Hudon
 -/
+import algebra.hom.equiv
 import category_theory.groupoid
 import category_theory.opposites
-import data.equiv.mul_add
 import group_theory.group_action.defs
 
 /-!

diff --git a/src/category_theory/functor/fully_faithful.lean b/src/category_theory/functor/fully_faithful.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.natural_isomorphism
-import data.equiv.basic
+import logic.equiv.basic
 
 /-!
 # Full and faithful functors

diff --git a/src/category_theory/limits/constructions/finite_products_of_binary_products.lean b/src/category_theory/limits/constructions/finite_products_of_binary_products.lean
@@ -8,7 +8,7 @@ import category_theory.limits.preserves.shapes.products
 import category_theory.limits.shapes.binary_products
 import category_theory.limits.shapes.finite_products
 import category_theory.pempty
-import data.equiv.fin
+import logic.equiv.fin
 
 /-!
 # Constructing finite products from binary products and terminal.

diff --git a/src/category_theory/preadditive/opposite.lean b/src/category_theory/preadditive/opposite.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison, Adam Topaz
 -/
 import category_theory.preadditive
 import category_theory.preadditive.additive_functor
-import data.equiv.transfer_instance
+import logic.equiv.transfer_instance
 
 /-!
 # If `C` is preadditive, `Cᵒᵖ` has a natural preadditive structure.

diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean
@@ -5,7 +5,7 @@ Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl
 -/
 import category_theory.epi_mono
 import category_theory.functor.fully_faithful
-import data.equiv.basic
+import logic.equiv.basic
 
 /-!
 # The category `Type`.

diff --git a/src/combinatorics/derangements/basic.lean b/src/combinatorics/derangements/basic.lean
@@ -3,10 +3,10 @@ Copyright (c) 2021 Henry Swanson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henry Swanson
 -/
-import data.equiv.basic
-import data.equiv.option
 import dynamics.fixed_points.basic
 import group_theory.perm.option
+import logic.equiv.basic
+import logic.equiv.option
 
 /-!
 # Derangements on types

diff --git a/src/computability/primrec.lean b/src/computability/primrec.lean
@@ -3,8 +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
 -/
-import data.equiv.list
 import data.list.join
+import logic.equiv.list
 import logic.function.iterate
 
 /-!

diff --git a/src/control/equiv_functor.lean b/src/control/equiv_functor.lean
@@ -3,7 +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 data.equiv.basic
+import logic.equiv.basic
 
 /-!
 # Functions functorial with respect to equivalences

diff --git a/src/control/monad/basic.lean b/src/control/monad/basic.lean
@@ -3,8 +3,8 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
+import logic.equiv.basic
 import tactic.basic
-import data.equiv.basic
 
 /-!
 # Monad

diff --git a/src/control/monad/writer.lean b/src/control/monad/writer.lean
@@ -6,7 +6,7 @@ Authors: Simon Hudon
 The writer monad transformer for passing immutable state.
 -/
 import algebra.group.defs
-import data.equiv.basic
+import logic.equiv.basic
 
 universes u v w u₀ u₁ v₀ v₁