Theorems · Definition · commutative algebra

Module.Basis.ofIsCoprimeDifferentIdeal

(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. Construct a R₁-basis of B by lifting an A-basis of R₂.

Defined in

Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRingCommRingFieldAlgebraAlgebraAlgebraFiniteDimensionalIsScalarTowerCommRingCommRingIsDomainAlgebraAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsScalarTowerModule.FiniteAlgebraAlgebraModule.IsTorsionFreeIsScalarTowerIsScalarTowerIsScalarTowerIsScalarTowerAlgebra.IsSeparableAlgebra.IsSeparableIsDomainIsDedekindDomainIsDedekindDomainIsDedekindDomainIsFractionRingIsFractionRingIsFractionRingIsIntegrallyClosedIsIntegralClosureModule.IsTorsionFreeModule.IsTorsionFreeAlgebraModule.FiniteModule.IsTorsionFreeModule.IsTorsionFreeModule.IsTorsionFreeModule.FiniteModule.FiniteIsScalarTowerModule.FiniteAlgebra.IsSeparableIsScalarTower