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] [LocalRing R] (x : S) : (Algebra.trace (R ⧸ LocalRing.maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (LocalRing.maximalIdeal R))) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (LocalRing.maximalIdeal R))) x) = (Ideal.Quotient.mk (LocalRing.maximalIdeal R)) ((Algebra.trace R S) x)

noncomputable def equivQuotMaximalIdealOfIsLocalization {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsMaximal] (Rₚ : Type u_3) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [LocalRing Rₚ] : R ⧸ p ≃+* Rₚ ⧸ LocalRing.maximalIdeal Rₚ

The isomorphism R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ, where Rₚ satisfies IsLocalization.AtPrime Rₚ p. In particular, localization preserves the residue field.

Equations

• equivQuotMaximalIdealOfIsLocalization p Rₚ = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

theorem IsLocalization.AtPrime.map_eq_maximalIdeal {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsMaximal] (Rₚ : Type u_3) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [LocalRing Rₚ] : Ideal.map (algebraMap R Rₚ) p = LocalRing.maximalIdeal Rₚ

theorem comap_map_eq_map_of_isLocalization_algebraMapSubmonoid {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsMaximal] {Sₚ : Type u_4} [CommRing Sₚ] [Algebra S Sₚ] [Algebra R Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [IsScalarTower R S Sₚ] : Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap R Sₚ) p) = Ideal.map (algebraMap R S) p

noncomputable def quotMapEquivQuotMapMaximalIdealOfIsLocalization {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] [LocalRing 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ₚ] : S ⧸ Ideal.map (algebraMap R S) p ≃+* Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (LocalRing.maximalIdeal Rₚ)

The isomorphism S ⧸ pS ≃+* Sₚ ⧸ pSₚ.

Equations

• quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

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] [LocalRing 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) = (equivQuotMaximalIdealOfIsLocalization p Rₚ).symm ((Algebra.trace (Rₚ ⧸ LocalRing.maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (LocalRing.maximalIdeal Rₚ))) ((algebraMap S (Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (LocalRing.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] [NoZeroSMulDivisors R S] [Module.Finite R S] [IsIntegrallyClosed S] : (Algebra.trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) = (Ideal.Quotient.mk p) ((Algebra.intTrace R S) x)

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