map₂_inv_hom_isIso — Mathlib

English

Let F be a PrelaxFunctor. If η is an isomorphism between arrows f and g, then the composites F.map₂(inv η) and F.map₂(η) compose to the identity on F.map g.

Русский

Пусть F—это Прелакс-функтор. Пусть η является изоморфизмом между стрелками f и g. Тогда композиция F.map₂(inv η) с F.map₂ η равна тождественному морфизму на F.map g.

LaTeX

$$$\forall {B,C} (F: B \to C) \; \forall a,b \; \forall f,g: a \to b \; \forall \eta: f \to g \; [\IsIso\eta],\ F.map₂(\operatorname{inv}\eta) \; \circ \; F.map₂\eta = \mathbb{1}_{F.map\,g}$$$

Lean4

@[reassoc]
theorem map₂_inv_hom_isIso {f g : a ⟶ b} (η : f ⟶ g) [IsIso η] : F.map₂ (inv η) ≫ F.map₂ η = 𝟙 (F.map g) := by simp

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