chore(ring_theory): delete is_algebra_tower (#3785)

Delete the abbreviation `is_algebra_tower` for `is_scalar_tower`, and replace all references (including the usages of the `is_algebra_tower` namespace) with `is_scalar_tower`. Documentation should also have been updated accordingly.

This change was requested in a comment on #3717.




Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

src/field_theory/algebraic_closure.lean

@@ -217,8 +217,8 @@ rfl
 instance step.algebra (n) : algebra k (step k n) :=
 (to_step_of_le k 0 n n.zero_le).to_algebra
 
-instance step.algebra_tower (n) : is_algebra_tower k (step k n) (step k (n + 1)) :=
-is_algebra_tower.of_algebra_map_eq $ λ z,
+instance step.scalar_tower (n) : is_scalar_tower k (step k n) (step k (n + 1)) :=
+is_scalar_tower.of_algebra_map_eq $ λ z,
   @nat.le_rec_on_succ (step k) 0 n n.zero_le (n + 1).zero_le (λ n, to_step_succ k n) z
 
 theorem step.is_integral (n) : ∀ z : step k n, is_integral k z :=

src/field_theory/splitting_field.lean

@@ -283,15 +283,15 @@ begin
   haveI : finite_dimensional F (algebra.adjoin F (↑s : set K)) :=
     (submodule.fg_iff_finite_dimensional _).1 (fg_adjoin_of_finite (set.finite_mem_finset s) H3),
   letI := field_of_finite_dimensional F (algebra.adjoin F (↑s : set K)),
-  have H5 : is_integral (algebra.adjoin F (↑s : set K)) a := is_integral_of_is_algebra_tower a H1,
+  have H5 : is_integral (algebra.adjoin F (↑s : set K)) a := is_integral_of_is_scalar_tower a H1,
   have H6 : (minimal_polynomial H5).splits (algebra_map (algebra.adjoin F (↑s : set K)) L),
   { refine polynomial.splits_of_splits_of_dvd _
       (polynomial.map_ne_zero $ minimal_polynomial.ne_zero H1 :
         polynomial.map (algebra_map _ _) _ ≠ 0)
       ((polynomial.splits_map_iff _ _).2 _)
       (minimal_polynomial.dvd _ _),
-    { rw ← is_algebra_tower.algebra_map_eq, exact H2 },
-    { rw [← is_algebra_tower.aeval_apply, minimal_polynomial.aeval H1] } },
+    { rw ← is_scalar_tower.algebra_map_eq, exact H2 },
+    { rw [← is_scalar_tower.aeval_apply, minimal_polynomial.aeval H1] } },
   obtain ⟨y, hy⟩ := polynomial.exists_root_of_splits _ H6 (minimal_polynomial.degree_ne_zero H5),
   exact ⟨subalgebra.of_under _ _ $ (adjoin_root.alg_hom (minimal_polynomial H5) y hy).comp $
     alg_equiv.adjoin_singleton_equiv_adjoin_root_minimal_polynomial _ _ H5⟩
@@ -384,14 +384,14 @@ instance algebra''' {n : ℕ} {f : polynomial α} (hfn : f.nat_degree = n + 1) :
     (splitting_field_aux n f.remove_factor (nat_degree_remove_factor' hfn)) :=
 splitting_field_aux.algebra n _
 
-instance algebra_tower {n : ℕ} {f : polynomial α} (hfn : f.nat_degree = n + 1) :
-  is_algebra_tower α (adjoin_root f.factor) (splitting_field_aux _ _ hfn) :=
-is_algebra_tower.of_algebra_map_eq $ λ x, rfl
+instance scalar_tower {n : ℕ} {f : polynomial α} (hfn : f.nat_degree = n + 1) :
+  is_scalar_tower α (adjoin_root f.factor) (splitting_field_aux _ _ hfn) :=
+is_scalar_tower.of_algebra_map_eq $ λ x, rfl
 
-instance algebra_tower' {n : ℕ} {f : polynomial α} (hfn : f.nat_degree = n + 1) :
-  is_algebra_tower α (adjoin_root f.factor)
+instance scalar_tower' {n : ℕ} {f : polynomial α} (hfn : f.nat_degree = n + 1) :
+  is_scalar_tower α (adjoin_root f.factor)
     (splitting_field_aux n f.remove_factor (nat_degree_remove_factor' hfn)) :=
-is_algebra_tower.of_algebra_map_eq $ λ x, rfl
+is_scalar_tower.of_algebra_map_eq $ λ x, rfl
 
 theorem algebra_map_succ (n : ℕ) (f : polynomial α) (hfn : f.nat_degree = n + 1) :
   by exact algebra_map α (splitting_field_aux _ _ hfn) =
@@ -440,7 +440,7 @@ rw [roots_mul hmf0, map_sub, map_X, map_C, roots_X_sub_C, finset.coe_union, fins
     algebra.adjoin_union, ← set.image_singleton, algebra.adjoin_algebra_map α (adjoin_root f.factor)
       (splitting_field_aux n f.remove_factor (nat_degree_remove_factor' hfn)),
     adjoin_root.adjoin_root_eq_top, algebra.map_top,
-    is_algebra_tower.range_under_adjoin α (adjoin_root f.factor)
+    is_scalar_tower.range_under_adjoin α (adjoin_root f.factor)
       (splitting_field_aux n f.remove_factor (nat_degree_remove_factor' hfn)),
     ih, subalgebra.res_top] }
 
@@ -491,15 +491,15 @@ variables {α}
 instance splitting_field (f : polynomial α) : is_splitting_field α (splitting_field f) f :=
 ⟨splitting_field.splits f, splitting_field.adjoin_roots f⟩
 
-section algebra_tower
+section scalar_tower
 
-variables {α β γ} [algebra β γ] [algebra α γ] [is_algebra_tower α β γ]
+variables {α β γ} [algebra β γ] [algebra α γ] [is_scalar_tower α β γ]
 
 variables {α}
 instance map (f : polynomial α) [is_splitting_field α γ f] :
   is_splitting_field β γ (f.map $ algebra_map α β) :=
-⟨by { rw [splits_map_iff, ← is_algebra_tower.algebra_map_eq], exact splits γ f },
- subalgebra.res_inj α $ by { rw [map_map, ← is_algebra_tower.algebra_map_eq, subalgebra.res_top,
+⟨by { rw [splits_map_iff, ← is_scalar_tower.algebra_map_eq], exact splits γ f },
+ subalgebra.res_inj α $ by { rw [map_map, ← is_scalar_tower.algebra_map_eq, subalgebra.res_top,
     eq_top_iff, ← adjoin_roots γ f, algebra.adjoin_le_iff],
   exact λ x hx, @algebra.subset_adjoin β _ _ _ _ _ _ hx }⟩
 
@@ -516,17 +516,17 @@ theorem splits_iff (f : polynomial α) [is_splitting_field α β f] :
 theorem mul (f g : polynomial α) (hf : f ≠ 0) (hg : g ≠ 0) [is_splitting_field α β f]
   [is_splitting_field β γ (g.map $ algebra_map α β)] :
   is_splitting_field α γ (f * g) :=
-⟨(is_algebra_tower.algebra_map_eq α β γ).symm ▸ splits_mul _
+⟨(is_scalar_tower.algebra_map_eq α β γ).symm ▸ splits_mul _
   (splits_comp_of_splits _ _ (splits β f))
   ((splits_map_iff _ _).1 (splits γ $ g.map $ algebra_map α β)),
  by rw [map_mul, roots_mul (mul_ne_zero (map_ne_zero hf : f.map (algebra_map α γ) ≠ 0)
         (map_ne_zero hg)), finset.coe_union, algebra.adjoin_union,
-      is_algebra_tower.algebra_map_eq α β γ, ← map_map,
+      is_scalar_tower.algebra_map_eq α β γ, ← map_map,
       roots_map (algebra_map β γ) ((splits_id_iff_splits $ algebra_map α β).2 $ splits β f),
       finset.coe_image, algebra.adjoin_algebra_map, adjoin_roots, algebra.map_top,
-      is_algebra_tower.range_under_adjoin, ← map_map, adjoin_roots, subalgebra.res_top]⟩
+      is_scalar_tower.range_under_adjoin, ← map_map, adjoin_roots, subalgebra.res_top]⟩
 
-end algebra_tower
+end scalar_tower
 
 /-- Splitting field of `f` embeds into any field that splits `f`. -/
 def lift [algebra α γ] (f : polynomial α) [is_splitting_field α β f]

src/field_theory/tower.lean

@@ -37,7 +37,7 @@ open cardinal
 
 variables (F : Type u) (K : Type v) (A : Type w)
 variables [field F] [field K] [ring A]
-variables [algebra F K] [algebra K A] [algebra F A] [is_algebra_tower F K A]
+variables [algebra F K] [algebra K A] [algebra F A] [is_scalar_tower F K A]
 
 /-- Tower law: if `A` is a `K`-algebra and `K` is a field extension of `F` then
 `dim_F(A) = dim_F(K) * dim_K(A)`. -/
@@ -54,7 +54,7 @@ by rw [← (vector_space.dim F K).lift_id, ← hb.mk_eq_dim,
 /-- Tower law: if `A` is a `K`-algebra and `K` is a field extension of `F` then
 `dim_F(A) = dim_F(K) * dim_K(A)`. -/
 theorem dim_mul_dim (F : Type u) (K A : Type v) [field F] [field K] [ring A]
-  [algebra F K] [algebra K A] [algebra F A] [is_algebra_tower F K A] :
+  [algebra F K] [algebra K A] [algebra F A] [is_scalar_tower F K A] :
   vector_space.dim F K * vector_space.dim K A = vector_space.dim F A :=
 by convert dim_mul_dim' F K A; rw lift_id
 

src/ring_theory/algebra.lean

@@ -16,7 +16,7 @@ algebra equivalences `alg_equiv`, and `subalgebra`s. We also define usual operat
 
 If `S` is an `R`-algebra and `A` is an `S`-algebra then `algebra.comap.algebra R S A` can be used
 to provide `A` with a structure of an `R`-algebra. Other than that, `algebra.comap` is now
-deprecated and replcaed with `is_algebra_tower`.
+deprecated and replcaed with `is_scalar_tower`.
 
 ## Notations
 
@@ -577,7 +577,7 @@ include R S A
 /-- `comap R S A` is a type alias for `A`, and has an R-algebra structure defined on it
   when `algebra R S` and `algebra S A`. If `S` is an `R`-algebra and `A` is an `S`-algebra then
   `algebra.comap.algebra R S A` can be used to provide `A` with a structure of an `R`-algebra.
-  Other than that, `algebra.comap` is now deprecated and replcaed with `is_algebra_tower`. -/
+  Other than that, `algebra.comap` is now deprecated and replaced with `is_scalar_tower`. -/
 /- This is done to avoid a type class search with meta-variables `algebra R ?m_1` and
     `algebra ?m_1 A -/
 /- The `nolint` attribute is added because it has unused arguments `R` and `S`, but these are necessary for synthesizing the

src/ring_theory/algebra_tower.lean

@@ -10,9 +10,9 @@ import ring_theory.adjoin
 # Towers of algebras
 
 We set up the basic theory of algebra towers.
-The typeclass `is_algebra_tower R S A` expresses that `A` is an `S`-algebra,
-and both `S` and `A` are `R`-algebras, with the compatibility condition
-`(r • s) • a = r • (s • a)`.
+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)`.
 
 In `field_theory/tower.lean` we use this to prove the tower law for finite extensions,
 that if `R` and `S` are both fields, then `[A:R] = [A:S] [S:A]`.
@@ -27,22 +27,18 @@ universes u v w u₁
 
 variables (R : Type u) (S : Type v) (A : Type w) (B : Type u₁)
 
-/-- Typeclass for a tower of three algebras. -/
-abbreviation is_algebra_tower [comm_semiring R] [comm_semiring S] [semiring A]
-  [algebra R S] [algebra S A] [algebra R A] := is_scalar_tower R S A
-
-namespace is_algebra_tower
+namespace is_scalar_tower
 
 section semiring
 variables [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 {R S A}
 
 theorem of_algebra_map_eq (h : ∀ x, algebra_map R A x = algebra_map S A (algebra_map R S x)) :
-  is_algebra_tower R S A :=
+  is_scalar_tower R S A :=
 ⟨λ x y z, by simp_rw [algebra.smul_def, ring_hom.map_mul, mul_assoc, h]⟩
 
-variables [is_algebra_tower R S A] [is_algebra_tower R S B]
+variables [is_scalar_tower R S A] [is_scalar_tower R S B]
 
 variables (R S A)
 theorem algebra_map_eq :
@@ -71,7 +67,7 @@ begin
 end
 
 variables (R S A)
-theorem comap_eq : algebra.comap.algebra R S A = ‹_› :=
+theorem algebra_comap_eq : algebra.comap.algebra R S A = ‹_› :=
 algebra.ext _ _ $ λ x (z : A),
 calc  algebra_map R S x • z
     = (x • 1 : S) • z : by rw algebra.algebra_map_eq_smul_one
@@ -95,39 +91,39 @@ def restrict_base (f : A →ₐ[S] B) : A →ₐ[R] B :=
 
 @[simp] lemma restrict_base_apply (f : A →ₐ[S] B) (x : A) : restrict_base R f x = f x := rfl
 
-instance right : is_algebra_tower R S S :=
+instance right : is_scalar_tower R S S :=
 of_algebra_map_eq $ λ x, rfl
 
-instance nat : is_algebra_tower ℕ S A :=
+instance nat : is_scalar_tower ℕ S A :=
 of_algebra_map_eq $ λ x, ((algebra_map S A).map_nat_cast x).symm
 
 instance comap {R S A : Type*} [comm_semiring R] [comm_semiring S] [semiring A]
-  [algebra R S] [algebra S A] : is_algebra_tower R S (algebra.comap R S A) :=
+  [algebra R S] [algebra S A] : is_scalar_tower R S (algebra.comap R S A) :=
 of_algebra_map_eq $ λ x, rfl
 
-instance subsemiring (U : subsemiring S) : is_algebra_tower U S A :=
+instance subsemiring (U : subsemiring S) : is_scalar_tower U S A :=
 of_algebra_map_eq $ λ x, rfl
 
 instance subring {S A : Type*} [comm_ring S] [ring A] [algebra S A]
-  (U : set S) [is_subring U] : is_algebra_tower U S A :=
+  (U : set S) [is_subring U] : is_scalar_tower U S A :=
 of_algebra_map_eq $ λ x, rfl
 
 @[nolint instance_priority]
 instance of_ring_hom {R A B : Type*} [comm_semiring R] [comm_semiring A] [comm_semiring B]
   [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
-  @is_algebra_tower R A B _ _ _ _ (ring_hom.to_algebra f) _ :=
+  @is_scalar_tower R A B _ (f.to_ring_hom.to_algebra.to_has_scalar) _ :=
 by { letI := (f : A →+* B).to_algebra, exact of_algebra_map_eq (λ x, (f.commutes x).symm) }
 
 end semiring
 
 section comm_semiring
 variables [comm_semiring R] [comm_semiring A] [algebra R A]
-variables [comm_semiring B] [algebra A B] [algebra R B] [is_algebra_tower R A B]
+variables [comm_semiring B] [algebra A B] [algebra R B] [is_scalar_tower R A B]
 
-instance subalgebra (S : subalgebra R A) : is_algebra_tower R S A :=
+instance subalgebra (S : subalgebra R A) : is_scalar_tower R S A :=
 of_algebra_map_eq $ λ x, rfl
 
-instance polynomial : is_algebra_tower R A (polynomial B) :=
+instance polynomial : is_scalar_tower R A (polynomial B) :=
 of_algebra_map_eq $ λ x, congr_arg polynomial.C $ algebra_map_apply R A B x
 
 theorem aeval_apply (x : B) (p : polynomial R) : polynomial.aeval x p =
@@ -136,32 +132,24 @@ by rw [polynomial.aeval_def, polynomial.aeval_def, polynomial.eval₂_map, algeb
 
 end comm_semiring
 
-section ring
-variables [comm_ring R] [comm_ring S] [ring A] [algebra R S] [algebra S A] [algebra R A]
-variables [is_algebra_tower R S A]
-
-
-end ring
-
 section comm_ring
 variables [comm_ring R] [comm_ring S] [comm_ring A] [algebra R S] [algebra S A] [algebra R A]
-variables [is_algebra_tower R S A]
-
+variables [is_scalar_tower R S A]
 
-instance int : is_algebra_tower ℤ S A :=
+instance int : is_scalar_tower ℤ S A :=
 of_algebra_map_eq $ λ x, ((algebra_map S A).map_int_cast x).symm
 
 end comm_ring
 
 section division_ring
 variables [field R] [division_ring S] [algebra R S] [char_zero R] [char_zero S]
 
-instance rat : is_algebra_tower ℚ R S :=
+instance rat : is_scalar_tower ℚ R S :=
 of_algebra_map_eq $ λ x, ((algebra_map R S).map_rat_cast x).symm
 
 end division_ring
 
-end is_algebra_tower
+end is_scalar_tower
 
 namespace algebra
 
@@ -173,19 +161,19 @@ le_antisymm (adjoin_le $ set.image_subset_iff.2 $ λ y hy, ⟨y, subset_adjoin h
 
 theorem adjoin_algebra_map (R : Type u) (S : Type v) (A : Type w)
   [comm_ring R] [comm_ring S] [comm_ring A] [algebra R S] [algebra S A] [algebra R A]
-  [is_algebra_tower R S A] (s : set S) :
-  adjoin R (algebra_map S A '' s) = subalgebra.map (adjoin R s) (is_algebra_tower.to_alg_hom R S A) :=
+  [is_scalar_tower R S A] (s : set S) :
+  adjoin R (algebra_map S A '' s) = subalgebra.map (adjoin R s) (is_scalar_tower.to_alg_hom R S A) :=
 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⟩)
 
 end algebra
 
 namespace subalgebra
 
-open is_algebra_tower
+open is_scalar_tower
 
 variables (R) {S A} [comm_semiring R] [comm_semiring S] [semiring A]
-variables [algebra R S] [algebra S A] [algebra R A] [is_algebra_tower R S A]
+variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
 
 /-- If A/S/R is a tower of algebras then the `res`triction of a S-subalgebra of A is an R-subalgebra of A. -/
 def res (U : subalgebra S A) : subalgebra R A :=
@@ -203,18 +191,18 @@ ext $ λ x, by rw [← mem_res R, H, mem_res]
 /-- Produces a map from `subalgebra.under`. -/
 def of_under {R A B : Type*} [comm_semiring R] [comm_semiring A] [semiring B]
   [algebra R A] [algebra R B] (S : subalgebra R A) (U : subalgebra S A)
-  [algebra S B] [is_algebra_tower R S B] (f : U →ₐ[S] B) : S.under U →ₐ[R] B :=
+  [algebra S B] [is_scalar_tower R S B] (f : U →ₐ[S] B) : S.under U →ₐ[R] B :=
 { commutes' := λ r, (f.commutes (algebra_map R S r)).trans (algebra_map_apply R S B r).symm,
   .. f }
 
 end subalgebra
 
-namespace is_algebra_tower
+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_algebra_tower R S A]
+variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
 
 theorem range_under_adjoin (t : set A) :
   (to_alg_hom R S A).range.under (algebra.adjoin _ t) = res R (algebra.adjoin S t) :=
@@ -225,14 +213,14 @@ from suffices set.range (algebra_map (to_alg_hom R S A).range A) = set.range (al
   by rw this,
 by { ext z, exact ⟨λ ⟨⟨x, y, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y, hy⟩, ⟨⟨z, y, hy⟩, rfl⟩⟩ }
 
-end is_algebra_tower
+end is_scalar_tower
 
 namespace submodule
 
-open is_algebra_tower
+open is_scalar_tower
 
 variables [comm_semiring R] [comm_semiring S] [semiring A]
-variables [algebra R S] [algebra S A] [algebra R A] [is_algebra_tower R S A]
+variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
 
 variables (R) {S A}
 /-- Restricting the scalars of submodules in an algebra tower. -/
@@ -257,18 +245,18 @@ section semiring
 
 variables {R S A}
 variables [comm_semiring R] [comm_semiring S] [semiring A]
-variables [algebra R S] [algebra S A] [algebra R A] [is_algebra_tower R S A]
+variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
 
 namespace submodule
 
-open is_algebra_tower
+open is_scalar_tower
 
 theorem smul_mem_span_smul_of_mem {s : set S} {t : set A} {k : S} (hks : k ∈ span R s)
   {x : A} (hx : x ∈ t) : k • x ∈ span R (s • t) :=
 span_induction hks (λ c hc, subset_span $ set.mem_smul.2 ⟨c, x, hc, hx, rfl⟩)
   (by { rw zero_smul, exact zero_mem _ })
   (λ c₁ c₂ ih₁ ih₂, by { rw add_smul, exact add_mem _ ih₁ ih₂ })
-  (λ b c hc, by { rw smul_assoc, exact smul_mem _ _ hc })
+  (λ b c hc, by { rw is_scalar_tower.smul_assoc, exact smul_mem _ _ hc })
 
 theorem smul_mem_span_smul {s : set S} (hs : span R s = ⊤) {t : set A} {k : S}
   {x : A} (hx : x ∈ span R t) :
@@ -308,7 +296,7 @@ universes v₁ w₁
 
 variables {R S A}
 variables [comm_ring R] [comm_ring S] [ring A]
-variables [algebra R S] [algebra S A] [algebra R A] [is_algebra_tower R S A]
+variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
 
 theorem linear_independent_smul {ι : Type v₁} {b : ι → S} {κ : Type w₁} {c : κ → A}
   (hb : linear_independent R b) (hc : linear_independent S c) :

src/ring_theory/algebraic.lean

@@ -92,7 +92,7 @@ end field
 namespace algebra
 variables {K : Type*} {L : Type*} {A : Type*}
 variables [field K] [field L] [comm_ring A]
-variables [algebra K L] [algebra L A] [algebra K A] [is_algebra_tower K L A]
+variables [algebra K L] [algebra L A] [algebra K A] [is_scalar_tower K L A]
 
 /-- If L is an algebraic field extension of K and A is an algebraic algebra over L,
 then A is algebraic over K. -/