inf_pullback — Mathlib

English

`⊓` commutes with pullback: pulling back the infimum along g equals the infimum of pullbacks.

Русский

Оператор наименьшего сверху коммутирует с pullback: вытягивание наименьшего над g равняется наименьшему от вытягиваний.

LaTeX

$$$ (pullback\\ g).obj (f_1 \\inf f_2) = (pullback\\ g).obj f_1 \\inf (pullback\\ g).obj f_2 $$$

Lean4

/-- `⊓` commutes with pullback. -/
theorem inf_pullback {X Y : C} (g : X ⟶ Y) (f₁ f₂) :
    (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂ :=
  by
  revert f₁
  apply Quotient.ind'
  intro f₁
  erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← pullback_comp, ←
    map_pullback pullback.condition (pullbackIsPullback f₁.arrow g), ← pullback_comp, pullback.condition]
  rfl

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