map_comap_eq_self

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

← MathLib Explorer

English

If S is contained in the range of f, then (S.comap f).map f = S.

Русский

Если S ⊆ fieldRange(f), то (comap f S) затем map f возвращает S.

LaTeX

$$$ (S.comap f).map f = S \quad \text{if } S \le f.fieldRange$$$

Lean4

theorem map_comap_eq_self {f : L →ₐ[K] L'} {S : IntermediateField K L'} (h : S ≤ f.fieldRange) :
    (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