English
Existence of limits in the essentially small site after transporting by an equivalence and applying HasSheafify.
Русский
Существование пределов в существенно-малом сайте после переноса эквивалентностью и применения HasSheafify.
LaTeX
$$$HasLimitsOfSize (Sheaf J A)$$$
Lean4
theorem W_inverseImage_whiskeringLeft : K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) = J.W :=
by
ext P Q f
have h₁ :
K.W (A := A) =
Localization.LeftBousfield.W (· ∈ Set.range (sheafToPresheaf J A ⋙ ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op)).obj) :=
by
rw [W_eq_W_range_sheafToPresheaf_obj, ← LeftBousfield.W_isoClosure]
conv_rhs => rw [← LeftBousfield.W_isoClosure]
apply congr_arg
ext P
constructor
· rintro ⟨_, ⟨R, rfl⟩, ⟨e⟩⟩
exact
⟨_, ⟨_, rfl⟩,
⟨e.trans ((sheafToPresheaf _ _).mapIso ((G.sheafPushforwardContinuous A K J).objObjPreimageIso R).symm)⟩⟩
· rintro ⟨_, ⟨R, rfl⟩, ⟨e⟩⟩
exact ⟨G.op ⋙ R.val, ⟨(G.sheafPushforwardContinuous A K J).obj R, rfl⟩, ⟨e⟩⟩
have h₂ :
∀ (R : Sheaf J A),
Function.Bijective (fun (g : G.op ⋙ Q ⟶ G.op ⋙ R.val) ↦ whiskerLeft G.op f ≫ g) ↔
Function.Bijective (fun (g : Q ⟶ R.val) ↦ f ≫ g) :=
fun R ↦
by
rw [← Function.Bijective.of_comp_iff _ (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G Q R.val R.cond)]
exact
Function.Bijective.of_comp_iff' (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G P R.val R.cond)
(fun g ↦ f ≫ g)
rw [h₁, J.W_eq_W_range_sheafToPresheaf_obj, MorphismProperty.inverseImage_iff]
constructor
· rintro h _ ⟨R, rfl⟩
exact (h₂ R).1 (h _ ⟨R, rfl⟩)
· rintro h _ ⟨R, rfl⟩
exact (h₂ R).2 (h _ ⟨R, rfl⟩)
