trace_quotient_eq_trace_localization_quotient

English

For suitable rings and maximal ideals, the trace after passing to quotients equals the trace after localization after matching via the localization map; i.e., trace through (R/p) and (S/pS) matches the trace through the localized rings after applying the induced maps.

Русский

Для подходящих колец и максимальных идеалов след после перехода к фактору совпадает со следом после локализации через соответствующие отображения.

LaTeX

$$$\\operatorname{trace}_{(R/p)}^{(S/pS)} = \\text{localization-compatible transfer of } \\operatorname{trace}_{R}^{S}$$$

Lean4

theorem trace_quotient_eq_trace_localization_quotient (x) :
    Algebra.trace (R ⧸ p) (S ⧸ pS) (Ideal.Quotient.mk pS x) =
      (equivQuotMaximalIdealOfIsLocalization p Rₚ).symm
        (Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ) (algebraMap S _ x)) :=
  by
  have : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ) :=
    by
    apply IsScalarTower.of_algebraMap_eq'
    rw [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _), IsScalarTower.algebraMap_eq R Rₚ (Sₚ ⧸ _), ← RingHom.comp_assoc, ←
      IsScalarTower.algebraMap_eq Rₚ]
  rw [Algebra.trace_eq_of_equiv_equiv (equivQuotMaximalIdealOfIsLocalization p Rₚ)
      (quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ)]
  · congr
  · ext x
    simp only [equivQuotMaximalIdealOfIsLocalization, RingHom.quotientKerEquivOfSurjective, RingEquiv.coe_ringHom_trans,
      RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, Ideal.quotEquivOfEq_mk,
      RingHom.quotientKerEquivOfRightInverse.apply, RingHom.kerLift_mk, quotMapEquivQuotMapMaximalIdealOfIsLocalization,
      Ideal.Quotient.algebraMap_quotient_map_quotient]
    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]

Похожие утверждения