ψ — Mathlib · SciLib

English

The morphism ϕ is the map on F₁ to F₂ induced by left projections from K.

Русский

Морфизм ϕ — отображение F₁ в F₂, индуцируемое левыми проекциям из K.

LaTeX

$$$\varphi : F_1 f g P_1 P_2 \to F_2 f g P_1 P_2 \text{, with }\ app\ h := h.hom.1.left$$$

Lean4

/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
def ψ : F₁ f g P₁ P₂ ⟶ F₂ f g P₁ P₂ where
  app h := h.hom.2.left
  naturality _ _
    h := by
    have := h.w
    simp only [Functor.prod'_obj, Functor.comp_obj, prod_Hom, Functor.prod'_map, Functor.comp_map, prod_comp,
      Prod.mk.injEq, CostructuredArrow.hom_eq_iff, CostructuredArrow.map_obj_left,
      IndObjectPresentation.toCostructuredArrow_obj_left, CostructuredArrow.comp_left, CostructuredArrow.map_map_left,
      IndObjectPresentation.toCostructuredArrow_map_left] at this
    exact this.2

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