common_section

Mathlib.CategoryTheory.Limits.Shapes.Reflexive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsReflexivePair.common_section

English

There exists a morphism s: B → A such that s ∘ f = id_B and s ∘ g = id_B.

Русский

Существует морфизм s: B → A такой, что s ∘ f = id_B и s ∘ g = id_B.

LaTeX

$$$\exists s: B \to A,\; (s \circ f = \mathrm{id}_B) \land (s \circ g = \mathrm{id}_B)$$$

Lean4

theorem common_section (f g : A ⟶ B) [IsReflexivePair f g] : ∃ s : B ⟶ A, s ≫ f = 𝟙 B ∧ s ≫ g = 𝟙 B :=
  IsReflexivePair.common_section'

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

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

Разделы

Аффилиация

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