inf_map — Mathlib

English

Same as above: infimum commutes with pullback.

Русский

То же самое: наименьшее коммутирует с pullback.

LaTeX

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

Lean4

/-- `⊓` commutes with map. -/
theorem inf_map {X Y : C} (g : Y ⟶ X) [Mono g] (f₁ f₂) : (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂ :=
  by
  revert f₁
  apply Quotient.ind'
  intro f₁
  erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← map_comp]
  dsimp
  rw [pullback_comp, pullback_map_self]

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