obj_zero_map_μ_app — Mathlib

English

A unit-type interaction between δ, μ and η holds after inserting identities; the left side with (F.obj 1_M) and μ interacts with η and right unital maps to yield the same composite as a different arrangement.

Русский

Соотношение между δ, μ и η при вставке единичных объектов: левая и правая композиции эквивалентны.

LaTeX

$$$ (F.obj (\mathbf{1}_M)).map f \;\gg\; (\mu F m (\mathbf{1}_M)).app X = (\eta F).app X \gg f \gg (F.map (\rho_ m).inv).app X $$$

Lean4

@[reassoc (attr := simp)]
theorem obj_zero_map_μ_app {m : M} {X Y : C} (f : X ⟶ (F.obj m).obj Y) [F.Monoidal] :
    (F.obj (𝟙_ M)).map f ≫ (μ F m (𝟙_ M)).app _ = (η F).app _ ≫ f ≫ (F.map (ρ_ m).inv).app _ :=
  by
  rw [← cancel_epi ((ε F).app _), ← cancel_mono ((δ F _ _).app _)]
  simp

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