normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity

English

Given f: R/I ≃+* A/J, the image of a divisor lying in normalizedFactors I remains in normalizedFactors J.

Русский

При f: R/I ≃+* A/J образ делителя из нормализованных факторов I остаётся в нормализованныхFactors J.

LaTeX

$$⊢ ↑(idealFactorsEquivOfQuotEquiv f ⟨L, dvd_of_mem_normalizedFactors hL⟩) ∈ normalizedFactors J$$

Lean4

/-- The map `normalizedFactorsEquivOfQuotEquiv` preserves multiplicities. -/
theorem normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity (hI : I ≠ ⊥) (hJ : J ≠ ⊥) (L : Ideal R)
    (hL : L ∈ normalizedFactors I) :
    emultiplicity (↑(normalizedFactorsEquivOfQuotEquiv f hI hJ ⟨L, hL⟩)) J = emultiplicity L I :=
  by
  rw [normalizedFactorsEquivOfQuotEquiv, Equiv.coe_fn_mk, Subtype.coe_mk]
  refine
    emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors hI hJ hL (d :=
      (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_
  exact fun ⟨l, hl⟩ ⟨l', hl'⟩ => idealFactorsEquivOfQuotEquiv_is_dvd_iso f hl hl'

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