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

• FractionalIdeal.differentIdeal_eq_map_differentIdeal: 𝓓(B/R₁) = 𝓓(R₂/A)
• FractionalIdeal.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime: 𝓓(B/A) = 𝓓(R₁/A) * 𝓓(R₂/A).

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 FractionalIdeal.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 FractionalIdeal.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 FractionalIdeal.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 FractionalIdeal.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