Theorems · Theorem · commutative algebra

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} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [FiniteDimensional K L] [inst_10 : IsScalarTower A K L] (R₁ : Type u_5)
  (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [IsDomain R₁] [inst_14 : Algebra A R₁]
  [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B] [inst_18 : Algebra R₁ L]
  [inst_19 : Algebra R₂ L] [IsScalarTower A R₁ L] [IsScalarTower R₁ B L] [IsScalarTower R₂ B L] [Module.Finite A R₂]
  {F₁ F₂ : IntermediateField K L} [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂] [Module.IsTorsionFree 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] [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B]
  [inst_35 : IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂] [IsFractionRing B L] [IsFractionRing R₁ ↥F₁]
  [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L] [Module.IsTorsionFree R₁ B]
  [Module.IsTorsionFree 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. Then B is generated (as an A-algebra) by R₁ and R₂.

Defined in

Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Cited by

1 results in Mathlib

Foundations

Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFieldAlgebraIsFractionRingCommRingFieldAlgebraAlgebraAlgebraFiniteDimensionalIsScalarTowerCommRingCommRingIsDomainAlgebraAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsScalarTowerModule.FiniteAlgebraAlgebraModule.IsTorsionFreeIsScalarTowerIsScalarTowerIsScalarTowerIsScalarTowerAlgebra.IsSeparableAlgebra.IsSeparableIsDomainIsDedekindDomainIsDedekindDomainIsDedekindDomainIsFractionRingIsFractionRingIsFractionRingIsIntegrallyClosedIsIntegralClosureModule.IsTorsionFreeModule.IsTorsionFreeAlgebraModule.FiniteModule.IsTorsionFreeModule.IsTorsionFreeModule.IsTorsionFreeModule.FiniteModule.FiniteIsScalarTowerModule.FiniteAlgebra.IsSeparableIsScalarTowerModule.Free