inf_eq_map_pullback — Mathlib

English

Equality between the infimum object via quotient and the map-pullback construction.

Русский

Равенство между объектом наименьшего через квотирование и конструированием отображения через pullback.

LaTeX

$$$ (Subobject.inf.obj (\\mathrm{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) :
    (Quotient.mk'' f₁ ⊓ f₂ : Subobject A) = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂) :=
  inf_eq_map_pullback' f₁ f₂

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