coimageImageComparison_app' — Mathlib

English

A variant formula for the app component of the coimageImageComparison, expressing it as a triple composition of iso components.

Русский

Вариант формулы компоненты app для coimageImageComparison, выраженный как тройная композиция из изоморфизмов.

LaTeX

$$$ (\mathrm{coimageImageComparison}(\alpha)).\mathrm{app} X = (\mathrm{coimageObjIso}(\alpha,X)).\mathrm{hom} \\circ (\mathrm{coimageImageComparison}(\alpha.app X)) \\circ (\mathrm{imageObjIso}(\alpha,X)).\mathrm{inv} $$$

Lean4

theorem coimageImageComparison_app' :
    (coimageImageComparison α).app X =
      (coimageObjIso α X).hom ≫ coimageImageComparison (α.app X) ≫ (imageObjIso α X).inv :=
  by simp only [coimageImageComparison_app, Iso.hom_inv_id_assoc, Iso.hom_inv_id, Category.assoc, Category.comp_id]

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