English
The bijection is compatible with composition in the base category: precomposing f with g corresponds to composing under the bijection with g on the left.
Русский
Биекция согласована с композициями в базовой категории: предварительная композиция f с g соответствует композиции под биекцией слева.
LaTeX
$$$ \\mathrm{bijection}\; i\; A\; B\\; X' (f \\circ g) = \\mathrm{bijection}\; i\; A\; B\\; X (f) \\circ g $$$
Lean4
theorem bijection_natural (A B : C) (X X' : D) (f : (reflector i).obj (A ⊗ B) ⟶ X) (g : X ⟶ X') :
bijection i _ _ _ (f ≫ g) = bijection i _ _ _ f ≫ g :=
by
dsimp [bijection]
-- Porting note: added
erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq, homEquiv_symm_apply_eq,
homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]
apply i.map_injective
rw [Functor.FullyFaithful.map_preimage, i.map_comp, Adjunction.homEquiv_unit, Adjunction.homEquiv_unit]
simp only [comp_id, Functor.map_comp, Functor.FullyFaithful.map_preimage, assoc]
rw [← assoc, ← assoc, curry_natural_right _ (i.map g), unitCompPartialBijective_natural, uncurry_natural_right, ←
assoc, curry_natural_right, unitCompPartialBijective_natural, uncurry_natural_right, assoc]
