English
The naturality of normalization with respect to f is expressed as inclusionObj n ◁ f commuting with normalizeIsoApp' on X and the functor map on the discrete level.
Русский
Естественность нормализации по отношению к f выражается в commuting инклюзии inclusionObj n ◁ f и нормализации на уровнях объектов.
LaTeX
$$$ inclusionObj n ◁ f \;\gg\; (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom \gg inclusion.map (eqToHom (Discrete.ext (normalizeObj_congr n f))) $$$
Lean4
theorem normalize_naturality (n : NormalMonoidalObject C) {X Y : F C} (f : X ⟶ Y) :
inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom =
(normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom (Discrete.ext (normalizeObj_congr n f))) :=
by
revert n
induction f using Hom.inductionOn
case comp f g ihf ihg => simp [ihg, reassoc_of% (ihf _)]
case whiskerLeft X' X Y f ih =>
intro n
dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom, Iso.symm_hom,
whiskerRightIso_hom, Function.comp_apply, inclusion_obj]
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
simp
case whiskerRight X Y h η' ih =>
intro n
dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom, Iso.symm_hom,
whiskerRightIso_hom, Function.comp_apply, inclusion_obj]
rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih]
have := dcongr_arg (fun x => (normalizeIsoApp' C η' x).hom) (normalizeObj_congr n h)
simp [this]
all_goals simp
