Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit f0401b9

Browse files
committed
chore(ring_theory): split localization.lean and dedekind_domain.lean (#12206)
These files were rather long and had hundreds-deep dependency graphs. I split them into smaller files with less imports, so that they are easier to build and modify. Proof nothing was lost: ```bash $ cat src/ring_theory/localization/*.lean | sort | comm -23 <(sort src/ring_theory/localization.lean) - | grep -E 'lemma|theorem|def|instance|class' $ cat src/ring_theory/dedekind_domain/*.lean | sort | comm -23 <(sort src/ring_theory/dedekind_domain.lean) - | grep -E 'lemma|theorem|def|instance|class' giving three equivalent definitions (TODO: and shows that they are equivalent). ``` Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Splitting.20.60localization.2Elean.60.20and.20.60dedekind_domain.2Elean
1 parent deb5046 commit f0401b9

39 files changed

+3532
-3052
lines changed

src/algebra/category/CommRing/instances.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Andrew Yang
55
-/
66
import algebra.category.CommRing.basic
7-
import ring_theory.localization
7+
import ring_theory.localization.away
88

99
/-!
1010
# Ring-theoretic results in terms of categorical languages

src/algebra/char_p/algebra.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jon Eugster, Eric Wieser
55
-/
66
import algebra.char_p.basic
7-
import ring_theory.localization
7+
import ring_theory.localization.fraction_ring
88
import algebra.free_algebra
99

1010

src/algebraic_geometry/Spec.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Scott Morrison, Justus Springer
66
import algebraic_geometry.locally_ringed_space
77
import algebraic_geometry.structure_sheaf
88
import data.equiv.transfer_instance
9+
import ring_theory.localization.localization_localization
910
import topology.sheaves.sheaf_condition.sites
1011
import topology.sheaves.functors
1112

src/algebraic_geometry/prime_spectrum/basic.lean

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,13 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johan Commelin
55
-/
6-
import topology.opens
7-
import ring_theory.ideal.prod
8-
import ring_theory.ideal.over
9-
import linear_algebra.finsupp
106
import algebra.punit_instances
7+
import linear_algebra.finsupp
118
import ring_theory.nilpotent
9+
import ring_theory.localization.away
10+
import ring_theory.ideal.prod
11+
import ring_theory.ideal.over
12+
import topology.opens
1213
import topology.sober
1314

1415
/-!

src/algebraic_geometry/structure_sheaf.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ import algebraic_geometry.prime_spectrum.basic
77
import algebra.category.CommRing.colimits
88
import algebra.category.CommRing.limits
99
import topology.sheaves.local_predicate
10-
import ring_theory.localization
10+
import ring_theory.localization.at_prime
1111
import ring_theory.subring.basic
1212

1313
/-!

src/field_theory/ratfunc.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ Authors: Anne Baanen
66

77
import ring_theory.euclidean_domain
88
import ring_theory.laurent_series
9-
import ring_theory.localization
9+
import ring_theory.localization.fraction_ring
10+
import ring_theory.polynomial.content
1011

1112
/-!
1213
# The field of rational functions

src/linear_algebra/matrix/to_linear_equiv.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
66
import linear_algebra.matrix.nondegenerate
77
import linear_algebra.matrix.nonsingular_inverse
88
import linear_algebra.matrix.to_lin
9-
import ring_theory.localization
9+
import ring_theory.localization.fraction_ring
10+
import ring_theory.localization.integer
1011

1112
/-!
1213
# Matrices and linear equivalences

src/number_theory/class_number/finite.lean

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,12 @@ Authors: Anne Baanen
55
-/
66

77
import analysis.special_functions.pow
8-
import ring_theory.class_group
9-
import ring_theory.norm
108
import linear_algebra.free_module.pid
119
import linear_algebra.matrix.absolute_value
1210
import number_theory.class_number.admissible_absolute_value
11+
import ring_theory.class_group
12+
import ring_theory.dedekind_domain.integral_closure
13+
import ring_theory.norm
1314

1415
/-!
1516
# Class numbers of global fields

src/number_theory/function_field.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Anne Baanen, Ashvni Narayanan
55
-/
66
import field_theory.ratfunc
77
import ring_theory.algebraic
8-
import ring_theory.dedekind_domain
8+
import ring_theory.dedekind_domain.integral_closure
99
import ring_theory.integrally_closed
1010

1111
/-!

src/number_theory/number_field.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ Authors: Ashvni Narayanan, Anne Baanen
77
import algebra.field.basic
88
import data.rat.basic
99
import ring_theory.algebraic
10-
import ring_theory.dedekind_domain
10+
import ring_theory.dedekind_domain.integral_closure
1111
import ring_theory.integral_closure
1212
import ring_theory.polynomial.rational_root
1313

0 commit comments

Comments
 (0)