English
Under cocontinuity conditions, there exists a natural lift making a certain multifork commute with a right Kan extension in RanIsSheafOfIsCocontinuous.
Русский
При условиях коконтинуальности существует естественное подъёмное отображение, делающее commute в многоподвесе через правый Кан-расширение.
LaTeX
$$$Lift\\: s : s. pt \\to R.obj (op X)$$$
Lean4
/-- Auxiliary definition for `lift`. -/
def liftAux {Y : C} (f : G.obj Y ⟶ X) : s.pt ⟶ F.obj (op Y) :=
Multifork.IsLimit.lift (hF.isLimitMultifork ⟨_, G.cover_lift J K (K.pullback_stable f S.2)⟩)
(fun k ↦ s.ι (⟨_, G.map k.f ≫ f, k.hf⟩) ≫ α.app (op k.Y))
(by
intro { fst := ⟨Y₁, p₁, hp₁⟩, snd := ⟨Y₂, p₂, hp₂⟩, r := ⟨W, g₁, g₂, w⟩ }
dsimp at g₁ g₂ w ⊢
simp only [Category.assoc, ← α.naturality, Functor.comp_map, Functor.op_map, Quiver.Hom.unop_op]
apply
s.condition_assoc
{ fst.hf := hp₁
snd.hf := hp₂
r.g₁ := G.map g₁
r.g₂ := G.map g₂
r.w := by simpa using G.congr_map w =≫ f .. })
