chore(algebra/algebra): reduce imports for algebra.algebra.tower (#…

…17476)

This splits `algebra.algebra.tower` into two files: `algebra.algebra.tower.basic` and `algebra.algebra.subalgebra.tower`.

The motivation behind this PR is that `algebra.algebra.tower` is a relatively fundamental and popular file to import (especially since it used to contain `is_scalar_tower`), but its import tree also includes relatively complicated files such as `ring_theory.ideal.operations`. By splitting off these less popular dependencies we can save quite a bit of complexity in the import graph.



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

src/algebra/algebra/subalgebra/tower.lean

@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Anne Baanen
+-/
+
+import algebra.algebra.subalgebra.basic
+import algebra.algebra.tower
+
+/-!
+# Subalgebras in towers of algebras
+
+In this file we prove facts about subalgebras in towers of algebra.
+
+An algebra tower A/S/R is expressed by having instances of `algebra A S`,
+`algebra R S`, `algebra R A` and `is_scalar_tower R S A`, the later asserting the
+compatibility condition `(r • s) • a = r • (s • a)`.
+
+## Main results
+
+ * `is_scalar_tower.subalgebra`: if `A/S/R` is a tower and `S₀` is a subalgebra
+   between `S` and `R`, then `A/S/S₀` is a tower
+ * `is_scalar_tower.subalgebra'`: if `A/S/R` is a tower and `S₀` is a subalgebra
+   between `S` and `R`, then `A/S₀/R` is a tower
+ * `subalgebra.restrict_scalars`: turn an `S`-subalgebra of `A` into an `R`-subalgebra of `A`,
+   given that `A/S/R` is a tower
+
+-/
+
+open_locale pointwise
+universes u v w u₁ v₁
+
+variables (R : Type u) (S : Type v) (A : Type w) (B : Type u₁) (M : Type v₁)
+
+namespace algebra
+
+variables [comm_semiring R] [semiring A] [algebra R A]
+variables [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M]
+
+variables {A}
+
+lemma lmul_algebra_map (x : R) :
+  algebra.lmul R A (algebra_map R A x) = algebra.lsmul R A x :=
+eq.symm $ linear_map.ext $ smul_def x
+
+end algebra
+
+namespace is_scalar_tower
+
+section semiring
+variables [comm_semiring R] [comm_semiring S] [semiring A]
+variables [algebra R S] [algebra S A]
+
+variables (R S A)
+
+instance subalgebra (S₀ : subalgebra R S) : is_scalar_tower S₀ S A :=
+of_algebra_map_eq $ λ x, rfl
+
+variables [algebra R A] [is_scalar_tower R S A]
+
+instance subalgebra' (S₀ : subalgebra R S) : is_scalar_tower R S₀ A :=
+@is_scalar_tower.of_algebra_map_eq R S₀ A _ _ _ _ _ _ $ λ _,
+(is_scalar_tower.algebra_map_apply R S A _ : _)
+
+end semiring
+
+end is_scalar_tower
+
+namespace subalgebra
+
+open is_scalar_tower
+
+section semiring
+
+variables (R) {S A B} [comm_semiring R] [comm_semiring S] [semiring A] [semiring B]
+variables [algebra R S] [algebra S A] [algebra R A] [algebra S B] [algebra R B]
+variables [is_scalar_tower R S A] [is_scalar_tower R S B]
+
+/-- Given a tower `A / ↥U / S / R` of algebras, where `U` is an `S`-subalgebra of `A`, reinterpret
+`U` as an `R`-subalgebra of `A`. -/
+def restrict_scalars (U : subalgebra S A) : subalgebra R A :=
+{ algebra_map_mem' := λ x, by { rw algebra_map_apply R S A, exact U.algebra_map_mem _ },
+  .. U }
+
+@[simp] lemma coe_restrict_scalars {U : subalgebra S A} :
+  (restrict_scalars R U : set A) = (U : set A) := rfl
+
+@[simp] lemma restrict_scalars_top : restrict_scalars R (⊤ : subalgebra S A) = ⊤ :=
+set_like.coe_injective rfl
+
+@[simp] lemma restrict_scalars_to_submodule {U : subalgebra S A} :
+  (U.restrict_scalars R).to_submodule = U.to_submodule.restrict_scalars R :=
+set_like.coe_injective rfl
+
+@[simp] lemma mem_restrict_scalars {U : subalgebra S A} {x : A} :
+  x ∈ restrict_scalars R U ↔ x ∈ U := iff.rfl
+
+lemma restrict_scalars_injective :
+  function.injective (restrict_scalars R : subalgebra S A → subalgebra R A) :=
+λ U V H, ext $ λ x, by rw [← mem_restrict_scalars R, H, mem_restrict_scalars]
+
+/-- Produces an `R`-algebra map from `U.restrict_scalars R` given an `S`-algebra map from `U`.
+
+This is a special case of `alg_hom.restrict_scalars` that can be helpful in elaboration. -/
+@[simp]
+def of_restrict_scalars (U : subalgebra S A) (f : U →ₐ[S] B) : U.restrict_scalars R →ₐ[R] B :=
+f.restrict_scalars R
+
+end semiring
+
+end subalgebra
+
+namespace is_scalar_tower
+
+open subalgebra
+
+variables [comm_semiring R] [comm_semiring S] [comm_semiring A]
+variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
+
+theorem adjoin_range_to_alg_hom (t : set A) :
+  (algebra.adjoin (to_alg_hom R S A).range t).restrict_scalars R =
+    (algebra.adjoin S t).restrict_scalars R :=
+subalgebra.ext $ λ z,
+show z ∈ subsemiring.closure (set.range (algebra_map (to_alg_hom R S A).range A) ∪ t : set A) ↔
+  z ∈ subsemiring.closure (set.range (algebra_map S A) ∪ t : set A),
+from suffices set.range (algebra_map (to_alg_hom R S A).range A) = set.range (algebra_map S A),
+  by rw this,
+by { ext z, exact ⟨λ ⟨⟨x, y, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y, hy⟩, ⟨⟨z, y, hy⟩, rfl⟩⟩ }
+
+end is_scalar_tower

src/algebra/algebra/tower.lean

@@ -1,11 +1,10 @@
 /-
 Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kenny Lau
+Authors: Kenny Lau, Anne Baanen
 -/
 
-import algebra.algebra.subalgebra.basic
-import algebra.algebra.bilinear
+import algebra.algebra.basic
 
 /-!
 # Towers of algebras
@@ -47,10 +46,6 @@ def lsmul : A →ₐ[R] module.End R M :=
 
 @[simp] lemma lsmul_coe (a : A) : (lsmul R M a : M → M) = (•) a := rfl
 
-lemma lmul_algebra_map (x : R) :
-  algebra.lmul R A (algebra_map R A x) = algebra.lsmul R A x :=
-eq.symm $ linear_map.ext $ smul_def x
-
 end algebra
 
 namespace is_scalar_tower
@@ -84,9 +79,6 @@ of_algebra_map_eq $ ring_hom.ext_iff.1 h
 
 variables (R S A)
 
-instance subalgebra (S₀ : subalgebra R S) : is_scalar_tower S₀ S A :=
-of_algebra_map_eq $ λ x, rfl
-
 variables [algebra R A] [algebra R B]
 variables [is_scalar_tower R S A] [is_scalar_tower R S B]
 
@@ -98,10 +90,6 @@ ring_hom.ext $ λ x, by simp_rw [ring_hom.comp_apply, algebra.algebra_map_eq_smu
 theorem algebra_map_apply (x : R) : algebra_map R A x = algebra_map S A (algebra_map R S x) :=
 by rw [algebra_map_eq R S A, ring_hom.comp_apply]
 
-instance subalgebra' (S₀ : subalgebra R S) : is_scalar_tower R S₀ A :=
-@is_scalar_tower.of_algebra_map_eq R S₀ A _ _ _ _ _ _ $ λ _,
-(is_scalar_tower.algebra_map_apply R S A _ : _)
-
 @[ext] lemma algebra.ext {S : Type u} {A : Type v} [comm_semiring S] [semiring A]
   (h1 h2 : algebra S A) (h : ∀ (r : S) (x : A), (by haveI := h1; exact r • x) = r • x) : h1 = h2 :=
 algebra.algebra_ext _ _ $ λ r, by
@@ -202,50 +190,6 @@ end alg_equiv
 
 end homs
 
-namespace subalgebra
-
-open is_scalar_tower
-
-section semiring
-
-variables (R) {S A B} [comm_semiring R] [comm_semiring S] [semiring A] [semiring B]
-variables [algebra R S] [algebra S A] [algebra R A] [algebra S B] [algebra R B]
-variables [is_scalar_tower R S A] [is_scalar_tower R S B]
-
-/-- Given a tower `A / ↥U / S / R` of algebras, where `U` is an `S`-subalgebra of `A`, reinterpret
-`U` as an `R`-subalgebra of `A`. -/
-def restrict_scalars (U : subalgebra S A) : subalgebra R A :=
-{ algebra_map_mem' := λ x, by { rw algebra_map_apply R S A, exact U.algebra_map_mem _ },
-  .. U }
-
-@[simp] lemma coe_restrict_scalars {U : subalgebra S A} :
-  (restrict_scalars R U : set A) = (U : set A) := rfl
-
-@[simp] lemma restrict_scalars_top : restrict_scalars R (⊤ : subalgebra S A) = ⊤ :=
-set_like.coe_injective rfl
-
-@[simp] lemma restrict_scalars_to_submodule {U : subalgebra S A} :
-  (U.restrict_scalars R).to_submodule = U.to_submodule.restrict_scalars R :=
-set_like.coe_injective rfl
-
-@[simp] lemma mem_restrict_scalars {U : subalgebra S A} {x : A} :
-  x ∈ restrict_scalars R U ↔ x ∈ U := iff.rfl
-
-lemma restrict_scalars_injective :
-  function.injective (restrict_scalars R : subalgebra S A → subalgebra R A) :=
-λ U V H, ext $ λ x, by rw [← mem_restrict_scalars R, H, mem_restrict_scalars]
-
-/-- Produces an `R`-algebra map from `U.restrict_scalars R` given an `S`-algebra map from `U`.
-
-This is a special case of `alg_hom.restrict_scalars` that can be helpful in elaboration. -/
-@[simp]
-def of_restrict_scalars (U : subalgebra S A) (f : U →ₐ[S] B) : U.restrict_scalars R →ₐ[R] B :=
-f.restrict_scalars R
-
-end semiring
-
-end subalgebra
-
 namespace algebra
 
 variables {R A} [comm_semiring R] [semiring A] [algebra R A]
@@ -273,25 +217,6 @@ congr_arg coe (algebra.span_restrict_scalars_eq_span_of_surjective h s)
 
 end algebra
 
-namespace is_scalar_tower
-
-open subalgebra
-
-variables [comm_semiring R] [comm_semiring S] [comm_semiring A]
-variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
-
-theorem adjoin_range_to_alg_hom (t : set A) :
-  (algebra.adjoin (to_alg_hom R S A).range t).restrict_scalars R =
-    (algebra.adjoin S t).restrict_scalars R :=
-subalgebra.ext $ λ z,
-show z ∈ subsemiring.closure (set.range (algebra_map (to_alg_hom R S A).range A) ∪ t : set A) ↔
-  z ∈ subsemiring.closure (set.range (algebra_map S A) ∪ t : set A),
-from suffices set.range (algebra_map (to_alg_hom R S A).range A) = set.range (algebra_map S A),
-  by rw this,
-by { ext z, exact ⟨λ ⟨⟨x, y, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y, hy⟩, ⟨⟨z, y, hy⟩, rfl⟩⟩ }
-
-end is_scalar_tower
-
 section semiring
 
 variables {R S A}

src/data/mv_polynomial/basic.lean

@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 -/
 
-import ring_theory.adjoin.basic
-import data.finsupp.antidiagonal
+import algebra.algebra.tower
 import algebra.monoid_algebra.support
+import data.finsupp.antidiagonal
 import order.symm_diff
+import ring_theory.adjoin.basic
 
 /-!
 # Multivariate polynomials

src/ring_theory/adjoin/basic.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 algebra.algebra.tower
+import algebra.algebra.operations
+import algebra.algebra.subalgebra.tower
 import linear_algebra.prod
 import linear_algebra.finsupp
-import algebra.algebra.operations
 
 /-!
 # Adjoining elements to form subalgebras

src/ring_theory/adjoin/tower.lean

@@ -31,6 +31,23 @@ theorem adjoin_algebra_map (R : Type u) (S : Type v) (A : Type w)
 le_antisymm (adjoin_le $ set.image_subset_iff.2 $ λ y hy, ⟨y, subset_adjoin hy, rfl⟩)
   (subalgebra.map_le.2 $ adjoin_le $ λ y hy, subset_adjoin ⟨y, hy, rfl⟩)
 
+lemma adjoin_restrict_scalars (C D E : Type*) [comm_semiring C] [comm_semiring D] [comm_semiring E]
+  [algebra C D] [algebra C E] [algebra D E] [is_scalar_tower C D E] (S : set E) :
+(algebra.adjoin D S).restrict_scalars C =
+  (algebra.adjoin
+    ((⊤ : subalgebra C D).map (is_scalar_tower.to_alg_hom C D E)) S).restrict_scalars C :=
+begin
+  suffices : set.range (algebra_map D E) =
+    set.range (algebra_map ((⊤ : subalgebra C D).map (is_scalar_tower.to_alg_hom C D E)) E),
+  { ext x, change x ∈ subsemiring.closure (_ ∪ S) ↔ x ∈ subsemiring.closure (_ ∪ S), rw this },
+  ext x,
+  split,
+  { rintros ⟨y, hy⟩,
+    exact ⟨⟨algebra_map D E y, ⟨y, ⟨algebra.mem_top, rfl⟩⟩⟩, hy⟩ },
+  { rintros ⟨⟨y, ⟨z, ⟨h0, h1⟩⟩⟩, h2⟩,
+    exact ⟨z, eq.trans h1 h2⟩ },
+end
+
 lemma adjoin_res_eq_adjoin_res (C D E F : Type*) [comm_semiring C] [comm_semiring D]
   [comm_semiring E] [comm_semiring F] [algebra C D] [algebra C E] [algebra C F] [algebra D F]
   [algebra E F] [is_scalar_tower C D F] [is_scalar_tower C E F] {S : set D} {T : set E}

src/ring_theory/algebra_tower.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import algebra.algebra.restrict_scalars
 import algebra.algebra.tower
 import algebra.invertible
 import linear_algebra.basis
@@ -62,27 +61,6 @@ end comm_semiring
 
 end is_scalar_tower
 
-namespace algebra
-
-lemma adjoin_restrict_scalars (C D E : Type*) [comm_semiring C] [comm_semiring D] [comm_semiring E]
-  [algebra C D] [algebra C E] [algebra D E] [is_scalar_tower C D E] (S : set E) :
-(algebra.adjoin D S).restrict_scalars C =
-  (algebra.adjoin
-    ((⊤ : subalgebra C D).map (is_scalar_tower.to_alg_hom C D E)) S).restrict_scalars C :=
-begin
-  suffices : set.range (algebra_map D E) =
-    set.range (algebra_map ((⊤ : subalgebra C D).map (is_scalar_tower.to_alg_hom C D E)) E),
-  { ext x, change x ∈ subsemiring.closure (_ ∪ S) ↔ x ∈ subsemiring.closure (_ ∪ S), rw this },
-  ext x,
-  split,
-  { rintros ⟨y, hy⟩,
-    exact ⟨⟨algebra_map D E y, ⟨y, ⟨algebra.mem_top, rfl⟩⟩⟩, hy⟩ },
-  { rintros ⟨⟨y, ⟨z, ⟨h0, h1⟩⟩⟩, h2⟩,
-    exact ⟨z, eq.trans h1 h2⟩ },
-end
-
-end algebra
-
 section algebra_map_coeffs
 
 variables {R} (A) {ι M : Type*} [comm_semiring R] [semiring A] [add_comm_monoid M]

src/ring_theory/noetherian.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro, Kevin Buzzard
 -/
 import group_theory.finiteness
 import data.multiset.finset_ops
-import algebra.algebra.tower
+import algebra.algebra.subalgebra.tower
 import order.order_iso_nat
 import ring_theory.nilpotent
 import order.compactly_generated