lift_ι

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.equalizer.lift_ι

English

If k: W → X and h: k ≫ f = k ≫ g, then equalizer.lift k h ≫ equalizer.ι f g = k.

Русский

Если k: W → X и h: k ≫ f = k ≫ g, то equalizer.lift k h ≫ equalizer.ι f g = k.

LaTeX

$$$\forall W\, (k: W \to X)\, (h: k \circ f = k \circ g),\ equalizer.lift k h \circ equalizer.\iota f g = k$$$

Lean4

@[reassoc]
theorem lift_ι {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : equalizer.lift k h ≫ equalizer.ι f g = k :=
  limit.lift_π _ _

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

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

Разделы

Аффилиация

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