English
If F is compatible-preserving and cover-preserving, then F is continuous.
Русский
Если F совместимо сохраняет, то F непрерывна.
LaTeX
$$$\text{IsContinuous}(F,J,K)$$$
Lean4
/-- If `F` is cover-preserving and compatible-preserving, then `F` is a continuous functor. -/
@[stacks 00WW "This is basically this Stacks entry."]
theorem isContinuous_of_coverPreserving (hF₁ : CompatiblePreserving.{w} K F) (hF₂ : CoverPreserving J K F) :
Functor.IsContinuous.{w} F J K where
op_comp_isSheaf_of_types G X S hS x
hx := by
apply existsUnique_of_exists_of_unique
· have H := (isSheaf_iff_isSheaf_of_type _ _).1 G.2 _ (hF₂.cover_preserve hS)
exact
⟨H.amalgamate (x.functorPushforward F) (hx.functorPushforward hF₁), fun V f hf =>
(H.isAmalgamation (hx.functorPushforward hF₁) (F.map f) _).trans (hF₁.apply_map _ hx hf)⟩
· intro y₁ y₂ hy₁ hy₂
apply (((isSheaf_iff_isSheaf_of_type _ _).1 G.2).isSeparated _ (hF₂.cover_preserve hS)).ext
rintro Y _ ⟨Z, g, h, hg, rfl⟩
dsimp
simp only [Functor.map_comp, types_comp_apply]
have H := (hy₁ g hg).trans (hy₂ g hg).symm
dsimp at H
rw [H]
