map — Mathlib

English

Two BasedNatTrans morphisms are equal if their underlying natural transformations are equal.

Русский

Два морфизма BasedNatTrans равны, если их базовые натуральные преобразования равны.

LaTeX

$$$\\text{BasedNatTrans.ext }(α,β):\\; α.toNatTrans = β.toNatTrans \\Rightarrow α=β$$$

Lean4

/-- Given a diagram
```
a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S
```
such that `φ` is strongly Cartesian, and a morphism `φ' : a' ⟶ b`. Then `map` is the map `a' ⟶ a`
lying over `g` obtained from the universal property of `φ`. -/
noncomputable def map : a' ⟶ a :=
  Classical.choose <| universal_property p f φ _ _ hf' φ'

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