English
Given localization data and two functors, a natural transformation between their uncurry images is determined by its components after localization.
Русский
При заданных данных локализации и двух функторов натурная трансформация между их образами через uncurry определяется компонентами после локализации.
LaTeX
$$$\\text{lift₂NatTrans } L_1 L_2 W_1 W_2 F_1 F_2 F'_1 F'_2 : \\; (F_1 \\Rightarrow F_2) \\Rightarrow (F'_1 \\Rightarrow F'_2)$$$
Lean4
@[simp]
theorem lift₂NatTrans_app_app (τ : F₁ ⟶ F₂) (X₁ : C₁) (X₂ : C₂) :
((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂) =
((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
(τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂ :=
by
dsimp [lift₂NatTrans, fullyFaithfulUncurry, Equivalence.fullyFaithfulFunctor]
simp only [comp_id, id_comp]
exact liftNatTrans_app _ _ _ _ (uncurry.obj F₁') (uncurry.obj F₂') (uncurry.map τ) ⟨X₁, X₂⟩
