inf_eq_map_pullback' — Mathlib

English

The infimum computed via Quotient.mk'' on f₁ equals the pullback-map construction on f₁.arrow and f₂.

Русский

Наименьшее, вычисляемое через Quotient.mk'' на f₁, равно конструированию отображения-множителя через f₁.arrow и f₂ через pullback.

LaTeX

$$$ (Subobject.inf.obj (Quotient.mk'' f_1)).obj f_2 = (Subobject.map f_1.arrow).obj ((Subobject.pullback f_1.arrow).obj f_2) $$$

Lean4

theorem inf_eq_map_pullback' {A : C} (f₁ : MonoOver A) (f₂ : Subobject A) :
    (Subobject.inf.obj (Quotient.mk'' f₁)).obj f₂ =
      (Subobject.map f₁.arrow).obj ((Subobject.pullback f₁.arrow).obj f₂) :=
  by
  induction f₂ using Quotient.inductionOn'
  rfl

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