forkMap — Mathlib

English

The fork map from P.obj(op X) to the equalizer first object is defined by Pi.lift of P.map.

Русский

Форк-мэп из P.obj(op X) в равновесный первый объект задаётся Pi.lift от P.map.

LaTeX

$$$$ \mathrm{forkMap} : P.obj(\mathrm{op}\; X) \to \mathrm{FirstObj} P R $$$$

Lean4

/-- The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram
of the Stacks entry.
-/
@[stacks 00VM "This is the left morphism of the fork diagram there."]
def forkMap : P.obj (op X) ⟶ FirstObj P R :=
  Pi.lift fun f => P.map f.2.1.op

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