comp_unit_app — Mathlib

English

For adjunctions adj1 : F ⊣ G and adj2 : H ⊣ I, the unit of the composite adj1.comp adj2 is the composition of units: (adj1.comp adj2).unit_X = adj1.unit_X ≫ G.map (adj2.unit_(F.obj X)).

Русский

Единица композиции двух адъюнкций равна композиции единиц: (adj1.comp adj2).unit_X = adj1.unit_X ≫ G.map (adj2.unit_(F.obj X)).

LaTeX

$$$ (adj_1 \cdot adj_2).unit_{X} = adj_1.unit_{X} \circ G.map (adj_2.unit_{F.obj X}) $$$

Lean4

@[simp, reassoc]
theorem comp_unit_app (X : C) : (adj₁.comp adj₂).unit.app X = adj₁.unit.app X ≫ G.map (adj₂.unit.app (F.obj X)) := by
  simp [Adjunction.comp]

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