English
The bijection applied to a composed morphism f ≫ f3 equals the composite of the images under the corresponding functorial maps (via various isomorphisms) of f and f3.
Русский
Биекция, применённая к композиции f ≫ f3, равна композиции образов под соответствующими отображениями-функториалами f и f3 через соответствующие изоморфизмы.
LaTeX
$$$ \\mathrm{bijection}\; i\; A\; B\; X \\; = \\; \\text{(long composite of isomorphisms and functorial maps)} $$$
Lean4
/-- We construct a bijection between morphisms `L(A ⊗ B) ⟶ X` and morphisms `LA ⊗ LB ⟶ X`.
This bijection has two key properties:
* It is natural in `X`: See `bijection_natural`.
* When `X = LA ⨯ LB`, then the backwards direction sends the identity morphism to the product
comparison morphism: See `bijection_symm_apply_id`.
Together these help show that `L` preserves binary products. This should be considered
*internal implementation* towards `preservesBinaryProductsOfExponentialIdeal`.
-/
noncomputable def bijection (A B : C) (X : D) :
((reflector i).obj (A ⊗ B) ⟶ X) ≃ ((reflector i).obj A ⊗ (reflector i).obj B ⟶ X) :=
calc
_ ≃ (A ⊗ B ⟶ i.obj X) := (reflectorAdjunction i).homEquiv _ _
_ ≃ (B ⊗ A ⟶ i.obj X) := ((β_ _ _).homCongr (Iso.refl _))
_ ≃ (A ⟶ B ⟹ i.obj X) := ((exp.adjunction _).homEquiv _ _)
_ ≃ (i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X) :=
(unitCompPartialBijective _ (ExponentialIdeal.exp_closed (i.obj_mem_essImage _) _))
_ ≃ (B ⊗ i.obj ((reflector i).obj A) ⟶ i.obj X) := ((exp.adjunction _).homEquiv _ _).symm
_ ≃ (i.obj ((reflector i).obj A) ⊗ B ⟶ i.obj X) := ((β_ _ _).homCongr (Iso.refl _))
_ ≃ (B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X) := ((exp.adjunction _).homEquiv _ _)
_ ≃ (i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X) :=
(unitCompPartialBijective _ (ExponentialIdeal.exp_closed (i.obj_mem_essImage _) _))
_ ≃ (i.obj ((reflector i).obj A) ⊗ i.obj ((reflector i).obj B) ⟶ i.obj X) := ((exp.adjunction _).homEquiv _ _).symm
_ ≃ (i.obj ((reflector i).obj A ⊗ (reflector i).obj B) ⟶ i.obj X) :=
(haveI : Limits.PreservesLimits i := (reflectorAdjunction i).rightAdjoint_preservesLimits
haveI := Limits.preservesSmallestLimits_of_preservesLimits i
Iso.homCongr (prodComparisonIso _ _ _).symm (Iso.refl (i.obj X)))
_ ≃ ((reflector i).obj A ⊗ (reflector i).obj B ⟶ X) := i.fullyFaithfulOfReflective.homEquiv.symm
