Localization of the different ideal #
This file proves that trace duals and different ideals commute with localization, so localization preserves the coefficient of the different ideal at every nonzero prime. This is the localization input needed to read the transitivity theorem for different ideals coefficientwise at a tower of discrete valuations.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Sections III.4–III.5.
- A. Yang, Mathlib's different-ideal formalization.
theorem
TauCeti.span_traceDual_one_eq_traceDual_one
{R : Type uR}
{Rₘ : Type uRm}
{S : Type uS}
{Sₘ : Type uSm}
{K : Type uK}
{L : Type uL}
[CommRing R]
[CommRing Rₘ]
[CommRing S]
[CommRing Sₘ]
[Field K]
[Field L]
{M : Submonoid R}
[Algebra R Rₘ]
[Algebra R S]
[Algebra Rₘ Sₘ]
[Algebra S Sₘ]
[Algebra R Sₘ]
[IsScalarTower R S Sₘ]
[Algebra R K]
[Algebra Rₘ K]
[IsScalarTower R Rₘ K]
[Algebra K L]
[Algebra R L]
[Algebra Rₘ L]
[Algebra S L]
[Algebra Sₘ L]
[IsScalarTower R K L]
[IsScalarTower Rₘ K L]
[IsScalarTower R S L]
[IsScalarTower Rₘ Sₘ L]
[IsScalarTower S Sₘ L]
[IsScalarTower R Sₘ L]
[IsLocalization M Rₘ]
[IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[Module.Finite R S]
:
The trace dual of a finite algebra commutes with localization.
theorem
TauCeti.extended_dual_one_eq_dual_one
{R : Type uR}
{Rₘ : Type uRm}
{S : Type uS}
{Sₘ : Type uSm}
{K : Type uK}
{L : Type uL}
[CommRing R]
[CommRing Rₘ]
[CommRing S]
[CommRing Sₘ]
[Field K]
[Field L]
{M : Submonoid R}
[Algebra R Rₘ]
[Algebra R S]
[Algebra Rₘ Sₘ]
[Algebra S Sₘ]
[Algebra R Sₘ]
[IsScalarTower R S Sₘ]
[Algebra R K]
[Algebra Rₘ K]
[IsScalarTower R Rₘ K]
[Algebra K L]
[Algebra R L]
[Algebra Rₘ L]
[Algebra S L]
[Algebra Sₘ L]
[IsScalarTower R K L]
[IsScalarTower Rₘ K L]
[IsScalarTower R S L]
[IsScalarTower Rₘ Sₘ L]
[IsScalarTower S Sₘ L]
[IsScalarTower R Sₘ L]
[IsLocalization M Rₘ]
[IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[Module.Finite R S]
[IsDomain R]
[IsFractionRing R K]
[IsFractionRing S L]
[IsIntegrallyClosed R]
[IsIntegralClosure S R L]
[IsIntegralClosure Sₘ Rₘ L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[IsDomain S]
:
have x := ⋯;
have hM := ⋯;
have x := ⋯;
have hMS := ⋯;
have x_1 := ⋯;
have x_2 := ⋯;
have x_3 := ⋯;
have x_4 := ⋯;
FractionalIdeal.extended L ⋯ (FractionalIdeal.dual R K 1) = FractionalIdeal.dual Rₘ K 1
The trace-dual fractional ideal commutes with localization.
theorem
TauCeti.map_differentIdeal_eq_differentIdeal
{R : Type uR}
{Rₘ : Type uRm}
{S : Type uS}
{Sₘ : Type uSm}
{K : Type uK}
{L : Type uL}
[CommRing R]
[CommRing Rₘ]
[CommRing S]
[CommRing Sₘ]
[Field K]
[Field L]
{M : Submonoid R}
[Algebra R Rₘ]
[Algebra R S]
[Algebra Rₘ Sₘ]
[Algebra S Sₘ]
[Algebra R Sₘ]
[IsScalarTower R S Sₘ]
[Algebra R K]
[Algebra Rₘ K]
[IsScalarTower R Rₘ K]
[Algebra K L]
[Algebra R L]
[Algebra Rₘ L]
[Algebra S L]
[Algebra Sₘ L]
[IsScalarTower R K L]
[IsScalarTower Rₘ K L]
[IsScalarTower R S L]
[IsScalarTower Rₘ Sₘ L]
[IsScalarTower S Sₘ L]
[IsScalarTower R Sₘ L]
[IsLocalization M Rₘ]
[IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[Module.Finite R S]
[IsDomain R]
[IsFractionRing R K]
[IsFractionRing S L]
[IsIntegrallyClosed R]
[IsIntegralClosure S R L]
[IsIntegralClosure Sₘ Rₘ L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[IsDedekindDomain S]
:
have x := ⋯;
have hM := ⋯;
have x_1 := ⋯;
have hMS := ⋯;
have x_2 := ⋯;
have x_3 := ⋯;
have x_4 := ⋯;
have x_5 := ⋯;
have x_6 := ⋯;
have x_7 := ⋯;
have x := ⋯;
have x_8 := ⋯;
have x := ⋯;
Ideal.map (algebraMap S Sₘ) (differentIdeal R S) = differentIdeal Rₘ Sₘ
The different ideal commutes with localization.
theorem
TauCeti.multiplicity_differentIdeal_eq_multiplicity_under
{R : Type uR}
{Rₘ : Type uRm}
{S : Type uS}
{Sₘ : Type uSm}
{K : Type uK}
{L : Type uL}
[CommRing R]
[CommRing Rₘ]
[CommRing S]
[CommRing Sₘ]
[Field K]
[Field L]
{M : Submonoid R}
[Algebra R Rₘ]
[Algebra R S]
[Algebra Rₘ Sₘ]
[Algebra S Sₘ]
[Algebra R Sₘ]
[IsScalarTower R S Sₘ]
[Algebra R K]
[Algebra Rₘ K]
[IsScalarTower R Rₘ K]
[Algebra K L]
[Algebra R L]
[Algebra Rₘ L]
[Algebra S L]
[Algebra Sₘ L]
[IsScalarTower R K L]
[IsScalarTower Rₘ K L]
[IsScalarTower R S L]
[IsScalarTower Rₘ Sₘ L]
[IsScalarTower S Sₘ L]
[IsScalarTower R Sₘ L]
[IsLocalization M Rₘ]
[IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[Module.Finite R S]
[IsDomain R]
[IsFractionRing R K]
[IsFractionRing S L]
[IsIntegrallyClosed R]
[IsIntegralClosure S R L]
[IsIntegralClosure Sₘ Rₘ L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[Module.IsTorsionFree R S]
[Module.IsTorsionFree Rₘ Sₘ]
[IsDedekindDomain S]
[IsDomain Rₘ]
[IsDedekindDomain Sₘ]
{P : Ideal Sₘ}
[P.IsPrime]
(hP : P ≠ ⊥)
:
Localization preserves the coefficients of the different ideal: at a nonzero prime P of
Sₘ, the coefficient of 𝔇(Sₘ / Rₘ) is the coefficient of 𝔇(S / R) at P ∩ S.