English
Equality expressing that the diagonal-trivial isomorphism at level n matches the canonical unit/tensorial structure at level n with a specified base isomorphism.
Русский
Равенство, выражающее совпадение диагонального тривиального изоморфизма на уровне n с канонической единицей/тензионной структурой уровня n с заданной базовой процедурой.
LaTeX
$$$\text{diagonalSuccIsoTensorTrivial G n} = \text{...}$ (natural isomorphism identity)$$
Lean4
/-- A lax monoidal functor induces a lax monoidal functor between
the categories of `G`-actions within those categories. -/
instance [F.LaxMonoidal] : (F.mapAction G).LaxMonoidal
where
ε :=
{ hom := ε F
comm := fun g => by
dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction]
rw [Category.id_comp, F.map_id, Category.comp_id] }
μ X
Y :=
{ hom := μ F X.V Y.V
comm := fun g => μ_natural F (X.ρ g) (Y.ρ g) }
μ_natural_left _ _ := by ext; simp
μ_natural_right _ _ := by ext; simp
associativity _ _ _ := by ext; simp
left_unitality _ := by ext; simp
right_unitality _ := by ext; simp
