Lean4
/-- This is the main construction in this file showing that the right Kan extension
of `F : X ⥤ C` along `principals : X ⥤ (Opens X)ᵒᵖ` is a sheaf, by showing that a certain
cone is a limit cone.
See `isSheaf_principalsKanExtension` for the main application.
-/
def isLimit {X : TopCat.{v}} [Preorder X] [Topology.IsUpperSet X] (F : X ⥤ C) (α : Type v) (Us : α → Opens X) :
IsLimit (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
where
lift S := limit.lift _ (lowerCone Us S)
fac := by
rintro S ⟨V, i, hV⟩
dsimp [forget, opensLeCoverCocone]
ext ⟨_, x, f⟩
simp only [comp_obj, StructuredArrow.proj_obj, Category.assoc, limit.lift_π, lowerCone_pt, lowerCone_π_app,
const_obj_obj, projSup_obj, StructuredArrow.map_obj_right, op_obj, ObjectProperty.ι_obj,
pointwiseRightKanExtension_obj]
have e : principalOpen x ≤ V := f.unop.le
let VV : (ObjectProperty.FullSubcategory fun V => ∃ i, V ≤ Us i) := ⟨V, i, hV⟩
let xx : (ObjectProperty.FullSubcategory fun V => ∃ i, V ≤ Us i) := ⟨principalOpen x, i, le_trans e hV⟩
let ee : xx ⟶ VV := e.hom
rw [← S.w ee.op, Category.assoc]
congr 1
simp only [comp_obj, op_obj, ObjectProperty.ι_obj, pointwiseRightKanExtension_obj, Functor.comp_map, op_map,
Quiver.Hom.unop_op, pointwiseRightKanExtension_map, limit.lift_π, xx, VV]
congr
uniq := by
intro S m hm
dsimp
symm
ext ⟨_, x, f⟩
simp only [lowerCone_pt, comp_obj, limit.lift_π, lowerCone_π_app, const_obj_obj, projSup_obj, op_obj,
ObjectProperty.ι_obj, pointwiseRightKanExtension_obj]
specialize hm ⟨principalOpen x, ?_⟩
· apply exists_le_of_le_sup
exact f.unop.le
· rw [← hm]
simp only [mapCone_pt, Cocone.op_pt, pointwiseRightKanExtension_obj, const_obj_obj, comp_obj, op_obj,
ObjectProperty.ι_obj, mapCone_π_app, Cocone.op_π, NatTrans.op_app, pointwiseRightKanExtension_map,
Category.assoc, limit.lift_π]
congr
