English
The composition of two monoidal adjunctions is again monoidal.
Русский
Сложение двух моноидальных сопряжений снова моноидально.
LaTeX
$$$\\text{IsMonoidal}(adj \\circ adj')$$$
Lean4
instance isMonoidal_comp {F' : D ⥤ E} {G' : E ⥤ D} (adj' : F' ⊣ G') [F'.OplaxMonoidal] [G'.LaxMonoidal]
[adj'.IsMonoidal] : (adj.comp adj').IsMonoidal
where
leftAdjoint_ε := by
dsimp [homEquiv]
rw [← adj.unit_app_unit_comp_map_η, ← adj'.unit_app_unit_comp_map_η, assoc, comp_unit_app, assoc, ←
Functor.map_comp, ← adj'.unit_naturality_assoc, ← map_comp, ← map_comp]
leftAdjoint_μ X
Y := by
apply ((adj.comp adj').homEquiv _ _).symm.injective
dsimp only [comp_obj, comp_μ, id_obj, comp_δ]
rw [Equiv.symm_apply_apply]
dsimp [homEquiv]
rw [comp_counit_app, comp_counit_app, comp_counit_app, assoc, ← tensorHom_comp_tensorHom, δ_natural_assoc]
dsimp
rw [← adj'.map_μ_comp_counit_app_tensor, ← map_comp_assoc, ← map_comp_assoc, ← map_comp_assoc, ←
adj.map_μ_comp_counit_app_tensor, assoc, F.map_comp_assoc, counit_naturality]
