isDPMorphism — Mathlib

English

There exists a divided-power morphism from I to J given by the identity map on A; more precisely, the structure (IsSubDPIdeal.dividedPowers hI hJ) is a DPMorphism with f = id_A.

Русский

Существует разделённопowers-морфизм из I в J, задаваемый тождественным отображением на A; точнее, структура (IsSubDPIdeal.dividedPowers hI hJ) является DP-морфизмом с f = id_A.

LaTeX

$$$(IsSubDPIdeal.dividedPowers hI hJ).IsDPMorphism\; hI\; (\text{RingHom.id } A)$$

Lean4

theorem isDPMorphism (hJ : IsSubDPIdeal hI J) : (IsSubDPIdeal.dividedPowers hI hJ).IsDPMorphism hI (RingHom.id A) := by
  simpa only [isDPMorphism_iff, Ideal.map_id, RingHom.id_apply] using
    ⟨hJ.1, fun _ _ _ ha ↦ by rw [dpow_eq_of_mem _ _ ha]⟩

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