Disjoint extensions with coprime different ideals

Let A ⊆ B be a finite extension of Dedekind domains and assume that A ⊆ R₁, R₂ ⊆ B are two subrings such that Frac R₁ ⊔ Frac R₂ = Frac B, Frac R₁ and Frac R₂ are linearly disjoint over Frac A, and that 𝓓(R₁/A) and 𝓓(R₂/A) are coprime where 𝓓 denotes the different ideal and Frac R denotes the fraction field of a domain R.

Main results and definitions

• FractionalIdeal.differentIdeal_eq_map_differentIdeal: 𝓓(B/R₁) = 𝓓(R₂/A)
• FractionalIdeal.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime: 𝓓(B/A) = 𝓓(R₁/A) * 𝓓(R₂/A).
• Module.Basis.ofIsCoprimeDifferentIdeal: Construct a R₁-basis of B by lifting an A-basis of R₂.
• IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal: B is generated (as an A-algebra) by R₁ and R₂.

theorem Submodule.traceDual_le_span_map_traceDual (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Field L] [Algebra B L] [Algebra A L] [Algebra K L] [FiniteDimensional K L] [IsScalarTower A K L] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [Algebra R₁ ↥F₁] [Algebra R₂ ↥F₂] [NoZeroSMulDivisors R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [Module.Free A R₂] [IsLocalization (Algebra.algebraMapSubmonoid R₂ (nonZeroDivisors A)) ↥F₂] (h₁ : F₁.LinearDisjoint ↥F₂) (h₂ : F₁ ⊔ F₂ = ⊤) : restrictScalars R₁ (traceDual R₁ (↥F₁) 1) ≤ span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))

theorem IsDedekindDomain.differentIdeal_dvd_map_differentIdeal (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Field L] [Algebra B L] [Algebra A L] [Algebra K L] [FiniteDimensional K L] [IsScalarTower A K L] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [Algebra R₁ ↥F₁] [Algebra R₂ ↥F₂] [NoZeroSMulDivisors R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [NoZeroSMulDivisors R₁ B] [NoZeroSMulDivisors R₂ B] [Algebra.IsIntegral R₂ B] [Module.Free A R₂] [IsLocalization (Algebra.algebraMapSubmonoid R₂ (nonZeroDivisors A)) ↥F₂] (h₁ : F₁.LinearDisjoint ↥F₂) (h₂ : F₁ ⊔ F₂ = ⊤) : differentIdeal R₁ B ∣ Ideal.map (algebraMap R₂ B) (differentIdeal A R₂)

theorem IsDedekindDomain.map_differentIdeal_dvd_differentIdeal (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Module.Finite A R₂] [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDomain R₂] [IsIntegrallyClosed A] [NoZeroSMulDivisors R₁ B] [NoZeroSMulDivisors R₂ B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [NoZeroSMulDivisors A R₁] [NoZeroSMulDivisors A R₂] [Module.Finite A R₁] [Module.Finite R₂ B] [IsScalarTower A R₂ B] [Module.Finite R₁ B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsScalarTower A R₁ B] (h : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))) : Ideal.map (algebraMap R₂ B) (differentIdeal A R₂) ∣ differentIdeal R₁ B

theorem IsDedekindDomain.differentIdeal_eq_map_differentIdeal (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Field L] [Algebra B L] [Algebra A L] [Algebra K L] [FiniteDimensional K L] [IsScalarTower A K L] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [Algebra R₁ ↥F₁] [Algebra R₂ ↥F₂] [NoZeroSMulDivisors R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [NoZeroSMulDivisors R₁ B] [NoZeroSMulDivisors R₂ B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [NoZeroSMulDivisors A R₁] [NoZeroSMulDivisors A R₂] [Module.Finite A R₁] [Module.Finite R₂ B] [IsScalarTower A R₂ B] [Module.Finite R₁ B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsScalarTower A R₁ B] [Module.Free A R₂] (h₁ : F₁.LinearDisjoint ↥F₂) (h₂ : F₁ ⊔ F₂ = ⊤) (h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))) : differentIdeal R₁ B = Ideal.map (algebraMap R₂ B) (differentIdeal A R₂)

theorem IsDedekindDomain.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Field L] [Algebra B L] [Algebra A L] [Algebra K L] [FiniteDimensional K L] [IsScalarTower A K L] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [Algebra R₁ ↥F₁] [Algebra R₂ ↥F₂] [NoZeroSMulDivisors R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [NoZeroSMulDivisors R₁ B] [NoZeroSMulDivisors R₂ B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [NoZeroSMulDivisors A R₁] [NoZeroSMulDivisors A R₂] [Module.Finite A R₁] [Module.Finite R₂ B] [IsScalarTower A R₂ B] [Module.Finite R₁ B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsScalarTower A R₁ B] [Module.Free A R₂] (h₁ : F₁.LinearDisjoint ↥F₂) (h₂ : F₁ ⊔ F₂ = ⊤) (h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))) : differentIdeal A B = differentIdeal R₁ B * differentIdeal R₂ B

Let A ⊆ B be a finite extension of Dedekind domains and assume that A ⊆ R₁, R₂ ⊆ B are two subrings such that Frac R₁ ⊔ Frac R₂ = Frac B, Frac R₁ and Frac R₂ are linearly disjoint over Frac A, and that 𝓓(R₁/A) and 𝓓(R₂/A) are coprime where 𝓓 denotes the different ideal and Frac R denotes the fraction field of a domain R. We have 𝓓(B/A) = 𝓓(R₁/A) * 𝓓(R₂/A).

theorem Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Field L] [Algebra B L] [Algebra A L] [Algebra K L] [FiniteDimensional K L] [IsScalarTower A K L] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [Algebra R₁ ↥F₁] [Algebra R₂ ↥F₂] [NoZeroSMulDivisors R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [NoZeroSMulDivisors R₁ B] [NoZeroSMulDivisors R₂ B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [NoZeroSMulDivisors A R₁] [NoZeroSMulDivisors A R₂] [Module.Finite A R₁] [Module.Finite R₂ B] [IsScalarTower A R₂ B] [Module.Finite R₁ B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsScalarTower A R₁ B] [Module.Free A R₂] [IsLocalization (Algebra.algebraMapSubmonoid R₂ (nonZeroDivisors A)) ↥F₂] (h₁ : F₁.LinearDisjoint ↥F₂) (h₂ : F₁ ⊔ F₂ = ⊤) (h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))) : span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1)) = restrictScalars R₁ (traceDual R₁ (↥F₁) 1)

noncomputable def Module.Basis.ofIsCoprimeDifferentIdeal (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Field L] [Algebra B L] [Algebra A L] [Algebra K L] [FiniteDimensional K L] [IsScalarTower A K L] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [Algebra R₁ ↥F₁] [Algebra R₂ ↥F₂] [NoZeroSMulDivisors R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [NoZeroSMulDivisors R₁ B] [NoZeroSMulDivisors R₂ B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [NoZeroSMulDivisors A R₁] [NoZeroSMulDivisors A R₂] [Module.Finite A R₁] [Module.Finite R₂ B] [IsScalarTower A R₂ B] [Module.Finite R₁ B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsScalarTower A R₁ B] (h₁ : F₁.LinearDisjoint ↥F₂) (h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤) (h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))) {ι : Type u_7} (b : Basis ι A R₂) : Basis ι R₁ B

Let A ⊆ B be a finite extension of Dedekind domains and assume that A ⊆ R₁, R₂ ⊆ B are two subrings such that Frac R₁ ⊔ Frac R₂ = Frac B, Frac R₁ and Frac R₂ are linearly disjoint over Frac A, and that 𝓓(R₁/A) and 𝓓(R₂/A) are coprime where 𝓓 denotes the different ideal and Frac R denotes the fraction field of a domain R. Construct a R₁-basis of B by lifting an A-basis of R₂.

Equations

• Module.Basis.ofIsCoprimeDifferentIdeal A B R₁ R₂ h₁ h₂ h₃ b = Module.Basis.mk ⋯ ⋯

@[simp]

theorem Module.Basis.ofIsCoprimeDifferentIdeal_apply (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Field L] [Algebra B L] [Algebra A L] [Algebra K L] [FiniteDimensional K L] [IsScalarTower A K L] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [Algebra R₁ ↥F₁] [Algebra R₂ ↥F₂] [NoZeroSMulDivisors R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [NoZeroSMulDivisors R₁ B] [NoZeroSMulDivisors R₂ B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [NoZeroSMulDivisors A R₁] [NoZeroSMulDivisors A R₂] [Module.Finite A R₁] [Module.Finite R₂ B] [IsScalarTower A R₂ B] [Module.Finite R₁ B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsScalarTower A R₁ B] (h₁ : F₁.LinearDisjoint ↥F₂) (h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤) (h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))) {ι : Type u_7} (b : Basis ι A R₂) (i : ι) : (ofIsCoprimeDifferentIdeal A B R₁ R₂ h₁ h₂ h₃ b) i = (algebraMap R₂ B) (b i)

theorem IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Field L] [Algebra B L] [Algebra A L] [Algebra K L] [FiniteDimensional K L] [IsScalarTower A K L] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [Algebra R₁ ↥F₁] [Algebra R₂ ↥F₂] [NoZeroSMulDivisors R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [NoZeroSMulDivisors R₁ B] [NoZeroSMulDivisors R₂ B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [NoZeroSMulDivisors A R₁] [NoZeroSMulDivisors A R₂] [Module.Finite A R₁] [Module.Finite R₂ B] [IsScalarTower A R₂ B] [Module.Finite R₁ B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsScalarTower A R₁ B] (h₁ : F₁.LinearDisjoint ↥F₂) (h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤) (h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))) [Module.Free A R₂] : (IsScalarTower.toAlgHom A R₁ B).range ⊔ (IsScalarTower.toAlgHom A R₂ B).range = ⊤

Let A ⊆ B be a finite extension of Dedekind domains and assume that A ⊆ R₁, R₂ ⊆ B are two subrings such that Frac R₁ ⊔ Frac R₂ = Frac B, Frac R₁ and Frac R₂ are linearly disjoint over Frac A, and that 𝓓(R₁/A) and 𝓓(R₂/A) are coprime where 𝓓 denotes the different ideal and Frac R denotes the fraction field of a domain R. Then B is generated (as an A-algebra) by R₁ and R₂.

theorem IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [Field L] [Algebra B L] [Algebra A L] [Algebra K L] [FiniteDimensional K L] [IsScalarTower A K L] (R₁ : Type u_5) (R₂ : Type u_6) [CommRing R₁] [CommRing R₂] [Algebra A R₁] [Algebra A R₂] [Algebra R₁ B] [Algebra R₂ B] [Algebra R₁ L] [Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [Algebra R₁ ↥F₁] [Algebra R₂ ↥F₂] [NoZeroSMulDivisors R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L] [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [IsDomain A] [IsDedekindDomain B] [IsDedekindDomain R₁] [IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [NoZeroSMulDivisors R₁ B] [NoZeroSMulDivisors R₂ B] [Algebra A B] [Module.Finite A B] [NoZeroSMulDivisors A B] [NoZeroSMulDivisors A R₁] [NoZeroSMulDivisors A R₂] [Module.Finite A R₁] [Module.Finite R₂ B] [IsScalarTower A R₂ B] [Module.Finite R₁ B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsScalarTower A R₁ B] [Module.Free A R₂] (h₁ : F₁.LinearDisjoint ↥F₂) (h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤) (h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))) {s : Set R₁} {t : Set R₂} (hs : Algebra.adjoin A s = ⊤) (ht : Algebra.adjoin A t = ⊤) : Algebra.adjoin A (⇑(algebraMap R₁ B) '' s ∪ ⇑(algebraMap R₂ B) '' t) = ⊤