common_retraction

Mathlib.CategoryTheory.Limits.Shapes.Reflexive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsCoreflexivePair.common_retraction

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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