English
The natural equivalence between CostructuredArrow (S.prod S') (T, T') and the product of CostructuredArrow S T and CostructuredArrow S' T'.
Русский
Естественная эквалентность CostructuredArrow (S.prod S') (T, T') и произведения CostructuredArrow S T и CostructuredArrow S' T'.
LaTeX
$$$$ \text{prodEquivalence} : \text{CostructuredArrow} (S \prod S') (T,T') \simeq \text{CostructuredArrow} S T \ × \text{CostructuredArrow} S' T' . $$$$
Lean4
/-- A functor `L : A ⥤ T` is final if there is a final functor `R : B ⥤ T` such that for all
`b : B`, the canonical functor `CostructuredArrow L (R.obj b) ⥤ Over (R.obj b)` is final. -/
theorem final_of_final_costructuredArrowToOver (L : A ⥤ T) (R : B ⥤ T) [Final R]
[hB : ∀ b : B, Final (CostructuredArrow.toOver L (R.obj b))] : Final L :=
by
let sA : A ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} A := AsSmall.equiv
let sB : B ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} B := AsSmall.equiv
let sT : T ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} T := AsSmall.equiv
let L' := sA.inverse ⋙ L ⋙ sT.functor
let R' := sB.inverse ⋙ R ⋙ sT.functor
have (b : _) : (CostructuredArrow.toOver L' (R'.obj b)).Final :=
by
dsimp only [L', R', CostructuredArrow.toOver] at hB ⊢
let x := (sB.inverse ⋙ R ⋙ sT.functor).obj b
let F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 _) x :=
map₂ (F := sA.inverse) (G := sT.inverse) (whiskerLeft (sA.inverse ⋙ L) sT.unit) (𝟙 _) ⋙
pre L (𝟭 T) (R.obj _) ⋙ map₂ (F := sT.functor) (G := sT.functor) (𝟙 _) (𝟙 _)
apply final_of_natIso (F := F'')
have hsT (X) : sT.counitInv.app X = 𝟙 _ := rfl
exact NatIso.ofComponents (fun X => CostructuredArrow.isoMk (Iso.refl _) (by simp [F'', hsT]))
have := final_of_final_costructuredArrowToOver_small L' R'
apply final_of_natIso (F := (sA.functor ⋙ L' ⋙ sT.inverse))
exact
(sA.functor.associator (sA.inverse ⋙ L ⋙ sT.functor) sT.inverse).symm ≪≫
((sA.functor.associator sA.inverse (L ⋙ sT.functor)).symm ≪≫
isoWhiskerRight sA.unitIso.symm _ ≪≫ (L ⋙ sT.functor).leftUnitor).compInverseIso
