English
The symmetry of the bijection sends the identity to the product comparison morphism: the backwards direction of the identity corresponds to prodComparison.
Русский
Симметрия биекции отправляет тождественный морфизм в соответствующий произведению сравнения: обратная карта тождественного образа даёт prodComparison.
LaTeX
$$$ (\\mathrm{bijection}\; i\\; A\\; B\\; _).\\mathrm{symm}(\\mathrm{id}) = \\mathrm{prodComparison} $$
Lean4
theorem bijection_symm_apply_id (A B : C) : (bijection i A B _).symm (𝟙 _) = prodComparison _ _ _ :=
by
simp only [bijection, Equiv.trans_def, curriedTensor_obj_obj, Equiv.symm_trans_apply, Equiv.symm_symm,
Functor.FullyFaithful.homEquiv_apply, Functor.map_id, Iso.homCongr_symm, Iso.symm_symm_eq, Iso.refl_symm,
Iso.homCongr_apply, Iso.refl_hom, comp_id, unitCompPartialBijective_symm_apply, Functor.id_obj, Functor.comp_obj,
Iso.symm_inv]
-- Porting note: added
erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]
rw [uncurry_natural_left, uncurry_curry, uncurry_natural_left, uncurry_curry, ←
BraidedCategory.braiding_naturality_left_assoc, SymmetricCategory.symmetry_assoc, ←
MonoidalCategory.whisker_exchange_assoc, ← tensorHom_def'_assoc, Adjunction.homEquiv_symm_apply, ←
Adjunction.eq_unit_comp_map_iff, Iso.comp_inv_eq, assoc,
prodComparisonIso_hom i ((reflector i).obj A) ((reflector i).obj B)]
apply hom_ext
· rw [tensorHom_fst, assoc, assoc, prodComparison_fst, ← i.map_comp, prodComparison_fst]
apply (reflectorAdjunction i).unit.naturality
· rw [tensorHom_snd, assoc, assoc, prodComparison_snd, ← i.map_comp, prodComparison_snd]
apply (reflectorAdjunction i).unit.naturality
