hasPullback_symmetry — Mathlib

English

If a pullback exists for f: X → Z and g: Y → Z, then a pullback also exists for g: Y → Z and f: X → Z; the pullback square is symmetric under swapping the legs.

Русский

Если существует правая точка сопряжения для f: X → Z и g: Y → Z, то существует и для g: Y → Z и f: X → Z; диаграмма pullback сохраняется при обмене ролями сторон.

LaTeX

$$$$ \text{HasPullback}(f,g) \implies \text{HasPullback}(g,f). $$$$

Lean4

/-- Making this a global instance would make the typeclass search go in an infinite loop. -/
theorem hasPullback_symmetry [HasPullback f g] : HasPullback g f :=
  ⟨⟨⟨_, PullbackCone.flipIsLimit (pullbackIsPullback f g)⟩⟩⟩

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