The trace map on quotients and localizations

We gather results about the relations between the trace map on B → A and the trace map on quotients and localizations.

Main results

• Algebra.trace_quotient_eq_of_isDedekindDomain : The trace map on B → A coincides with the trace map on B⧸pB → A⧸p.

theorem Algebra.trace_quotient_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] [Module.Finite R S] [IsLocalRing R] (x : S) : (trace (R ⧸ IsLocalRing.maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) x) = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R)) ((trace R S) x)

theorem trace_quotient_eq_trace_localization_quotient {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsMaximal] (Rₚ : Type u_3) (Sₚ : Type u_4) [CommRing Rₚ] [CommRing Sₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] [Algebra S Sₚ] [Algebra R Sₚ] [Algebra Rₚ Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] (x : S) : (Algebra.trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) = (IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ).symm ((Algebra.trace (Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (IsLocalRing.maximalIdeal Rₚ))) ((algebraMap S (Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (IsLocalRing.maximalIdeal Rₚ))) x))

theorem Algebra.trace_quotient_eq_of_isDedekindDomain {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsMaximal] (x : S) [IsDedekindDomain R] [IsDomain S] [Module.IsTorsionFree R S] [Module.Finite R S] [IsIntegrallyClosed S] : (trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

The trace map on B → A coincides with the trace map on B⧸pB → A⧸p.