From 4b262b8463002087e407be07080b91d213361e64 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 14 Nov 2022 06:55:43 +0000 Subject: [PATCH] refactor(topology/algebra/module/basic): don't import determinant (#17517) More files on the longest import chain in mathlib. Co-authored-by: Scott Morrison --- src/analysis/normed/field/basic.lean | 4 +++ src/analysis/normed_space/basic.lean | 1 + src/topology/algebra/algebra.lean | 1 + src/topology/algebra/module/basic.lean | 12 ------- src/topology/algebra/module/determinant.lean | 31 +++++++++++++++++++ .../algebra/module/finite_dimension.lean | 1 + src/topology/algebra/module/weak_dual.lean | 1 + 7 files changed, 39 insertions(+), 12 deletions(-) create mode 100644 src/topology/algebra/module/determinant.lean diff --git a/src/analysis/normed/field/basic.lean b/src/analysis/normed/field/basic.lean index 6439e69a9d53c..b03d62964bfc9 100644 --- a/src/analysis/normed/field/basic.lean +++ b/src/analysis/normed/field/basic.lean @@ -3,6 +3,7 @@ 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.algebra.subalgebra.basic import analysis.normed.group.infinite_sum import topology.algebra.module.basic import topology.instances.ennreal @@ -1013,3 +1014,6 @@ instance to_normed_comm_ring [normed_comm_ring R] [subring_class S R] (s : S) : { mul_comm := mul_comm, .. subring_class.to_normed_ring s } end subring_class + +-- Guard again import creep. +assert_not_exists restrict_scalars diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean index 6e8d418fabda2..bd87a3b7ba45f 100644 --- a/src/analysis/normed_space/basic.lean +++ b/src/analysis/normed_space/basic.lean @@ -3,6 +3,7 @@ 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.algebra.restrict_scalars import analysis.normed.field.basic import analysis.normed.group.infinite_sum import data.real.sqrt diff --git a/src/topology/algebra/algebra.lean b/src/topology/algebra/algebra.lean index f79c7f66f4cc1..a46420a82c09b 100644 --- a/src/topology/algebra/algebra.lean +++ b/src/topology/algebra/algebra.lean @@ -6,6 +6,7 @@ Authors: Scott Morrison import algebra.algebra.subalgebra.basic import topology.algebra.module.basic import topology.algebra.field +import ring_theory.adjoin.basic /-! # Topological (sub)algebras diff --git a/src/topology/algebra/module/basic.lean b/src/topology/algebra/module/basic.lean index ae512a0739c2b..d7a93e1e3db5e 100644 --- a/src/topology/algebra/module/basic.lean +++ b/src/topology/algebra/module/basic.lean @@ -11,7 +11,6 @@ import topology.uniform_space.uniform_embedding import algebra.algebra.basic import linear_algebra.projection import linear_algebra.pi -import linear_algebra.determinant import ring_theory.simple_module /-! @@ -1319,12 +1318,6 @@ end smul_rightₗ section comm_ring -/-- The determinant of a continuous linear map, mainly as a convenience device to be able to -write `A.det` instead of `(A : M →ₗ[R] M).det`. -/ -@[reducible] noncomputable def det {R : Type*} [comm_ring R] - {M : Type*} [topological_space M] [add_comm_group M] [module R M] (A : M →L[R] M) : R := -linear_map.det (A : M →ₗ[R] M) - variables {R : Type*} [comm_ring R] {M : Type*} [topological_space M] [add_comm_group M] @@ -1938,11 +1931,6 @@ def fin_two_arrow : (fin 2 → M) ≃L[R] M × M := end -@[simp] lemma det_coe_symm {R : Type*} [field R] - {M : Type*} [topological_space M] [add_comm_group M] [module R M] (A : M ≃L[R] M) : - (A.symm : M →L[R] M).det = (A : M →L[R] M).det ⁻¹ := -linear_equiv.det_coe_symm A.to_linear_equiv - end continuous_linear_equiv namespace continuous_linear_map diff --git a/src/topology/algebra/module/determinant.lean b/src/topology/algebra/module/determinant.lean new file mode 100644 index 0000000000000..e57201fa2bb0c --- /dev/null +++ b/src/topology/algebra/module/determinant.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis, + Heather Macbeth +-/ +import topology.algebra.module.basic +import linear_algebra.determinant + +/-! +# The determinant of a continuous linear map. +-/ + +namespace continuous_linear_map + +/-- The determinant of a continuous linear map, mainly as a convenience device to be able to +write `A.det` instead of `(A : M →ₗ[R] M).det`. -/ +@[reducible] noncomputable def det {R : Type*} [comm_ring R] + {M : Type*} [topological_space M] [add_comm_group M] [module R M] (A : M →L[R] M) : R := +linear_map.det (A : M →ₗ[R] M) + +end continuous_linear_map + +namespace continuous_linear_equiv + +@[simp] lemma det_coe_symm {R : Type*} [field R] + {M : Type*} [topological_space M] [add_comm_group M] [module R M] (A : M ≃L[R] M) : + (A.symm : M →L[R] M).det = (A : M →L[R] M).det ⁻¹ := +linear_equiv.det_coe_symm A.to_linear_equiv + +end continuous_linear_equiv diff --git a/src/topology/algebra/module/finite_dimension.lean b/src/topology/algebra/module/finite_dimension.lean index 2ab66f3826958..877d9486194a2 100644 --- a/src/topology/algebra/module/finite_dimension.lean +++ b/src/topology/algebra/module/finite_dimension.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel, Anatole Dedecker -/ import analysis.locally_convex.balanced_core_hull +import topology.algebra.module.determinant /-! # Finite dimensional topological vector spaces over complete fields diff --git a/src/topology/algebra/module/weak_dual.lean b/src/topology/algebra/module/weak_dual.lean index b69a3329ea8c2..5b1339fe4fb96 100644 --- a/src/topology/algebra/module/weak_dual.lean +++ b/src/topology/algebra/module/weak_dual.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kalle Kytölä, Moritz Doll -/ import topology.algebra.module.basic +import linear_algebra.bilinear_map /-! # Weak dual topology