coprodMk_inl — Mathlib

English

The image of inl under coprodMk corresponds to the left coprojection.

Русский

Образ Inl под CoprodMk соответствует левой копроподии.

LaTeX

$$$coprodMk X Y (.inl x) = (coprod.inl : X ⟶ X ⨿ Y).base x$$$

Lean4

@[simp]
theorem coprodMk_inl (x : X) : coprodMk X Y (.inl x) = (coprod.inl : X ⟶ X ⨿ Y).base x :=
  by
  change
    ((TopCat.binaryCofan X Y).inl ≫ (colimit.isoColimitCocone ⟨_, TopCat.binaryCofanIsColimit _ _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map coprod.inl x
  congr 2
  refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_
  exact coprodComparison_inl Scheme.forgetToTop

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