English
If e: F1 ⋙ F2 ≅ F12, and F1, F2 satisfy the cocontinuity/continuity hypotheses, then lift respects the isomorphism, giving a canonical lift for F12.
Русский
Если есть изоморфизм F1 ⋙ F2 ≅ F12 и выполняются условия коконтинуальности/непрерывности, то подъем сохраняет изоморфизм и даёт канонический подъем для F12.
LaTeX
$$$e: F_1 \\circ F_2 \\cong F_{12} \\;\\Rightarrow\\; \\text{lift}(F_{12}) = \\text{lift}(F_1) \\text{ transported by } e$$$
Lean4
theorem liftAux_map {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y) (i : S.Arrow) (h : G.obj W ⟶ i.Y)
(w : h ≫ i.f = G.map g ≫ f) : liftAux hF α s f ≫ F.map g.op = s.ι i ≫ R.map h.op ≫ α.app _ :=
(Multifork.IsLimit.fac (hF.isLimitMultifork ⟨_, G.cover_lift J K (K.pullback_stable f S.2)⟩) _ _
⟨W, g, by
simpa only [Sieve.functorPullback_apply, functorPullback_mem, Sieve.pullback_apply, ← w] using
S.1.downward_closed i.hf h⟩).trans
(by
dsimp
simp only [← Category.assoc]
congr 1
let r : S.Relation :=
{ fst.f := G.map g ≫ f
fst.hf := by simpa only [← w] using S.1.downward_closed i.hf h
snd := i
r.g₁ := 𝟙 _
r.g₂ := h
r.w := by simpa using w.symm .. }
simpa [r] using s.condition r)
