chore(RingTheory): equivalence between algebraicity over IntermediateField.adjoin and Algebra.adjoin (#24004)

Author: alreadydone

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -623,7 +623,7 @@ open Algebra
 
 variable {R : Type u} {A : Type v} {B : Type w}
 variable [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
-variable (S : Subalgebra R A)
+variable (S T U : Subalgebra R A)
 
 instance subsingleton_of_subsingleton [Subsingleton A] : Subsingleton (Subalgebra R A) :=
   ⟨fun B C => ext fun x => by simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]⟩
@@ -642,31 +642,55 @@ def inclusion {S T : Subalgebra R A} (h : S ≤ T) : S →ₐ[R] T where
   map_zero' := rfl
   commutes' _ := rfl
 
-theorem inclusion_injective {S T : Subalgebra R A} (h : S ≤ T) : Function.Injective (inclusion h) :=
+variable {S T U} (h : S ≤ T)
+
+theorem inclusion_injective : Function.Injective (inclusion h) :=
   fun _ _ => Subtype.ext ∘ Subtype.mk.inj
 
 @[simp]
-theorem inclusion_self {S : Subalgebra R A} : inclusion (le_refl S) = AlgHom.id R S :=
+theorem inclusion_self : inclusion (le_refl S) = AlgHom.id R S :=
   AlgHom.ext fun _x => Subtype.ext rfl
 
 @[simp]
-theorem inclusion_mk {S T : Subalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S) :
-    inclusion h ⟨x, hx⟩ = ⟨x, h hx⟩ :=
+theorem inclusion_mk (x : A) (hx : x ∈ S) : inclusion h ⟨x, hx⟩ = ⟨x, h hx⟩ :=
   rfl
 
-theorem inclusion_right {S T : Subalgebra R A} (h : S ≤ T) (x : T) (m : (x : A) ∈ S) :
-    inclusion h ⟨x, m⟩ = x :=
+theorem inclusion_right (x : T) (m : (x : A) ∈ S) : inclusion h ⟨x, m⟩ = x :=
   Subtype.ext rfl
 
 @[simp]
-theorem inclusion_inclusion {S T U : Subalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : S) :
+theorem inclusion_inclusion (hst : S ≤ T) (htu : T ≤ U) (x : S) :
     inclusion htu (inclusion hst x) = inclusion (le_trans hst htu) x :=
   Subtype.ext rfl
 
 @[simp]
-theorem coe_inclusion {S T : Subalgebra R A} (h : S ≤ T) (s : S) : (inclusion h s : A) = s :=
+theorem coe_inclusion (s : S) : (inclusion h s : A) = s :=
   rfl
 
+namespace inclusion
+
+scoped instance isScalarTower_left (X) [SMul X R] [SMul X A] [IsScalarTower X R A] :
+    letI := (inclusion h).toModule; IsScalarTower X S T :=
+  letI := (inclusion h).toModule
+  ⟨fun x s t ↦ Subtype.ext <| by
+    rw [← one_smul R s, ← smul_assoc, one_smul, ← one_smul R (s • t), ← smul_assoc,
+      Algebra.smul_def, Algebra.smul_def]
+    apply mul_assoc⟩
+
+scoped instance isScalarTower_right (X) [MulAction A X] :
+    letI := (inclusion h).toModule; IsScalarTower S T X :=
+  letI := (inclusion h).toModule; ⟨fun _ ↦ mul_smul _⟩
+
+scoped instance faithfulSMul :
+    letI := (inclusion h).toModule; FaithfulSMul S T :=
+  letI := (inclusion h).toModule
+  ⟨fun {x y} h ↦ Subtype.ext <| by
+    convert Subtype.ext_iff.mp (h 1) using 1 <;> exact (mul_one _).symm⟩
+
+end inclusion
+
+variable (S)
+
 /-- Two subalgebras that are equal are also equivalent as algebras.
 
 This is the `Subalgebra` version of `LinearEquiv.ofEq` and `Equiv.setCongr`. -/

Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

@@ -24,6 +24,31 @@ variable (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E] (S : Set E)
 theorem algebra_adjoin_le_adjoin : Algebra.adjoin F S ≤ (adjoin F S).toSubalgebra :=
   Algebra.adjoin_le (subset_adjoin _ _)
 
+namespace algebraAdjoinAdjoin
+
+/-- `IntermediateField.adjoin` as an algebra over `Algebra.adjoin`. -/
+scoped instance : Algebra (Algebra.adjoin F S) (adjoin F S) :=
+  (Subalgebra.inclusion <| algebra_adjoin_le_adjoin F S).toAlgebra
+
+scoped instance (X) [SMul X F] [SMul X E] [IsScalarTower X F E] :
+    IsScalarTower X (Algebra.adjoin F S) (adjoin F S) :=
+  Subalgebra.inclusion.isScalarTower_left (algebra_adjoin_le_adjoin F S) _
+
+scoped instance (X) [MulAction E X] : IsScalarTower (Algebra.adjoin F S) (adjoin F S) X :=
+  Subalgebra.inclusion.isScalarTower_right (algebra_adjoin_le_adjoin F S) _
+
+scoped instance : FaithfulSMul (Algebra.adjoin F S) (adjoin F S) :=
+  Subalgebra.inclusion.faithfulSMul (algebra_adjoin_le_adjoin F S)
+
+scoped instance : IsFractionRing (Algebra.adjoin F S) (adjoin F S) :=
+  .of_field _ _ fun ⟨_, h⟩ ↦ have ⟨x, hx, y, hy, eq⟩ := mem_adjoin_iff_div.mp h
+    ⟨⟨x, hx⟩, ⟨y, hy⟩, Subtype.ext eq⟩
+
+scoped instance : Algebra.IsAlgebraic (Algebra.adjoin F S) (adjoin F S) :=
+  IsLocalization.isAlgebraic _ (nonZeroDivisors (Algebra.adjoin F S))
+
+end algebraAdjoinAdjoin
+
 theorem adjoin_eq_algebra_adjoin (inv_mem : ∀ x ∈ Algebra.adjoin F S, x⁻¹ ∈ Algebra.adjoin F S) :
     (adjoin F S).toSubalgebra = Algebra.adjoin F S :=
   le_antisymm

Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

@@ -32,10 +32,8 @@ variable (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E] {S : Set E}
 theorem mem_adjoin_range_iff {ι : Type*} (i : ι → E) (x : E) :
     x ∈ adjoin F (Set.range i) ↔ ∃ r s : MvPolynomial ι F,
       x = MvPolynomial.aeval i r / MvPolynomial.aeval i s := by
-  simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
-    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring,
-    Algebra.adjoin_range_eq_range_aeval, AlgHom.mem_range, exists_exists_eq_and]
-  tauto
+  simp_rw [mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval,
+    AlgHom.mem_range, exists_exists_eq_and]
 
 theorem mem_adjoin_iff (x : E) :
     x ∈ adjoin F S ↔ ∃ r s : MvPolynomial S F,
@@ -44,10 +42,8 @@ theorem mem_adjoin_iff (x : E) :
 
 theorem mem_adjoin_simple_iff {α : E} (x : E) :
     x ∈ adjoin F {α} ↔ ∃ r s : F[X], x = aeval α r / aeval α s := by
-  simp only [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
-    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring,
-    Algebra.adjoin_singleton_eq_range_aeval, AlgHom.mem_range, exists_exists_eq_and]
-  tauto
+  simp only [mem_adjoin_iff_div, Algebra.adjoin_singleton_eq_range_aeval,
+    AlgHom.mem_range, exists_exists_eq_and]
 
 variable {F}
 

Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean

@@ -35,6 +35,12 @@ def adjoin : IntermediateField F E :=
 theorem adjoin_toSubfield :
     (adjoin F S).toSubfield = Subfield.closure (Set.range (algebraMap F E) ∪ S) := rfl
 
+variable {F S} in
+theorem mem_adjoin_iff_div {x : E} : x ∈ adjoin F S ↔
+    ∃ r ∈ Algebra.adjoin F S, ∃ s ∈ Algebra.adjoin F S, x = r / s := by
+  simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
+    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_comm]
+
 end AdjoinDef
 
 section Lattice

Mathlib/GroupTheory/GroupAction/SubMulAction.lean

@@ -136,6 +136,9 @@ variable {N α : Type*} [SetLike S α] [SMul M N] [SMul M α] [Monoid N]
 instance (priority := 50) smul' : SMul M s where
   smul r x := ⟨r • x.1, smul_one_smul N r x.1 ▸ smul_mem _ x.2⟩
 
+instance (priority := 50) : IsScalarTower M N s where
+  smul_assoc m n x := Subtype.ext (smul_assoc m n x.1)
+
 @[to_additive (attr := simp, norm_cast)]
 protected theorem val_smul_of_tower (r : M) (x : s) : (↑(r • x) : α) = r • (x : α) :=
   rfl

Mathlib/RingTheory/Algebraic/Integral.lean

@@ -312,6 +312,28 @@ theorem IsAlgebraic.trans_isIntegral [Algebra.IsAlgebraic R S] [int : Algebra.Is
     Algebra.IsAlgebraic R A :=
   ⟨fun _ ↦ (int.1 _).trans_isAlgebraic _⟩
 
+variable {A}
+
+protected theorem IsIntegral.isAlgebraic_iff [Algebra.IsIntegral R S] [FaithfulSMul R S]
+    {a : A} : IsAlgebraic R a ↔ IsAlgebraic S a :=
+  ⟨.extendScalars (FaithfulSMul.algebraMap_injective ..), .restrictScalars_of_isIntegral _⟩
+
+theorem IsIntegral.isAlgebraic_iff_top [Algebra.IsIntegral R S]
+    [FaithfulSMul R S] : Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A := by
+  simp_rw [Algebra.isAlgebraic_def, Algebra.IsIntegral.isAlgebraic_iff R S]
+
+protected theorem IsAlgebraic.isAlgebraic_iff [Algebra.IsAlgebraic R S] [FaithfulSMul R S]
+    {a : A} : IsAlgebraic R a ↔ IsAlgebraic S a :=
+  ⟨.extendScalars (FaithfulSMul.algebraMap_injective ..), .restrictScalars _⟩
+
+theorem IsAlgebraic.isAlgebraic_iff_top [Algebra.IsAlgebraic R S]
+    [FaithfulSMul R S] : Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A := by
+  simp_rw [Algebra.isAlgebraic_def, Algebra.IsAlgebraic.isAlgebraic_iff R S]
+
+theorem IsAlgebraic.isAlgebraic_iff_bot [Algebra.IsAlgebraic S A] [FaithfulSMul S A] :
+    Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R A :=
+  ⟨fun _ ↦ .trans R S A, fun _ ↦ .tower_bot_of_injective (FaithfulSMul.algebraMap_injective S A)⟩
+
 end Algebra
 
 variable (R S)
@@ -391,29 +413,43 @@ namespace Transcendental
 
 section
 
-variable (S) {a : A} (ha : Transcendental R a)
+variable (S) [NoZeroDivisors S] {a : A} (ha : Transcendental R a)
 include ha
 
-lemma extendScalars_of_isIntegral [NoZeroDivisors S] [Algebra.IsIntegral R S] :
+lemma extendScalars_of_isIntegral [Algebra.IsIntegral R S] :
     Transcendental S a := by
   contrapose ha
   rw [Transcendental, not_not] at ha ⊢
   exact ha.restrictScalars_of_isIntegral _
 
-lemma extendScalars [NoZeroDivisors S] [Algebra.IsAlgebraic R S] : Transcendental S a := by
+lemma extendScalars [Algebra.IsAlgebraic R S] : Transcendental S a := by
   contrapose ha
   rw [Transcendental, not_not] at ha ⊢
   exact ha.restrictScalars _
 
 end
 
-variable {a : S} (ha : Transcendental R a)
+variable [NoZeroDivisors S] {a : S} (ha : Transcendental R a)
 include ha
 
-protected lemma integralClosure [NoZeroDivisors S] : Transcendental (integralClosure R S) a :=
+protected lemma integralClosure : Transcendental (integralClosure R S) a :=
   ha.extendScalars_of_isIntegral _
 
-lemma subalgebraAlgebraicClosure [IsDomain R] [NoZeroDivisors S] :
+lemma subalgebraAlgebraicClosure [IsDomain R] :
     Transcendental (Subalgebra.algebraicClosure R S) a := ha.extendScalars _
 
 end Transcendental
+
+namespace Algebra
+
+variable (R S) [NoZeroDivisors S] [FaithfulSMul R S] {a : A}
+
+protected theorem IsIntegral.transcendental_iff [Algebra.IsIntegral R S] :
+    Transcendental R a ↔ Transcendental S a :=
+  ⟨(·.extendScalars_of_isIntegral _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩
+
+protected theorem IsAlgebraic.transcendental_iff [Algebra.IsAlgebraic R S] :
+    Transcendental R a ↔ Transcendental S a :=
+  ⟨(·.extendScalars _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩
+
+end Algebra

Mathlib/RingTheory/AlgebraicIndependent/AlgebraicClosure.lean

@@ -22,14 +22,16 @@ algebraically independent over the algebraic closure.
 
 open Function Algebra
 
-namespace AlgebraicIndependent
+section
 
 variable {ι R S A : Type*} {x : ι → A} (S)
 variable [CommRing R] [CommRing S] [CommRing A]
 variable [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A]
 variable [NoZeroDivisors S] (hx : AlgebraicIndependent R x)
 include hx
 
+namespace AlgebraicIndependent
+
 theorem extendScalars [alg : Algebra.IsAlgebraic R S] : AlgebraicIndependent S x := by
   refine algebraicIndependent_of_finite_type'
     (Algebra.IsAlgebraic.injective_tower_top S hx.algebraMap_injective) fun t fin ind i hi ↦ ?_
@@ -76,3 +78,71 @@ protected theorem algebraicClosure {F E : Type*} [Field F] [Field E] [Algebra F
   hx.extendScalars _
 
 end AlgebraicIndependent
+
+namespace Algebra
+
+variable (R) [FaithfulSMul R S]
+omit hx
+
+protected theorem IsIntegral.algebraicIndependent_iff [Algebra.IsIntegral R S] :
+    AlgebraicIndependent R x ↔ AlgebraicIndependent S x :=
+  ⟨(·.extendScalars_of_isIntegral _),
+    (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩
+
+protected theorem IsIntegral.isTranscendenceBasis_iff [Algebra.IsIntegral R S] :
+    IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x := by
+  simp_rw [IsTranscendenceBasis, IsIntegral.algebraicIndependent_iff R S]
+
+protected theorem IsAlgebraic.algebraicIndependent_iff [Algebra.IsAlgebraic R S] :
+    AlgebraicIndependent R x ↔ AlgebraicIndependent S x :=
+  ⟨(·.extendScalars _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩
+
+protected theorem IsAlgebraic.isTranscendenceBasis_iff [Algebra.IsAlgebraic R S] :
+    IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x := by
+  simp_rw [IsTranscendenceBasis, IsAlgebraic.algebraicIndependent_iff R S]
+
+end Algebra
+
+end
+
+namespace IntermediateField
+
+variable {ι F E R S : Type*} {s : Set E}
+variable [Field F] [Field E] [Algebra F E]
+variable [CommRing R] [Algebra R F] [Algebra R E] [IsScalarTower R F E]
+
+open scoped algebraAdjoinAdjoin
+
+section Ring
+
+variable [Ring S] [Algebra E S]
+
+theorem isAlgebraic_adjoin_iff {x : S} :
+    IsAlgebraic (adjoin F s) x ↔ IsAlgebraic (Algebra.adjoin F s) x :=
+  (IsAlgebraic.isAlgebraic_iff ..).symm
+
+theorem isAlgebraic_adjoin_iff_top :
+    Algebra.IsAlgebraic (adjoin F s) S ↔ Algebra.IsAlgebraic (Algebra.adjoin F s) S :=
+  (IsAlgebraic.isAlgebraic_iff_top ..).symm
+
+theorem isAlgebraic_adjoin_iff_bot :
+    Algebra.IsAlgebraic R (adjoin F s) ↔ Algebra.IsAlgebraic R (Algebra.adjoin F s) :=
+  (IsAlgebraic.isAlgebraic_iff_bot ..).symm
+
+theorem transcendental_adjoin_iff {x : S} :
+    Transcendental (adjoin F s) x ↔ Transcendental (Algebra.adjoin F s) x :=
+  (IsAlgebraic.transcendental_iff ..).symm
+
+end Ring
+
+variable [CommRing S] [Algebra E S]
+
+theorem algebraicIndependent_adjoin_iff {x : ι → S} :
+    AlgebraicIndependent (adjoin F s) x ↔ AlgebraicIndependent (Algebra.adjoin F s) x :=
+  (Algebra.IsAlgebraic.algebraicIndependent_iff ..).symm
+
+theorem isTranscendenceBasis_adjoin_iff {x : ι → S} :
+    IsTranscendenceBasis (adjoin F s) x ↔ IsTranscendenceBasis (Algebra.adjoin F s) x :=
+  (Algebra.IsAlgebraic.isTranscendenceBasis_iff ..).symm
+
+end IntermediateField

Mathlib/RingTheory/Localization/FractionRing.lean

@@ -66,6 +66,23 @@ namespace IsFractionRing
 
 open IsLocalization
 
+theorem of_field [Field K] [Algebra R K] [FaithfulSMul R K]
+    (surj : ∀ z : K, ∃ x y, z = algebraMap R K x / algebraMap R K y) :
+    IsFractionRing R K :=
+  have inj := FaithfulSMul.algebraMap_injective R K
+  have := inj.noZeroDivisors _ (map_zero _) (map_mul _)
+  have := Module.nontrivial R K
+{ map_units' x :=
+    .mk0 _ <| (map_ne_zero_iff _ inj).mpr <| mem_nonZeroDivisors_iff_ne_zero.mp x.2
+  surj' z := by
+    have ⟨x, y, eq⟩ := surj z
+    obtain rfl | hy := eq_or_ne y 0
+    · obtain rfl : z = 0 := by simpa using eq
+      exact ⟨(0, 1), by simp⟩
+    exact ⟨⟨x, y, mem_nonZeroDivisors_iff_ne_zero.mpr hy⟩,
+      (eq_div_iff_mul_eq <| (map_ne_zero_iff _ inj).mpr hy).mp eq⟩
+  exists_of_eq eq := ⟨1, by simpa using inj eq⟩ }
+
 variable {R K}
 
 section CommRing