map_reflexion_comp_map_left — Mathlib

English

For a functor F from WalkingReflexivePair to C, F.map reflexion ≫ F.map left = id on F.obj zero.

Русский

Для функторa F: WalkingReflexivePair ⥤ C выполняется F.map reflexion ≫ F.map left = id_{F.obj zero}.

LaTeX

$$$\bigl(F.map \text{reflexion}\bigr) \;\circ\; \bigl(F.map \text{left}\bigr) = \mathrm{id}_{F(\text{zero})}$$$

Lean4

@[reassoc (attr := simp)]
theorem map_reflexion_comp_map_left (F : WalkingReflexivePair ⥤ C) : F.map reflexion ≫ F.map left = 𝟙 (F.obj zero) := by
  rw [← F.map_comp, reflexion_comp_left, F.map_id]

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