pullbackπ — Mathlib

English

There is an order isomorphism between Subobject X and Subobject Y for an isomorphism X ≅ Y.

Русский

Для изоморфизма X ≅ Y существует упорядоченная изоморфность между Subobject(X) и Subobject(Y).

LaTeX

$$$\text{Subobject}(X) \cong_{\mathrm{ord}} \text{Subobject}(Y)$$$

Lean4

/-- For any morphism `f : X ⟶ Y` and subobject `y` of `Y`, `Subobject.pullbackπ f y` is the first
    projection in the following pullback square:

    ```
    (Subobject.pullback f).obj y ----pullbackπ f y---> (y : C)
             |                                            |
    ((Subobject.pullback f).obj y).arrow               y.arrow
             |                                            |
             v                                            v
             X ---------------------f-------------------> Y
    ```

    For instance in the category of sets, `Subobject.pullbackπ f y` is the restriction of `f` to
    elements of `X` that are in the preimage of `y ⊆ Y`.
-/
noncomputable def pullbackπ (f : X ⟶ Y) (y : Subobject Y) : ((Subobject.pullback f).obj y : C) ⟶ (y : C) :=
  (isPullback_aux f y).choose

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