biprodComparison'_comp_biprodComparison

English

The composite biprodComparison' F X Y ≫ biprodComparison F X Y is the identity on F.obj X ⊞ F.obj Y; i.e., the two maps form an inverse pair.

Русский

Составные biprodComparison' F X Y ≫ biprodComparison F X Y есть тождественный отображение на F.obj X ⊞ F.obj Y; эти отображения образуют взаимно обратную пару.

LaTeX

$$$\\text{biprodComparison}'(F,X,Y) \\;\\circ\\; \\text{biprodComparison}(F,X,Y) = \\mathrm{Id}_{F(X) \\oplus F(Y)}$$$

Lean4

/-- The composition in the opposite direction is equal to the identity if and only if `F` preserves
the biproduct, see `preservesBinaryBiproduct_of_monoBiprodComparison`. -/
@[reassoc (attr := simp)]
theorem biprodComparison'_comp_biprodComparison :
    biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y) := by ext <;> simp [← Functor.map_comp]

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