Lean4
/-- The right adjoint of an oplax monoidal functor is lax monoidal. -/
@[simps]
def rightAdjointLaxMonoidal : G.LaxMonoidal
where
ε := adj.homEquiv _ _ (η F)
μ X Y := adj.homEquiv _ _ (δ F _ _ ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y))
μ_natural_left {X Y} f
X' :=
by
simp only [Adjunction.homEquiv_apply, ← adj.unit_naturality_assoc, ← G.map_comp, assoc, ← δ_natural_left_assoc F]
suffices F.map (G.map f) ▷ F.obj (G.obj X') ≫ _ = (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]
simpa using NatTrans.whiskerRight_app_tensor_app adj.counit adj.counit (f := f) X'
μ_natural_right {X' Y'} X
g :=
by
simp only [Adjunction.homEquiv_apply, ← adj.unit_naturality_assoc, ← G.map_comp, assoc, ← δ_natural_right_assoc F]
suffices F.obj (G.obj X) ◁ F.map (G.map g) ≫ _ = (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]
simpa using NatTrans.whiskerLeft_app_tensor_app adj.counit adj.counit (f := g) _
associativity X Y
Z :=
(adj.homEquiv _ _).symm.injective
(by
simp only [homEquiv_unit, comp_obj, map_comp, comp_whiskerRight, assoc, homEquiv_counit, counit_naturality,
id_obj, counit_naturality_assoc, left_triangle_components_assoc, MonoidalCategory.whiskerLeft_comp]
rw [← δ_natural_left_assoc, ← δ_natural_left_assoc, ← δ_natural_left_assoc]
haveI := @NatTrans.whiskerRight_app_tensor_app_assoc _ _ _ _ _ _ _ _ _ adj.counit adj.counit
dsimp only [id_obj, comp_obj, Functor.comp_map, Functor.id_map] at this
rw [this, this, tensorHom_def, assoc, ← comp_whiskerRight_assoc, left_triangle_components, id_whiskerRight,
id_comp, whisker_exchange_assoc, whisker_exchange_assoc, ← tensorHom_def_assoc, associator_naturality,
OplaxMonoidal.associativity_assoc]
rw [← δ_natural_right_assoc, ← δ_natural_right_assoc, ← δ_natural_right_assoc]
nth_rw 4 [tensorHom_def]
rw [← whisker_exchange, ← MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, ←
MonoidalCategory.whiskerLeft_comp_assoc, assoc, assoc, counit_naturality, counit_naturality_assoc,
left_triangle_components_assoc, MonoidalCategory.whiskerLeft_comp, assoc, tensorHom_def, whisker_exchange])
left_unitality
X :=
(adj.homEquiv _ _).symm.injective
(by
rw [homEquiv_counit, homEquiv_counit, homEquiv_unit, homEquiv_unit, comp_whiskerRight, map_comp, map_comp,
map_comp, map_comp, map_comp, map_comp, assoc, assoc, assoc, assoc, assoc, counit_naturality,
counit_naturality_assoc, counit_naturality_assoc, left_triangle_components_assoc, ← δ_natural_left_assoc, ←
δ_natural_left_assoc, tensorHom_def, assoc, ← MonoidalCategory.comp_whiskerRight_assoc, ←
MonoidalCategory.comp_whiskerRight_assoc, assoc, counit_naturality, left_triangle_components_assoc,
id_whiskerLeft, assoc, assoc, Iso.inv_hom_id, comp_id, left_unitality_hom_assoc])
right_unitality
X :=
(adj.homEquiv _ _).symm.injective
(by
rw [homEquiv_counit, homEquiv_unit, MonoidalCategory.whiskerLeft_comp, homEquiv_unit, homEquiv_counit, map_comp,
map_comp, map_comp, map_comp, map_comp, map_comp, assoc, assoc, assoc, assoc, assoc, counit_naturality,
counit_naturality_assoc, counit_naturality_assoc, left_triangle_components_assoc, ← δ_natural_right_assoc, ←
δ_natural_right_assoc, tensorHom_def, assoc, ← whisker_exchange_assoc, ←
MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, assoc, counit_naturality,
left_triangle_components_assoc, MonoidalCategory.whiskerRight_id, assoc, assoc, Iso.inv_hom_id, comp_id,
right_unitality_hom_assoc])
