Theorems · Theorem · commutative algebra

differentIdeal_eq_differentIdeal_mul_differentIdeal

∀ (A : Type u_1) (B : Type u_4) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [IsIntegrallyClosed A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B] (C : Type u_3)
  [inst_7 : IsDomain B] [inst_8 : CommRing C] [inst_9 : Algebra B C] [inst_10 : Algebra A C]
  [inst_11 : IsDedekindDomain C] [Module.Finite A B] [Module.Finite A C] [Module.Finite B C]
  [inst_15 : Module.IsTorsionFree A C] [inst_16 : Module.IsTorsionFree B C] [IsScalarTower A B C]
  [Algebra.IsSeparable (FractionRing A) (FractionRing C)],
  differentIdeal A C = differentIdeal B C * Ideal.map (algebraMap B C) (differentIdeal A B)

Transitivity of the different ideal.

Defined in

Mathlib.RingTheory.DedekindDomain.Different

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDomainIsIntegrallyClosedIsDedekindDomainModule.IsTorsionFreeIsDomainCommRingAlgebraAlgebraIsDedekindDomainModule.FiniteModule.FiniteModule.FiniteModule.IsTorsionFreeModule.IsTorsionFreeIsScalarTowerAlgebra.IsSeparable