π — Mathlib · SciLib

English

`h.π m` is the first projection in the pullback square with h.χ m and h.Ω₀.

Русский

`h.π m` — первая проекция в квадрате вытягивания с `h.χ m` и `h.Ω₀`.

LaTeX

$$π : U ⟶ Subobject.underlying.obj h.Ω₀$$

Lean4

/-- `h.π m` is the first projection in the following pullback square:

    ```
    U --h.π m--> (Ω₀ : C)
    |                |
    m             Ω₀.arrow
    |                |
    v                v
    X -----h.χ m---> Ω
    ```
-/
noncomputable def π : U ⟶ Subobject.underlying.obj h.Ω₀ :=
  (h.iso m).hom.left ≫ Subobject.pullbackπ (h.χ m) h.Ω₀

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