chore(algebra/algebra/subalgebra): reduce imports (#12636)

Splitting a file, and reducing imports. No change in contents.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/algebra/subalgebra.lean → src/algebra/algebra/subalgebra/basic.lean

@@ -3,9 +3,8 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import algebra.algebra.operations
+import algebra.algebra.basic
 import data.set.Union_lift
-import ring_theory.subring.pointwise
 
 /-!
 # Subalgebras over Commutative Semiring
@@ -16,7 +15,7 @@ More lemmas about `adjoin` can be found in `ring_theory.adjoin`.
 -/
 universes u u' v w w'
 
-open_locale tensor_product big_operators
+open_locale big_operators
 
 set_option old_structure_cmd true
 
@@ -321,19 +320,6 @@ rfl
   [algebra R A] (S : subalgebra R A) : S.to_subring.subtype = (S.val : S →+* A) :=
 rfl
 
-
-/-- As submodules, subalgebras are idempotent. -/
-@[simp] theorem mul_self : S.to_submodule * S.to_submodule = S.to_submodule :=
-begin
-  apply le_antisymm,
-  { rw submodule.mul_le,
-    intros y hy z hz,
-    exact mul_mem S hy hz },
-  { intros x hx1,
-    rw ← mul_one x,
-    exact submodule.mul_mem_mul hx1 (one_mem S) }
-end
-
 /-- Linear equivalence between `S : submodule R A` and `S`. Though these types are equal,
 we define it as a `linear_equiv` to avoid type equalities. -/
 def to_submodule_equiv (S : subalgebra R A) : S.to_submodule ≃ₗ[R] S :=
@@ -1009,39 +995,6 @@ instance no_zero_smul_divisors_top [no_zero_divisors A] (S : subalgebra R A) :
 
 end actions
 
-section pointwise
-variables {R' : Type*} [semiring R'] [mul_semiring_action R' A] [smul_comm_class R' R A]
-
-/-- The action on a subalgebra corresponding to applying the action to every element.
-
-This is available as an instance in the `pointwise` locale. -/
-protected def pointwise_mul_action : mul_action R' (subalgebra R A) :=
-{ smul := λ a S, S.map (mul_semiring_action.to_alg_hom _ _ a),
-  one_smul := λ S,
-    (congr_arg (λ f, S.map f) (alg_hom.ext $ by exact one_smul R')).trans S.map_id,
-  mul_smul := λ a₁ a₂ S,
-    (congr_arg (λ f, S.map f) (alg_hom.ext $ by exact mul_smul _ _)).trans (S.map_map _ _).symm }
-
-localized "attribute [instance] subalgebra.pointwise_mul_action" in pointwise
-open_locale pointwise
-
-@[simp] lemma coe_pointwise_smul (m : R') (S : subalgebra R A) : ↑(m • S) = m • (S : set A) := rfl
-
-@[simp] lemma pointwise_smul_to_subsemiring (m : R') (S : subalgebra R A) :
-  (m • S).to_subsemiring = m • S.to_subsemiring := rfl
-
-@[simp] lemma pointwise_smul_to_submodule (m : R') (S : subalgebra R A) :
-  (m • S).to_submodule = m • S.to_submodule := rfl
-
-@[simp] lemma pointwise_smul_to_subring {R' R A : Type*} [semiring R'] [comm_ring R] [ring A]
-  [mul_semiring_action R' A] [algebra R A] [smul_comm_class R' R A] (m : R') (S : subalgebra R A) :
-  (m • S).to_subring = m • S.to_subring := rfl
-
-lemma smul_mem_pointwise_smul (m : R') (r : A) (S : subalgebra R A) : r ∈ S → m • r ∈ m • S :=
-(set.smul_mem_smul_set : _ → _ ∈ m • (S : set A))
-
-end pointwise
-
 section center
 
 lemma _root_.set.algebra_map_mem_center (r : R) : algebra_map R A r ∈ set.center A :=

src/algebra/algebra/subalgebra/pointwise.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2021 Eric Weiser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import algebra.algebra.operations
+import algebra.algebra.subalgebra.basic
+import ring_theory.subring.pointwise
+
+/-!
+# Pointwise actions on subalgebras.
+
+If `R'` acts on an `R`-algebra `A` (so that `R'` and `R` actions commute)
+then we get an `R'` action on the collection of `R`-subalgebras.
+-/
+
+namespace subalgebra
+
+section pointwise
+variables {R : Type*} {A : Type*} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A)
+
+/-- As submodules, subalgebras are idempotent. -/
+@[simp] theorem mul_self : S.to_submodule * S.to_submodule = S.to_submodule :=
+begin
+  apply le_antisymm,
+  { rw submodule.mul_le,
+    intros y hy z hz,
+    exact mul_mem S hy hz },
+  { intros x hx1,
+    rw ← mul_one x,
+    exact submodule.mul_mem_mul hx1 (one_mem S) }
+end
+
+variables {R' : Type*} [semiring R'] [mul_semiring_action R' A] [smul_comm_class R' R A]
+
+/-- The action on a subalgebra corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale. -/
+protected def pointwise_mul_action : mul_action R' (subalgebra R A) :=
+{ smul := λ a S, S.map (mul_semiring_action.to_alg_hom _ _ a),
+  one_smul := λ S,
+    (congr_arg (λ f, S.map f) (alg_hom.ext $ by exact one_smul R')).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (alg_hom.ext $ by exact mul_smul _ _)).trans (S.map_map _ _).symm }
+
+localized "attribute [instance] subalgebra.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (m : R') (S : subalgebra R A) : ↑(m • S) = m • (S : set A) := rfl
+
+@[simp] lemma pointwise_smul_to_subsemiring (m : R') (S : subalgebra R A) :
+  (m • S).to_subsemiring = m • S.to_subsemiring := rfl
+
+@[simp] lemma pointwise_smul_to_submodule (m : R') (S : subalgebra R A) :
+  (m • S).to_submodule = m • S.to_submodule := rfl
+
+@[simp] lemma pointwise_smul_to_subring {R' R A : Type*} [semiring R'] [comm_ring R] [ring A]
+  [mul_semiring_action R' A] [algebra R A] [smul_comm_class R' R A] (m : R') (S : subalgebra R A) :
+  (m • S).to_subring = m • S.to_subring := rfl
+
+lemma smul_mem_pointwise_smul (m : R') (r : A) (S : subalgebra R A) : r ∈ S → m • r ∈ m • S :=
+(set.smul_mem_smul_set : _ → _ ∈ m • (S : set A))
+
+end pointwise
+
+end subalgebra

src/algebra/algebra/tower.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
-import algebra.algebra.subalgebra
+import algebra.algebra.subalgebra.basic
+import algebra.algebra.bilinear
 
 /-!
 # Towers of algebras

src/algebra/category/Algebra/basic.lean

@@ -3,8 +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 algebra.algebra.basic
-import algebra.algebra.subalgebra
+import algebra.algebra.subalgebra.basic
 import algebra.free_algebra
 import algebra.category.CommRing.basic
 import algebra.category.Module.basic

src/algebra/direct_sum/internal.lean

@@ -5,7 +5,7 @@ Authors: Eric Wieser, Kevin Buzzard, Jujian Zhang
 -/
 
 import algebra.algebra.operations
-import algebra.algebra.subalgebra
+import algebra.algebra.subalgebra.basic
 import algebra.direct_sum.algebra
 
 /-!

src/algebra/free_algebra.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Adam Topaz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Adam Topaz
 -/
-import algebra.algebra.subalgebra
+import algebra.algebra.subalgebra.basic
 import algebra.monoid_algebra.basic
 
 /-!

src/algebra/lie/of_associative.lean

@@ -6,7 +6,7 @@ Authors: Oliver Nash
 import algebra.lie.basic
 import algebra.lie.subalgebra
 import algebra.lie.submodule
-import algebra.algebra.subalgebra
+import algebra.algebra.subalgebra.basic
 
 /-!
 # Lie algebras of associative algebras

src/linear_algebra/finite_dimensional.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import algebra.algebra.subalgebra
+import algebra.algebra.subalgebra.basic
 import field_theory.finiteness
 
 /-!

src/linear_algebra/tensor_algebra/basic.lean

@@ -6,6 +6,7 @@ Authors: Adam Topaz
 import algebra.free_algebra
 import algebra.ring_quot
 import algebra.triv_sq_zero_ext
+import algebra.algebra.operations
 
 /-!
 # Tensor Algebras

src/ring_theory/adjoin/basic.lean

@@ -6,6 +6,7 @@ Authors: Kenny Lau
 import algebra.algebra.tower
 import linear_algebra.prod
 import linear_algebra.finsupp
+import algebra.algebra.operations
 
 /-!
 # Adjoining elements to form subalgebras

src/ring_theory/dedekind_domain/ideal.lean

@@ -6,6 +6,7 @@ Authors: Kenji Nakagawa, Anne Baanen, Filippo A. E. Nuccio
 import algebraic_geometry.prime_spectrum.noetherian
 import ring_theory.fractional_ideal
 import ring_theory.dedekind_domain.basic
+import algebra.algebra.subalgebra.pointwise
 
 /-!
 # Dedekind domains and ideals

src/ring_theory/polynomial/symmetric.lean

@@ -6,7 +6,7 @@ Authors: Hanting Zhang, Johan Commelin
 import data.fintype.card
 import data.mv_polynomial.rename
 import data.mv_polynomial.comm_ring
-import algebra.algebra.subalgebra
+import algebra.algebra.subalgebra.basic
 
 /-!
 # Symmetric Polynomials and Elementary Symmetric Polynomials

src/topology/algebra/algebra.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import algebra.algebra.subalgebra
+import algebra.algebra.subalgebra.basic
 import topology.algebra.module.basic
 
 /-!

src/topology/continuous_function/algebra.lean

@@ -7,7 +7,7 @@ import topology.algebra.module.basic
 import topology.continuous_function.ordered
 import topology.algebra.uniform_group
 import topology.uniform_space.compact_convergence
-import algebra.algebra.subalgebra
+import algebra.algebra.subalgebra.basic
 import tactic.field_simp
 
 /-!