feat(field_theory/tower): tower law (#3355)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/big_operators.lean

@@ -459,6 +459,11 @@ by simp [prod_apply_dite _ _ (λ x, x)]
   (∏ x in s.filter p, f x) * (∏ x in s.filter (λ x, ¬ p x), g x) :=
 by simp [prod_apply_ite _ _ (λ x, x)]
 
+@[to_additive]
+lemma prod_extend_by_one [decidable_eq α] (s : finset α) (f : α → β) :
+  ∏ i in s, (if i ∈ s then f i else 1) = ∏ i in s, f i :=
+prod_congr rfl $ λ i hi, if_pos hi
+
 @[simp, to_additive]
 lemma prod_dite_eq [decidable_eq α] (s : finset α) (a : α) (b : Π x : α, a = x → β) :
   (∏ x in s, (if h : a = x then b x h else 1)) = ite (a ∈ s) (b a rfl) 1 :=

src/algebra/pointwise.lean

@@ -259,6 +259,12 @@ lemma image_smul_prod [has_scalar α β] {t : set β} :
   (λ x : α × β, x.fst • x.snd) '' s.prod t = s • t :=
 image_prod _
 
+theorem range_smul_range [has_scalar α β] {ι κ : Type*} (b : ι → α) (c : κ → β) :
+  range b • range c = range (λ p : ι × κ, b p.1 • c p.2) :=
+ext $ λ x, ⟨λ hx, let ⟨p, q, ⟨i, hi⟩, ⟨j, hj⟩, hpq⟩ := set.mem_smul.1 hx in
+  ⟨(i, j), hpq ▸ hi ▸ hj ▸ rfl⟩,
+λ ⟨⟨i, j⟩, h⟩, set.mem_smul.2 ⟨b i, c j, ⟨i, rfl⟩, ⟨j, rfl⟩, h⟩⟩
+
 lemma singleton_smul [has_scalar α β] {t : set β} : ({a} : set α) • t = a • t :=
 image2_singleton_left
 

src/data/finset/basic.lean

@@ -1770,6 +1770,10 @@ protected def product (s : finset α) (t : finset β) : finset (α × β) := ⟨
 
 @[simp] theorem mem_product {p : α × β} : p ∈ s.product t ↔ p.1 ∈ s ∧ p.2 ∈ t := mem_product
 
+theorem subset_product [decidable_eq α] [decidable_eq β] {s : finset (α × β)} :
+  s ⊆ (s.image prod.fst).product (s.image prod.snd) :=
+λ p hp, mem_product.2 ⟨mem_image_of_mem _ hp, mem_image_of_mem _ hp⟩
+
 theorem product_eq_bind [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
  s.product t = s.bind (λa, t.image $ λb, (a, b)) :=
 ext $ λ ⟨x, y⟩, by simp only [mem_product, mem_bind, mem_image, exists_prop, prod.mk.inj_iff,

src/field_theory/tower.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+
+import ring_theory.algebra_tower
+import linear_algebra.finite_dimensional
+
+/-!
+# Tower of field extensions
+
+In this file we prove the tower law for arbitrary extensions and finite extensions.
+Suppose `L` is a field extension of `K` and `K` is a field extension of `F`.
+Then `[L:F] = [L:K] [K:F]` where `[E₁:E₂]` means the `E₂`-dimension of `E₁`.
+
+In fact we generalize it to algebras, where `L` is not necessarily a field, but just a `K`-algebra.
+
+## Implementation notes
+
+We prove two versions, since there are two notions of dimensions: `vector_space.dim` which gives
+the dimension of an arbitrary vector space as a cardinal, and `finite_dimensional.findim` which
+gives the dimension of a finitely-dimensional vector space as a natural number.
+
+## Tags
+
+tower law
+
+-/
+
+universes u v w u₁ v₁ w₁
+open_locale classical big_operators
+
+section field
+
+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]
+
+/-- 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' :
+  (cardinal.lift.{v w} (vector_space.dim F K) *
+      cardinal.lift.{w v} (vector_space.dim K A) : cardinal.{max w v}) =
+  cardinal.lift.{w v} (vector_space.dim F A) :=
+let ⟨b, hb⟩ := exists_is_basis F K, ⟨c, hc⟩ := exists_is_basis K A in
+by rw [← (vector_space.dim F K).lift_id, ← hb.mk_eq_dim,
+    ← (vector_space.dim K A).lift_id, ← hc.mk_eq_dim,
+    ← lift_umax.{w v}, ← (hb.smul hc).mk_eq_dim, mk_prod, lift_mul,
+    lift_lift, lift_lift, lift_lift, lift_lift, lift_umax]
+
+/-- 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] :
+  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
+
+namespace finite_dimensional
+
+theorem trans [finite_dimensional F K] [finite_dimensional K A] : finite_dimensional F A :=
+let ⟨b, hb⟩ := finite_dimensional.exists_is_basis_finset F K in
+let ⟨c, hc⟩ := finite_dimensional.exists_is_basis_finset K A in
+finite_dimensional.of_finite_basis $ hb.smul hc
+
+/-- 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 findim_mul_findim [finite_dimensional F K] [finite_dimensional K A] :
+  findim F K * findim K A = findim F A :=
+let ⟨b, hb⟩ := finite_dimensional.exists_is_basis_finset F K in
+let ⟨c, hc⟩ := finite_dimensional.exists_is_basis_finset K A in
+by rw [findim_eq_card_basis hb, findim_eq_card_basis hc,
+    findim_eq_card_basis (hb.smul hc), fintype.card_prod]
+
+end finite_dimensional
+
+end field

src/linear_algebra/basis.lean

@@ -101,6 +101,14 @@ linear_independent_iff.trans
 λ hf l hl, finsupp.ext $ λ i, classical.by_contradiction $ λ hni, hni $ hf _ _ hl _ $
   finsupp.mem_support_iff.2 hni⟩
 
+theorem linear_independent_iff'' :
+  linear_independent R v ↔ ∀ (s : finset ι) (g : ι → R) (hg : ∀ i ∉ s, g i = 0),
+    ∑ i in s, g i • v i = 0 → ∀ i, g i = 0 :=
+linear_independent_iff'.trans ⟨λ H s g hg hv i, if his : i ∈ s then H s g hv i his else hg i his,
+λ H s g hg i hi, by { convert H s (λ j, if j ∈ s then g j else 0) (λ j hj, if_neg hj)
+    (by simp_rw [ite_smul, zero_smul, finset.sum_extend_by_zero, hg]) i,
+  exact (if_pos hi).symm }⟩
+
 theorem linear_dependent_iff : ¬ linear_independent R v ↔
   ∃ s : finset ι, ∃ g : ι → R, s.sum (λ i, g i • v i) = 0 ∧ (∃ i ∈ s, g i ≠ 0) :=
 begin

src/ring_theory/algebra_tower.lean

@@ -6,6 +6,23 @@ Authors: Kenny Lau
 
 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)`.
+
+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]`.
+
+In this file we prepare the main lemma:
+if `{bi | i ∈ I}` is an `R`-basis of `S` and `{cj | j ∈ J}` is a `S`-basis
+of `A`, then `{bi cj | i ∈ I, j ∈ J}` is an `R`-basis of `A`. This statement does not require the
+base rings to be a field, so we also generalize the lemma to rings in this file.
+-/
+
 universes u v w u₁
 
 variables (R : Type u) (S : Type v) (A : Type w) (B : Type u₁)
@@ -21,19 +38,30 @@ 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]
 
-theorem algebra_map_eq [is_algebra_tower R S A] :
+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 :=
+⟨λ 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 (R S A)
+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 [is_algebra_tower R S A] (x : R) :
-  algebra_map R A x = algebra_map S A (algebra_map R S x) :=
+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]
 
+variables {R} (S) {A}
+theorem algebra_map_smul (r : R) (x : A) : algebra_map R S r • x = r • x :=
+by rw [algebra.algebra_map_eq_smul_one, smul_assoc, one_smul]
+
 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 :=
-⟨λ x y z, by simp_rw [algebra.smul_def, ring_hom.map_mul, mul_assoc, h]⟩
+theorem smul_left_comm (r : R) (s : S) (x : A) : r • s • x = s • r • x :=
+by simp_rw [algebra.smul_def, ← mul_assoc, algebra_map_apply R S A,
+    ← (algebra_map S A).map_mul, mul_comm s]
 
 @[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 clear h2; exact r • x) = r • x) : h1 = h2 :=
@@ -43,8 +71,6 @@ begin
   ext r, erw [← mul_one (g1 r), ← h12, ← mul_one (g2 r), ← h22, h], refl }
 end
 
-variables [is_algebra_tower R S A] [is_algebra_tower R S B]
-
 variables (R S A)
 theorem comap_eq : algebra.comap.algebra R S A = ‹_› :=
 algebra.ext _ _ $ λ x (z : A),
@@ -167,3 +193,109 @@ le_antisymm (adjoin_le $ set.image_subset_iff.2 $ λ y hy, ⟨y, subset_adjoin h
   (subalgebra.map_le.2 $ adjoin_le $ λ y hy, subset_adjoin ⟨y, hy, rfl⟩)
 
 end algebra
+
+namespace submodule
+
+open is_algebra_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 (R) {S A}
+/-- Restricting the scalars of submodules in an algebra tower. -/
+def restrict_scalars' (U : submodule S A) : submodule R A :=
+{ smul_mem' := λ r x hx, algebra_map_smul S r x ▸ U.smul_mem _ hx, .. U }
+
+variables (R S A)
+theorem restrict_scalars'_top : restrict_scalars' R (⊤ : submodule S A) = ⊤ := rfl
+
+variables {R S A}
+theorem restrict_scalars'_injective (U₁ U₂ : submodule S A)
+  (h : restrict_scalars' R U₁ = restrict_scalars' R U₂) : U₁ = U₂ :=
+ext $ by convert set.ext_iff.1 (ext'_iff.1 h); refl
+
+theorem restrict_scalars'_inj {U₁ U₂ : submodule S A} :
+  restrict_scalars' R U₁ = restrict_scalars' R U₂ ↔ U₁ = U₂ :=
+⟨restrict_scalars'_injective U₁ U₂, congr_arg _⟩
+
+end submodule
+
+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]
+
+namespace submodule
+
+open is_algebra_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_algebra_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_left_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_left_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
+
+
+section ring
+
+open_locale big_operators classical
+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]
+
+theorem linear_independent_smul {ι : Type v₁} {b : ι → S} {κ : Type w₁} {c : κ → A}
+  (hb : linear_independent R b) (hc : linear_independent S c) :
+  linear_independent R (λ p : ι × κ, b p.1 • c p.2) :=
+begin
+  rw linear_independent_iff' at hb hc, rw linear_independent_iff'', rintros s g hg hsg ⟨i, k⟩,
+  by_cases hik : (i, k) ∈ s,
+  { have h1 : ∑ i in (s.image prod.fst).product (s.image prod.snd), g i • b i.1 • c i.2 = 0,
+    { rw ← hsg, exact (finset.sum_subset finset.subset_product $ λ p _ hp,
+        show g p • b p.1 • c p.2 = 0, by rw [hg p hp, zero_smul]).symm },
+    rw [finset.sum_product, finset.sum_comm] at h1,
+    simp_rw [← is_algebra_tower.smul_assoc, ← finset.sum_smul] at h1,
+    exact hb _ _ (hc _ _ h1 k (finset.mem_image_of_mem _ hik)) i (finset.mem_image_of_mem _ hik) },
+  exact hg _ hik
+end
+
+theorem is_basis.smul {ι : Type v₁} {b : ι → S} {κ : Type w₁} {c : κ → A}
+  (hb : is_basis R b) (hc : is_basis S c) : is_basis R (λ p : ι × κ, b p.1 • c p.2) :=
+⟨linear_independent_smul hb.1 hc.1,
+by rw [← set.range_smul_range, submodule.span_smul hb.2, ← submodule.restrict_scalars'_top R S A,
+    submodule.restrict_scalars'_inj, hc.2]⟩
+
+end ring