ker

Mathlib.RingTheory.DividedPowers.SubDPIdeal

URI: https://scilib.ai/kg/mathlib#DividedPowers.DPMorphism.ker

Lean4

/-- The kernel of a divided power morphism, as a `SubDPIdeal`. -/
def ker (f : DPMorphism hI hJ) : SubDPIdeal hI
    where
  carrier := RingHom.ker f.toRingHom ⊓ I
  isSubideal := inf_le_right
  dpow_mem _ hn
    a := by
    simp only [mem_inf, and_imp, RingHom.mem_ker]
    intro ha ha'
    rw [← f.isDPMorphism.2 a ha', ha]
    exact ⟨dpow_eval_zero hJ hn, hI.dpow_mem hn ha'⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru