lift_surjective_of_surjective

Mathlib.RingTheory.Ideal.Quotient.Defs

URI: https://scilib.ai/kg/mathlib#Ideal.Quotient.lift_surjective_of_surjective

← MathLib Explorer

English

The lift map evaluated on mk I a equals f a.

Русский

Лифтинг на mk I a даёт f a.

LaTeX

$$$\\mathrm{lift}\\ I\\ f\\ H (\\mathrm{mk}\\ I\\ a) = f(a)$$$

Lean4

theorem lift_surjective_of_surjective {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0) (hf : Function.Surjective f) :
    Function.Surjective (Ideal.Quotient.lift I f H) := by
  intro y
  obtain ⟨x, rfl⟩ := hf y
  use Ideal.Quotient.mk I x
  simp only [Ideal.Quotient.lift_mk]

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

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

Разделы

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

Аффилиация

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