map_comap_eq_self

Mathlib.Algebra.Algebra.Subalgebra.Lattice

URI: https://scilib.ai/kg/mathlib#Subalgebra.map_comap_eq_self

← MathLib Explorer

English

If S is contained in the range of f, then pulling back S and pushing forward along f recovers S.

Русский

Если S ⊆ range(f), то обратная связка и прямое отображение восстанавливают S.

LaTeX

$$$ (S.comap f).map f = S $$$

Lean4

theorem map_comap_eq_self {f : A →ₐ[R] B} {S : Subalgebra R B} (h : S ≤ f.range) : (S.comap f).map f = S := by
  simpa only [inf_of_le_left h] using map_comap_eq f S

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

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

Разделы

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

Аффилиация

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