noncomputable def
discrIdeal
(A : Type u_1)
(B : Type u_2)
[CommRing A]
[IsDomain A]
[IsIntegrallyClosed A]
[CommRing B]
[IsDomain B]
[IsIntegrallyClosed B]
[IsDedekindDomain B]
[Algebra A B]
[Module.Finite A B]
[Module.IsTorsionFree A B]
:
Ideal A
Instances For
theorem
different_tower
(A : Type u_1)
(B : Type u_2)
(C : Type u_3)
[CommRing A]
[IsDomain A]
[IsIntegrallyClosed A]
[IsDedekindDomain A]
[CommRing B]
[IsDomain B]
[IsIntegrallyClosed B]
[IsDedekindDomain B]
[CommRing C]
[IsDomain C]
[IsIntegrallyClosed C]
[IsDedekindDomain C]
[Algebra A B]
[Algebra B C]
[Algebra A C]
[IsScalarTower A B C]
[Module.Finite A B]
[Module.Finite A C]
[Module.Finite B C]
[Module.IsTorsionFree A B]
[Module.IsTorsionFree A C]
[Module.IsTorsionFree B C]
[Algebra.IsSeparable (FractionRing A) (FractionRing C)]
:
theorem
discr_tower
(A : Type u_1)
(B : Type u_2)
(C : Type u_3)
[CommRing A]
[IsDomain A]
[IsIntegrallyClosed A]
[IsDedekindDomain A]
[CommRing B]
[IsDomain B]
[IsIntegrallyClosed B]
[IsDedekindDomain B]
[CommRing C]
[IsDomain C]
[IsIntegrallyClosed C]
[IsDedekindDomain C]
[Algebra A B]
[Algebra B C]
[Algebra A C]
[IsScalarTower A B C]
[Module.Finite A B]
[Module.Finite A C]
[Module.Finite B C]
[Module.IsTorsionFree A B]
[Module.IsTorsionFree A C]
[Module.IsTorsionFree B C]
[Algebra.IsSeparable (FractionRing A) (FractionRing C)]
:
discrIdeal A C = discrIdeal A B ^ Module.finrank (FractionRing B) (FractionRing C) * Ideal.spanNorm A (discrIdeal B C)
theorem
proposition_12_28
(A : Type u_1)
(B : Type u_2)
(C : Type u_3)
[CommRing A]
[IsDomain A]
[IsIntegrallyClosed A]
[IsDedekindDomain A]
[CommRing B]
[IsDomain B]
[IsIntegrallyClosed B]
[IsDedekindDomain B]
[CommRing C]
[IsDomain C]
[IsIntegrallyClosed C]
[IsDedekindDomain C]
[Algebra A B]
[Algebra B C]
[Algebra A C]
[IsScalarTower A B C]
[Module.Finite A B]
[Module.Finite A C]
[Module.Finite B C]
[Module.IsTorsionFree A B]
[Module.IsTorsionFree A C]
[Module.IsTorsionFree B C]
[Algebra.IsSeparable (FractionRing A) (FractionRing C)]
:
differentIdeal A C = differentIdeal B C * Ideal.map (algebraMap B C) (differentIdeal A B) ∧ discrIdeal A C = discrIdeal A B ^ Module.finrank (FractionRing B) (FractionRing C) * Ideal.spanNorm A (discrIdeal B C)