feat({Ring|Field}Theory/Adjoin): add various results on adjoin (#9790)

Main changes:

- for intermediate fields: add `extendScalars_adjoin`, `restrictScalars_adjoin_of_algEquiv`, `sup_toSubalgebra_of_isAlgebraic`, `adjoin_toSubalgebra_of_isAlgebraic`, `adjoin_rank_le_of_isAlgebraic`, and golf `sup_toSubalgebra`
- for subalgebras: add `adjoin_eq_span_of_eq_span`, `adjoin_eq_span_basis`, `restrictScalars_adjoin`, `restrictScalars_adjoin_of_algEquiv`, `adjoin_rank_le`



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/FieldTheory/Adjoin.lean

@@ -484,6 +484,31 @@ theorem restrictScalars_adjoin (K : IntermediateField F E) (S : Set E) :
     restrictScalars F (adjoin K S) = adjoin F (K ∪ S) := by
   rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]
 
+variable {F} in
+theorem extendScalars_adjoin {K : IntermediateField F E} {S : Set E} (h : K ≤ adjoin F S) :
+    extendScalars h = adjoin K S := restrictScalars_injective F <| by
+  rw [extendScalars_restrictScalars, restrictScalars_adjoin]
+  exact le_antisymm (adjoin.mono F S _ <| Set.subset_union_right _ S) <| adjoin_le_iff.2 <|
+    Set.union_subset h (subset_adjoin F S)
+
+variable {F} in
+/-- If `E / L / F` and `E / L' / F` are two field extension towers, `L ≃ₐ[F] L'` is an isomorphism
+compatible with `E / L` and `E / L'`, then for any subset `S` of `E`, `L(S)` and `L'(S)` are
+equal as intermediate fields of `E / F`. -/
+theorem restrictScalars_adjoin_of_algEquiv
+    {L L' : Type*} [Field L] [Field L']
+    [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E]
+    [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L')
+    (hi : algebraMap L E = (algebraMap L' E) ∘ i) (S : Set E) :
+    (adjoin L S).restrictScalars F = (adjoin L' S).restrictScalars F := by
+  apply_fun toSubfield using (fun K K' h ↦ by
+    ext x; change x ∈ K.toSubfield ↔ x ∈ K'.toSubfield; rw [h])
+  change Subfield.closure _ = Subfield.closure _
+  congr
+  ext x
+  exact ⟨fun ⟨y, h⟩ ↦ ⟨i y, by rw [← h, hi]; rfl⟩,
+    fun ⟨y, h⟩ ↦ ⟨i.symm y, by rw [← h, hi, Function.comp_apply, AlgEquiv.apply_symm_apply]⟩⟩
+
 theorem algebra_adjoin_le_adjoin : Algebra.adjoin F S ≤ (adjoin F S).toSubalgebra :=
   Algebra.adjoin_le (subset_adjoin _ _)
 #align intermediate_field.algebra_adjoin_le_adjoin IntermediateField.algebra_adjoin_le_adjoin
@@ -648,37 +673,47 @@ theorem le_sup_toSubalgebra : E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2
   sup_le (show E1 ≤ E1 ⊔ E2 from le_sup_left) (show E2 ≤ E1 ⊔ E2 from le_sup_right)
 #align intermediate_field.le_sup_to_subalgebra IntermediateField.le_sup_toSubalgebra
 
-theorem sup_toSubalgebra [h1 : FiniteDimensional K E1] [h2 : FiniteDimensional K E2] :
+theorem sup_toSubalgebra_of_isAlgebraic_right (halg : Algebra.IsAlgebraic K E2) :
     (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra := by
-  let S1 := E1.toSubalgebra
-  let S2 := E2.toSubalgebra
-  refine'
-    le_antisymm
-      (show _ ≤ (S1 ⊔ S2).toIntermediateField _ from
-        sup_le (show S1 ≤ _ from le_sup_left) (show S2 ≤ _ from le_sup_right))
-      (le_sup_toSubalgebra E1 E2)
-  suffices IsField (S1 ⊔ S2 : Subalgebra K L) by
-    intro x hx
-    by_cases hx' : (⟨x, hx⟩ : (S1 ⊔ S2 : Subalgebra K L)) = 0
-    · rw [← Subtype.coe_mk x, hx', Subalgebra.coe_zero, inv_zero]
-      exact (S1 ⊔ S2).zero_mem
-    · obtain ⟨y, h⟩ := this.mul_inv_cancel hx'
-      exact (congr_arg (· ∈ S1 ⊔ S2) <| eq_inv_of_mul_eq_one_right <| Subtype.ext_iff.mp h).mp y.2
-  exact
-    isField_of_isIntegral_of_isField'
-      (Algebra.isIntegral_sup.mpr
-        ⟨Algebra.IsIntegral.of_finite K E1, Algebra.IsIntegral.of_finite K E2⟩)
-      (Field.toIsField K)
-#align intermediate_field.sup_to_subalgebra IntermediateField.sup_toSubalgebra
-
-instance finiteDimensional_sup [h1 : FiniteDimensional K E1] [h2 : FiniteDimensional K E2] :
+  have : (adjoin E1 (E2 : Set L)).toSubalgebra = _ := adjoin_algebraic_toSubalgebra fun x h ↦
+    IsAlgebraic.tower_top E1 (isAlgebraic_iff.1 (halg ⟨x, h⟩))
+  apply_fun Subalgebra.restrictScalars K at this
+  erw [← restrictScalars_toSubalgebra, restrictScalars_adjoin,
+    Algebra.restrictScalars_adjoin] at this
+  exact this
+
+theorem sup_toSubalgebra_of_isAlgebraic_left (halg : Algebra.IsAlgebraic K E1) :
+    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra := by
+  have := sup_toSubalgebra_of_isAlgebraic_right E2 E1 halg
+  rwa [sup_comm (a := E1), sup_comm (a := E1.toSubalgebra)]
+
+/-- The compositum of two intermediate fields is equal to the compositum of them
+as subalgebras, if one of them is algebraic over the base field. -/
+theorem sup_toSubalgebra_of_isAlgebraic
+    (halg : Algebra.IsAlgebraic K E1 ∨ Algebra.IsAlgebraic K E2) :
+    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
+  halg.elim (sup_toSubalgebra_of_isAlgebraic_left E1 E2)
+    (sup_toSubalgebra_of_isAlgebraic_right E1 E2)
+
+theorem sup_toSubalgebra_of_left [FiniteDimensional K E1] :
+    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
+  sup_toSubalgebra_of_isAlgebraic_left E1 E2 (Algebra.IsAlgebraic.of_finite K _)
+#align intermediate_field.sup_to_subalgebra IntermediateField.sup_toSubalgebra_of_left
+
+@[deprecated] alias sup_toSubalgebra := sup_toSubalgebra_of_left
+
+theorem sup_toSubalgebra_of_right [FiniteDimensional K E2] :
+    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
+  sup_toSubalgebra_of_isAlgebraic_right E1 E2 (Algebra.IsAlgebraic.of_finite K _)
+
+instance finiteDimensional_sup [FiniteDimensional K E1] [FiniteDimensional K E2] :
     FiniteDimensional K (E1 ⊔ E2 : IntermediateField K L) := by
   let g := Algebra.TensorProduct.productMap E1.val E2.val
   suffices g.range = (E1 ⊔ E2).toSubalgebra by
     have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) :=
       g.toLinearMap.finiteDimensional_range
     rwa [this] at h
-  rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra]
+  rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]
 #align intermediate_field.finite_dimensional_sup IntermediateField.finiteDimensional_sup
 
 variable {ι : Type*} {t : ι → IntermediateField K L}
@@ -749,6 +784,61 @@ theorem isSplittingField_iSup {p : ι → K[X]}
 
 end Supremum
 
+section Tower
+
+variable (E)
+
+variable {K : Type*} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K]
+
+/-- If `K / E / F` is a field extension tower, `L` is an intermediate field of `K / F`, such that
+either `E / F` or `L / F` is algebraic, then `E(L) = E[L]`. -/
+theorem adjoin_toSubalgebra_of_isAlgebraic (L : IntermediateField F K)
+    (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) :
+    (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) := by
+  let i := IsScalarTower.toAlgHom F E K
+  let E' := i.fieldRange
+  let i' : E ≃ₐ[F] E' := AlgEquiv.ofInjectiveField i
+  have hi : algebraMap E K = (algebraMap E' K) ∘ i' := by ext x; rfl
+  apply_fun _ using Subalgebra.restrictScalars_injective F
+  erw [← restrictScalars_toSubalgebra, restrictScalars_adjoin_of_algEquiv i' hi,
+    Algebra.restrictScalars_adjoin_of_algEquiv i' hi, restrictScalars_adjoin,
+    Algebra.restrictScalars_adjoin]
+  exact E'.sup_toSubalgebra_of_isAlgebraic L (halg.imp i'.isAlgebraic id)
+
+theorem adjoin_toSubalgebra_of_isAlgebraic_left (L : IntermediateField F K)
+    (halg : Algebra.IsAlgebraic F E) :
+    (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) :=
+  adjoin_toSubalgebra_of_isAlgebraic E L (Or.inl halg)
+
+theorem adjoin_toSubalgebra_of_isAlgebraic_right (L : IntermediateField F K)
+    (halg : Algebra.IsAlgebraic F L) :
+    (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) :=
+  adjoin_toSubalgebra_of_isAlgebraic E L (Or.inr halg)
+
+/-- If `K / E / F` is a field extension tower, `L` is an intermediate field of `K / F`, such that
+either `E / F` or `L / F` is algebraic, then `[E(L) : E] ≤ [L : F]`. A corollary of
+`Subalgebra.adjoin_rank_le` since in this case `E(L) = E[L]`. -/
+theorem adjoin_rank_le_of_isAlgebraic (L : IntermediateField F K)
+    (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) :
+    Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L := by
+  have h : (adjoin E (L.toSubalgebra : Set K)).toSubalgebra =
+      Algebra.adjoin E (L.toSubalgebra : Set K) :=
+    L.adjoin_toSubalgebra_of_isAlgebraic E halg
+  have := L.toSubalgebra.adjoin_rank_le E
+  rwa [(Subalgebra.equivOfEq _ _ h).symm.toLinearEquiv.rank_eq] at this
+
+theorem adjoin_rank_le_of_isAlgebraic_left (L : IntermediateField F K)
+    (halg : Algebra.IsAlgebraic F E) :
+    Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L :=
+  adjoin_rank_le_of_isAlgebraic E L (Or.inl halg)
+
+theorem adjoin_rank_le_of_isAlgebraic_right (L : IntermediateField F K)
+    (halg : Algebra.IsAlgebraic F L) :
+    Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L :=
+  adjoin_rank_le_of_isAlgebraic E L (Or.inr halg)
+
+end Tower
+
 open Set CompleteLattice
 
 /- Porting note: this was tagged `simp`, but the LHS can be simplified now that the notation

Mathlib/RingTheory/Adjoin/Basic.lean

@@ -480,4 +480,52 @@ def Subring.closureEquivAdjoinInt {R : Type*} [Ring R] (s : Set R) :
     Subring.closure s ≃ₐ[ℤ] Algebra.adjoin ℤ s :=
   Subalgebra.equivOfEq (subalgebraOfSubring <| Subring.closure s) _ (adjoin_int s).symm
 
-  end NatInt
+end NatInt
+
+section
+
+variable (F E : Type*) {K : Type*} [CommSemiring E] [Semiring K] [SMul F E] [Algebra E K]
+
+/-- If `K / E / F` is a ring extension tower, `L` is a submonoid of `K / F` which is generated by
+`S` as an `F`-module, then `E[L]` is generated by `S` as an `E`-module. -/
+theorem Submonoid.adjoin_eq_span_of_eq_span [Semiring F] [Module F K] [IsScalarTower F E K]
+    (L : Submonoid K) {S : Set K} (h : (L : Set K) = span F S) :
+    toSubmodule (adjoin E (L : Set K)) = span E S := by
+  rw [adjoin_eq_span, L.closure_eq, h]
+  exact (span_le.mpr <| span_subset_span _ _ _).antisymm (span_mono subset_span)
+
+variable [CommSemiring F] [Algebra F K] [IsScalarTower F E K] (L : Subalgebra F K) {F}
+
+/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F` which is generated by
+`S` as an `F`-module, then `E[L]` is generated by `S` as an `E`-module. -/
+theorem Subalgebra.adjoin_eq_span_of_eq_span {S : Set K} (h : toSubmodule L = span F S) :
+    toSubmodule (adjoin E (L : Set K)) = span E S :=
+  L.toSubmonoid.adjoin_eq_span_of_eq_span F E (congr_arg ((↑) : _ → Set K) h)
+
+/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F`,
+then `E[L]` is generated by any basis of `L / F` as an `E`-module. -/
+theorem Subalgebra.adjoin_eq_span_basis {ι : Type*} (bL : Basis ι F L) :
+    toSubmodule (adjoin E (L : Set K)) = span E (Set.range fun i : ι ↦ (bL i).1) :=
+  L.adjoin_eq_span_of_eq_span E <| by
+    simpa only [← L.range_val, Submodule.map_span, Submodule.map_top, ← Set.range_comp]
+      using congr_arg (Submodule.map L.val) bL.span_eq.symm
+
+theorem Algebra.restrictScalars_adjoin (F : Type*) [CommSemiring F] {E : Type*} [CommSemiring E]
+    [Algebra F E] (K : Subalgebra F E) (S : Set E) :
+    (Algebra.adjoin K S).restrictScalars F = Algebra.adjoin F (K ∪ S) := by
+  conv_lhs => rw [← Algebra.adjoin_eq K, ← Algebra.adjoin_union_eq_adjoin_adjoin]
+
+/-- If `E / L / F` and `E / L' / F` are two ring extension towers, `L ≃ₐ[F] L'` is an isomorphism
+compatible with `E / L` and `E / L'`, then for any subset `S` of `E`, `L[S]` and `L'[S]` are
+equal as subalgebras of `E / F`. -/
+theorem Algebra.restrictScalars_adjoin_of_algEquiv
+    {F E L L' : Type*} [CommSemiring F] [CommSemiring L] [CommSemiring L'] [Semiring E]
+    [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E] [Algebra F E]
+    [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L')
+    (hi : algebraMap L E = (algebraMap L' E) ∘ i) (S : Set E) :
+    (Algebra.adjoin L S).restrictScalars F = (Algebra.adjoin L' S).restrictScalars F := by
+  apply_fun Subalgebra.toSubsemiring using fun K K' h ↦ by rwa [SetLike.ext'_iff] at h ⊢
+  change Subsemiring.closure _ = Subsemiring.closure _
+  erw [hi, Set.range_comp, i.toEquiv.range_eq_univ, Set.image_univ]
+
+end

Mathlib/RingTheory/Adjoin/Field.lean

@@ -108,3 +108,14 @@ theorem IsIntegral.minpoly_splits_tower_top [Algebra K L] [IsScalarTower R K L]
     Splits (algebraMap K L) (minpoly K x) := by
   rw [IsScalarTower.algebraMap_eq R K L] at h
   exact int.minpoly_splits_tower_top' h
+
+/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F`,
+then `[E[L] : E] ≤ [L : F]`. -/
+lemma Subalgebra.adjoin_rank_le {F : Type*} (E : Type*) {K : Type*}
+    [CommRing F] [StrongRankCondition F] [CommRing E] [StrongRankCondition E] [Ring K]
+    [SMul F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K]
+    (L : Subalgebra F K) [Module.Free F L] :
+    Module.rank E (Algebra.adjoin E (L : Set K)) ≤ Module.rank F L := by
+  rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex F L,
+    L.adjoin_eq_span_basis E (Module.Free.chooseBasis F L)]
+  exact rank_span_le _ |>.trans Cardinal.mk_range_le