chore(algebra): move lemmas from ring_theory.algebra_tower to algebra.algebra.tower (#5506)

Moved some basic lemmas from `ring_theory.algebra_tower` to `algebra.algebra.tower`.

Author: kckennylau

src/algebra/algebra/tower.lean

@@ -0,0 +1,277 @@
+/-
+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.subalgebra
+
+/-!
+# Towers of algebras
+
+In this file we prove basic facts about 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)`.
+
+An important definition is `to_alg_hom R S A`, the canonical `R`-algebra homomorphism `S →ₐ[R] A`.
+
+-/
+
+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] [semimodule R M] [semimodule A M] [is_scalar_tower R A M]
+
+variables {A}
+
+/-- The `R`-algebra morphism `A → End (M)` corresponding to the representation of the algebra `A`
+on the `R`-module `M`. -/
+def lsmul : A →ₐ[R] module.End R M :=
+{ map_one' := by { ext m, exact one_smul A m },
+  map_mul' := by { intros a b, ext c, exact smul_assoc a b c },
+  map_zero' := by { ext m, exact zero_smul A m },
+  commutes' := by { intro r, ext m, exact algebra_map_smul A r m },
+  .. (show A →ₗ[R] M →ₗ[R] M, from linear_map.mk₂ R (•)
+  (λ x y z, add_smul x y z)
+  (λ c x y, smul_assoc c x y)
+  (λ x y z, smul_add x y z)
+  (λ c x y, smul_algebra_smul_comm c x y)) }
+
+@[simp] lemma lsmul_coe (a : A) : (lsmul R M a : M → M) = (•) a := rfl
+
+end algebra
+
+namespace is_scalar_tower
+
+section semimodule
+
+variables [comm_semiring R] [semiring A] [algebra R A]
+variables [add_comm_monoid M] [semimodule R M] [semimodule A M] [is_scalar_tower R A M]
+
+variables {R} (A) {M}
+theorem algebra_map_smul (r : R) (x : M) : algebra_map R A r • x = r • x :=
+by rw [algebra.algebra_map_eq_smul_one, smul_assoc, one_smul]
+
+end semimodule
+
+section semiring
+variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B]
+variables [algebra R S] [algebra S A] [algebra S B]
+
+variables {R S A}
+theorem of_algebra_map_eq [algebra R A]
+  (h : ∀ x, algebra_map R A x = algebra_map S A (algebra_map R S x)) :
+  is_scalar_tower R S A :=
+⟨λ x y z, by simp_rw [algebra.smul_def, ring_hom.map_mul, mul_assoc, h]⟩
+
+/-- See note [partially-applied ext lemmas]. -/
+theorem of_algebra_map_eq' [algebra R A]
+  (h : algebra_map R A = (algebra_map S A).comp (algebra_map R S)) :
+  is_scalar_tower R S A :=
+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]
+
+theorem algebra_map_eq :
+  algebra_map R A = (algebra_map S A).comp (algebra_map R S) :=
+ring_hom.ext $ λ x, by simp_rw [ring_hom.comp_apply, algebra.algebra_map_eq_smul_one,
+    smul_assoc, one_smul]
+
+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 :=
+begin
+  unfreezingI { cases h1 with f1 g1 h11 h12, cases h2 with f2 g2 h21 h22,
+  cases f1, cases f2, congr', { ext r x, exact h },
+  ext r, erw [← mul_one (g1 r), ← h12, ← mul_one (g2 r), ← h22, h], refl }
+end
+
+variables (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
+... = x • (1 : S) • z : by rw smul_assoc
+... = (by exact x • z : A) : by rw one_smul
+
+/-- In a tower, the canonical map from the middle element to the top element is an
+algebra homomorphism over the bottom element. -/
+def to_alg_hom : S →ₐ[R] A :=
+{ commutes' := λ _, (algebra_map_apply _ _ _ _).symm,
+  .. algebra_map S A }
+
+lemma to_alg_hom_apply (y : S) : to_alg_hom R S A y = algebra_map S A y := rfl
+
+@[simp] lemma coe_to_alg_hom : ↑(to_alg_hom R S A) = algebra_map S A :=
+ring_hom.ext $ λ _, rfl
+
+@[simp] lemma coe_to_alg_hom' : (to_alg_hom R S A : S → A) = algebra_map S A :=
+rfl
+
+variables (R) {S A B}
+/-- R ⟶ S induces S-Alg ⥤ R-Alg -/
+def restrict_base (f : A →ₐ[S] B) : A →ₐ[R] B :=
+{ commutes' := λ r, by { rw [algebra_map_apply R S A, algebra_map_apply R S B],
+    exact f.commutes (algebra_map R S r) },
+  .. (f : A →+* B) }
+
+lemma restrict_base_apply (f : A →ₐ[S] B) (x : A) : restrict_base R f x = f x := rfl
+
+@[simp] lemma coe_restrict_base (f : A →ₐ[S] B) : (restrict_base R f : A →+* B) = f := rfl
+
+@[simp] lemma coe_restrict_base' (f : A →ₐ[S] B) : (restrict_base R f : A → B) = f := rfl
+
+instance right : is_scalar_tower S A A :=
+⟨λ x y z, by rw [smul_eq_mul, smul_eq_mul, algebra.smul_mul_assoc]⟩
+
+instance comap {R S A : Type*} [comm_semiring R] [comm_semiring S] [semiring A]
+  [algebra R S] [algebra S A] : is_scalar_tower R S (algebra.comap R S A) :=
+of_algebra_map_eq $ λ x, rfl
+
+-- conflicts with is_scalar_tower.subalgebra
+@[priority 999] instance subsemiring (U : subsemiring S) : is_scalar_tower U S A :=
+of_algebra_map_eq $ λ x, rfl
+
+section
+local attribute [instance] algebra.of_is_subring subset.comm_ring
+-- conflicts with is_scalar_tower.subalgebra
+@[priority 999] instance subring {S A : Type*} [comm_ring S] [ring A] [algebra S A]
+  (U : set S) [is_subring U] : is_scalar_tower U S A :=
+of_algebra_map_eq $ λ x, rfl
+end
+
+@[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_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 division_ring
+variables [field R] [division_ring S] [algebra R S] [char_zero R] [char_zero 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_scalar_tower
+
+namespace subalgebra
+
+open is_scalar_tower
+
+section semiring
+
+variables (R) {S A} [comm_semiring R] [comm_semiring S] [semiring 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 :=
+{ algebra_map_mem' := λ x, by { rw algebra_map_apply R S A, exact U.algebra_map_mem _ },
+  .. U }
+
+@[simp] lemma res_top : res R (⊤ : subalgebra S A) = ⊤ :=
+algebra.eq_top_iff.2 $ λ _, show _ ∈ (⊤ : subalgebra S A), from algebra.mem_top
+
+@[simp] lemma mem_res {U : subalgebra S A} {x : A} : x ∈ res R U ↔ x ∈ U := iff.rfl
+
+lemma res_inj {U V : subalgebra S A} (H : res R U = res R V) : U = V :=
+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_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 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 range_under_adjoin (t : set A) :
+  (to_alg_hom R S A).range.under (algebra.adjoin _ t) = res R (algebra.adjoin S t) :=
+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, set.mem_univ _, hy⟩, rfl⟩⟩ }
+
+end is_scalar_tower
+
+section semiring
+
+variables {R S A}
+variables [comm_semiring R] [semiring S] [add_comm_monoid A]
+variables [algebra R S] [semimodule S A] [semimodule R A] [is_scalar_tower R S A]
+
+namespace submodule
+
+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 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) :
+  k • x ∈ span R (s • t) :=
+span_induction hx (λ x hx, smul_mem_span_smul_of_mem (hs.symm ▸ mem_top) hx)
+  (by { rw smul_zero, exact zero_mem _ })
+  (λ x y ihx ihy, by { rw smul_add, exact add_mem _ ihx ihy })
+  (λ c x hx, smul_comm c k x ▸ smul_mem _ _ hx)
+
+theorem smul_mem_span_smul' {s : set S} (hs : span R s = ⊤) {t : set A} {k : S}
+  {x : A} (hx : x ∈ span R (s • t)) :
+  k • x ∈ span R (s • t) :=
+span_induction hx (λ x hx, let ⟨p, q, hp, hq, hpq⟩ := set.mem_smul.1 hx in
+    by { rw [← hpq, smul_smul], exact smul_mem_span_smul_of_mem (hs.symm ▸ mem_top) hq })
+  (by { rw smul_zero, exact zero_mem _ })
+  (λ x y ihx ihy, by { rw smul_add, exact add_mem _ ihx ihy })
+  (λ c x hx, smul_comm c k x ▸ smul_mem _ _ hx)
+
+theorem span_smul {s : set S} (hs : span R s = ⊤) (t : set A) :
+  span R (s • t) = (span S t).restrict_scalars R :=
+le_antisymm (span_le.2 $ λ x hx, let ⟨p, q, hps, hqt, hpqx⟩ := set.mem_smul.1 hx in
+  hpqx ▸ (span S t).smul_mem p (subset_span hqt)) $
+λ p hp, span_induction hp (λ x hx, one_smul S x ▸ smul_mem_span_smul hs (subset_span hx))
+  (zero_mem _)
+  (λ _ _, add_mem _)
+  (λ k x hx, smul_mem_span_smul' hs hx)
+
+end submodule
+
+end semiring